git.iko.soy/Idris-dev
on master help sign in
Make things compile, punt on bounds checking
30d2a54Niklas Larsson
libs/contrib/CFFI/Memory.idr+11−6
compare with master
unifiedsplit
@@ -39,10 +39,15 @@ put : (p : CPtr) -> (translate (ctype p)) -> IO ()
39put _ _ = putStrLn "putting"
39put _ _ = putStrLn "putting"
40
40
41-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
41-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
42−
42+-- TODO : Fix bounds checking
43−field : CPtr -> Nat -> CPtr
43+field : CPtr -> Nat -> CPtr
44−field (CPt p o arr@(ARRAY n t)) i = CPt p (o + index i (offsets arr)) t
44+field (CPt p o arr@(ARRAY n t)) i = CPt p (o + offset arr i) t
45−field (CPt p o (UNION xs)) i = CPt p o (index i xs)
45+field (CPt p o un@(UNION xs)) i = CPt p o (select un i)
46−field (CPt p o st@(STRUCT xs)) i = CPt p (o + index i (offsets st)) (index i xs)
46+field (CPt p o st@(STRUCT xs)) i = CPt p (o + offset st i) (select st i)
47−field (CPt p o ps@(PACKEDSTRUCT xs)) i = CPt p (o + index i (offsets st)) (index i xs)
47+field (CPt p o ps@(PACKEDSTRUCT xs)) i = CPt p (o + offset ps i) (select ps i)
48field p Z = p
48field p Z = p
49+
50+infixl 10 #
51+
52+(#) : CPtr -> Nat -> CPtr
53+(#) = field
libs/contrib/CFFI/Types.idr+15
@@ -88,9 +88,24 @@ offsetsPacked xs = offsets' xs [] 0
88 offsets' [] acc _ = reverse acc
88 offsets' [] acc _ = reverse acc
89 offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
89 offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
90
90
91+-- TODO: Use index and fix upp proofs.
92+offset : CType -> Nat -> Int
93+offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
94+offset (PACKEDSTRUCT xs) i = fromMaybe 0 $ index' i (offsetsPacked xs)
95+offset (ARRAY _ t) i = sizeOf t * toIntNat i
96+offset _ _ = 0
97+
91offsets : CType -> List Int
98offsets : CType -> List Int
92offsets (STRUCT xs) = offsetsStruct xs
99offsets (STRUCT xs) = offsetsStruct xs
93offsets (PACKEDSTRUCT xs) = offsetsPacked xs
100offsets (PACKEDSTRUCT xs) = offsetsPacked xs
94offsets (UNION xs) = replicate (length xs) 0
101offsets (UNION xs) = replicate (length xs) 0
95offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n]]
102offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n]]
96offsets _ = [0]
103offsets _ = [0]
104+
105+-- TODO: handle out of bounds with proofs
106+select : CType -> Nat -> CType
107+select (STRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
108+select (PACKEDSTRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
109+select (UNION xs@(y::_)) i = fromMaybe y (index' i xs)
110+select (ARRAY n t) _ = t
111+select t _ = t