git.iko.soy/Idris-dev
on master help sign in
Rename to peek and poke
d82f489Niklas Larsson
libs/contrib/CFFI/Memory.idr+48−35
compare with master
unifiedsplit
@@ -2,6 +2,8 @@
2module CFFI.Memory
2module CFFI.Memory
3
3
4import CFFI.Types
4import CFFI.Types
5+import Data.Vect
6+import Data.HVect
5
7
6%include C "memory.h"
8%include C "memory.h"
7
9
@@ -30,41 +32,52 @@ free (CPt p _ _) = mfree p
30
32
31ctype : CPtr -> CType
33ctype : CPtr -> CType
32ctype (CPt _ _ t) = t
34ctype (CPt _ _ t) = t
33−
35+mutual
34−
36+ peekArray : (c : CPtr) -> IO (translate (ctype c))
37+ peekArray (CPt p o a@(ARRAY n t)) = do
38+ os <- return $ fromList (offsets a)
39+ return $ map (\x => peek (CPt p x t)) os
40+
41+ pokeArray : (c : CPtr) -> translate (ctype c) -> IO ()
42+ pokeArray (CPt p o a@(ARRAY n t)) x = do
43+ os <- fromList $ offsets a
44+ ox <- zip os x
45+ map (\(x, y)=>poke (CPt p x t) y) ox
46+ return ()
47+
35−get : (p : CPtr) -> IO (translate (ctype p))
48+ peek : (p : CPtr) -> IO (translate (ctype p))
36−get (CPt p o I8) = prim_peek8 p o
49+ peek (CPt p o I8) = prim_peek8 p o
37−get (CPt p o I16) = prim_peek16 p o
50+ peek (CPt p o I16) = prim_peek16 p o
38−get (CPt p o I32) = prim_peek32 p o
51+ peek (CPt p o I32) = prim_peek32 p o
39−get (CPt p o I64) = prim_peek64 p o
52+ peek (CPt p o I64) = prim_peek64 p o
40−get (CPt p o FLOAT) = prim_peekSingle p o
53+ peek (CPt p o FLOAT) = prim_peekSingle p o
41−get (CPt p o DOUBLE) = prim_peekDouble p o
54+ peek (CPt p o DOUBLE) = prim_peekDouble p o
42−get (CPt p o PTR) = prim_peekPtr p o
55+ peek (CPt p o PTR) = prim_peekPtr p o
43−-- get (CPt p o (ARRAY n t)) = ?getArray
56+ peek cp@(CPt p o (ARRAY n t)) = peekArray cp
44−-- get (CPt p o (UNION xs)) = ?getUnion
57+ -- peek (CPt p o (UNION xs)) = ?peekUnion
45−-- get (CPt p o (STRUCT xs)) = ?getStruct
58+ -- peek (CPt p o (STRUCT xs)) = ?peekStruct
46−-- get (CPt p o (PACKEDSTRUCT xs)) = ?getPacked
59+ -- peek (CPt p o (PACKEDSTRUCT xs)) = ?peekPacked
47−
60+
48−
61+
49−put : (p : CPtr) -> (translate (ctype p)) -> IO ()
62+ poke : (p : CPtr) -> translate $ ctype p -> IO ()
50−put (CPt p o I8) x = do _ <- prim_poke8 p o x
63+ poke (CPt p o I8) x = do _ <- prim_poke8 p o x
51− return ()
64+ return ()
52−put (CPt p o I16) x = do _ <- prim_poke16 p o x
65+ poke (CPt p o I16) x = do _ <- prim_poke16 p o x
53− return ()
66+ return ()
54−put (CPt p o I32) x = do _ <- prim_poke32 p o x
67+ poke (CPt p o I32) x = do _ <- prim_poke32 p o x
55− return ()
68+ return ()
56−put (CPt p o I64) x = do _ <- prim_poke64 p o x
69+ poke (CPt p o I64) x = do _ <- prim_poke64 p o x
57− return ()
70+ return ()
58−put (CPt p o PTR) x = do _ <- prim_pokePtr p o x
71+ poke (CPt p o PTR) x = do _ <- prim_pokePtr p o x
59− return ()
72+ return ()
60−put (CPt p o FLOAT) x = do _ <- prim_pokeSingle p o x
73+ poke (CPt p o FLOAT) x = do _ <- prim_pokeSingle p o x
61− return ()
74+ return ()
62−put (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
75+ poke (CPt p o DOUBLE) x = do _ <- prim_pokeDouble p o x
63− return ()
76+ return ()
64−-- put (CPt p o (ARRAY n t)) x = ?putArray
77+ poke cp@(CPt p o (ARRAY n t)) x = pokeArray cp x
65−-- put (CPt p o (UNION xs)) x = ?putUnion
78+ -- poke (CPt p o (UNION xs)) x = ?pokeUnion
66−-- put (CPt p o (STRUCT xs)) x = ?putStruct
79+ -- poke (CPt p o (STRUCT xs)) x = ?pokeStruct
67−-- put (CPt p o (PACKEDSTRUCT xs)) x = ?putPacked
80+ -- poke (CPt p o (PACKEDSTRUCT xs)) x = ?pokePacked
68
81
69-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
82-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
70-- TODO : Fix bounds checking
83-- TODO : Fix bounds checking
libs/contrib/CFFI/Types.idr+1−1
@@ -113,7 +113,7 @@ offsets : CType -> List Int
113offsets (STRUCT xs) = offsetsStruct xs
113offsets (STRUCT xs) = offsetsStruct xs
114offsets (PACKEDSTRUCT xs) = offsetsPacked xs
114offsets (PACKEDSTRUCT xs) = offsetsPacked xs
115offsets (UNION xs) = replicate (length xs) 0
115offsets (UNION xs) = replicate (length xs) 0
116−offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n]]
116+offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
117offsets _ = [0]
117offsets _ = [0]
118
118
119-- TODO: handle out of bounds with proofs
119-- TODO: handle out of bounds with proofs