@@ -3,6 +3,7 @@
3module CFFI.Types
3module CFFI.Types
5import Data.Vect
5import Data.Vect
7%access public export
8%access public export
8%default partial
9%default partial
@@ -110,10 +111,16 @@ offsetsPacked xs = offsets' xs [] 0
110 offsets' [] acc _ = reverse acc
111 offsets' [] acc _ = reverse acc
111 offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
112 offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
113−-- TODO: Use index and fix upp proofs.
114+private
115+indexOrFail : Nat -> List a -> a
116+indexOrFail i xs = case index' i xs of
118+ Nothing => error "Out of bounds access"
114offset : Composite -> Nat -> Int
121offset : Composite -> Nat -> Int
115−offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
122+offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)
116−offset (PACKEDSTRUCT xs) i = fromMaybe 0 $ index' i (offsetsPacked xs)
123+offset (PACKEDSTRUCT xs) i = indexOrFail i (offsetsPacked xs)
117offset (ARRAY _ t) i = sizeOf t * toIntNat i
124offset (ARRAY _ t) i = sizeOf t * toIntNat i
118offset (T _) _ = 0
125offset (T _) _ = 0
@@ -124,11 +131,11 @@ offsets (UNION xs) = replicate (length xs) 0
124offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
131offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
125offsets (T _) = [0]
132offsets (T _) = [0]
127−-- TODO: handle out of bounds with proofs
134+
128−-- Also choose a better name.
135+export
129−select : Composite -> Nat -> Composite
136+fieldType : Composite -> Nat -> Composite
130−select (STRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
137+fieldType (STRUCT xs@(y::_)) i = indexOrFail i xs
131−select (PACKEDSTRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
138+fieldType (PACKEDSTRUCT xs@(y::_)) i = indexOrFail i xs
132−select (UNION xs@(y::_)) i = fromMaybe y (index' i xs)
139+fieldType (UNION xs@(y::_)) i = indexOrFail i xs
133−select (ARRAY n t) _ = t
140+fieldType (ARRAY n t) _ = t
134−select t _ = t
141+fieldType t _ = t