0 | module Data.List1.Quantifiers
5 | import Data.List1.Elem
6 | import Data.List.Quantifiers
19 | data Any : (0 p : a -> Type) -> List1 a -> Type where
21 | Here : {0 xs : List a} -> p x -> Any p (x ::: xs)
23 | There : {0 xs : List a} -> Any p xs -> Any p (x ::: xs)
30 | data All : (0 p : a -> Type) -> List1 a -> Type where
31 | (:::) : {0 xs : List a} -> p x -> All p xs -> All p (x ::: xs)
39 | {0 xs : List1 a} -> All (Uninhabited . p) xs => Uninhabited (Any p xs) where
40 | uninhabited @{s:::ss} (Here y) = uninhabited y
41 | uninhabited @{s:::ss} (There y) = uninhabited y
45 | mapProperty : {l : List1 a} -> (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 : List1 a) -> Dec (Any p xs)
57 | any p (head:::tail) with (p head)
58 | any p (head:::tail) | Yes prf = Yes (Here prf)
59 | any p (head:::tail) | No ctra =
61 | Yes prf' => Yes (There prf')
62 | No ctra' => No $
\case
64 | There ptail => ctra' ptail
68 | toDPair : {xs : List1 a} -> Any p xs -> DPair a p
69 | toDPair (Here prf) = (
_ ** prf)
70 | toDPair (There p) = toDPair p
74 | toExists : {0 xs : List1 a} -> Any p xs -> Exists p
75 | toExists (Here prf) = Evidence _ prf
76 | toExists (There prf) = toExists prf
79 | anyToFin : {0 xs : List1 a} -> Any p xs -> Fin $
length xs
80 | anyToFin (Here _) = FZ
81 | anyToFin (There later) = FS (anyToFin later)
84 | pushOut : Functor p => {0 xs : List1 a} -> Any (p . q) xs -> p $
Any q xs
85 | pushOut @{fp} (Here v) = map @{fp} Here v
86 | pushOut @{fp} (There n) = map @{fp} There $
pushOut n
89 | {0 xs : List1 a} -> All (Show . p) xs => Show (Any p xs) where
90 | showPrec d @{s:::ss} (Here x) = showCon d "Here" $
showArg x
91 | showPrec d @{s:::ss} (There x) = showCon d "There" $
showArg x
94 | {0 xs : List1 a} -> All (Eq . p) xs => Eq (Any p xs) where
95 | (==) @{s:::ss} (Here x) (Here y) = x == y
96 | (==) @{s:::ss} (There x) (There y) = x == y
101 | Either (Uninhabited $
p x) (Uninhabited $
All p xs) => Uninhabited (All p $
x:::xs) where
102 | uninhabited @{Left _} (px:::pxs) = uninhabited px
103 | uninhabited @{Right _} (px:::pxs) = uninhabited pxs
107 | mapProperty : {l : List1 a} -> (f : {0 x : a} -> p x -> q x) -> All p l -> All q l
108 | mapProperty f (p:::pl) = f p ::: mapProperty f pl
112 | imapProperty : (0 i : Type -> Type)
113 | -> (f : {0 a : Type} -> i a => p a -> q a)
114 | -> {0 types : List1 Type}
115 | -> All i types => All p types -> All q types
116 | imapProperty i f @{ix ::: ixs} (x ::: xs) = f @{ix} x ::: imapProperty i f @{ixs} xs
120 | forget : {types : List1 _} -> All (const type) types -> List1 type
121 | forget (x ::: xs) = x ::: forget xs
130 | all : (dec : (x : a) -> Dec (p x)) -> (xs : List1 a) -> Dec (All p xs)
131 | all d (head:::tail) with (d head)
132 | all d (head:::tail) | No ctra = No $
\(p:::_) => ctra p
133 | all d (head:::tail) | Yes prf =
135 | Yes prf' => Yes (prf ::: prf')
136 | No ctra' => No $
\(_:::ps) => ctra' ps
139 | zipPropertyWith : {xs : List1 _} -> (f : {0 x : a} -> p x -> q x -> r x) ->
140 | All p xs -> All q xs -> All r xs
141 | zipPropertyWith f (px ::: pxs) (qx ::: qxs)
142 | = f px qx ::: zipPropertyWith f pxs qxs
154 | HList1 : List1 Type -> Type
159 | pushIn : (xs : List1 a) -> (0 _ : All p xs) -> List1 $
Subset a p
160 | pushIn (x:::xs) (p:::ps) = Element x p ::: pushIn xs ps
164 | pullOut : (xs : List1 $
Subset a p) -> Subset (List1 a) (All p)
165 | pullOut (Element x p ::: xs) = let Element ss ps = pullOut xs in Element (x:::ss) (p:::ps)
168 | pushInOutInverse : (xs : List1 a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf
169 | pushInOutInverse (x:::xs) (p:::ps) = rewrite pushInOutInverse xs ps in Refl
172 | pushOutInInverse : (xs : List1 $
Subset a p) -> uncurry All.pushIn (pullOut xs) = xs
173 | pushOutInInverse (Element x p ::: xs) with (pushOutInInverse xs)
174 | pushOutInInverse (Element x p ::: xs) | subprf with (pullOut xs)
175 | pushOutInInverse (Element x p ::: xs) | subprf | Element ss ps = rewrite subprf in Refl
179 | indexAll : {xs : List1 _} -> Elem x xs -> All p xs -> p x
180 | indexAll Here (p::: _) = p
181 | indexAll (There e) (_:::ps) = indexAll e ps
184 | pushOut : Applicative p => {0 xs : List1 a} -> All (p . q) xs -> p $
All q xs
185 | pushOut (x:::xs) = [| x ::: pushOut xs |]
193 | negAnyAll : {xs : List1 a} -> Not (Any p xs) -> All (Not . p) xs
194 | negAnyAll {xs=x:::xs} f = (f . Here) ::: negAnyAll (f . There)
199 | anyNegAll : {xs : List1 _} -> Any (Not . p) xs -> Not (All p xs)
200 | anyNegAll (Here ctra) (p:::_) = ctra p
201 | anyNegAll (There np) (_:::ps) = anyNegAll np ps
205 | allNegAny : {xs : List1 _} -> All (Not . p) xs -> Not (Any p xs)
206 | allNegAny (np ::: npxs) (Here p) = absurd (np p)
207 | allNegAny (np ::: npxs) (There p) = allNegAny npxs p
210 | allAnies : {0 xs : List1 a} -> All p xs -> List1 (Any p xs)
211 | allAnies (x:::xs) = Here x ::: map There (allAnies xs)
214 | altAll : {0 xs : List1 a} -> Alternative p => All (p . q) xs -> p $
Any q xs
215 | altAll (a:::as) = Here <$> a <|> There <$> altAll as