git.iko.soy/Idris-dev
on master help sign in
Add put cases
98b1298Niklas Larsson
libs/contrib/CFFI/Memory.idr+23−1
compare with master
unifiedsplit
@@ -25,6 +25,7 @@ free (CPt p _ _) = mfree p
25ctype : CPtr -> CType
25ctype : CPtr -> CType
26ctype (CPt _ _ t) = t
26ctype (CPt _ _ t) = t
27
27
28+
28get : (p : CPtr) -> IO (translate (ctype p))
29get : (p : CPtr) -> IO (translate (ctype p))
29get (CPt p o I8) = prim_peek8 p o
30get (CPt p o I8) = prim_peek8 p o
30get (CPt p o I16) = prim_peek16 p o
31get (CPt p o I16) = prim_peek16 p o
@@ -33,10 +34,31 @@ get (CPt p o I64) = prim_peek64 p o
33get (CPt p o FLOAT) = prim_peekSingle p o
34get (CPt p o FLOAT) = prim_peekSingle p o
34get (CPt p o DOUBLE) = prim_peekDouble p o
35get (CPt p o DOUBLE) = prim_peekDouble p o
35get (CPt p o PTR) = prim_peekPtr p o
36get (CPt p o PTR) = prim_peekPtr p o
37+get (CPt p o (ARRAY n t)) = ?getArray
38+get (CPt p o (UNION xs)) = ?getUnion
39+get (CPt p o (STRUCT xs)) = ?getStruct
40+get (CPt p o (PACKEDSTRUCT xs)) = ?getPacked
36
41
37
42
38put : (p : CPtr) -> (translate (ctype p)) -> IO ()
43put : (p : CPtr) -> (translate (ctype p)) -> IO ()
39−put _ _ = putStrLn "putting"
44+put (CPt p o I8) x = do _ <- prim_poke8 p o x
45+ return ()
46+put (CPt p o I16) x = do _ <- prim_poke16 p o x
47+ return ()
48+put (CPt p o I32) x = do _ <- prim_poke32 p o x
49+ return ()
50+put (CPt p o I64) x = do _ <- prim_poke64 p o x
51+ return ()
52+put (CPt p o PTR) x = do _ <- prim_pokePtr p o x
53+ return ()
54+put (CPt p o FLOAT) x = do _ <- prim_pokeSingle p o x
55+ return ()
56+put (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
57+ return ()
58+put (CPt p o (ARRAY n t)) x = ?putArray
59+put (CPt p o (UNION xs)) x = ?putUnion
60+put (CPt p o (STRUCT xs)) x = ?putStruct
61+put (CPt p o (PACKEDSTRUCT xs)) x = ?putPacked
40
62
41-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
63-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
42-- TODO : Fix bounds checking
64-- TODO : Fix bounds checking
libs/contrib/CFFI/Types.idr+2
@@ -1,4 +1,5 @@
1||| Types for interfacing with C.
1||| Types for interfacing with C.
2+||| This file should be kept free from IO.
2module CFFI.Types
3module CFFI.Types
3
4
4import Data.Vect
5import Data.Vect
@@ -103,6 +104,7 @@ offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n]]
103offsets _ = [0]
104offsets _ = [0]
104
105
105-- TODO: handle out of bounds with proofs
106-- TODO: handle out of bounds with proofs
107+-- Also choose a better name.
106select : CType -> Nat -> CType
108select : CType -> Nat -> CType
107select (STRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
109select (STRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
108select (PACKEDSTRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
110select (PACKEDSTRUCT xs@(y::_)) i = fromMaybe y (index' i xs)