Idris2Doc : Data.C.Array8

Data.C.Array8

(source)
Reexports
import public Data.Fin
import public Data.Linear.Token
import public Data.Array.Index
Definitions
prim__setbits8 : AnyPtr -> Integer -> Bits8 -> PrimIO ()
prim__getbits8 : AnyPtr -> Integer -> Bits8
record CIArray8 : Nat -> Type
  Totality: total
  Visibility: export
  Constructor: 
IA : AnyPtr -> CIArray8 n

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

  Totality: total
  Visibility: export
foldrKV : (Fin n -> Bits8 -> b -> b) -> b -> CIArray8 n -> b
  Right fold over the values of an array plus their indices.

  Totality: total
  Visibility: export
foldr : (Bits8 -> b -> b) -> b -> CIArray8 n -> b
  Right fold over the values of an array

  Totality: total
  Visibility: export
foldlKV : (Fin n -> b -> Bits8 -> b) -> b -> CIArray8 n -> b
  Left fold over the values of an array plus their indices.

  Totality: total
  Visibility: export
foldl : (b -> Bits8 -> b) -> b -> CIArray8 n -> b
  Left fold over the values of an array

  Totality: total
  Visibility: export
record CArray8 : Type -> Nat -> Type
  Totality: total
  Visibility: export
  Constructor: 
CA : AnyPtr -> CArray8 s n

  Projection: 
.ptr : CArray8 s n -> AnyPtr

  Hint: 
ELift1 s f => Resource f (CArray8 s n)
0 CArray8IO : Nat -> Type
  Convenience alias for `CArray8' RIO`

  Totality: total
  Visibility: public export
unsafeUnwrap : CArray8 s n -> AnyPtr
  Totality: total
  Visibility: export
unsafeWrap : AnyPtr -> CArray8 s n
  Totality: total
  Visibility: export
malloc1 : (n : Nat) -> F1 s (CArray8 s n)
  Allocates a new C-pointer of `sizeof a * n` bytes.

  Totality: total
  Visibility: export
calloc1 : (n : Nat) -> F1 s (CArray8 s n)
  Like `malloc1` but resets all allocated bytes to zero.

  Totality: total
  Visibility: export
free1 : CArray8 s n -> 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
get : CArray8 s n -> Fin n -> F1 s Bits8
  Reads a value from a C-pointer at the given position.

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

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

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

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

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

  Totality: total
  Visibility: export
writeVect : CArray8 s n -> Vect n Bits8 -> F1' s
  Writes the values from a vector to a C pointer

  Totality: total
  Visibility: export
withIArray : CArray8 s n -> (CIArray8 n -> 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 : (as : List Bits8) -> CArray8 s (length as) -> F1' s
  Writes the values from a list to a C pointer

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

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

  Totality: total
  Visibility: export
free : Lift1 s f => CArray8 s n -> f ()
  Totality: total
  Visibility: export
fromList : Lift1 s f => (as : List Bits8) -> f (CArray8 s (length as))
  Totality: total
  Visibility: export