prim__emptyArray : Integer -> PrimIO AnyPtrprim__newArray : Integer -> AnyPtr -> PrimIO AnyPtrprim__arrayGet : AnyPtr -> Integer -> AnyPtrprim__arraySet : AnyPtr -> Integer -> AnyPtr -> PrimIO ()prim__casSet : AnyPtr -> Integer -> a -> a -> Bits8prim__copyArray : AnyPtr -> Integer -> Integer -> AnyPtr -> Integer -> PrimIO ()prim__bufToArr : Buffer -> Integer -> Integer -> AnyPtr -> Integer -> PrimIO ()prim__arrToBuf : AnyPtr -> Integer -> Integer -> Buffer -> Integer -> PrimIO ()prim__jsArrLength : AnyPtr -> PrimIO Bits32record IArray : Nat -> Type -> Type An immutable array of size `n` holding values of type `a`.
Totality: total
Visibility: export
Constructor: IA : AnyPtr -> IArray n a
Projection: .arr : IArray n a -> AnyPtr
at : IArray n a -> Fin n -> a Safely access a value in an array at the given position.
Totality: total
Visibility: exportatByte : IArray 256 a -> Bits8 -> a Safely use a byte as an index into an array.
Totality: total
Visibility: exportatOffset : IArray n a -> Fin m -> (off : Nat) -> {auto 0 _ : LTE (off + m) n} -> a Safely access a value in an array at the given position
and offset.
Totality: total
Visibility: exporttake : (0 m : Nat) -> IArray n a -> {auto 0 _ : LTE m n} -> IArray m a We can wrap a prefix of an array in O(1) simply by giving it
a new size index.
Note: If you only need a small portion of a potentially large
array the rest of which you no longer need, consider to
release the large array from memory by invoking `force`.
Totality: total
Visibility: exportunsafeToPtr : IArray n a -> AnyPtr Extracts the wrapped `AnyPtr` value of an immutable array.
This can be used to pass the array in a foreign function call.
Client code is responsible to make sure the array is not
mutated in its raw form.
Totality: total
Visibility: exportdata MArray : Type -> Nat -> Type -> Type A mutable array.
Totality: total
Visibility: export
Constructor: MA : AnyPtr -> MArray s n a
0 IOArray : Nat -> Type -> Type Convenience alias for `MArray' RIO`.
Totality: total
Visibility: public exportunsafeMToPtr : MArray s n a -> AnyPtr Extracts the wrapped `AnyPtr` value of a mutable array.
This can be used to pass the array in a foreign function call.
Client code is responsible to make sure the array is not
mutated in its raw form.
Totality: total
Visibility: exportmarray1 : (n : Nat) -> a -> F1 s (MArray s n a) Fills a new mutable bound to linear computation `s`.
Totality: total
Visibility: exportmarray : Lift1 s f => (n : Nat) -> a -> f (MArray s n a) Fills a new mutable array in `IO`.
Totality: total
Visibility: exportunsafeMArray1 : (n : Nat) -> F1 s (MArray s n a)- Totality: total
Visibility: export unsafeMArray : Lift1 s f => (n : Nat) -> f (MArray s n a) Allocates a new, empty, mutable array in `IO`.
Totality: total
Visibility: exportset : MArray s n a -> Fin n -> a -> F1' s Safely write a value to a mutable array.
Totality: total
Visibility: exportsetBits8 : MArray s 256 a -> Bits8 -> a -> F1' s Safely write a value to a mutable array.
Totality: total
Visibility: exportget : MArray s n a -> Fin n -> F1 s a Safely read a value from a mutable array.
This returns the values thus read with unrestricted quantity, paired
with a new linear token of quantity one to be further used in the
linear context.
Totality: total
Visibility: exportgetBits8 : MArray s 256 a -> Bits8 -> F1 s a Safely read a value from a mutable array.
This returns the values thus read with unrestricted quantity, paired
with a new linear token of quantity one to be further used in the
linear context.
Totality: total
Visibility: exportmodify : MArray s n a -> Fin n -> (a -> a) -> F1' s Safely modify a value in a mutable array.
Totality: total
Visibility: exportcasset : MArray s n a -> Fin n -> a -> a -> F1 s Bool Atomically writes `val` at the given position of the mutable array
if its current value is equal to `pre`.
This is supported and has been tested on the Chez and Racket backends.
It trivially works on the JavaScript backends, which are single-threaded
anyway.
Totality: total
Visibility: exportcasswap : MArray s n a -> Fin n -> a -> F1' s Atomically overwrites at the given position of the mutable array.
This is supported and has been tested on the Chez and Racket backends.
It trivially works on the JavaScript backends, which are single-threaded
anyway.
Totality: total
Visibility: exportcasupdate : MArray s n a -> Fin n -> (a -> (a, b)) -> F1 s b Atomic modification of an array position using a CAS-loop internally.
This is supported and has been tested on the Chez and Racket backends.
It trivially works on the JavaScript backends, which are single-threaded
anyway.
Totality: total
Visibility: exportcasmodify : MArray s n a -> Fin n -> (a -> a) -> F1' s Atomic modification of an array position reference using a CAS-loop
internally.
This is supported and has been tested on the Chez and Racket backends.
It trivially works on the JavaScript backends, which are single-threaded
anyway.
Totality: total
Visibility: exportmtake : MArray s n a -> (0 m : Nat) -> {auto 0 _ : LTE m n} -> F1 s (MArray s m a) Wraps a mutable array in a shorter one.
Totality: total
Visibility: exportcopy : MArray s m a -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> MArray s n a -> F1' s- Totality: total
Visibility: export icopy : IArray m a -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> MArray s n a -> F1' s- Totality: total
Visibility: export copyToBuf : MArray s m Bits8 -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> MBuffer s n -> F1' s- Totality: total
Visibility: export icopyToBuf : IArray m Bits8 -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> MBuffer s n -> F1' s- Totality: total
Visibility: export copyToArray : MBuffer s m -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> MArray s n Bits8 -> F1' s- Totality: total
Visibility: export icopyToArray : IBuffer m -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> MArray s n Bits8 -> F1' s- Totality: total
Visibility: export thaw : IArray n a -> F1 s (MArray s n a) Copy the content of an immutable array to a new mutable array.
Totality: total
Visibility: exportunsafeThaw : IArray n a -> MArray s n a Make the content of an immutable array accessible as a mutable array.
This is obviously unsafe. Don't use if you don't know exactly what you
are doing.
Totality: total
Visibility: export0 WithMArray : Nat -> Type -> Type -> Type- Totality: total
Visibility: public export alloc : (n : Nat) -> a -> WithMArray n a b -> b Allocate and use a mutable array in a linear context.
Totality: total
Visibility: exportunsafeAlloc : (n : Nat) -> WithMArray n a b -> b Like `create` but the initially created array will not hold any
sensible data.
Use with care: Client code is responsible to properly initialize
the array with data. This is usefule for creating arrays of unknown
size, when it is not immediately clear, whether it will hold any
data at all.
See for instance the implementation of `filter` or `mapMaybe`.
Totality: total
Visibility: exportunsafeFreezeLTE : {auto 0 _ : LTE m n} -> MArray s n a -> (0 m : Nat) -> F1 s (IArray m a) Wrap a mutable array in an immutable array, which can then be freely shared.
It is not possible the extract and share the underlying `ArrayData`
wrapped in an `IArray`, so we don't have to be afraid of shared mutable
state: The interface of `IArray` does not support to further mutate
the wrapped array.
It is safe to only use a prefix of a properly constructed array,
therefore we are free to give the resulting array a smaller size.
Most of the time, we'd like to use the whole array, in which case
we can just use `unsafeFreeze`.
Note: For reasons of efficiency, this does not copy the mutable array,
and therefore, it must no longer be modified after calling
this function.
Totality: total
Visibility: exportunsafeFreeze : MArray s n a -> F1 s (IArray n a) Wrap a mutable array in an immutable array, which can then be freely shared.
Note: For reasons of efficiency, this does not copy the mutable array,
and therefore, it must no longer be modified after calling
this function.
Totality: total
Visibility: exportfreezeLTE : MArray s n a -> (m : Nat) -> {auto 0 _ : LTE m n} -> F1 s (IArray m a) Copy a prefix of a mutable array into an immutable array.
Totality: total
Visibility: exportfreeze : MArray s n a -> F1 s (IArray n a) Copy a mutable buffer into an `IBuffer`.
Totality: total
Visibility: exporttoIBuffer : IArray n Bits8 -> IBuffer n Copies an immutable array of bytes to a immutable buffer.
Totality: total
Visibility: exporttoIArray : IBuffer n -> IArray n Bits8 Copies an immtuable buffer to an immutable array of bytes.
Totality: total
Visibility: exportunsafeJSMArrayOf1 : (0 a : Type) -> AnyPtr -> F1 s (n : Nat ** MArray s n a) Utility for wrapping an array result from the FFI in a proper
Idris array.
Since we are wrapping a raw pointer, this is obviously an unsafe
operation and client code is responsible to make sure that the pointer
actually corresponds to a JS array or array-like.
Totality: total
Visibility: exportunsafeJSMArrayOf : HasIO io => (0 a : Type) -> AnyPtr -> io (n : Nat ** IOArray n a) Like `unsafeJSMArrayOf1` but runs in an `IO` monad.
Totality: total
Visibility: export