IdrisDoc: CFFI.Types

# CFFI.Types

Types for interfacing with C.
This file should be kept free from IO.

data CType : Type

  An universe of C types.

  I8 : CType
  I16 : CType
  I32 : CType
  I64 : CType
  FLOAT : CType
  DOUBLE : CType
  PTR : CType
data Composite : Type

  Composites of C types

  T : CType -> Composite
  ARRAY : Int -> Composite -> Composite
  STRUCT : List Composite -> Composite
  UNION : List Composite -> Composite
  PACKEDSTRUCT : List Composite -> Composite
alignOf : Composite -> Int

  Alignment requirement of the type

fieldType : Composite -> Nat -> Composite

  The type of a field in a composite type.

fields : Composite -> Nat

  Number of fields in a composite type

mkComposite : CType -> Composite

  Implicit conversion of primitive C types to composites

offset : Composite -> Nat -> Int

  The offset of a field in a composite type

offsets : Composite -> List Int

  All offsets of a composite type

sizeOf : Composite -> Int

  Size of value of the type in bytes

translate : CType -> Type

  What Idris type the C type is marshalled to