System.FFI

Additional FFI help for more interesting C types

Definitions

data Struct : String -> List (String, Type) -> Type

  A struct with a name and a list of key-value pairs of field names and their
  types.

Totality: total
Visibility: export

data FieldType : String -> Type -> List (String, Type) -> Type

  A proof that the field exists as an entry in the list of field names and
  their types.

Totality: total
Visibility: public export
Constructors:

First : FieldType n t ((n, t) :: ts)

Later : FieldType n t ts -> FieldType n t (f :: ts)

getField : Struct sn fs -> (n : String) -> FieldType n ty fs => ty

  Retrieve the value of the specified field in the given `Struct`.
  
  @ s the `Struct` to retrieve the value from
  @ n the name of the field in the `Struct`.

Totality: total
Visibility: public export

setField : Struct sn fs -> (n : String) -> FieldType n ty fs => ty -> IO ()

  Set the value of the specified field in the given `Struct`.
  
  @ s   the `Struct` in which the field exists
  @ n   the name of the field to set
  @ val the value to set the field to

Totality: total
Visibility: public export

malloc : HasIO io => Int -> io AnyPtr

  Allocate memory with libc `malloc`.
  
  @ size the number of bytes to allocate

Totality: total
Visibility: export

free : HasIO io => AnyPtr -> io ()

  Release memory with libc `free`.

Totality: total
Visibility: export