7 | import public Data.Fin
9 | import Decidable.Equality
11 | %hide Prelude.Types.elem
21 | data FVect : (capacity : Nat) -> (len : Fin (S capacity)) -> (elem : Type) -> Type where
22 | Nil : FVect capacity FZ elem
28 | -> (xs : FVect capacity len elem)
29 | -> FVect (S capacity) (FS len) elem
31 | %name FVect
xs, ys, zs
33 | Uninhabited (FVect 0 (FS l) e) where
34 | uninhabited []
impossible
35 | uninhabited (x :: xs
) impossible
50 | consWeaker : {n : Nat}
51 | -> {len' : Fin (S n)}
53 | -> FVect (S n) (weaken len') elem
54 | -> FVect (S n) (FS len') elem
55 | consWeaker {n = n} {len' = FZ} v _ = [v]
56 | consWeaker {n = 0} {len' = (FS l')} _ _ = absurd l'
57 | consWeaker {n = (S k)} {len' = (FS l')} v (x :: xs) = v :: (x
61 | strengthenLT : {0 n : _}
63 | -> (0 prf : (finToNat j) `LT` n) =>
65 | strengthenLT FZ @{(LTESucc _)} = FZ
66 | strengthenLT (FS x) @{(LTESucc _)} = FS (strengthenLT x)
68 | weakenStrengthenCancel : {0 n : _}
70 | -> (0 prf : (finToNat x) `LT` n) =>
71 | (weaken (strengthenLT x)) = x
72 | weakenStrengthenCancel FZ @{(LTESucc y)} = Refl
73 | weakenStrengthenCancel (FS x) @{(LTESucc y)} =
74 | cong FS (weakenStrengthenCancel x)
84 | -> {len : Fin (S (S n))}
85 | -> (0 ltPrf : (finToNat len) `LT` (S n)) =>
87 | -> FVect (S n) len elem
88 | -> FVect (S n) (FS (strengthenLT len)) elem
89 | consLT v xs with (weakenStrengthenCancel len)
90 | consLT v xs | cancelPrf = v `consWeaker` (rewrite cancelPrf in xs)
100 | -> {len : Fin (S (S n))}
101 | -> (0 ltPrf : (finToNat len) `LT` (S n)) =>
103 | -> FVect (S n) len elem
104 | -> FVect (S n) (FS (strengthenLT len)) elem
110 | empty : (capacity : Nat) -> FVect capacity FZ elem
116 | replicate : {capacity : Nat}
117 | -> (l : Fin (S capacity))
119 | -> FVect capacity l elem
120 | replicate {capacity} FZ x = []
121 | replicate {capacity = (S k)} (FS y) x = x :: replicate y x
126 | addCapacity : FVect c l a -> (FVect (S c) (weaken l) a)
127 | addCapacity [] = []
128 | addCapacity (x :: xs) = x :: (addCapacity xs)
133 | addCapacityN : (n : Nat)
134 | -> FVect capacity l a
135 | -> (FVect (capacity + n) (weakenN n l) a)
136 | addCapacityN n [] = Nil
137 | addCapacityN n (x :: xs) = x :: (addCapacityN n xs)
141 | removeCapacity : {n : Nat}
142 | -> {len' : Fin (S n)}
143 | -> FVect (S n) (weaken len') a
145 | removeCapacity {n = n} {len' = FZ} [] = []
146 | removeCapacity {n = 0} {len' = (FS l')} (x :: xs) = absurd l'
147 | removeCapacity {n = (S k)} {len' = (FS l')} (x :: xs) =
148 | x :: (removeCapacity xs)
152 | length : FVect capacity l a
155 | length (x :: xs) = S (length xs)
163 | fromVect : Vect l a -> FVect l (last {n=l}) a
165 | fromVect (x :: xs) = x :: fromVect xs
168 | toVect : FVect c l elem -> Vect (finToNat l) elem
170 | toVect (x :: xs) = x :: (toVect xs)
184 | tail : FVect c (FS l) elem -> FVect c (weaken l) elem
185 | tail (x :: xs) = addCapacity xs
190 | dropFirst : FVect (S c) (FS l) elem -> FVect c l elem
191 | dropFirst (x :: xs) = xs
194 | head : FVect c (FS l) elem -> elem
198 | last : FVect c (FS l) elem -> elem
200 | last (x :: (y :: xs)) = last $
y :: xs
208 | init : FVect c (FS l) elem -> FVect c (weaken l) elem
210 | init (x :: (y :: xs)) = x :: (init $
y :: xs)
215 | dropLast : FVect (S c) (FS l) elem -> FVect c l elem
217 | dropLast (x :: (y :: xs)) = x :: (dropLast $
y :: xs)
225 | fVectInjective : {0 xs : FVect c l elem}
226 | -> {0 ys : FVect c l elem}
227 | -> x :: xs = y :: ys
228 | -> (x = y, xs = ys)
229 | fVectInjective Refl = (Refl, Refl)
235 | addRemoveCapacityInverse : (xs : FVect c l elem)
236 | -> (removeCapacity (addCapacity xs)) = xs
237 | addRemoveCapacityInverse [] = Refl
238 | addRemoveCapacityInverse (x :: xs) =
239 | cong (x ::) (addRemoveCapacityInverse xs)
244 | lengthReifies : (v : FVect c l elem) -> length v = finToNat l
245 | lengthReifies [] = Refl
246 | lengthReifies (x :: xs) = cong S (lengthReifies xs)
253 | Functor (FVect c l) where
255 | map f (x :: xs) = f x :: map f xs
262 | {capacity : Nat} -> {l : Fin (S capacity)} -> Applicative (FVect capacity l) where
266 | (f :: fs) <*> (x :: xs) = f x :: (fs <*> xs)
273 | Foldable (FVect c l) where
274 | foldr _ acc [] = acc
275 | foldr f acc (x :: xs) = f x $
foldr f acc xs
282 | Eq elem => Eq (FVect c l elem) where
284 | (x :: xs) == (y :: ys) = if x == y
289 | DecEq elem => DecEq (FVect c l elem) where
290 | decEq [] [] = Yes Refl
291 | decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)
292 | decEq (y :: ys) (y :: ys) | (Yes Refl, Yes Refl) = Yes Refl
293 | decEq (x :: xs) (y :: ys) | (_, No contra) = No $
contra . snd . fVectInjective
294 | decEq (x :: xs) (y :: ys) | (No contra, _) = No $
contra . fst . fVectInjective
305 | catMaybes : {len : Fin (S capacity)}
306 | -> FVect capacity len (Maybe elem)
307 | -> (len' : Fin (S capacity) ** FVect capacity len' elem)
308 | catMaybes {len = FZ} [] = (
FZ ** [])
309 | catMaybes {len = (FS k)} (Nothing :: xs) = let (
l' ** rest)
= catMaybes xs in
310 | (
weaken l' ** addCapacity rest)
311 | catMaybes {len = (FS k)} ((Just x) :: xs) = let (
l' ** rest)
= catMaybes xs in
312 | (
FS l' ** x :: rest)
319 | mapMaybes : {len : Fin (S capacity)}
320 | -> (f : elem -> Maybe elem')
321 | -> FVect capacity len elem
322 | -> (len' : Fin (S capacity) ** FVect capacity len' elem')
323 | mapMaybes {len = FZ} f [] = (
FZ ** [])
324 | mapMaybes {len = (FS k)} f (x :: xs) = case (f x) of
325 | Nothing => let (
l' ** rest)
= mapMaybes f xs in
326 | (
weaken l' ** addCapacity rest)
327 | (Just y) => let (
l' ** rest)
= mapMaybes f xs in
328 | (
FS l' ** y :: rest)
335 | filter : (elem -> Bool)
336 | -> FVect capacity len elem
337 | -> (len' : Fin (S capacity) ** FVect capacity len' elem)
338 | filter p [] = (
FZ ** [])
339 | filter p (x :: xs) = let (
l' ** rest)
= filter p xs in
341 | then (
FS l' ** x :: rest)
342 | else (
weaken l' ** addCapacity rest)