Idris2Doc : Data.C.Array

Data.C.Array

(source)
Reexports
import public Data.Fin
import public Data.Linear.Token
import public Data.Array.Index
import public Data.C.Struct
Definitions
prim__copy_pp : AnyPtr -> AnyPtr -> Bits32 -> PrimIO ()
prim__copy_pb : AnyPtr -> Buffer -> Bits32 -> PrimIO ()
prim__copy_bp : Buffer -> AnyPtr -> Bits32 -> PrimIO ()
prim__inc_ptr : AnyPtr -> Bits32 -> Bits32 -> AnyPtr
prim__scrub : AnyPtr -> Bits32 -> PrimIO ()
record CIArray : Nat -> Type -> Type
  A wrapped pointer to a C-array holding `n` values of (C-primitive)
  type `a`.
  
  Reading from such an array is O(1) and can be done in pure functions.
  
  See `CArrayIO` for a version of mutable C arrays running in `IO`.
  See `CArray` for an mutable wrapper to be used in pure (linear) code.
  
  Note : In general, this type is not for prolonged storage in an Idris data
         structure (although this is still possible), because it needs to be
         eventually freed. A typical use case is to make use of this for
         its pure and clean API, but to do so from within `IO` or `F1` by
         using `withIArray`.

  Totality: total
  Visibility: export
  Constructor: 
IA : AnyPtr -> CIArray n a

  Projection: 
.ptr : CIArray n a -> AnyPtr
at : SizeOf a => Deref a => CIArray n a -> Fin n -> a
  Totality: total
  Visibility: export
ix : SizeOf a => Deref a => CIArray n a -> (0 m : Nat) -> Ix (S m) n => a
  Totality: total
  Visibility: export
atNat : SizeOf a => Deref a => CIArray n a -> (m : Nat) -> {auto 0 _ : LT m n} -> a
  Totality: total
  Visibility: export
toVect : SizeOf a => Deref a => CIArray n a -> Vect n a
  Reads the values from a C pointer into a vector.

  Totality: total
  Visibility: export
foldrKV : SizeOf a => Deref a => (Fin n -> a -> b -> b) -> b -> CIArray n a -> b
  Right fold over the values of an array plus their indices.

  Totality: total
  Visibility: export
foldr : SizeOf a => Deref a => (a -> b -> b) -> b -> CIArray n a -> b
  Right fold over the values of an array

  Totality: total
  Visibility: export
foldlKV : SizeOf a => Deref a => (Fin n -> b -> a -> b) -> b -> CIArray n a -> b
  Left fold over the values of an array plus their indices.

  Totality: total
  Visibility: export
foldl : SizeOf a => Deref a => (b -> a -> b) -> b -> CIArray n a -> b
  Left fold over the values of an array

  Totality: total
  Visibility: export
withPtr : HasIO io => Bits32 -> (AnyPtr -> io a) -> io a
  Allocates a pointer of the given size and uses it for running
  the given computation. The pointer is freed afterwards.

  Totality: total
  Visibility: export
record PrimCArray : Type -> Bool -> Nat -> Type -> Type
  A wrapped pointer to a C-array holding `n` values of (C-primitive)
  type `a`.
  
  Reading from and writing to such an array is O(1) and runs in `IO`.
  
  See `CArray` for a pure version of mutable C arrays using linear types.
  See `CArrayS` for a pure versoin of mutable C arrays using linear types (overwritting/scrubbing before freeing).
  See `CArrayIO` for a version of mutable C arrays usable in IO.
  See `CArrayIOS` for a version of the mutable C arrays usuable in IO (overwritting/scrubbing before freeing)
  
  Note : In typical use cases, the memory allocated for a C array must
         be manually released with a call to `free` unless it is part
         of a larger structure `Struct` or managed by an external library.

  Totality: total
  Visibility: export
  Constructor: 
PCA : AnyPtr -> PrimCArray s b n a

  Projection: 
.ptr : PrimCArray s b n a -> AnyPtr
0 CArray : Type -> Nat -> Type -> Type
  Convenience alias for `PrimCArray s False n a`

  Totality: total
  Visibility: public export
0 CArrayS : Type -> Nat -> Type -> Type
  Convenience alias for `PrimCArray s True n a`

  Totality: total
  Visibility: public export
0 CArrayIO : Nat -> Type -> Type
  Convenience alias for `PrimCArray World False n a`

  Totality: total
  Visibility: public export
0 CArrayIOS : Nat -> Type -> Type
  Convenience alias for `PrimCArray World True n a`

  Totality: total
  Visibility: public export
unsafeUnwrap : CArray s n a -> AnyPtr
  Totality: total
  Visibility: export
unsafeWrap : AnyPtr -> CArray s n a
  Totality: total
  Visibility: export
0 IOBox : Type -> Type
  Totality: total
  Visibility: public export
0 Box : Type -> Type -> Type
  Totality: total
  Visibility: public export
malloc1 : (0 a : Type) -> SizeOf a => (n : Nat) -> F1 s (CArray s n a)
  Allocates a new C-pointer of `sizeof a * n` bytes.

  Totality: total
  Visibility: export
calloc1 : (0 a : Type) -> SizeOf a => (n : Nat) -> F1 s (CArray s n a)
  Like `malloc1` but resets all allocated bytes to zero.

  Totality: total
  Visibility: export
free1 : CArray s n a -> F1' s
  Frees the memory allocated for a C pointer and removes it from the
  resources bound to the linear token.

  Totality: total
  Visibility: export
frees1 : SizeOf a => CArrayS s n a -> F1' s
  Frees the memory allocated for a C pointer, after overwriting the data,
  and removes it from the resources bound to the linear token.

  Totality: total
  Visibility: export
unbox : Deref a => CArray s (S n) a -> F1 s a
  Extracts the first value stored in a C pointer.

  Totality: total
  Visibility: export
getStruct : Struct f => SizeOf (f s) => CArray s n (f s) -> Fin n -> F1 s (f s)
  Reads a struct from a C-pointer at the given position.

  Totality: total
  Visibility: export
getStructIx : Struct f => SizeOf (f s) => CArray s n (f s) -> (0 m : Nat) -> Ix (S m) n => F1 s (f s)
  Reads a struct from a C-pointer at the given position.

  Totality: total
  Visibility: export
getStructNat : Struct f => SizeOf (f s) => CArray s n (f s) -> (m : Nat) -> {auto 0 _ : LT m n} -> F1 s (f s)
  Reads a struct from a C-pointer at the given position.

  Totality: total
  Visibility: export
get : SizeOf a => CArray s n a -> Deref a => Fin n -> F1 s a
  Reads a value from a C-pointer at the given position.

  Totality: total
  Visibility: export
getIx : SizeOf a => CArray s n a -> Deref a => (0 m : Nat) -> Ix (S m) n => F1 s a
  Reads a value from a C-pointer at the given position.

  Totality: total
  Visibility: export
getNat : SizeOf a => CArray s n a -> Deref a => (m : Nat) -> {auto 0 _ : LT m n} -> F1 s a
  Reads a value from a C-pointer at the given position.

  Totality: total
  Visibility: export
set : SizeOf a => CArray s n a -> SetPtr a => Fin n -> a -> F1' s
  Writes a value to a C pointer at the given position.

  Totality: total
  Visibility: export
setIx : SizeOf a => CArray s n a -> SetPtr a => (0 m : Nat) -> Ix (S m) n => a -> F1' s
  Writes a value to a C pointer at the given position.

  Totality: total
  Visibility: export
setNat : SizeOf a => CArray s n a -> SetPtr a => (m : Nat) -> {auto 0 _ : LT m n} -> a -> F1' s
  Writes a value to a C pointer at the given position.

  Totality: total
  Visibility: export
writeVect : SizeOf a => CArray s n a -> SetPtr a => Vect n a -> F1' s
  Writes the values from a vector to a C pointer

  Totality: total
  Visibility: export
withIArray : SizeOf a => CArray s n a -> (CIArray n a -> b) -> F1 s b
  Temporarily wraps the mutable array in an immutable wrapper and
  run a computation with that.
  
  This is safe, because the pure function cannot possibly share the
  immutable array by storing it in a mutable reference. It is
  referentially transparent, because we call it from a linear context.

  Totality: total
  Visibility: export
writeList : SizeOf a => SetPtr a => (as : List a) -> CArray s (length as) a -> F1' s
  Writes the values from a list to a C pointer

  Totality: total
  Visibility: export
withCArray : SizeOf a => (n : Nat) -> (CArray s n a -> F1 s b) -> b
  Totality: total
  Visibility: export
malloc : Lift1 s f => (0 a : Type) -> SizeOf a => (n : Nat) -> f (CArray s n a)
  Allocates a new C-pointer of `sizeof a * n` bytes.

  Totality: total
  Visibility: export
calloc : Lift1 s f => (0 a : Type) -> SizeOf a => (n : Nat) -> f (CArray s n a)
  Like `malloc` but resets all allocated bytes to zero.

  Totality: total
  Visibility: export
free : Lift1 s f => CArray s n a -> f ()
  Frees the memory allocated for a C-array.
  
  Note: Only call this if the C array is no longer used and has been
        allocated via a call to `malloc` or `alloc` (either in C land
        or in Idris). Afterwards, it is no longer safe to use the array
        for reading or writing, nor is it safe to call `free` on it again.
  
        For safe resource management, use the linear version of
        C arrays if possible. Otherwise, consider using a safer monad
        than `IO` if possible.

  Totality: total
  Visibility: export
fromList : Lift1 s f => SizeOf a => SetPtr a => (as : List a) -> f (CArray s (length as) a)
  Totality: total
  Visibility: export