-- | Arrays of pointers to boxed values. module Runtime.Prim.Array export value allocArray : [r1 r2 : Region]. Nat# -> Ptr# r1 Obj -> Ptr# r2 Obj writeArray : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj -> Ptr# r1 Obj readArray : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj fillArray : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Nat# -> Ptr# r2 Obj -> Ptr# r1 Obj import value allocBoxed : [r1 : Region]. Tag# -> Nat# -> Ptr# r1 Obj setBoxed : [r1 r2 : Region]. Ptr# r1 Obj -> Nat# -> Ptr# r2 Obj -> Void# with letrec -- | Allocate an array of boxed values, consisting of the same element -- for all positions. allocArray [r1 r2: Region] (len: Nat#) (val: Ptr# r1 Obj): Ptr# r2 Obj = do arr = allocBoxed [r2] (truncate# 0#) len fillArray arr 0# len val arr -- | Write an element into an array. writeArray [r1 r2: Region] (obj: Ptr# r1 Obj) (ix: Nat#) (val: Ptr# r2 Obj): Ptr# r1 Obj = do -- Get address of the first byte after the end of the array. len = promote# (peek# [r1] [Word32#] (castPtr# obj) 4#) top = add# 8# (shl# len (size2# [Addr#])) -- Bounded poke. -- If the requested address is past the end of the array then abort. off = add# 8# (shl# ix (size2# [Addr#])) _ = pokeBounded# (castPtr# obj) off top val obj -- | Read an element from an array. readArray [r1 r2: Region] (obj: Ptr# r1 Obj) (ix: Nat#): Ptr# r2 Obj = do -- Get address of the first byte after the end of the array. len = promote# (peek# [r1] [Word32#] (castPtr# obj) 4#) top = add# 8# (shl# len (size2# [Addr#])) -- Bounded peek. -- If the requested address is past the end of the array then abort. off = add# 8# (shl# ix (size2# [Addr#])) result = peekBounded# (castPtr# obj) off top result -- | Fill all elements of an array with the same value. fillArray [r1 r2: Region] (arr: Ptr# r1 Obj) (start end: Nat#) (val: Ptr# r2 Obj): Ptr# r1 Obj = case ge# start end of True# -> arr False# -> do setBoxed arr start val fillArray arr (add# start 1#) end val