@@ -0,0 +1,159 @@
1+||| Types for interfacing with C.
2+||| This file should be kept free from IO.
3+module CFFI.Types
4+
5+import Data.Vect
6+import Debug.Error
7+
8+%access public export
9+%default partial
10+
11+||| An universe of C types.
12+data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
13+
14+||| Composites of C types
15+data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
16+ | PACKEDSTRUCT (List Composite)
17+
18+||| Implicit conversion of primitive C types to composites
19+implicit mkComposite : CType -> Composite
20+mkComposite x = T x
21+
22+Show CType where
23+ show I8 = "I8"
24+ show I16 = "I16"
25+ show I32 = "I32"
26+ show I64 = "I64"
27+ show FLOAT = "FLOAT"
28+ show DOUBLE = "DOUBLE"
29+ show PTR = "PTR"
30+
31+Show Composite where
32+ show (T ct) = show ct
33+ show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t
34+ show (STRUCT xs) = "STRUCT " ++ show xs
35+ show (UNION xs) = "UNION " ++ show xs
36+ show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs
37+
38+||| What Idris type the C type is marshalled to
39+translate : CType -> Type
40+translate I8 = Bits8
41+translate I16 = Bits16
42+translate I32 = Bits32
43+translate I64 = Bits64
44+translate FLOAT = Double
45+translate DOUBLE = Double
46+translate PTR = Ptr
47+
48+mutual
49+ private
50+ sizeOfCT : CType -> Int
51+ sizeOfCT I8 = 1
52+ sizeOfCT I16 = 2
53+ sizeOfCT I32 = 4
54+ sizeOfCT I64 = 8
55+ sizeOfCT FLOAT = 4
56+ sizeOfCT DOUBLE = 8
57+ sizeOfCT PTR = prim__sizeofPtr
58+
59+ ||| Size of value of the type in bytes
60+ export
61+ sizeOf : Composite -> Int
62+ sizeOf (T ct) = sizeOfCT ct
63+ sizeOf (ARRAY n t) = n * sizeOf t
64+ sizeOf (STRUCT xs) = sizeOfStruct xs
65+ sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
66+ sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
67+
68+ private
69+ alignOfCT : CType -> Int
70+ alignOfCT I8 = 1
71+ alignOfCT I16 = 2
72+ alignOfCT I32 = 4
73+ alignOfCT I64 = prim__sizeofPtr
74+ alignOfCT FLOAT = 4
75+ alignOfCT DOUBLE = prim__sizeofPtr
76+ alignOfCT PTR = prim__sizeofPtr
77+
78+ ||| Alignment requirement of the type
79+ export
80+ alignOf : Composite -> Int
81+ alignOf (T t) = alignOfCT t
82+ alignOf (ARRAY n t) = alignOf t
83+ alignOf (STRUCT xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
84+ alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
85+ alignOf (PACKEDSTRUCT xs) = 1
86+
87+ private
88+ pad : Int -> Int -> Int
89+ pad pos align = let c = pos `mod` align in if c == 0 then 0 else align - c
90+
91+ private
92+ nextOffset : Composite -> Int -> Int
93+ nextOffset ty pos = pos + pad pos (alignOf ty)
94+
95+ private
96+ offsetsStruct : List Composite -> List Int
97+ offsetsStruct xs = offsets' xs 0
98+ where
99+ offsets' : List Composite -> Int -> List Int
100+ offsets' [] _ = []
101+ offsets' (x::xs) pos = (nextOffset x pos)::(offsets' xs (nextOffset x pos + sizeOf x))
102+
103+ private
104+ sizeOfStruct : List Composite -> Int
105+ sizeOfStruct xs = sizeStruct' xs 0 1
106+ where
107+ sizeStruct' : List Composite -> Int -> Int -> Int
108+ sizeStruct' [] pos maxAlign = pos + (pad pos maxAlign)
109+ sizeStruct' (x::xs) pos maxAlign = sizeStruct' xs (nextOffset x pos + sizeOf x)
110+ (max maxAlign (alignOf x))
111+
112+||| Number of fields in a composite type
113+export
114+fields : Composite -> Nat
115+fields (STRUCT xs) = length xs
116+fields (PACKEDSTRUCT xs) = length xs
117+fields (UNION xs) = length xs
118+fields (ARRAY n _) = toNat n
119+fields (T _) = 1
120+
121+private
122+offsetsPacked : List Composite -> List Int
123+offsetsPacked xs = offsets' xs [] 0
124+ where
125+ offsets' : List Composite -> List Int -> Int -> List Int
126+ offsets' [] acc _ = reverse acc
127+ offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
128+
129+private
130+indexOrFail : Nat -> List a -> a
131+indexOrFail i xs = case index' i xs of
132+ Just x => x
133+ Nothing => error "Out of bounds access"
134+
135+||| The offset of a firld in a composite type
136+export
137+offset : Composite -> Nat -> Int
138+offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)
139+offset (PACKEDSTRUCT xs) i = indexOrFail i (offsetsPacked xs)
140+offset (ARRAY _ t) i = sizeOf t * toIntNat i
141+offset (T _) _ = 0
142+
143+||| All offsets of a composite type
144+export
145+offsets : Composite -> List Int
146+offsets (STRUCT xs) = offsetsStruct xs
147+offsets (PACKEDSTRUCT xs) = offsetsPacked xs
148+offsets (UNION xs) = replicate (length xs) 0
149+offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
150+offsets (T _) = [0]
151+
152+||| The type of a field in a composite type.
153+export
154+fieldType : Composite -> Nat -> Composite
155+fieldType (STRUCT xs@(y::_)) i = indexOrFail i xs
156+fieldType (PACKEDSTRUCT xs@(y::_)) i = indexOrFail i xs
157+fieldType (UNION xs@(y::_)) i = indexOrFail i xs
158+fieldType (ARRAY n t) _ = t
159+fieldType t _ = t