git.iko.soy/Idris-dev
on master help sign in
Split Ctype into composite and primitive
commit33166ee9504dd9d7a8d67fcbb8ee7c78148ab1de authorNiklas Larsson <niklas@mm.st> dateSun 14 Feb 2016, 11:47 (11 years ago) parent2d3bbcc
3 files changed+100−82
compare with master
unifiedsplit
libs/contrib/CFFI/Memory.idr+42−41 libs/contrib/CFFI/Types.idr+46−30 test/ffi008/ffi008.idr+12−11
libs/contrib/CFFI/Memory.idr+42−41
@@ -10,7 +10,7 @@ import Data.HVect
1010%access public export
1111%default partial
1212
13−data CPtr = CPt Ptr Int CType
13+data CPtr = CPt Ptr Int Composite
1414
1515implicit decayCPtr : CPtr -> Ptr
1616decayCPtr (CPt p _ _) = p
@@ -24,66 +24,67 @@ malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
2424mfree : Ptr -> IO ()
2525mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
2626
27−alloc : CType -> IO CPtr
28−alloc t = return $ CPt !(malloc (sizeOf t)) 0 t
27+alloc : Composite -> IO CPtr
28+alloc t = return $ CPt !(malloc (sizeOfComp t)) 0 t
2929
3030free : CPtr -> IO ()
3131free (CPt p _ _) = mfree p
3232
33−withAlloc : CType -> (CPtr -> IO ()) -> IO ()
33+withAlloc : Composite -> (CPtr -> IO ()) -> IO ()
3434withAlloc t f = do m <- alloc t
3535 f m
3636 free m
3737
3838infixl 1 ~~>
3939
40−(~~>) : CType -> (CPtr -> IO ()) -> IO ()
40+(~~>) : Composite-> (CPtr -> IO ()) -> IO ()
4141(~~>) = withAlloc
4242
4343ctype : CPtr -> CType
44−ctype (CPt _ _ t) = t
44+ctype (CPt _ _ (T t)) = t
45+
4546mutual
46− -- peekArray : (c : CPtr) -> IO (translate (ctype c))
47− -- peekArray (CPt p o a@(ARRAY n t)) = do
48− -- os <- return $ fromList (offsets a)
49− -- map (\x => peek (CPt p x t)) os
50−
51− -- pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()
52− -- pokeArray (CPt p o a@(ARRAY n t)) x = do
53− -- os <- fromList $ offsets a
54− -- ox <- zip os x
55− -- map (\(x, y)=>poke (CPt p x t) y) ox
56− -- return ()
57−
58− peek : (p : CPtr) -> IO (translate (ctype p))
59− peek (CPt p o I8) = prim_peek8 p o
60− peek (CPt p o I16) = prim_peek16 p o
61− peek (CPt p o I32) = prim_peek32 p o
62− peek (CPt p o I64) = prim_peek64 p o
63− peek (CPt p o FLOAT) = prim_peekSingle p o
64− peek (CPt p o DOUBLE) = prim_peekDouble p o
65− peek (CPt p o PTR) = prim_peekPtr p o
47+{-
48+ peekArray : (c : CPtr) -> IO (translate (ctype c))
49+ peekArray (CPt p o a@(ARRAY n t)) = do
50+ os <- return $ fromList (offsets a)
51+ traverse (\x => peek (CPt p x t)) os
52+
53+ pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()
54+ pokeArray (CPt p o a@(ARRAY n t)) x = do
55+ os <- fromList $ offsets a
56+ ox <- zip os x
57+ traverse_ (\(x, y)=>poke (CPt p x t) y) ox
58+-}
59+ peek : (p : CPtr) -> (t: CType) -> IO (translate t)
60+ peek (CPt p o (T I8)) I8 = prim_peek8 p o
61+ peek (CPt p o (T I16)) I16= prim_peek16 p o
62+ peek (CPt p o (T I32)) I32 = prim_peek32 p o
63+ peek (CPt p o (T I64)) I64 = prim_peek64 p o
64+ peek (CPt p o (T FLOAT)) FLOAT = prim_peekSingle p o
65+ peek (CPt p o (T DOUBLE)) DOUBLE = prim_peekDouble p o
66+ peek (CPt p o (T PTR)) PTR = prim_peekPtr p o
6667 -- peek cp@(CPt p o (ARRAY n t)) = peekArray cp
6768 -- peek (CPt p o (UNION xs)) = ?peekUnion
6869 -- peek (CPt p o (STRUCT xs)) = ?peekStruct
6970 -- peek (CPt p o (PACKEDSTRUCT xs)) = ?peekPacked
7071
7172
72− poke : (p : CPtr) -> translate $ ctype p -> IO ()
73− poke (CPt p o I8) x = do _ <- prim_poke8 p o x
74− return ()
75− poke (CPt p o I16) x = do _ <- prim_poke16 p o x
76− return ()
77− poke (CPt p o I32) x = do _ <- prim_poke32 p o x
78− return ()
79− poke (CPt p o I64) x = do _ <- prim_poke64 p o x
80− return ()
81− poke (CPt p o PTR) x = do _ <- prim_pokePtr p o x
82− return ()
83− poke (CPt p o FLOAT) x = do _ <- prim_pokeSingle p o x
84− return ()
85− poke (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
86− return ()
73+ poke : (p : CPtr) -> (t : CType) -> translate t -> IO ()
74+ poke (CPt p o (T I8)) I8 x = do _ <- prim_poke8 p o x
75+ return ()
76+ poke (CPt p o (T I16)) I16 x = do _ <- prim_poke16 p o x
77+ return ()
78+ poke (CPt p o (T I32)) I32 x = do _ <- prim_poke32 p o x
79+ return ()
80+ poke (CPt p o (T I64)) I64 x = do _ <- prim_poke64 p o x
81+ return ()
82+ poke (CPt p o (T PTR)) PTR x = do _ <- prim_pokePtr p o x
83+ return ()
84+ poke (CPt p o (T FLOAT)) FLOAT x = do _ <- prim_pokeSingle p o x
85+ return ()
86+ poke (CPt p o (T DOUBLE)) DOUBLE x = do _ <- prim_pokeDouble p o x
87+ return ()
8788 -- poke cp@(CPt p o (ARRAY n t)) x = pokeArray cp x
8889 -- poke (CPt p o (UNION xs)) x = ?pokeUnion
8990 -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct
libs/contrib/CFFI/Types.idr+46−30
@@ -10,8 +10,12 @@ import Data.HVect
1010
1111||| An universe of C types.
1212data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
13− | ARRAY Int CType | STRUCT (List CType) | UNION (List CType)
14− | PACKEDSTRUCT (List CType)
13+
14+data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
15+ | PACKEDSTRUCT (List Composite)
16+
17+implicit mkComposite : CType -> Composite
18+mkComposite x = T x
1519
1620Show CType where
1721 show I8 = "I8"
@@ -21,6 +25,9 @@ Show CType where
2125 show FLOAT = "FLOAT"
2226 show DOUBLE = "DOUBLE"
2327 show PTR = "PTR"
28+
29+Show Composite where
30+ show (T ct) = show ct
2431 show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t
2532 show (STRUCT xs) = "STRUCT " ++ show xs
2633 show (UNION xs) = "UNION " ++ show xs
@@ -34,10 +41,13 @@ translate I64 = Bits64
3441translate FLOAT = Double
3542translate DOUBLE = Double
3643translate PTR = Ptr
37−translate (ARRAY n t) = Vect (toNat n) (translate t)
38−translate (STRUCT xs) = HVect $ fromList (map translate xs)
39−translate (UNION xs) = HVect $ fromList (map translate xs)
40−translate (PACKEDSTRUCT xs) = HVect $ fromList (map translate xs)
44+
45+translateComp : Composite -> Type
46+translateComp (T ct) = translate ct
47+translateComp (ARRAY n t) = Vect (toNat n) (translateComp t)
48+translateComp (STRUCT xs) = HVect $ fromList (map translateComp xs)
49+translateComp (UNION xs) = HVect $ fromList (map translateComp xs)
50+translateComp (PACKEDSTRUCT xs) = HVect $ fromList (map translateComp xs)
4151
4252mutual
4353 sizeOf : CType -> Int
@@ -48,10 +58,13 @@ mutual
4858 sizeOf FLOAT = 4
4959 sizeOf DOUBLE = 8
5060 sizeOf PTR = prim__sizeofPtr
51− sizeOf (ARRAY n t) = n * sizeOf t
52− sizeOf (STRUCT xs) = sizeOfStruct xs
53− sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
54− sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
61+
62+ sizeOfComp : Composite -> Int
63+ sizeOfComp (T ct) = sizeOf ct
64+ sizeOfComp (ARRAY n t) = n * sizeOfComp t
65+ sizeOfComp (STRUCT xs) = sizeOfStruct xs
66+ sizeOfComp (UNION xs) = foldl (\acc, x =>max acc $ sizeOfComp x) 0 xs
67+ sizeOfComp (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOfComp x) 0 xs
5568
5669 alignOf : CType -> Int
5770 alignOf I8 = 1
@@ -61,64 +74,67 @@ mutual
6174 alignOf FLOAT = 4
6275 alignOf DOUBLE = prim__sizeofPtr
6376 alignOf PTR = prim__sizeofPtr
64− alignOf (ARRAY n t) = alignOf t
65− alignOf (STRUCT xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
66− alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
67− alignOf (PACKEDSTRUCT xs) = 1
6877
69− offsetsStruct : List CType -> List Int
78+ alignOfComp : Composite -> Int
79+ alignOfComp (T t) = alignOf t
80+ alignOfComp (ARRAY n t) = alignOfComp t
81+ alignOfComp (STRUCT xs) = foldl (\acc, x => max acc $ alignOfComp x) 0 xs
82+ alignOfComp (UNION xs) = foldl (\acc, x => max acc $ alignOfComp x) 0 xs
83+ alignOfComp (PACKEDSTRUCT xs) = 1
84+
85+ offsetsStruct : List Composite -> List Int
7086 offsetsStruct xs = offsets' xs [] 0
7187 where
72− offsets' : List CType -> List Int -> Int -> List Int
88+ offsets' : List Composite -> List Int -> Int -> List Int
7389 offsets' [] acc _ = reverse acc
74− offsets' (x::xs) ys curr = let a = alignOf x
90+ offsets' (x::xs) ys curr = let a = alignOfComp x
7591 padding = let c = curr `mod` a
7692 in if c == 0 then 0 else a - c
7793 off = curr + padding
78− in offsets' xs (off::ys) (off + sizeOf x)
94+ in offsets' xs (off::ys) (off + sizeOfComp x)
7995
80− sizeOfStruct : List CType -> Int
96+ sizeOfStruct : List Composite -> Int
8197 sizeOfStruct xs = case (reverse xs, reverse (offsetsStruct xs)) of
8298 ([], _) => 0
83− (x::_, y::_) => let end = y + sizeOf x
99+ (x::_, y::_) => let end = y + sizeOfComp x
84100 endPadding = let c = end `mod` align in
85101 if c == 0 then 0 else align - c
86102 in end + endPadding
87103 where
88104 align : Int
89− align = foldl (\acc, x => max acc $ alignOf x) 1 xs
105+ align = foldl (\acc, x => max acc $ alignOfComp x) 1 xs
90106
91−fields : CType -> Nat
107+fields : Composite -> Nat
92108fields (STRUCT xs) = length xs
93109fields (PACKEDSTRUCT xs) = length xs
94110fields (UNION xs) = length xs
95111fields (ARRAY n _) = toNat n
96112fields _ = 1
97113
98−offsetsPacked : List CType -> List Int
114+offsetsPacked : List Composite -> List Int
99115offsetsPacked xs = offsets' xs [] 0
100116 where
101− offsets' : List CType -> List Int -> Int -> List Int
117+ offsets' : List Composite -> List Int -> Int -> List Int
102118 offsets' [] acc _ = reverse acc
103− offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
119+ offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOfComp x)
104120
105121-- TODO: Use index and fix upp proofs.
106−offset : CType -> Nat -> Int
122+offset : Composite -> Nat -> Int
107123offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
108124offset (PACKEDSTRUCT xs) i = fromMaybe 0 $ index' i (offsetsPacked xs)
109−offset (ARRAY _ t) i = sizeOf t * toIntNat i
125+offset (ARRAY _ t) i = sizeOfComp t * toIntNat i
110126offset _ _ = 0
111127
112−offsets : CType -> List Int
128+offsets : Composite -> List Int
113129offsets (STRUCT xs) = offsetsStruct xs
114130offsets (PACKEDSTRUCT xs) = offsetsPacked xs
115131offsets (UNION xs) = replicate (length xs) 0
116−offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
132+offsets (ARRAY n t) = [ x*sizeOfComp t | x <- [0..n-1]]
117133offsets _ = [0]
118134
119135-- TODO: handle out of bounds with proofs
120136-- Also choose a better name.
121−select : CType -> Nat -> CType
137+select : Composite -> Nat -> Composite
122138select (STRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
123139select (PACKEDSTRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
124140select (UNION xs@(y::_)) i = fromMaybe y (index' i xs)
test/ffi008/ffi008.idr+12−11
@@ -18,23 +18,24 @@ mystruct = foreign FFI_C "&mystruct" (IO Ptr)
1818print_mystruct : IO ()
1919print_mystruct = foreign FFI_C "print_mystruct" (IO ())
2020
21−test1 : CType
21+test1 : Composite
2222test1 = STRUCT [I8, I64]
2323
24−test2 : CType
24+test2 : Composite
2525test2 = STRUCT [I32, I16]
2626
27−test3 : CType
27+test3 : Composite
2828test3 = STRUCT [DOUBLE, DOUBLE, I8, I64]
2929
30−test4 : CType
30+test4 : Composite
3131test4 = PACKEDSTRUCT [I8, I8, I8, I64]
3232
3333printMore : IO ()
3434printMore = do
3535 p <- alloc test3
3636 f3 <- return $ p # 1
37− a <- peek f3
37+ a <- peek f3 DOUBLE
38+ printLn a
3839 printLn p
3940 printLn f3
4041 free p
@@ -42,19 +43,19 @@ printMore = do
4243 cms <- return $ CPt ms 0 (STRUCT [I32, I16])
4344 f1 <- return $ cms # 0
4445 printLn f1
45− prim_poke32 f1 0 122
46−
46+ poke f1 I32 122
47+
4748 print_mystruct
4849 printLn test4
4950 printLn !size1
5051 printLn !size2
5152 printLn $ fields test3
5253 printLn $ offsets (STRUCT [I8, I8, I8, I64, test3])
53− printLn $ sizeOf (ARRAY 67 I32)
54− printLn $ sizeOf test3
54+ printLn $ sizeOfComp (ARRAY 67 I32)
55+ printLn $ sizeOfComp test3
5556
5657main : IO ()
5758main = do
58− printLn $ sizeOf test1 == !size1
59− printLn $ sizeOf test2 == !size2
59+ printLn $ sizeOfComp test1 == !size1
60+ printLn $ sizeOfComp test2 == !size2
6061 printMore