git.iko.soy/Idris-dev
on master help sign in
Add show instance for CType and CPtr
87785d8Niklas Larsson
libs/contrib/CFFI/Memory.idr+14−8
compare with master
unifiedsplit
@@ -10,6 +10,12 @@ import CFFI.Types
10
10
11data CPtr = CPt Ptr Int CType
11data CPtr = CPt Ptr Int CType
12
12
13+implicit decayCPtr : CPtr -> Ptr
14+decayCPtr (CPt p _ _) = p
15+
16+Show CPtr where
17+ show (CPt _ os t) = "CPtr ptr " ++ show os ++ " " ++ show t
18+
13malloc : Int -> IO Ptr
19malloc : Int -> IO Ptr
14malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
20malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
15
21
@@ -34,10 +40,10 @@ get (CPt p o I64) = prim_peek64 p o
34get (CPt p o FLOAT) = prim_peekSingle p o
40get (CPt p o FLOAT) = prim_peekSingle p o
35get (CPt p o DOUBLE) = prim_peekDouble p o
41get (CPt p o DOUBLE) = prim_peekDouble p o
36get (CPt p o PTR) = prim_peekPtr p o
42get (CPt p o PTR) = prim_peekPtr p o
37−get (CPt p o (ARRAY n t)) = ?getArray
43+-- get (CPt p o (ARRAY n t)) = ?getArray
38−get (CPt p o (UNION xs)) = ?getUnion
44+-- get (CPt p o (UNION xs)) = ?getUnion
39−get (CPt p o (STRUCT xs)) = ?getStruct
45+-- get (CPt p o (STRUCT xs)) = ?getStruct
40−get (CPt p o (PACKEDSTRUCT xs)) = ?getPacked
46+-- get (CPt p o (PACKEDSTRUCT xs)) = ?getPacked
41
47
42
48
43put : (p : CPtr) -> (translate (ctype p)) -> IO ()
49put : (p : CPtr) -> (translate (ctype p)) -> IO ()
@@ -55,10 +61,10 @@ put (CPt p o FLOAT) x = do _ <- prim_pokeSingle p o x
55 return ()
61 return ()
56put (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
62put (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
57 return ()
63 return ()
58−put (CPt p o (ARRAY n t)) x = ?putArray
64+-- put (CPt p o (ARRAY n t)) x = ?putArray
59−put (CPt p o (UNION xs)) x = ?putUnion
65+-- put (CPt p o (UNION xs)) x = ?putUnion
60−put (CPt p o (STRUCT xs)) x = ?putStruct
66+-- put (CPt p o (STRUCT xs)) x = ?putStruct
61−put (CPt p o (PACKEDSTRUCT xs)) x = ?putPacked
67+-- put (CPt p o (PACKEDSTRUCT xs)) x = ?putPacked
62
68
63-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
69-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
64-- TODO : Fix bounds checking
70-- TODO : Fix bounds checking
libs/contrib/CFFI/Types.idr+17−4
@@ -3,7 +3,7 @@
3module CFFI.Types
3module CFFI.Types
4
4
5import Data.Vect
5import Data.Vect
6−import Data.HList
6+import Data.HVect
7
7
8%access public export
8%access public export
9%default partial
9%default partial
@@ -13,6 +13,19 @@ data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
13 | ARRAY Int CType | STRUCT (List CType) | UNION (List CType)
13 | ARRAY Int CType | STRUCT (List CType) | UNION (List CType)
14 | PACKEDSTRUCT (List CType)
14 | PACKEDSTRUCT (List CType)
15
15
16+Show CType where
17+ show I8 = "I8"
18+ show I16 = "I16"
19+ show I32 = "I32"
20+ show I64 = "I64"
21+ show FLOAT = "FLOAT"
22+ show DOUBLE = "DOUBLE"
23+ show PTR = "PTR"
24+ show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t
25+ show (STRUCT xs) = "STRUCT " ++ show xs
26+ show (UNION xs) = "UNION " ++ show xs
27+ show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs
28+
16translate : CType -> Type
29translate : CType -> Type
17translate I8 = Bits8
30translate I8 = Bits8
18translate I16 = Bits16
31translate I16 = Bits16
@@ -22,9 +35,9 @@ translate FLOAT = Double
22translate DOUBLE = Double
35translate DOUBLE = Double
23translate PTR = Ptr
36translate PTR = Ptr
24translate (ARRAY n t) = Vect (toNat n) (translate t)
37translate (ARRAY n t) = Vect (toNat n) (translate t)
25−translate (STRUCT xs) = HList (map translate xs)
38+translate (STRUCT xs) = HVect $ fromList (map translate xs)
26−translate (UNION xs) = HList (map translate xs)
39+translate (UNION xs) = HVect $ fromList (map translate xs)
27−translate (PACKEDSTRUCT xs) = HList (map translate xs)
40+translate (PACKEDSTRUCT xs) = HVect $ fromList (map translate xs)
28
41
29mutual
42mutual
30 sizeOf : CType -> Int
43 sizeOf : CType -> Int