git.iko.soy/Idris-dev
on master help sign in
Simplify
d06ca16Niklas Larsson
libs/contrib/CFFI/Memory.idr+42−67
compare with master
unifiedsplit
@@ -3,20 +3,16 @@ module CFFI.Memory
3
3
4import CFFI.Types
4import CFFI.Types
5import Data.Vect
5import Data.Vect
6−import Data.HVect
7
6
8%include C "memory.h"
7%include C "memory.h"
9
8
10%access public export
9%access public export
11%default partial
10%default partial
12
11
13−data CPtr = CPt Ptr Int Composite
12+data CPtr = CPt Ptr Int
14
13
15−implicit decayCPtr : CPtr -> Ptr
14+implicit toCPtr : Ptr -> CPtr
16−decayCPtr (CPt p _ _) = p
15+toCPtr p = CPt p 0
17−
18−Show CPtr where
19− show (CPt _ os t) = "CPtr ptr " ++ show os ++ " " ++ show t
20
16
21malloc : Int -> IO Ptr
17malloc : Int -> IO Ptr
22malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
18malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
@@ -25,10 +21,10 @@ mfree : Ptr -> IO ()
25mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
21mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
26
22
27alloc : Composite -> IO CPtr
23alloc : Composite -> IO CPtr
28−alloc t = return $ CPt !(malloc (sizeOfComp t)) 0 t
24+alloc t = return $ CPt !(malloc (sizeOf t)) 0
29
25
30free : CPtr -> IO ()
26free : CPtr -> IO ()
31−free (CPt p _ _) = mfree p
27+free (CPt p _ ) = mfree p
32
28
33withAlloc : Composite -> (CPtr -> IO ()) -> IO ()
29withAlloc : Composite -> (CPtr -> IO ()) -> IO ()
34withAlloc t f = do m <- alloc t
30withAlloc t f = do m <- alloc t
@@ -40,66 +36,45 @@ infixl 1 ~~>
40(~~>) : Composite-> (CPtr -> IO ()) -> IO ()
36(~~>) : Composite-> (CPtr -> IO ()) -> IO ()
41(~~>) = withAlloc
37(~~>) = withAlloc
42
38
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)
39+peek : (t: CType) -> CPtr -> IO (translate t)
60− peek (CPt p o (T I8)) I8 = prim_peek8 p o
40+peek I8 (CPt p o) = prim_peek8 p o
61− peek (CPt p o (T I16)) I16= prim_peek16 p o
41+peek I16 (CPt p o) = prim_peek16 p o
62− peek (CPt p o (T I32)) I32 = prim_peek32 p o
42+peek I32 (CPt p o) = prim_peek32 p o
63− peek (CPt p o (T I64)) I64 = prim_peek64 p o
43+peek I64 (CPt p o) = prim_peek64 p o
64− peek (CPt p o (T FLOAT)) FLOAT = prim_peekSingle p o
44+peek FLOAT (CPt p o) = prim_peekSingle p o
65− peek (CPt p o (T DOUBLE)) DOUBLE = prim_peekDouble p o
45+peek DOUBLE (CPt p o) = prim_peekDouble p o
66− peek (CPt p o (T PTR)) PTR = prim_peekPtr p o
46+peek PTR (CPt p o) = prim_peekPtr p o
67− -- peek cp@(CPt p o (ARRAY n t)) = peekArray cp
47+
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 ()
48+poke : (t : CType) -> CPtr -> translate t -> IO ()
74− poke (CPt p o (T I8)) I8 x = do _ <- prim_poke8 p o x
49+poke I8 (CPt p o) x = do _ <- prim_poke8 p o x
75− return ()
50+ return ()
76− poke (CPt p o (T I16)) I16 x = do _ <- prim_poke16 p o x
51+poke I16 (CPt p o) x = do _ <- prim_poke16 p o x
77− return ()
52+ return ()
78− poke (CPt p o (T I32)) I32 x = do _ <- prim_poke32 p o x
53+poke I32 (CPt p o) x = do _ <- prim_poke32 p o x
79− return ()
54+ return ()
80− poke (CPt p o (T I64)) I64 x = do _ <- prim_poke64 p o x
55+poke I64 (CPt p o) x = do _ <- prim_poke64 p o x
81− return ()
56+ return ()
82− poke (CPt p o (T PTR)) PTR x = do _ <- prim_pokePtr p o x
57+poke PTR (CPt p o) x = do _ <- prim_pokePtr p o x
83− return ()
58+ return ()
84− poke (CPt p o (T FLOAT)) FLOAT x = do _ <- prim_pokeSingle p o x
59+poke FLOAT (CPt p o) x = do _ <- prim_pokeSingle p o x
85− return ()
60+ return ()
86− poke (CPt p o (T DOUBLE)) DOUBLE x = do _ <- prim_pokeDouble p o x
61+poke DOUBLE (CPt p o) x = do _ <- prim_pokeDouble p o x
87− return ()
62+ return ()
88− -- poke cp@(CPt p o (ARRAY n t)) x = pokeArray cp x
63+
89− -- poke (CPt p o (UNION xs)) x = ?pokeUnion
64+update : (t: CType) -> CPtr -> (translate t -> translate t) -> IO ()
90− -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct
65+update ty cp f = do val <- peek ty cp
91− -- poke (CPt p o (PACKEDSTRUCT xs)) x = ?pokePacked
66+ out <- return $ f val
92−
67+ poke ty cp out
93−-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
68+
94-- TODO : Fix bounds checking
69-- TODO : Fix bounds checking
95−field : CPtr -> Nat -> CPtr
70+field : Composite -> Nat -> CPtr -> CPtr
96−field (CPt p o arr@(ARRAY n t)) i = CPt p (o + offset arr i) t
71+field arr@(ARRAY n t) i (CPt p o ) = CPt p (o + offset arr i)
97−field (CPt p o un@(UNION xs)) i = CPt p o (select un i)
72+field un@(UNION xs) i (CPt p o ) = CPt p o
98−field (CPt p o st@(STRUCT xs)) i = CPt p (o + offset st i) (select st i)
73+field st@(STRUCT xs) i (CPt p o ) = CPt p (o + offset st i)
99−field (CPt p o ps@(PACKEDSTRUCT xs)) i = CPt p (o + offset ps i) (select ps i)
74+field ps@(PACKEDSTRUCT xs) i (CPt p o ) = CPt p (o + offset ps i)
100−field p Z = p
75+field (T t) Z p = p
101
76
102infixl 10 #
77infixl 10 #
103
78
104−(#) : CPtr -> Nat -> CPtr
79+(#) : Composite -> Nat -> CPtr -> CPtr
105(#) = field
80(#) = field
libs/contrib/CFFI/Types.idr+53−61
@@ -3,7 +3,6 @@
3module CFFI.Types
3module CFFI.Types
4
4
5import Data.Vect
5import Data.Vect
6−import Data.HVect
7
6
8%access public export
7%access public export
9%default partial
8%default partial
@@ -11,6 +10,7 @@ import Data.HVect
11||| An universe of C types.
10||| An universe of C types.
12data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
11data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
13
12
13+||| Composites of C types
14data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
14data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
15 | PACKEDSTRUCT (List Composite)
15 | PACKEDSTRUCT (List Composite)
16
16
@@ -42,95 +42,87 @@ translate FLOAT = Double
42translate DOUBLE = Double
42translate DOUBLE = Double
43translate PTR = Ptr
43translate PTR = Ptr
44
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)
51−
52mutual
45mutual
53− sizeOf : CType -> Int
46+ sizeOfCT : CType -> Int
54− sizeOf I8 = 1
47+ sizeOfCT I8 = 1
55− sizeOf I16 = 2
48+ sizeOfCT I16 = 2
56− sizeOf I32 = 4
49+ sizeOfCT I32 = 4
57− sizeOf I64 = 8
50+ sizeOfCT I64 = 8
58− sizeOf FLOAT = 4
51+ sizeOfCT FLOAT = 4
59− sizeOf DOUBLE = 8
52+ sizeOfCT DOUBLE = 8
60− sizeOf PTR = prim__sizeofPtr
53+ sizeOfCT PTR = prim__sizeofPtr
61−
54+
62− sizeOfComp : Composite -> Int
55+ sizeOf : Composite -> Int
63− sizeOfComp (T ct) = sizeOf ct
56+ sizeOf (T ct) = sizeOfCT ct
64− sizeOfComp (ARRAY n t) = n * sizeOfComp t
57+ sizeOf (ARRAY n t) = n * sizeOf t
65− sizeOfComp (STRUCT xs) = sizeOfStruct xs
58+ sizeOf (STRUCT xs) = sizeOfStruct xs
66− sizeOfComp (UNION xs) = foldl (\acc, x =>max acc $ sizeOfComp x) 0 xs
59+ sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
67− sizeOfComp (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOfComp x) 0 xs
60+ sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
68−
61+
69− alignOf : CType -> Int
62+ alignOfCT : CType -> Int
70− alignOf I8 = 1
63+ alignOfCT I8 = 1
71− alignOf I16 = 2
64+ alignOfCT I16 = 2
72− alignOf I32 = 4
65+ alignOfCT I32 = 4
73− alignOf I64 = prim__sizeofPtr
66+ alignOfCT I64 = prim__sizeofPtr
74− alignOf FLOAT = 4
67+ alignOfCT FLOAT = 4
75− alignOf DOUBLE = prim__sizeofPtr
68+ alignOfCT DOUBLE = prim__sizeofPtr
76− alignOf PTR = prim__sizeofPtr
69+ alignOfCT PTR = prim__sizeofPtr
77−
70+
78− alignOfComp : Composite -> Int
71+ alignOf : Composite -> Int
79− alignOfComp (T t) = alignOf t
72+ alignOf (T t) = alignOfCT t
80− alignOfComp (ARRAY n t) = alignOfComp t
73+ alignOf (ARRAY n t) = alignOf t
81− alignOfComp (STRUCT xs) = foldl (\acc, x => max acc $ alignOfComp x) 0 xs
74+ alignOf (STRUCT xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
82− alignOfComp (UNION xs) = foldl (\acc, x => max acc $ alignOfComp x) 0 xs
75+ alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
83− alignOfComp (PACKEDSTRUCT xs) = 1
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)
84
83
85 offsetsStruct : List Composite -> List Int
84 offsetsStruct : List Composite -> List Int
86− offsetsStruct xs = offsets' xs [] 0
85+ offsetsStruct xs = offsets' xs 0
87 where
86 where
88− offsets' : List Composite -> List Int -> Int -> List Int
87+ offsets' : List Composite -> Int -> List Int
89− offsets' [] acc _ = reverse acc
88+ offsets' [] _ = []
90− offsets' (x::xs) ys curr = let a = alignOfComp x
89+ offsets' (x::xs) pos = (nextOffset x pos)::(offsets' xs (nextOffset x pos + sizeOf 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)
95
90
96 sizeOfStruct : List Composite -> Int
91 sizeOfStruct : List Composite -> Int
97− sizeOfStruct xs = case (reverse xs, reverse (offsetsStruct xs)) of
92+ sizeOfStruct xs = sizeStruct' xs 0 1
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
103 where
93 where
104− align : Int
94+ sizeStruct' : List Composite -> Int -> Int -> Int
105− align = foldl (\acc, x => max acc $ alignOfComp x) 1 xs
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))
106
98
107fields : Composite -> Nat
99fields : Composite -> Nat
108fields (STRUCT xs) = length xs
100fields (STRUCT xs) = length xs
109fields (PACKEDSTRUCT xs) = length xs
101fields (PACKEDSTRUCT xs) = length xs
110fields (UNION xs) = length xs
102fields (UNION xs) = length xs
111fields (ARRAY n _) = toNat n
103fields (ARRAY n _) = toNat n
112−fields _ = 1
104+fields (T _) = 1
113
105
114offsetsPacked : List Composite -> List Int
106offsetsPacked : List Composite -> List Int
115offsetsPacked xs = offsets' xs [] 0
107offsetsPacked xs = offsets' xs [] 0
116 where
108 where
117 offsets' : List Composite -> List Int -> Int -> List Int
109 offsets' : List Composite -> List Int -> Int -> List Int
118 offsets' [] acc _ = reverse acc
110 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)
120
112
121-- TODO: Use index and fix upp proofs.
113-- TODO: Use index and fix upp proofs.
122offset : Composite -> Nat -> Int
114offset : Composite -> Nat -> Int
123offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
115offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
124offset (PACKEDSTRUCT xs) i = fromMaybe 0 $ index' i (offsetsPacked xs)
116offset (PACKEDSTRUCT xs) i = fromMaybe 0 $ index' i (offsetsPacked xs)
125−offset (ARRAY _ t) i = sizeOfComp t * toIntNat i
117+offset (ARRAY _ t) i = sizeOf t * toIntNat i
126−offset _ _ = 0
118+offset (T _) _ = 0
127
119
128offsets : Composite -> List Int
120offsets : Composite -> List Int
129offsets (STRUCT xs) = offsetsStruct xs
121offsets (STRUCT xs) = offsetsStruct xs
130offsets (PACKEDSTRUCT xs) = offsetsPacked xs
122offsets (PACKEDSTRUCT xs) = offsetsPacked xs
131offsets (UNION xs) = replicate (length xs) 0
123offsets (UNION xs) = replicate (length xs) 0
132−offsets (ARRAY n t) = [ x*sizeOfComp t | x <- [0..n-1]]
124+offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
133−offsets _ = [0]
125+offsets (T _) = [0]
134
126
135-- TODO: handle out of bounds with proofs
127-- TODO: handle out of bounds with proofs
136-- Also choose a better name.
128-- Also choose a better name.
libs/contrib/contrib.ipkg+1−1
@@ -13,7 +13,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
13 Classes.Verified,
13 Classes.Verified,
14
14
15 Data.Fun, Data.Rel,
15 Data.Fun, Data.Rel,
16− Data.Hash, Data.HList,
16+ Data.Hash,
17 Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,
17 Data.Matrix, Data.Matrix.Algebraic, Data.Matrix.Numeric,
18 Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,
18 Data.Nat.DivMod, Data.Nat.DivMod.IteratedSubtraction,
19 Data.ZZ, Data.Sign,
19 Data.ZZ, Data.Sign,
test/ffi008/ffi008.idr+9−14
@@ -33,29 +33,24 @@ test4 = PACKEDSTRUCT [I8, I8, I8, I64]
33printMore : IO ()
33printMore : IO ()
34printMore = do
34printMore = do
35 p <- alloc test3
35 p <- alloc test3
36− f3 <- return $ p # 1
36+ f3 <- return $ (test3 # 1) p
37− a <- peek f3 DOUBLE
37+ a <- peek DOUBLE f3
38 printLn a
38 printLn a
39− printLn p
40− printLn f3
41 free p
39 free p
42− ms <- mystruct
40+ fms <- return $ (test2#0) !mystruct
43− cms <- return $ CPt ms 0 (STRUCT [I32, I16])
44− f1 <- return $ cms # 0
45− printLn f1
46− poke f1 I32 122
41+ poke I32 fms 122
47−
48 print_mystruct
42 print_mystruct
49 printLn test4
43 printLn test4
50 printLn !size1
44 printLn !size1
51 printLn !size2
45 printLn !size2
52 printLn $ fields test3
46 printLn $ fields test3
53 printLn $ offsets (STRUCT [I8, I8, I8, I64, test3])
47 printLn $ offsets (STRUCT [I8, I8, I8, I64, test3])
54− printLn $ sizeOfComp (ARRAY 67 I32)
48+ printLn $ sizeOf (ARRAY 67 I32)
55− printLn $ sizeOfComp test3
49+ printLn $ sizeOf test1
50+ printLn $ sizeOf test2
56
51
57main : IO ()
52main : IO ()
58main = do
53main = do
59− printLn $ sizeOfComp test1 == !size1
54+ printLn $ sizeOf test1 == !size1
60− printLn $ sizeOfComp test2 == !size2
55+ printLn $ sizeOf test2 == !size2
61 printMore
56 printMore