git.iko.soy/Idris-dev
on master help sign in
Simplify
commitd06ca16222a8e805504c1cb72281c7abdd286caf authorNiklas Larsson <niklas@mm.st> dateTue 16 Feb 2016, 00:34 (11 years ago) parent33166ee
4 files changed+105−143
compare with master
unifiedsplit
libs/contrib/CFFI/Memory.idr+42−67 libs/contrib/CFFI/Types.idr+53−61 libs/contrib/contrib.ipkg+1−1 test/ffi008/ffi008.idr+9−14
libs/contrib/CFFI/Memory.idr+42−67
@@ -3,20 +3,16 @@ module CFFI.Memory
33
44import CFFI.Types
55import Data.Vect
6−import Data.HVect
76
87%include C "memory.h"
98
109%access public export
1110%default partial
1211
13−data CPtr = CPt Ptr Int Composite
12+data CPtr = CPt Ptr Int
1413
15−implicit decayCPtr : CPtr -> Ptr
16−decayCPtr (CPt p _ _) = p
17−
18−Show CPtr where
19− show (CPt _ os t) = "CPtr ptr " ++ show os ++ " " ++ show t
14+implicit toCPtr : Ptr -> CPtr
15+toCPtr p = CPt p 0
2016
2117malloc : Int -> IO Ptr
2218malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
@@ -25,10 +21,10 @@ mfree : Ptr -> IO ()
2521mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
2622
2723alloc : Composite -> IO CPtr
28−alloc t = return $ CPt !(malloc (sizeOfComp t)) 0 t
24+alloc t = return $ CPt !(malloc (sizeOf t)) 0
2925
3026free : CPtr -> IO ()
31−free (CPt p _ _) = mfree p
27+free (CPt p _ ) = mfree p
3228
3329withAlloc : Composite -> (CPtr -> IO ()) -> IO ()
3430withAlloc t f = do m <- alloc t
@@ -40,66 +36,45 @@ infixl 1 ~~>
4036(~~>) : Composite-> (CPtr -> IO ()) -> IO ()
4137(~~>) = withAlloc
4238
43−ctype : CPtr -> CType
44−ctype (CPt _ _ (T t)) = t
45−
46−mutual
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
67− -- peek cp@(CPt p o (ARRAY n t)) = peekArray cp
68− -- peek (CPt p o (UNION xs)) = ?peekUnion
69− -- peek (CPt p o (STRUCT xs)) = ?peekStruct
70− -- peek (CPt p o (PACKEDSTRUCT xs)) = ?peekPacked
71−
72−
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 ()
88− -- poke cp@(CPt p o (ARRAY n t)) x = pokeArray cp x
89− -- poke (CPt p o (UNION xs)) x = ?pokeUnion
90− -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct
91− -- poke (CPt p o (PACKEDSTRUCT xs)) x = ?pokePacked
92−
93−-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
39+peek : (t: CType) -> CPtr -> IO (translate t)
40+peek I8 (CPt p o) = prim_peek8 p o
41+peek I16 (CPt p o) = prim_peek16 p o
42+peek I32 (CPt p o) = prim_peek32 p o
43+peek I64 (CPt p o) = prim_peek64 p o
44+peek FLOAT (CPt p o) = prim_peekSingle p o
45+peek DOUBLE (CPt p o) = prim_peekDouble p o
46+peek PTR (CPt p o) = prim_peekPtr p o
47+
48+poke : (t : CType) -> CPtr -> translate t -> IO ()
49+poke I8 (CPt p o) x = do _ <- prim_poke8 p o x
50+ return ()
51+poke I16 (CPt p o) x = do _ <- prim_poke16 p o x
52+ return ()
53+poke I32 (CPt p o) x = do _ <- prim_poke32 p o x
54+ return ()
55+poke I64 (CPt p o) x = do _ <- prim_poke64 p o x
56+ return ()
57+poke PTR (CPt p o) x = do _ <- prim_pokePtr p o x
58+ return ()
59+poke FLOAT (CPt p o) x = do _ <- prim_pokeSingle p o x
60+ return ()
61+poke DOUBLE (CPt p o) x = do _ <- prim_pokeDouble p o x
62+ return ()
63+
64+update : (t: CType) -> CPtr -> (translate t -> translate t) -> IO ()
65+update ty cp f = do val <- peek ty cp
66+ out <- return $ f val
67+ poke ty cp out
68+
9469-- TODO : Fix bounds checking
95−field : CPtr -> Nat -> CPtr
96−field (CPt p o arr@(ARRAY n t)) i = CPt p (o + offset arr i) t
97−field (CPt p o un@(UNION xs)) i = CPt p o (select un i)
98−field (CPt p o st@(STRUCT xs)) i = CPt p (o + offset st i) (select st i)
99−field (CPt p o ps@(PACKEDSTRUCT xs)) i = CPt p (o + offset ps i) (select ps i)
100−field p Z = p
70+field : Composite -> Nat -> CPtr -> CPtr
71+field arr@(ARRAY n t) i (CPt p o ) = CPt p (o + offset arr i)
72+field un@(UNION xs) i (CPt p o ) = CPt p o
73+field st@(STRUCT xs) i (CPt p o ) = CPt p (o + offset st i)
74+field ps@(PACKEDSTRUCT xs) i (CPt p o ) = CPt p (o + offset ps i)
75+field (T t) Z p = p
10176
10277infixl 10 #
10378
104−(#) : CPtr -> Nat -> CPtr
79+(#) : Composite -> Nat -> CPtr -> CPtr
10580(#) = field
libs/contrib/CFFI/Types.idr+53−61
@@ -3,7 +3,6 @@
33module CFFI.Types
44
55import Data.Vect
6−import Data.HVect
76
87%access public export
98%default partial
@@ -11,6 +10,7 @@ import Data.HVect
1110||| An universe of C types.
1211data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
1312
13+||| Composites of C types
1414data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
1515 | PACKEDSTRUCT (List Composite)
1616
@@ -42,95 +42,87 @@ translate FLOAT = Double
4242translate DOUBLE = Double
4343translate PTR = Ptr
4444
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)
51−
5245mutual
53− sizeOf : CType -> Int
54− sizeOf I8 = 1
55− sizeOf I16 = 2
56− sizeOf I32 = 4
57− sizeOf I64 = 8
58− sizeOf FLOAT = 4
59− sizeOf DOUBLE = 8
60− sizeOf PTR = prim__sizeofPtr
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
68−
69− alignOf : CType -> Int
70− alignOf I8 = 1
71− alignOf I16 = 2
72− alignOf I32 = 4
73− alignOf I64 = prim__sizeofPtr
74− alignOf FLOAT = 4
75− alignOf DOUBLE = prim__sizeofPtr
76− alignOf PTR = prim__sizeofPtr
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
46+ sizeOfCT : CType -> Int
47+ sizeOfCT I8 = 1
48+ sizeOfCT I16 = 2
49+ sizeOfCT I32 = 4
50+ sizeOfCT I64 = 8
51+ sizeOfCT FLOAT = 4
52+ sizeOfCT DOUBLE = 8
53+ sizeOfCT PTR = prim__sizeofPtr
54+
55+ sizeOf : Composite -> Int
56+ sizeOf (T ct) = sizeOfCT ct
57+ sizeOf (ARRAY n t) = n * sizeOf t
58+ sizeOf (STRUCT xs) = sizeOfStruct xs
59+ sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
60+ sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
61+
62+ alignOfCT : CType -> Int
63+ alignOfCT I8 = 1
64+ alignOfCT I16 = 2
65+ alignOfCT I32 = 4
66+ alignOfCT I64 = prim__sizeofPtr
67+ alignOfCT FLOAT = 4
68+ alignOfCT DOUBLE = prim__sizeofPtr
69+ alignOfCT PTR = prim__sizeofPtr
70+
71+ alignOf : Composite -> Int
72+ alignOf (T t) = alignOfCT t
73+ alignOf (ARRAY n t) = alignOf t
74+ alignOf (STRUCT xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
75+ alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
76+ alignOf (PACKEDSTRUCT xs) = 1
77+
78+ pad : Int -> Int -> Int
79+ pad pos align = let c = pos `mod` align in if c == 0 then 0 else align - c
80+
81+ nextOffset : Composite -> Int -> Int
82+ nextOffset ty pos = pos + pad pos (alignOf ty)
8483
8584 offsetsStruct : List Composite -> List Int
86− offsetsStruct xs = offsets' xs [] 0
85+ offsetsStruct xs = offsets' xs 0
8786 where
88− offsets' : List Composite -> List Int -> Int -> List Int
89− offsets' [] acc _ = reverse acc
90− offsets' (x::xs) ys curr = let a = alignOfComp x
91− padding = let c = curr `mod` a
92− in if c == 0 then 0 else a - c
93− off = curr + padding
94− in offsets' xs (off::ys) (off + sizeOfComp x)
87+ offsets' : List Composite -> Int -> List Int
88+ offsets' [] _ = []
89+ offsets' (x::xs) pos = (nextOffset x pos)::(offsets' xs (nextOffset x pos + sizeOf x))
9590
9691 sizeOfStruct : List Composite -> Int
97− sizeOfStruct xs = case (reverse xs, reverse (offsetsStruct xs)) of
98− ([], _) => 0
99− (x::_, y::_) => let end = y + sizeOfComp x
100− endPadding = let c = end `mod` align in
101− if c == 0 then 0 else align - c
102− in end + endPadding
92+ sizeOfStruct xs = sizeStruct' xs 0 1
10393 where
104− align : Int
105− align = foldl (\acc, x => max acc $ alignOfComp x) 1 xs
94+ sizeStruct' : List Composite -> Int -> Int -> Int
95+ sizeStruct' [] pos maxAlign = pos + (pad pos maxAlign)
96+ sizeStruct' (x::xs) pos maxAlign = sizeStruct' xs (nextOffset x pos + sizeOf x)
97+ (max maxAlign (alignOf x))
10698
10799fields : Composite -> Nat
108100fields (STRUCT xs) = length xs
109101fields (PACKEDSTRUCT xs) = length xs
110102fields (UNION xs) = length xs
111103fields (ARRAY n _) = toNat n
112−fields _ = 1
104+fields (T _) = 1
113105
114106offsetsPacked : List Composite -> List Int
115107offsetsPacked xs = offsets' xs [] 0
116108 where
117109 offsets' : List Composite -> List Int -> Int -> List Int
118110 offsets' [] acc _ = reverse acc
119− offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOfComp x)
111+ offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
120112
121113-- TODO: Use index and fix upp proofs.
122114offset : Composite -> Nat -> Int
123115offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
124116offset (PACKEDSTRUCT xs) i = fromMaybe 0 $ index' i (offsetsPacked xs)
125−offset (ARRAY _ t) i = sizeOfComp t * toIntNat i
126−offset _ _ = 0
117+offset (ARRAY _ t) i = sizeOf t * toIntNat i
118+offset (T _) _ = 0
127119
128120offsets : Composite -> List Int
129121offsets (STRUCT xs) = offsetsStruct xs
130122offsets (PACKEDSTRUCT xs) = offsetsPacked xs
131123offsets (UNION xs) = replicate (length xs) 0
132−offsets (ARRAY n t) = [ x*sizeOfComp t | x <- [0..n-1]]
133−offsets _ = [0]
124+offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
125+offsets (T _) = [0]
134126
135127-- TODO: handle out of bounds with proofs
136128-- Also choose a better name.
libs/contrib/contrib.ipkg+1−1
@@ -13,7 +13,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
1313 Classes.Verified,
1414
1515 Data.Fun, Data.Rel,
16− Data.Hash, Data.HList,
16+ Data.Hash,
1717 Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,
1818 Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,
1919 Data.ZZ, Data.Sign,
test/ffi008/ffi008.idr+9−14
@@ -33,29 +33,24 @@ test4 = PACKEDSTRUCT [I8, I8, I8, I64]
3333printMore : IO ()
3434printMore = do
3535 p <- alloc test3
36− f3 <- return $ p # 1
37− a <- peek f3 DOUBLE
36+ f3 <- return $ (test3 # 1) p
37+ a <- peek DOUBLE f3
3838 printLn a
39− printLn p
40− printLn f3
4139 free p
42− ms <- mystruct
43− cms <- return $ CPt ms 0 (STRUCT [I32, I16])
44− f1 <- return $ cms # 0
45− printLn f1
46− poke f1 I32 122
47−
40+ fms <- return $ (test2#0) !mystruct
41+ poke I32 fms 122
4842 print_mystruct
4943 printLn test4
5044 printLn !size1
5145 printLn !size2
5246 printLn $ fields test3
5347 printLn $ offsets (STRUCT [I8, I8, I8, I64, test3])
54− printLn $ sizeOfComp (ARRAY 67 I32)
55− printLn $ sizeOfComp test3
48+ printLn $ sizeOf (ARRAY 67 I32)
49+ printLn $ sizeOf test1
50+ printLn $ sizeOf test2
5651
5752main : IO ()
5853main = do
59− printLn $ sizeOfComp test1 == !size1
60− printLn $ sizeOfComp test2 == !size2
54+ printLn $ sizeOf test1 == !size1
55+ printLn $ sizeOf test2 == !size2
6156 printMore