0 | module Data.C.Struct
 1 |
 2 | import Control.Monad.Resource
 3 | import Data.C.Integer
 4 | import Data.C.SizeOf
 5 | import Data.Linear.ELift1
 6 | import Data.Linear.Token
 7 |
 8 | %default total
 9 |
10 | --------------------------------------------------------------------------------
11 | -- FFI
12 | --------------------------------------------------------------------------------
13 |
14 | export %foreign "C:cptr_malloc, cptr-idris"
15 |                 "scheme,chez:(lambda (x) (if (= 0 x) 0 (foreign-alloc x)))"
16 | prim__malloc : (size : Bits32) -> AnyPtr
17 |
18 | export %foreign "C:cptr_calloc, cptr-idris"
19 | prim__calloc : (n, size : Bits32) -> AnyPtr
20 |
21 | export %foreign "C:cptr_free, cptr-idris"
22 |                 "scheme,chez:(lambda (x) (if (= 0 x) '() (foreign-free x)))"
23 | prim__free : AnyPtr -> PrimIO ()
24 |
25 | --------------------------------------------------------------------------------
26 | -- WrappedPtr
27 | --------------------------------------------------------------------------------
28 |
29 | public export
30 | interface WrappedPtr (0 a : Type) where
31 |   wrap   : AnyPtr -> a
32 |   unwrap : a -> AnyPtr
33 |
34 | --------------------------------------------------------------------------------
35 | -- Struct
36 | --------------------------------------------------------------------------------
37 |
38 | ||| Interface for wrappers around `struct` pointers.
39 | |||
40 | ||| Functions `wrap` and `unwrap` are used to convert from and
41 | ||| to the underlying pointer.
42 | public export
43 | interface Struct (0 f : Type -> Type) where
44 |   swrap   : AnyPtr -> f s
45 |   sunwrap : f s -> AnyPtr
46 |
47 | export %inline
48 | Struct f => WrappedPtr (f s) where
49 |   wrap   = swrap
50 |   unwrap = sunwrap
51 |
52 | ||| Frees the memory allocated for a `struct`
53 | export %inline
54 | freeStruct1 : Struct f => f s -> F1' s
55 | freeStruct1 v = ffi $ prim__free (sunwrap v)
56 |
57 | ||| Allocates memory for a single `struct`
58 | export %inline
59 | allocStruct1 : (0 f : Type -> Type) -> SizeOf (f s) => Struct f => F1 s (f s)
60 | allocStruct1 f t = swrap (prim__malloc (cast $ sizeof (f s))) # t
61 |
62 | ||| Allocates memory for a single `struct`
63 | export %inline
64 | callocStruct1 : (0 f : Type -> Type) -> SizeOf (f s) => Struct f => F1 s (f s)
65 | callocStruct1 f t = swrap (prim__calloc 1 (cast $ sizeof (f s))) # t
66 |
67 | parameters {auto l1 : Lift1 s m}
68 |   ||| Frees the memory allocated for a `struct`
69 |   export %inline
70 |   freeStruct : Struct f => f s -> m ()
71 |   freeStruct v = lift1 (freeStruct1 v)
72 |
73 |   ||| Allocates memory for a single `struct` with all bits set to 0.
74 |   export %inline
75 |   allocStruct : (0 f : _) -> SizeOf (f s) => Struct f => m (f s)
76 |   allocStruct f = lift1 (allocStruct1 f)
77 |
78 |   ||| Allocates memory for a single `struct` with all bits set to 0.
79 |   export %inline
80 |   callocStruct : (0 f : _) -> SizeOf (f s) => Struct f => m (f s)
81 |   callocStruct f = lift1 (callocStruct1 f)
82 |
83 | --------------------------------------------------------------------------------
84 | -- Resource
85 | --------------------------------------------------------------------------------
86 |
87 | export %inline
88 | ELift1 s m => Struct f => Resource m (f s) where
89 |   cleanup v = lift1 (freeStruct1 v)
90 |