0 | module Data.Vect.Quantifiers
4 | import Data.Vect.Elem
6 | import Decidable.Equality
19 | data Any : (0 p : a -> Type) -> Vect n a -> Type where
21 | Here : {0 xs : Vect n a} -> p x -> Any p (x :: xs)
23 | There : {0 xs : Vect n a} -> Any p xs -> Any p (x :: xs)
30 | data All : (0 p : a -> Type) -> Vect n a -> Type where
32 | (::) : {0 xs : Vect n a} -> p x -> All p xs -> All p (x :: xs)
40 | All (Uninhabited . p) xs => Uninhabited (Any p xs) where
41 | uninhabited @{s::ss} (Here y) = uninhabited y
42 | uninhabited @{s::ss} (There y) = uninhabited y
46 | anyElim : {0 xs : Vect n a} -> {0 p : a -> Type} -> (Any p xs -> b) -> (p x -> b) -> Any p (x :: xs) -> b
47 | anyElim _ f (Here p) = f p
48 | anyElim f _ (There p) = f p
57 | any : (dec : (x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (Any p xs)
58 | any _ Nil = No uninhabited
59 | any p (x::xs) with (p x)
60 | any p (x::xs) | Yes prf = Yes (Here prf)
61 | any p (x::xs) | No prf =
63 | Yes prf' => Yes (There prf')
64 | No prf' => No (anyElim prf' prf)
67 | mapProperty : (f : forall x. p x -> q x) -> Any p l -> Any q l
68 | mapProperty f (Here p) = Here (f p)
69 | mapProperty f (There p) = There (mapProperty f p)
73 | toDPair : {xs : Vect n a} -> Any p xs -> DPair a p
74 | toDPair (Here prf) = (
_ ** prf)
75 | toDPair (There p) = toDPair p
78 | toExists : Any p xs -> Exists p
79 | toExists (Here prf) = Evidence _ prf
80 | toExists (There prf) = toExists prf
84 | anyToFin : {0 xs : Vect n a} -> Any p xs -> Fin n
85 | anyToFin (Here _) = FZ
86 | anyToFin (There later) = FS (anyToFin later)
90 | anyToFinCorrect : {0 xs : Vect n a} ->
91 | (witness : Any p xs) ->
92 | p (anyToFin witness `index` xs)
93 | anyToFinCorrect (Here prf) = prf
94 | anyToFinCorrect (There later) = anyToFinCorrect later
97 | anyToFinV : Any {n} p xs -> (idx : Fin n ** p $
index idx xs)
98 | anyToFinV $
Here x = (
FZ ** x)
99 | anyToFinV $
There x = let (
idx ** v)
= anyToFinV x in (
FS idx ** v)
102 | pushOut : Functor p => Any (p . q) xs -> p $
Any q xs
103 | pushOut @{fp} (Here v) = map @{fp} Here v
104 | pushOut @{fp} (There n) = map @{fp} There $
pushOut n
107 | All (Show . p) xs => Show (Any p xs) where
108 | showPrec d @{s::ss} (Here x) = showCon d "Here" $
showArg x
109 | showPrec d @{s::ss} (There x) = showCon d "There" $
showArg x
112 | All (Eq . p) xs => Eq (Any p xs) where
113 | (==) @{s::ss} (Here x) (Here y) = x == y
114 | (==) @{s::ss} (There x) (There y) = x == y
120 | notAllHere : {0 p : a -> Type} -> {xs : Vect n a} -> Not (p x) -> Not (All p (x :: xs))
121 | notAllHere _ Nil
impossible
122 | notAllHere np (p :: _) = np p
125 | notAllThere : {0 p : a -> Type} -> {xs : Vect n a} -> Not (All p xs) -> Not (All p (x :: xs))
126 | notAllThere _ Nil
impossible
127 | notAllThere np (_ :: ps) = np ps
136 | all : (dec : (x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (All p xs)
137 | all _ Nil = Yes Nil
138 | all d (x::xs) with (d x)
139 | all d (x::xs) | No prf = No (notAllHere prf)
140 | all d (x::xs) | Yes prf =
142 | Yes prf' => Yes (prf :: prf')
143 | No prf' => No (notAllThere prf')
146 | Either (Uninhabited $
p x) (Uninhabited $
All p xs) => Uninhabited (All p $
x::xs) where
147 | uninhabited @{Left _} (px::pxs) = uninhabited px
148 | uninhabited @{Right _} (px::pxs) = uninhabited pxs
151 | mapProperty : (f : forall x. p x -> q x) -> All p l -> All q l
152 | mapProperty f [] = []
153 | mapProperty f (p::pl) = f p :: mapProperty f pl
158 | mapPropertyRelevant : {xs : Vect n a} ->
159 | (f : (x : a) -> p x -> q x) ->
162 | mapPropertyRelevant f [] = []
163 | mapPropertyRelevant f (p :: ps) = f _ p :: mapPropertyRelevant f ps
166 | imapProperty : {0 a : Type}
167 | -> {0 p,q : a -> Type}
168 | -> (0 i : a -> Type)
169 | -> (f : {0 x : a} -> i x => p x -> q x)
170 | -> {0 as : Vect n a}
171 | -> All i as => All p as -> All q as
172 | imapProperty _ _ [] = []
173 | imapProperty i f @{ix :: ixs} (x::xs) = f @{ix} x :: imapProperty i f @{ixs} xs
178 | forget : All (const p) {n} xs -> Vect n p
180 | forget (x::xs) = x :: forget xs
185 | remember : (xs : Vect n ty) -> All (const ty) xs
187 | remember (x :: xs) = x :: remember xs
190 | forgetRememberId : (xs : Vect n ty) -> forget (remember xs) = xs
191 | forgetRememberId [] = Refl
192 | forgetRememberId (x :: xs) = cong (x ::) (forgetRememberId xs)
195 | castAllConst : {0 xs, ys : Vect n a} -> All (const ty) xs -> All (const ty) ys
196 | castAllConst [] = rewrite invertVectZ ys in []
197 | castAllConst (x :: xs) = rewrite invertVectS ys in x :: castAllConst xs
200 | rememberForgetId : (vs : All (const ty) xs) ->
201 | castAllConst (remember (forget vs)) === vs
202 | rememberForgetId [] = Refl
203 | rememberForgetId (x :: xs) = cong (x ::) (rememberForgetId xs)
206 | zipPropertyWith : (f : {0 x : a} -> p x -> q x -> r x) ->
207 | All p xs -> All q xs -> All r xs
208 | zipPropertyWith f [] [] = []
209 | zipPropertyWith f (px :: pxs) (qx :: qxs)
210 | = f px qx :: zipPropertyWith f pxs qxs
215 | traverseProperty : Applicative f =>
216 | {0 xs : Vect n a} ->
217 | (forall x. p x -> f (q x)) ->
220 | traverseProperty f [] = pure []
221 | traverseProperty f (x :: xs) = [| f x :: traverseProperty f xs |]
226 | traversePropertyRelevant : Applicative f =>
228 | ((x : a) -> p x -> f (q x)) ->
231 | traversePropertyRelevant f [] = pure []
232 | traversePropertyRelevant f (x :: xs) = [| f _ x :: traversePropertyRelevant f xs |]
235 | consInjective : {0 xs, ys: All p ts} -> {0 x, y: p a} -> (x :: xs = y :: ys) -> (x = y, xs = ys)
236 | consInjective Refl = (Refl, Refl)
239 | tabulate : {n : _} ->
240 | {0 xs : Vect n _} ->
241 | (f : (ix : Fin n) -> p (ix `index` xs)) ->
243 | tabulate {xs = []} f = []
244 | tabulate {xs = _ :: _} f = f FZ :: tabulate (\ix => f (FS ix))
247 | (++) : (axs : All p xs) -> (ays : All p ys) -> All p (xs ++ ys)
249 | (ax :: axs) ++ ays = ax :: (axs ++ ays)
252 | All (Show . p) xs => Show (All p xs) where
253 | show pxs = "[" ++ show' "" pxs ++ "]"
255 | show' : String -> All (Show . p) xs' => All p xs' -> String
256 | show' acc @{[]} [] = acc
257 | show' acc @{[_]} [px] = acc ++ show px
258 | show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
261 | All (DecEq . p) xs => DecEq (All p xs) where
262 | decEq [] [] = Yes Refl
263 | decEq @{deq :: deqs} (x :: xs) (y :: ys) with (decEq x y)
264 | decEq @{deq :: deqs} (x :: xs) (y :: ys) | (Yes prf) with (decEq xs ys)
265 | decEq @{deq :: deqs} (x :: xs) (y :: ys) | (Yes prf) | (Yes prf') =
266 | Yes (rewrite prf in rewrite prf' in Refl)
267 | decEq @{deq :: deqs} (x :: xs) (y :: ys) | (Yes prf) | (No contra) =
268 | No (contra . snd . consInjective)
269 | decEq @{deq :: deqs} (x :: xs) (y :: ys) | (No contra) =
270 | No (contra . fst . consInjective)
273 | All (Eq . p) xs => Eq (All p xs) where
275 | (==) @{_ :: _} (h1::t1) (h2::t2) = h1 == h2 && t1 == t2
278 | allEq : All (Ord . p) xs => All (Eq . p) xs
280 | allEq @{_ :: _} = %search :: allEq
283 | All (Ord . p) xs => Ord (All p xs) where
285 | compare @{_ :: _} (h1::t1) (h2::t2) = case compare h1 h2 of
286 | EQ => compare t1 t2
290 | All (Semigroup . p) xs => Semigroup (All p xs) where
292 | (<+>) @{_ :: _} (h1::t1) (h2::t2) = (h1 <+> h2) :: (t1 <+> t2)
295 | allSemigroup : All (Monoid . p) xs => All (Semigroup . p) xs
296 | allSemigroup @{[]} = []
297 | allSemigroup @{_ :: _} = %search :: allSemigroup
300 | All (Monoid . p) xs => Monoid (All p xs) where
302 | neutral @{_::_} = neutral :: neutral
306 | HVect : Vect n Type -> Type
311 | head : All p (x :: xs) -> p x
316 | tail : All p (x :: xs) -> All p xs
317 | tail (_ :: ys) = ys
322 | drop : {0 m : _} -> (n : Nat) -> {0 xs : Vect (n + m) a} -> All p xs -> All p (the (Vect m a) (Vect.drop n xs))
324 | drop (S k) (y :: ys) = drop k ys
329 | drop' : {0 k : _} -> {0 xs : Vect k _} -> (l : Nat) -> All p xs -> All p (Vect.drop' l xs)
330 | drop' 0 ys = rewrite minusZeroRight k in ys
331 | drop' (S k) [] = []
332 | drop' (S k) (y :: ys) = drop' k ys
341 | index : (i : Fin k) -> All p ts -> p (index i ts)
342 | index FZ (x :: xs) = x
343 | index (FS j) (x :: xs) = index j xs
352 | deleteAt : (i : Fin (S l)) -> All p ts -> All p (deleteAt i ts)
353 | deleteAt FZ (x :: xs) = xs
354 | deleteAt (FS FZ) (x :: (y :: xs)) = x :: xs
355 | deleteAt (FS (FS j)) (x :: (y :: xs)) = x :: deleteAt (FS j) (y :: xs)
364 | replaceAt : (i : Fin k) ->
367 | All p (replaceAt i t ts)
368 | replaceAt FZ y (x :: xs) = y :: xs
369 | replaceAt (FS j) y (x :: xs) = x :: replaceAt j y xs
378 | updateAt : (i : Fin k) ->
379 | (p (index i ts) -> p t) ->
381 | All p (replaceAt i t ts)
382 | updateAt FZ f (x :: xs) = f x :: xs
383 | updateAt (FS j) f (x :: xs) = x :: updateAt j f xs
392 | get : All p ts -> Elem x ts -> p x
393 | get (x :: xs) Here = x
394 | get (x :: xs) (There e') = get xs e'
403 | replaceElem : All p ts -> (e : Elem t ts) -> p t' -> All p (replaceByElem ts e t')
404 | replaceElem (x :: xs) Here y = y :: xs
405 | replaceElem (x :: xs) (There p') y = x :: replaceElem xs p' y
414 | updateElem : {0 p : _} -> (p t -> p t') -> All p ts -> (e : Elem t ts) -> All p (replaceByElem ts e t')
415 | updateElem f (x :: xs) Here = f x :: xs
416 | updateElem f (x :: xs) (There p') = x :: updateElem f xs p'
420 | pushIn : (xs : Vect n a) -> (0 _ : All p xs) -> Vect n $
Subset a p
422 | pushIn (x::xs) (p::ps) = Element x p :: pushIn xs ps
426 | pullOut : (xs : Vect n $
Subset a p) -> Subset (Vect n a) (All p)
427 | pullOut [] = Element [] []
428 | pullOut (Element x p :: xs) = let Element ss ps = pullOut xs in Element (x::ss) (p::ps)
431 | pushInOutInverse : (xs : Vect n a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf
432 | pushInOutInverse [] [] = Refl
433 | pushInOutInverse (x::xs) (p::ps) = rewrite pushInOutInverse xs ps in Refl
436 | pushOutInInverse : (xs : Vect n $
Subset a p) -> uncurry All.pushIn (pullOut xs) = xs
437 | pushOutInInverse [] = Refl
438 | pushOutInInverse (Element x p :: xs) with (pushOutInInverse xs)
439 | pushOutInInverse (Element x p :: xs) | subprf with (pullOut xs)
440 | pushOutInInverse (Element x p :: xs) | subprf | Element ss ps = rewrite subprf in Refl
443 | pushOut : Applicative p => All (p . q) xs -> p $
All q xs
444 | pushOut [] = pure []
445 | pushOut (x::xs) = [| x :: pushOut xs |]
453 | negAnyAll : {xs : Vect n a} -> Not (Any p xs) -> All (Not . p) xs
454 | negAnyAll {xs=Nil} _ = Nil
455 | negAnyAll {xs=(x::xs)} f = (f . Here) :: negAnyAll (f . There)
460 | anyNegAll : Any (Not . p) xs -> Not (All p xs)
461 | anyNegAll (Here ctra) (p::_) = ctra p
462 | anyNegAll (There np) (_::ps) = anyNegAll np ps
466 | allNegAny : All (Not . p) xs -> Not (Any p xs)
467 | allNegAny [] p = absurd p
468 | allNegAny (np :: npxs) (Here p) = absurd (np p)
469 | allNegAny (np :: npxs) (There p) = allNegAny npxs p
472 | allAnies : {xs : Vect n a} -> All p xs -> Vect n (Any p xs)
474 | allAnies (x::xs) = Here x :: map There (allAnies xs)
477 | altAll : Alternative p => All (p . q) xs -> p $
Any q xs
479 | altAll (a::as) = Here <$> a <|> There <$> altAll as