git.iko.soy/Idris-dev
on master help sign in
Make things compile, punt on bounds checking
commit30d2a549671832a397e8043fd96faf56a4c1c64c authorNiklas Larsson <niklas@mm.st> dateSat 13 Feb 2016, 20:36 (11 years ago) parentb990e17
2 files changed+26−6
compare with master
unifiedsplit
libs/contrib/CFFI/Memory.idr+11−6 libs/contrib/CFFI/Types.idr+15
libs/contrib/CFFI/Memory.idr+11−6
@@ -39,10 +39,15 @@ put : (p : CPtr) -> (translate (ctype p)) -> IO ()
3939put _ _ = putStrLn "putting"
4040
4141-- update : (p : CPtr) -> ((translate(ctype p)) -> (translate (ctype p)) -> IO ()
42−
43−field : CPtr -> Nat -> CPtr
44−field (CPt p o arr@(ARRAY n t)) i = CPt p (o + index i (offsets arr)) t
45−field (CPt p o (UNION xs)) i = CPt p o (index i xs)
46−field (CPt p o st@(STRUCT xs)) i = CPt p (o + index i (offsets st)) (index i xs)
47−field (CPt p o ps@(PACKEDSTRUCT xs)) i = CPt p (o + index i (offsets st)) (index i xs)
42+-- TODO : Fix bounds checking
43+field : CPtr -> Nat -> CPtr
44+field (CPt p o arr@(ARRAY n t)) i = CPt p (o + offset arr i) t
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 + offset st i) (select st i)
47+field (CPt p o ps@(PACKEDSTRUCT xs)) i = CPt p (o + offset ps i) (select ps i)
4848field 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
8888 offsets' [] acc _ = reverse acc
8989 offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
9090
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+
9198offsets : CType -> List Int
9299offsets (STRUCT xs) = offsetsStruct xs
93100offsets (PACKEDSTRUCT xs) = offsetsPacked xs
94101offsets (UNION xs) = replicate (length xs) 0
95102offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n]]
96103offsets _ = [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