git.iko.soy/Idris-dev
on master help sign in
Add a little documentation
e4a16c7Niklas Larsson
libs/contrib/CFFI/Memory.idr+12−2
compare with master
unifiedsplit
@@ -9,33 +9,40 @@ import Data.Vect
9%access public export
9%access public export
10%default partial
10%default partial
11
11
12+
12data CPtr = CPt Ptr Int
13data CPtr = CPt Ptr Int
13
14
14implicit toCPtr : Ptr -> CPtr
15implicit toCPtr : Ptr -> CPtr
15toCPtr p = CPt p 0
16toCPtr p = CPt p 0
16
17
18+||| Import of malloc from the C standard library.
17malloc : Int -> IO Ptr
19malloc : Int -> IO Ptr
18malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
20malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
19
21
22+||| Import of free from the C standard library.
20mfree : Ptr -> IO ()
23mfree : Ptr -> IO ()
21mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
24mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
22
25
26+||| Allocate enough memory to hold an instance of a C typr
23alloc : Composite -> IO CPtr
27alloc : Composite -> IO CPtr
24alloc t = return $ CPt !(malloc (sizeOf t)) 0
28alloc t = return $ CPt !(malloc (sizeOf t)) 0
25
29
30+||| Free memory allocated with alloc
26free : CPtr -> IO ()
31free : CPtr -> IO ()
27free (CPt p _ ) = mfree p
32free (CPt p _ ) = mfree p
28
33
34+||| Perform an IO action with memory that is freed afterwards
29withAlloc : Composite -> (CPtr -> IO ()) -> IO ()
35withAlloc : Composite -> (CPtr -> IO ()) -> IO ()
30withAlloc t f = do m <- alloc t
36withAlloc t f = do m <- alloc t
31 f m
37 f m
32 free m
38 free m
33
39
34infixl 1 ~~>
40infixl 1 ~~>
35−
41+||| Perform an IO action with memory that is freed afterwards
36(~~>) : Composite-> (CPtr -> IO ()) -> IO ()
42(~~>) : Composite-> (CPtr -> IO ()) -> IO ()
37(~~>) = withAlloc
43(~~>) = withAlloc
38
44
45+||| Read from memory
39peek : (t: CType) -> CPtr -> IO (translate t)
46peek : (t: CType) -> CPtr -> IO (translate t)
40peek I8 (CPt p o) = prim_peek8 p o
47peek I8 (CPt p o) = prim_peek8 p o
41peek I16 (CPt p o) = prim_peek16 p o
48peek I16 (CPt p o) = prim_peek16 p o
@@ -45,6 +52,7 @@ peek FLOAT (CPt p o) = prim_peekSingle p o
45peek DOUBLE (CPt p o) = prim_peekDouble p o
52peek DOUBLE (CPt p o) = prim_peekDouble p o
46peek PTR (CPt p o) = prim_peekPtr p o
53peek PTR (CPt p o) = prim_peekPtr p o
47
54
55+||| Write to memory
48poke : (t : CType) -> CPtr -> translate t -> IO ()
56poke : (t : CType) -> CPtr -> translate t -> IO ()
49poke I8 (CPt p o) x = do _ <- prim_poke8 p o x
57poke I8 (CPt p o) x = do _ <- prim_poke8 p o x
50 return ()
58 return ()
@@ -61,12 +69,13 @@ poke FLOAT (CPt p o) x = do _ <- prim_pokeSingle p o x
61poke DOUBLE (CPt p o) x = do _ <- prim_pokeDouble p o x
69poke DOUBLE (CPt p o) x = do _ <- prim_pokeDouble p o x
62 return ()
70 return ()
63
71
72+||| Update memory with a function.
64update : (t: CType) -> CPtr -> (translate t -> translate t) -> IO ()
73update : (t: CType) -> CPtr -> (translate t -> translate t) -> IO ()
65update ty cp f = do val <- peek ty cp
74update ty cp f = do val <- peek ty cp
66 out <- return $ f val
75 out <- return $ f val
67 poke ty cp out
76 poke ty cp out
68
77
69−-- TODO : Fix bounds checking
78+||| Get a pointer to a field in a composite value
70field : Composite -> Nat -> CPtr -> CPtr
79field : Composite -> Nat -> CPtr -> CPtr
71field arr@(ARRAY n t) i (CPt p o ) = CPt p (o + offset arr i)
80field arr@(ARRAY n t) i (CPt p o ) = CPt p (o + offset arr i)
72field un@(UNION xs) i (CPt p o ) = CPt p o
81field un@(UNION xs) i (CPt p o ) = CPt p o
@@ -76,5 +85,6 @@ field (T t) Z p = p
76
85
77infixl 10 #
86infixl 10 #
78
87
88+||| Get a pointer to a field in a composite value
79(#) : Composite -> Nat -> CPtr -> CPtr
89(#) : Composite -> Nat -> CPtr -> CPtr
80(#) = field
90(#) = field
libs/contrib/CFFI/Types.idr+19−1
@@ -15,6 +15,7 @@ data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
15data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
15data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
16 | PACKEDSTRUCT (List Composite)
16 | PACKEDSTRUCT (List Composite)
17
17
18+||| Implicit conversion of primitive C types to composites
18implicit mkComposite : CType -> Composite
19implicit mkComposite : CType -> Composite
19mkComposite x = T x
20mkComposite x = T x
20
21
@@ -34,6 +35,7 @@ Show Composite where
34 show (UNION xs) = "UNION " ++ show xs
35 show (UNION xs) = "UNION " ++ show xs
35 show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs
36 show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs
36
37
38+||| What Idris type the C type is marshalled to
37translate : CType -> Type
39translate : CType -> Type
38translate I8 = Bits8
40translate I8 = Bits8
39translate I16 = Bits16
41translate I16 = Bits16
@@ -44,6 +46,7 @@ translate DOUBLE = Double
44translate PTR = Ptr
46translate PTR = Ptr
45
47
46mutual
48mutual
49+ private
47 sizeOfCT : CType -> Int
50 sizeOfCT : CType -> Int
48 sizeOfCT I8 = 1
51 sizeOfCT I8 = 1
49 sizeOfCT I16 = 2
52 sizeOfCT I16 = 2
@@ -53,6 +56,8 @@ mutual
53 sizeOfCT DOUBLE = 8
56 sizeOfCT DOUBLE = 8
54 sizeOfCT PTR = prim__sizeofPtr
57 sizeOfCT PTR = prim__sizeofPtr
55
58
59+ ||| Size of value of the type in bytes
60+ export
56 sizeOf : Composite -> Int
61 sizeOf : Composite -> Int
57 sizeOf (T ct) = sizeOfCT ct
62 sizeOf (T ct) = sizeOfCT ct
58 sizeOf (ARRAY n t) = n * sizeOf t
63 sizeOf (ARRAY n t) = n * sizeOf t
@@ -60,6 +65,7 @@ mutual
60 sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
65 sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
61 sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
66 sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
62
67
68+ private
63 alignOfCT : CType -> Int
69 alignOfCT : CType -> Int
64 alignOfCT I8 = 1
70 alignOfCT I8 = 1
65 alignOfCT I16 = 2
71 alignOfCT I16 = 2
@@ -69,6 +75,8 @@ mutual
69 alignOfCT DOUBLE = prim__sizeofPtr
75 alignOfCT DOUBLE = prim__sizeofPtr
70 alignOfCT PTR = prim__sizeofPtr
76 alignOfCT PTR = prim__sizeofPtr
71
77
78+ ||| Alignment requirement of the type
79+ export
72 alignOf : Composite -> Int
80 alignOf : Composite -> Int
73 alignOf (T t) = alignOfCT t
81 alignOf (T t) = alignOfCT t
74 alignOf (ARRAY n t) = alignOf t
82 alignOf (ARRAY n t) = alignOf t
@@ -76,12 +84,15 @@ mutual
76 alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
84 alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
77 alignOf (PACKEDSTRUCT xs) = 1
85 alignOf (PACKEDSTRUCT xs) = 1
78
86
87+ private
79 pad : Int -> Int -> Int
88 pad : Int -> Int -> Int
80 pad pos align = let c = pos `mod` align in if c == 0 then 0 else align - c
89 pad pos align = let c = pos `mod` align in if c == 0 then 0 else align - c
81
90
91+ private
82 nextOffset : Composite -> Int -> Int
92 nextOffset : Composite -> Int -> Int
83 nextOffset ty pos = pos + pad pos (alignOf ty)
93 nextOffset ty pos = pos + pad pos (alignOf ty)
84
94
95+ private
85 offsetsStruct : List Composite -> List Int
96 offsetsStruct : List Composite -> List Int
86 offsetsStruct xs = offsets' xs 0
97 offsetsStruct xs = offsets' xs 0
87 where
98 where
@@ -89,6 +100,7 @@ mutual
89 offsets' [] _ = []
100 offsets' [] _ = []
90 offsets' (x::xs) pos = (nextOffset x pos)::(offsets' xs (nextOffset x pos + sizeOf x))
101 offsets' (x::xs) pos = (nextOffset x pos)::(offsets' xs (nextOffset x pos + sizeOf x))
91
102
103+ private
92 sizeOfStruct : List Composite -> Int
104 sizeOfStruct : List Composite -> Int
93 sizeOfStruct xs = sizeStruct' xs 0 1
105 sizeOfStruct xs = sizeStruct' xs 0 1
94 where
106 where
@@ -97,6 +109,8 @@ mutual
97 sizeStruct' (x::xs) pos maxAlign = sizeStruct' xs (nextOffset x pos + sizeOf x)
109 sizeStruct' (x::xs) pos maxAlign = sizeStruct' xs (nextOffset x pos + sizeOf x)
98 (max maxAlign (alignOf x))
110 (max maxAlign (alignOf x))
99
111
112+||| Number of fields in a composite type
113+export
100fields : Composite -> Nat
114fields : Composite -> Nat
101fields (STRUCT xs) = length xs
115fields (STRUCT xs) = length xs
102fields (PACKEDSTRUCT xs) = length xs
116fields (PACKEDSTRUCT xs) = length xs
@@ -104,6 +118,7 @@ fields (UNION xs) = length xs
104fields (ARRAY n _) = toNat n
118fields (ARRAY n _) = toNat n
105fields (T _) = 1
119fields (T _) = 1
106
120
121+private
107offsetsPacked : List Composite -> List Int
122offsetsPacked : List Composite -> List Int
108offsetsPacked xs = offsets' xs [] 0
123offsetsPacked xs = offsets' xs [] 0
109 where
124 where
@@ -117,6 +132,7 @@ indexOrFail i xs = case index' i xs of
117 Just x => x
132 Just x => x
118 Nothing => error "Out of bounds access"
133 Nothing => error "Out of bounds access"
119
134
135+||| The offset of a firld in a composite type
120export
136export
121offset : Composite -> Nat -> Int
137offset : Composite -> Nat -> Int
122offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)
138offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)
@@ -124,6 +140,8 @@ offset (PACKEDSTRUCT xs) i = indexOrFail i (offsetsPacked xs)
124offset (ARRAY _ t) i = sizeOf t * toIntNat i
140offset (ARRAY _ t) i = sizeOf t * toIntNat i
125offset (T _) _ = 0
141offset (T _) _ = 0
126
142
143+||| All offsets of a composite type
144+export
127offsets : Composite -> List Int
145offsets : Composite -> List Int
128offsets (STRUCT xs) = offsetsStruct xs
146offsets (STRUCT xs) = offsetsStruct xs
129offsets (PACKEDSTRUCT xs) = offsetsPacked xs
147offsets (PACKEDSTRUCT xs) = offsetsPacked xs
@@ -131,7 +149,7 @@ offsets (UNION xs) = replicate (length xs) 0
131offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
149offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
132offsets (T _) = [0]
150offsets (T _) = [0]
133
151
134−
152+||| The type of a field in a composite type.
135export
153export
136fieldType : Composite -> Nat -> Composite
154fieldType : Composite -> Nat -> Composite
137fieldType (STRUCT xs@(y::_)) i = indexOrFail i xs
155fieldType (STRUCT xs@(y::_)) i = indexOrFail i xs