@@ -3,6 +3,7 @@
33module CFFI.Types
44
55import Data.Vect
6+import Debug.Error
67
78%access public export
89%default partial
@@ -110,10 +111,16 @@ offsetsPacked xs = offsets' xs [] 0
110111 offsets' [] acc _ = reverse acc
111112 offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
112113
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
117+ Just x => x
118+ Nothing => error "Out of bounds access"
119+
120+export
114121offset : Composite -> Nat -> Int
115−offset (STRUCT xs) i = fromMaybe 0 $ index' i (offsetsStruct xs)
116−offset (PACKEDSTRUCT xs) i = fromMaybe 0 $ index' i (offsetsPacked xs)
122+offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)
123+offset (PACKEDSTRUCT xs) i = indexOrFail i (offsetsPacked xs)
117124offset (ARRAY _ t) i = sizeOf t * toIntNat i
118125offset (T _) _ = 0
119126
@@ -124,11 +131,11 @@ offsets (UNION xs) = replicate (length xs) 0
124131offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
125132offsets (T _) = [0]
126133
127−-- TODO: handle out of bounds with proofs
128−-- Also choose a better name.
129−select : Composite -> Nat -> Composite
130−select (STRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
131−select (PACKEDSTRUCT xs@(y::_)) i = fromMaybe y (index' i xs)
132−select (UNION xs@(y::_)) i = fromMaybe y (index' i xs)
133−select (ARRAY n t) _ = t
134−select t _ = t
134+
135+export
136+fieldType : Composite -> Nat -> Composite
137+fieldType (STRUCT xs@(y::_)) i = indexOrFail i xs
138+fieldType (PACKEDSTRUCT xs@(y::_)) i = indexOrFail i xs
139+fieldType (UNION xs@(y::_)) i = indexOrFail i xs
140+fieldType (ARRAY n t) _ = t
141+fieldType t _ = t