git.iko.soy/Idris-dev
on master help sign in
Split Ctype into composite and primitive
33166eeNiklas Larsson
libs/contrib/CFFI/Memory.idr+42−41
compare with master
unifiedsplit
@@ -10,7 +10,7 @@ import Data.HVect
10%access public export
10%access public export
11%default partial
11%default partial
12
12
13−data CPtr = CPt Ptr Int CType
13+data CPtr = CPt Ptr Int Composite
14
14
15implicit decayCPtr : CPtr -> Ptr
15implicit decayCPtr : CPtr -> Ptr
16decayCPtr (CPt p _ _) = p
16decayCPtr (CPt p _ _) = p
@@ -24,66 +24,67 @@ malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
24mfree : Ptr -> IO ()
24mfree : Ptr -> IO ()
25mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
25mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
26
26
27−alloc : CType -> IO CPtr
27+alloc : Composite -> IO CPtr
28−alloc t = return $ CPt !(malloc (sizeOf t)) 0 t
28+alloc t = return $ CPt !(malloc (sizeOfComp t)) 0 t
29
29
30free : CPtr -> IO ()
30free : CPtr -> IO ()
31free (CPt p _ _) = mfree p
31free (CPt p _ _) = mfree p
32
32
33−withAlloc : CType -> (CPtr -> IO ()) -> IO ()
33+withAlloc : Composite -> (CPtr -> IO ()) -> IO ()
34withAlloc t f = do m <- alloc t
34withAlloc t f = do m <- alloc t
35 f m
35 f m
36 free m
36 free m
37
37
38infixl 1 ~~>
38infixl 1 ~~>
39
39
40−(~~>) : CType -> (CPtr -> IO ()) -> IO ()
40+(~~>) : Composite-> (CPtr -> IO ()) -> IO ()
41(~~>) = withAlloc
41(~~>) = withAlloc
42
42
43ctype : CPtr -> CType
43ctype : CPtr -> CType
44−ctype (CPt _ _ t) = t
44+ctype (CPt _ _ (T t)) = t
45+
45mutual
46mutual
47+{-
46− -- peekArray : (c : CPtr) -> IO (translate (ctype c))
48+ peekArray : (c : CPtr) -> IO (translate (ctype c))
47− -- peekArray (CPt p o a@(ARRAY n t)) = do
49+ peekArray (CPt p o a@(ARRAY n t)) = do
48− -- os <- return $ fromList (offsets a)
50+ os <- return $ fromList (offsets a)
49− -- map (\x => peek (CPt p x t)) os
51+ traverse (\x => peek (CPt p x t)) os
50−
52+
51− -- pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()
53+ pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()
52− -- pokeArray (CPt p o a@(ARRAY n t)) x = do
54+ pokeArray (CPt p o a@(ARRAY n t)) x = do
53− -- os <- fromList $ offsets a
55+ os <- fromList $ offsets a
54− -- ox <- zip os x
56+ ox <- zip os x
55− -- map (\(x, y)=>poke (CPt p x t) y) ox
57+ traverse_ (\(x, y)=>poke (CPt p x t) y) ox
56− -- return ()
58+-}
57−
58− peek : (p : CPtr) -> IO (translate (ctype p))
59+ peek : (p : CPtr) -> (t: CType) -> IO (translate t)
59− peek (CPt p o I8) = prim_peek8 p o
60+ peek (CPt p o (T I8)) I8 = prim_peek8 p o
60− peek (CPt p o I16) = prim_peek16 p o
61+ peek (CPt p o (T I16)) I16= prim_peek16 p o
61− peek (CPt p o I32) = prim_peek32 p o
62+ peek (CPt p o (T I32)) I32 = prim_peek32 p o
62− peek (CPt p o I64) = prim_peek64 p o
63+ peek (CPt p o (T I64)) I64 = prim_peek64 p o
63− peek (CPt p o FLOAT) = prim_peekSingle p o
64+ peek (CPt p o (T FLOAT)) FLOAT = prim_peekSingle p o
64− peek (CPt p o DOUBLE) = prim_peekDouble p o
65+ peek (CPt p o (T DOUBLE)) DOUBLE = prim_peekDouble p o
65− peek (CPt p o PTR) = prim_peekPtr p o
66+ peek (CPt p o (T PTR)) PTR = prim_peekPtr p o
66 -- peek cp@(CPt p o (ARRAY n t)) = peekArray cp
67 -- peek cp@(CPt p o (ARRAY n t)) = peekArray cp
67 -- peek (CPt p o (UNION xs)) = ?peekUnion
68 -- peek (CPt p o (UNION xs)) = ?peekUnion
68 -- peek (CPt p o (STRUCT xs)) = ?peekStruct
69 -- peek (CPt p o (STRUCT xs)) = ?peekStruct
69 -- peek (CPt p o (PACKEDSTRUCT xs)) = ?peekPacked
70 -- peek (CPt p o (PACKEDSTRUCT xs)) = ?peekPacked
70
71
71
72
72− poke : (p : CPtr) -> translate $ ctype p -> IO ()
73+ poke : (p : CPtr) -> (t : CType) -> translate t -> IO ()
73− poke (CPt p o I8) x = do _ <- prim_poke8 p o x
74+ poke (CPt p o (T I8)) I8 x = do _ <- prim_poke8 p o x
74− return ()
75+ return ()
75− poke (CPt p o I16) x = do _ <- prim_poke16 p o x
76+ poke (CPt p o (T I16)) I16 x = do _ <- prim_poke16 p o x
76− return ()
77+ return ()
77− poke (CPt p o I32) x = do _ <- prim_poke32 p o x
78+ poke (CPt p o (T I32)) I32 x = do _ <- prim_poke32 p o x
78− return ()
79+ return ()
79− poke (CPt p o I64) x = do _ <- prim_poke64 p o x
80+ poke (CPt p o (T I64)) I64 x = do _ <- prim_poke64 p o x
80− return ()
81+ return ()
81− poke (CPt p o PTR) x = do _ <- prim_pokePtr p o x
82+ poke (CPt p o (T PTR)) PTR x = do _ <- prim_pokePtr p o x
82− return ()
83+ return ()
83− poke (CPt p o FLOAT) x = do _ <- prim_pokeSingle p o x
84+ poke (CPt p o (T FLOAT)) FLOAT x = do _ <- prim_pokeSingle p o x
84− return ()
85+ return ()
85− poke (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
86+ poke (CPt p o (T DOUBLE)) DOUBLE x = do _ <- prim_pokeDouble p o x
86− return ()
87+ return ()
87 -- poke cp@(CPt p o (ARRAY n t)) x = pokeArray cp x
88 -- poke cp@(CPt p o (ARRAY n t)) x = pokeArray cp x
88 -- poke (CPt p o (UNION xs)) x = ?pokeUnion
89 -- poke (CPt p o (UNION xs)) x = ?pokeUnion
89 -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct
90 -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct
libs/contrib/CFFI/Types.idr+46−30
@@ -10,8 +10,12 @@ import Data.HVect
10
10
11||| An universe of C types.
11||| An universe of C types.
12data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
12data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
13+
13− | ARRAY Int CType | STRUCT (List CType) | UNION (List CType)
14+data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
14− | PACKEDSTRUCT (List CType)
15+ | PACKEDSTRUCT (List Composite)
16+
17+implicit mkComposite : CType -> Composite
18+mkComposite x = T x
15
19
16Show CType where
20Show CType where
17 show I8 = "I8"
21 show I8 = "I8"
@@ -21,6 +25,9 @@ Show CType where
21 show FLOAT = "FLOAT"
25 show FLOAT = "FLOAT"
22 show DOUBLE = "DOUBLE"
26 show DOUBLE = "DOUBLE"
23 show PTR = "PTR"
27 show PTR = "PTR"
28+
29+Show Composite where
30+ show (T ct) = show ct
24 show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t
31 show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t
25 show (STRUCT xs) = "STRUCT " ++ show xs
32 show (STRUCT xs) = "STRUCT " ++ show xs
26 show (UNION xs) = "UNION " ++ show xs
33 show (UNION xs) = "UNION " ++ show xs
@@ -34,10 +41,13 @@ translate I64 = Bits64
34translate FLOAT = Double
41translate FLOAT = Double
35translate DOUBLE = Double
42translate DOUBLE = Double
36translate PTR = Ptr
43translate PTR = Ptr
44+
45+translateComp : Composite -> Type
46+translateComp (T ct) = translate ct
37−translate (ARRAY n t) = Vect (toNat n) (translate t)
47+translateComp (ARRAY n t) = Vect (toNat n) (translateComp t)
38−translate (STRUCT xs) = HVect $ fromList (map translate xs)
48+translateComp (STRUCT xs) = HVect $ fromList (map translateComp xs)
39−translate (UNION xs) = HVect $ fromList (map translate xs)
49+translateComp (UNION xs) = HVect $ fromList (map translateComp xs)
40−translate (PACKEDSTRUCT xs) = HVect $ fromList (map translate xs)
50+translateComp (PACKEDSTRUCT xs) = HVect $ fromList (map translateComp xs)
41
51
42mutual
52mutual
43 sizeOf : CType -> Int
53 sizeOf : CType -> Int
@@ -48,10 +58,13 @@ mutual
48 sizeOf FLOAT = 4
58 sizeOf FLOAT = 4
49 sizeOf DOUBLE = 8
59 sizeOf DOUBLE = 8
50 sizeOf PTR = prim__sizeofPtr
60 sizeOf PTR = prim__sizeofPtr
51− sizeOf (ARRAY n t) = n * sizeOf t
61+
62+ sizeOfComp : Composite -> Int
63+ sizeOfComp (T ct) = sizeOf ct
64+ sizeOfComp (ARRAY n t) = n * sizeOfComp t
52− sizeOf (STRUCT xs) = sizeOfStruct xs
65+ sizeOfComp (STRUCT xs) = sizeOfStruct xs
53− sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
66+ sizeOfComp (UNION xs) = foldl (\acc, x =>max acc $ sizeOfComp x) 0 xs
54− sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
67+ sizeOfComp (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOfComp x) 0 xs
55
68
56 alignOf : CType -> Int
69 alignOf : CType -> Int
57 alignOf I8 = 1
70 alignOf I8 = 1
@@ -61,64 +74,67 @@ mutual
61 alignOf FLOAT = 4
74 alignOf FLOAT = 4
62 alignOf DOUBLE = prim__sizeofPtr
75 alignOf DOUBLE = prim__sizeofPtr
63 alignOf PTR = prim__sizeofPtr
76 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
68
77
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+
69− offsetsStruct : List CType -> List Int
85+ offsetsStruct : List Composite -> List Int
70 offsetsStruct xs = offsets' xs [] 0
86 offsetsStruct xs = offsets' xs [] 0
71 where
87 where
72− offsets' : List CType -> List Int -> Int -> List Int
88+ offsets' : List Composite -> List Int -> Int -> List Int
73 offsets' [] acc _ = reverse acc
89 offsets' [] acc _ = reverse acc
74− offsets' (x::xs) ys curr = let a = alignOf x
90+ offsets' (x::xs) ys curr = let a = alignOfComp x
75 padding = let c = curr `mod` a
91 padding = let c = curr `mod` a
76 in if c == 0 then 0 else a - c
92 in if c == 0 then 0 else a - c
77 off = curr + padding
93 off = curr + padding
78− in offsets' xs (off::ys) (off + sizeOf x)
94+ in offsets' xs (off::ys) (off + sizeOfComp x)
79
95
80− sizeOfStruct : List CType -> Int
96+ sizeOfStruct : List Composite -> Int
81 sizeOfStruct xs = case (reverse xs, reverse (offsetsStruct xs)) of
97 sizeOfStruct xs = case (reverse xs, reverse (offsetsStruct xs)) of
82 ([], _) => 0
98 ([], _) => 0
83− (x::_, y::_) => let end = y + sizeOf x
99+ (x::_, y::_) => let end = y + sizeOfComp x
84 endPadding = let c = end `mod` align in
100 endPadding = let c = end `mod` align in
85 if c == 0 then 0 else align - c
101 if c == 0 then 0 else align - c
86 in end + endPadding
102 in end + endPadding
87 where
103 where
88 align : Int
104 align : Int
89− align = foldl (\acc, x => max acc $ alignOf x) 1 xs
105+ align = foldl (\acc, x => max acc $ alignOfComp x) 1 xs
90
106
91−fields : CType -> Nat
107+fields : Composite -> Nat
92fields (STRUCT xs) = length xs
108fields (STRUCT xs) = length xs
93fields (PACKEDSTRUCT xs) = length xs
109fields (PACKEDSTRUCT xs) = length xs
94fields (UNION xs) = length xs
110fields (UNION xs) = length xs
95fields (ARRAY n _) = toNat n
111fields (ARRAY n _) = toNat n
96fields _ = 1
112fields _ = 1
97
113
98−offsetsPacked : List CType -> List Int
114+offsetsPacked : List Composite -> List Int
99offsetsPacked xs = offsets' xs [] 0
115offsetsPacked xs = offsets' xs [] 0
100 where
116 where
101− offsets' : List CType -> List Int -> Int -> List Int
117+ offsets' : List Composite -> List Int -> Int -> List Int
102 offsets' [] acc _ = reverse acc
118 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)
104
120
105-- TODO: Use index and fix upp proofs.
121-- TODO: Use index and fix upp proofs.
106−offset : CType -> Nat -> Int
122+offset : Composite -> Nat -> Int
107offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
123offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
108offset (PACKEDSTRUCT xs) i = fromMaybe 0 $ index' i (offsetsPacked xs)
124offset (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
110offset _ _ = 0
126offset _ _ = 0
111
127
112−offsets : CType -> List Int
128+offsets : Composite -> List Int
113offsets (STRUCT xs) = offsetsStruct xs
129offsets (STRUCT xs) = offsetsStruct xs
114offsets (PACKEDSTRUCT xs) = offsetsPacked xs
130offsets (PACKEDSTRUCT xs) = offsetsPacked xs
115offsets (UNION xs) = replicate (length xs) 0
131offsets (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]]
117offsets _ = [0]
133offsets _ = [0]
118
134
119-- TODO: handle out of bounds with proofs
135-- TODO: handle out of bounds with proofs
120-- Also choose a better name.
136-- Also choose a better name.
121−select : CType -> Nat -> CType
137+select : Composite -> Nat -> Composite
122select (STRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
138select (STRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
123select (PACKEDSTRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
139select (PACKEDSTRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
124select (UNION xs@(y::_)) i = fromMaybe y (index' i xs)
140select (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)
18print_mystruct : IO ()
18print_mystruct : IO ()
19print_mystruct = foreign FFI_C "print_mystruct" (IO ())
19print_mystruct = foreign FFI_C "print_mystruct" (IO ())
20
20
21−test1 : CType
21+test1 : Composite
22test1 = STRUCT [I8, I64]
22test1 = STRUCT [I8, I64]
23
23
24−test2 : CType
24+test2 : Composite
25test2 = STRUCT [I32, I16]
25test2 = STRUCT [I32, I16]
26
26
27−test3 : CType
27+test3 : Composite
28test3 = STRUCT [DOUBLE, DOUBLE, I8, I64]
28test3 = STRUCT [DOUBLE, DOUBLE, I8, I64]
29
29
30−test4 : CType
30+test4 : Composite
31test4 = PACKEDSTRUCT [I8, I8, I8, I64]
31test4 = PACKEDSTRUCT [I8, I8, I8, I64]
32
32
33printMore : IO ()
33printMore : IO ()
34printMore = do
34printMore = do
35 p <- alloc test3
35 p <- alloc test3
36 f3 <- return $ p # 1
36 f3 <- return $ p # 1
37− a <- peek f3
37+ a <- peek f3 DOUBLE
38+ printLn a
38 printLn p
39 printLn p
39 printLn f3
40 printLn f3
40 free p
41 free p
@@ -42,19 +43,19 @@ printMore = do
42 cms <- return $ CPt ms 0 (STRUCT [I32, I16])
43 cms <- return $ CPt ms 0 (STRUCT [I32, I16])
43 f1 <- return $ cms # 0
44 f1 <- return $ cms # 0
44 printLn f1
45 printLn f1
45− prim_poke32 f1 0 122
46+ poke f1 I32 122
46−
47+
47 print_mystruct
48 print_mystruct
48 printLn test4
49 printLn test4
49 printLn !size1
50 printLn !size1
50 printLn !size2
51 printLn !size2
51 printLn $ fields test3
52 printLn $ fields test3
52 printLn $ offsets (STRUCT [I8, I8, I8, I64, test3])
53 printLn $ offsets (STRUCT [I8, I8, I8, I64, test3])
53− printLn $ sizeOf (ARRAY 67 I32)
54+ printLn $ sizeOfComp (ARRAY 67 I32)
54− printLn $ sizeOf test3
55+ printLn $ sizeOfComp test3
55
56
56main : IO ()
57main : IO ()
57main = do
58main = do
58− printLn $ sizeOf test1 == !size1
59+ printLn $ sizeOfComp test1 == !size1
59− printLn $ sizeOf test2 == !size2
60+ printLn $ sizeOfComp test2 == !size2
60 printMore
61 printMore