0 | ||| Additional FFI help for more interesting C types
 1 | module System.FFI
 2 | -- Some assumptions are made about the existence of this module in
 3 | -- Compiler.CompileExpr
 4 |
 5 |
 6 | %default total
 7 |
 8 | ||| A struct with a name and a list of key-value pairs of field names and their
 9 | ||| types.
10 | export
11 | data Struct : String -> -- C struct name
12 |               List (String, Type) -> -- field names and types
13 |               Type where
14 |
15 | ||| A proof that the field exists as an entry in the list of field names and
16 | ||| their types.
17 | public export
18 | data FieldType : String -> Type -> List (String, Type) -> Type where
19 |      First : FieldType n t ((n, t) :: ts)
20 |      Later : FieldType n t ts -> FieldType n t (f :: ts)
21 |
22 | %extern
23 | prim__getField : {s : _} -> forall fs, ty .
24 |                          Struct s fs -> (n : String) ->
25 |                          FieldType n ty fs -> ty
26 | %extern
27 | prim__setField : {s : _} -> forall fs, ty .
28 |                          Struct s fs -> (n : String) ->
29 |                          FieldType n ty fs -> ty -> PrimIO ()
30 |
31 | ||| Retrieve the value of the specified field in the given `Struct`.
32 | |||
33 | ||| @ s the `Struct` to retrieve the value from
34 | ||| @ n the name of the field in the `Struct`.
35 | public export %inline
36 | getField : {sn : _} -> (s : Struct sn fs) -> (n : String) ->
37 |            {auto fieldok : FieldType n ty fs} -> ty
38 | getField s n = prim__getField s n fieldok
39 |
40 | ||| Set the value of the specified field in the given `Struct`.
41 | |||
42 | ||| @ s   the `Struct` in which the field exists
43 | ||| @ n   the name of the field to set
44 | ||| @ val the value to set the field to
45 | public export %inline
46 | setField : {sn : _} -> (s : Struct sn fs) -> (n : String) ->
47 |            {auto fieldok : FieldType n ty fs} -> (val : ty) -> IO ()
48 | setField s n val = primIO (prim__setField s n fieldok val)
49 |
50 | %foreign "C:idris2_malloc, libidris2_support, idris_memory.h"
51 | prim__malloc : (size : Int) -> PrimIO AnyPtr
52 |
53 | %foreign "C:idris2_free, libidris2_support, idris_memory.h"
54 |          "javascript:lambda:()=>undefined"
55 | prim__free : AnyPtr -> PrimIO ()
56 |
57 | ||| Allocate memory with libc `malloc`.
58 | |||
59 | ||| @ size the number of bytes to allocate
60 | export
61 | malloc : HasIO io => (size : Int) -> io AnyPtr
62 | malloc size = primIO $ prim__malloc size
63 |
64 | ||| Release memory with libc `free`.
65 | export
66 | free : HasIO io => AnyPtr -> io ()
67 | free ptr = primIO $ prim__free ptr
68 |