0 | module Data.SnocList.Quantifiers
5 | import Data.SnocList.Elem
18 | data Any : (0 p : a -> Type) -> SnocList a -> Type where
20 | Here : {0 xs : SnocList a} -> p x -> Any p (xs :< x)
22 | There : {0 xs : SnocList a} -> Any p xs -> Any p (xs :< x)
29 | data All : (0 p : a -> Type) -> SnocList a -> Type where
31 | (:<) : All p xs -> p x -> All p (xs :< x)
39 | All (Uninhabited . p) xs => Uninhabited (Any p xs) where
40 | uninhabited @{ss:<s} (Here y) = uninhabited y
41 | uninhabited @{ss:<s} (There y) = uninhabited y
45 | mapProperty : (f : {0 x : a} -> p x -> q x) -> Any p l -> Any q l
46 | mapProperty f (Here p) = Here (f p)
47 | mapProperty f (There p) = There (mapProperty f p)
56 | any : (dec : (x : a) -> Dec (p x)) -> (xs : SnocList a) -> Dec (Any p xs)
57 | any _ Lin = No uninhabited
58 | any p (xs :< x) with (p x)
59 | any p (xs :< x) | Yes px = Yes (Here px)
60 | any p (xs :< x) | No npx =
62 | Yes pxs => Yes (There pxs)
63 | No npxs => No $
\case
65 | There pxs => npxs pxs
69 | toDPair : {xs : SnocList a} -> Any p xs -> DPair a p
70 | toDPair (Here prf) = (
_ ** prf)
71 | toDPair (There p) = toDPair p
75 | toExists : Any p xs -> Exists p
76 | toExists (Here prf) = Evidence _ prf
77 | toExists (There prf) = toExists prf
80 | anyToFin : Any p xs -> Fin $
length xs
81 | anyToFin (Here _) = FZ
82 | anyToFin (There later) = FS (anyToFin later)
85 | pushOut : Functor p => Any (p . q) xs -> p $
Any q xs
86 | pushOut @{fp} (Here v) = map @{fp} Here v
87 | pushOut @{fp} (There n) = map @{fp} There $
pushOut n
90 | All (Show . p) xs => Show (Any p xs) where
91 | showPrec d @{ss:<s} (Here x) = showCon d "Here" $
showArg x
92 | showPrec d @{ss:<s} (There x) = showCon d "There" $
showArg x
95 | All (Eq . p) xs => Eq (Any p xs) where
96 | (==) @{ss:<s} (Here x) (Here y) = x == y
97 | (==) @{ss:<s} (There x) (There y) = x == y
103 | length : All p xs -> Nat
105 | length (xs :< x) = S (length xs)
108 | (++) : All p xs -> All p ys -> All p (xs ++ ys)
110 | pxs ++ (pys :< py) = (pxs ++ pys) :< py
113 | lengthUnfold : (pxs : All p xs) -> length pxs === length xs
114 | lengthUnfold [<] = Refl
115 | lengthUnfold (pxs :< _) = cong S (lengthUnfold pxs)
119 | Either (Uninhabited (p x)) (Uninhabited (All p xs)) => Uninhabited (All p (xs :< x)) where
120 | uninhabited @{Left _} (pxs :< px) = uninhabited px
121 | uninhabited @{Right _} (pxs :< px) = uninhabited pxs
125 | mapProperty : (f : {0 x : a} -> p x -> q x) -> All p l -> All q l
126 | mapProperty f [<] = [<]
127 | mapProperty f (pxs :< px) = mapProperty f pxs :< f px
131 | imapProperty : (0 i : Type -> Type)
132 | -> (f : {0 a : Type} -> i a => p a -> q a)
133 | -> {0 types : SnocList Type}
134 | -> All i types => All p types -> All q types
135 | imapProperty i f @{[<]} [<] = [<]
136 | imapProperty i f @{ixs :< ix} (xs :< x) = imapProperty i f @{ixs} xs :< f @{ix} x
140 | forget : All (const type) types -> SnocList type
142 | forget (xs :< x) = forget xs :< x
151 | all : (dec : (x : a) -> Dec (p x)) -> (xs : SnocList a) -> Dec (All p xs)
152 | all _ Lin = Yes Lin
153 | all d (xs :< x) with (d x)
154 | all d (xs :< x) | No npx = No $
\(_ :< px) => npx px
155 | all d (xs :< x) | Yes px =
157 | Yes pxs => Yes (pxs :< px)
158 | No npxs => No $
\(pxs :< _) => npxs pxs
161 | zipPropertyWith : (f : {0 x : a} -> p x -> q x -> r x) ->
162 | All p xs -> All q xs -> All r xs
163 | zipPropertyWith f [<] [<] = [<]
164 | zipPropertyWith f (pxs :< px) (qxs :< qx)
165 | = zipPropertyWith f pxs qxs :< f px qx
168 | All Show (map p xs) => Show (All p xs) where
169 | show pxs = concat ("[<" :: show' pxs ["]"])
171 | show' : All Show (map p xs') => All p xs' ->
172 | List String -> List String
173 | show' @{[<]} [<] = id
174 | show' @{[<_]} [<px] = (show px ::)
175 | show' @{_ :< _} (pxs :< px) = show' pxs . (", " ::) . (show px ::)
178 | All (Eq . p) xs => Eq (All p xs) where
179 | (==) [<] [<] = True
180 | (==) @{_ :< _} (t1:<h1) (t2:<h2) = h1 == h2 && t1 == t2
183 | allEq : All (Ord . p) xs => All (Eq . p) xs
185 | allEq @{_ :< _} = allEq :< %search
188 | All (Ord . p) xs => Ord (All p xs) where
189 | compare [<] [<] = EQ
190 | compare @{_ :< _} (t1:<h1) (t2:<h2) = case compare h1 h2 of
191 | EQ => compare t1 t2
195 | All (Semigroup . p) xs => Semigroup (All p xs) where
196 | (<+>) [<] [<] = [<]
197 | (<+>) @{_ :< _} (t1:<h1) (t2:<h2) = (t1 <+> t2) :< (h1 <+> h2)
200 | allSemigroup : All (Monoid . p) xs => All (Semigroup . p) xs
201 | allSemigroup @{[<]} = [<]
202 | allSemigroup @{_ :< _} = allSemigroup :< %search
205 | All (Monoid . p) xs => Monoid (All p xs) where
206 | neutral @{[<]} = [<]
207 | neutral @{_:<_} = neutral :< neutral
211 | HSnocList : SnocList Type -> Type
216 | pushIn : (xs : SnocList a) -> (0 _ : All p xs) -> SnocList $
Subset a p
217 | pushIn [<] [<] = [<]
218 | pushIn (xs:<x) (ps:<p) = pushIn xs ps :< Element x p
222 | pullOut : (xs : SnocList $
Subset a p) -> Subset (SnocList a) (All p)
223 | pullOut [<] = Element [<] [<]
224 | pullOut (xs :< Element x p) = let Element ss ps = pullOut xs in Element (ss:<x) (ps:<p)
227 | pushInOutInverse : (xs : SnocList a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf
228 | pushInOutInverse [<] [<] = Refl
229 | pushInOutInverse (xs:<x) (ps:<p) = rewrite pushInOutInverse xs ps in Refl
232 | pushOutInInverse : (xs : SnocList $
Subset a p) -> uncurry All.pushIn (pullOut xs) = xs
233 | pushOutInInverse [<] = Refl
234 | pushOutInInverse (xs :< Element x p) with (pushOutInInverse xs)
235 | pushOutInInverse (xs :< Element x p) | subprf with (pullOut xs)
236 | pushOutInInverse (xs :< Element x p) | subprf | Element ss ps = rewrite subprf in Refl
240 | indexAll : Elem x xs -> All p xs -> p x
241 | indexAll Here (_ :< px) = px
242 | indexAll (There e) (pxs :< _) = indexAll e pxs
245 | pushOut : Applicative p => All (p . q) xs -> p $
All q xs
246 | pushOut [<] = pure [<]
247 | pushOut (xs:<x) = [| pushOut xs :< x |]
255 | negAnyAll : {xs : SnocList a} -> Not (Any p xs) -> All (Not . p) xs
256 | negAnyAll {xs=[<]} _ = [<]
257 | negAnyAll {xs=xs :< x} f = negAnyAll (f . There) :< (f . Here)
262 | anyNegAll : Any (Not . p) xs -> Not (All p xs)
263 | anyNegAll (Here npx) (_ :< px) = npx px
264 | anyNegAll (There npxs) (pxs :< _) = anyNegAll npxs pxs
268 | allNegAny : All (Not . p) xs -> Not (Any p xs)
269 | allNegAny [<] pxs = absurd pxs
270 | allNegAny (npxs :< npx) (Here px) = absurd (npx px)
271 | allNegAny (npxs :< npx) (There pxs) = allNegAny npxs pxs
274 | allAnies : All p xs -> SnocList (Any p xs)
276 | allAnies (xs:<x) = map There (allAnies xs) :< Here x
279 | altAll : Alternative p => All (p . q) xs -> p $
Any q xs
281 | altAll (as:<a) = Here <$> a <|> There <$> altAll as
287 | decide : ((x : a) -> Either (p x) (q x)) ->
288 | (xs : SnocList a) -> Either (All p xs) (Any q xs)
289 | decide dec [<] = Left [<]
290 | decide dec (xs :< x) = case dec x of
291 | Left px => case decide dec xs of
292 | Left pxs => Left (pxs :< px)
293 | Right pxs => Right (There pxs)
294 | Right px => Right (Here px)