0 | -- Despite the significant difference in the types, idea and function names taken from
  1 | -- https://github.com/idris-lang/Idris2/blob/7972c6acbd7276a53e00e038a09607fc4edad006/libs/base/Data/List/Quantifiers.idr
  2 |
  3 | module Data.CheckedEmpty.List.Quantifiers
  4 |
  5 | import Data.CheckedEmpty.List
  6 | import Data.CheckedEmpty.List.Elem
  7 |
  8 | import Data.DPair
  9 | import Data.Fin
 10 |
 11 | %default total
 12 |
 13 | namespace Any
 14 |
 15 |   public export
 16 |   data Any : (0 p : a -> Type) -> Lst ne a -> Type where
 17 |
 18 |     Here  : {0 u0 : _} -> {0 u1 : _} ->
 19 |             p x -> Any p $ (x :: xs) @{u0} @{u1}
 20 |
 21 |     There : {0 u0 : _} -> {0 u1 : _} ->
 22 |             Any p xs -> Any p $ (x :: xs) @{u0} @{u1}
 23 |
 24 |   export
 25 |   Uninhabited (Any p Nil) where
 26 |     uninhabited (Here _) impossible
 27 |     uninhabited (There _) impossible
 28 |
 29 |   export
 30 |   {0 p : a -> Type} -> {0 u0 : _} -> {0 u1 : _} ->
 31 |   Uninhabited (p x) => Uninhabited (Any p xs) => Uninhabited (Any p $ (x::xs) @{u0} @{u1}) where
 32 |     uninhabited $ Here  y = uninhabited y
 33 |     uninhabited $ There y = uninhabited y
 34 |
 35 |   public export
 36 |   mapProperty : (f : {0 x : a} -> p x -> q x) -> Any p l -> Any q l
 37 |   mapProperty f $ Here p  = Here  $ f p
 38 |   mapProperty f $ There p = There $ mapProperty f p
 39 |
 40 |   public export
 41 |   any : ((x : a) -> Dec $ p x) -> (xs : Lst ne a) -> Dec $ Any p xs
 42 |   any _ Nil = No uninhabited
 43 |   any p $ x::xs with (p x)
 44 |     any p $ _::_  | Yes px = Yes $ Here px
 45 |     any p $ x::xs | No npx = case any p xs of
 46 |       Yes pxs => Yes $ There pxs
 47 |       No npxs => No $ \case
 48 |         Here  px  => npx px
 49 |         There pxs => npxs pxs
 50 |
 51 |   public export
 52 |   toExists : Any p xs -> Exists p
 53 |   toExists $ Here  prf = Evidence _ prf
 54 |   toExists $ There prf = toExists prf
 55 |
 56 | namespace All
 57 |
 58 |   public export
 59 |   data All : (0 p : a -> Type) -> Lst ne a -> Type where
 60 |     Nil  : All p Nil
 61 |     (::) : {0 u0 : _} -> {0 u1 : _} ->
 62 |            p x -> All p xs -> All p $ (x :: xs) @{u0} @{u1}
 63 |
 64 |   export
 65 |   {0 u0 : _} -> {0 u1 : _} ->
 66 |   Either (Uninhabited $ p x) (Uninhabited $ All p xs) => Uninhabited (All p $ (x::xs) @{u0} @{u1}) where
 67 |     uninhabited @{Left  _} (px::pxs) = uninhabited px
 68 |     uninhabited @{Right _} (px::pxs) = uninhabited pxs
 69 |
 70 |   public export
 71 |   mapProperty : (f : {0 x : a} -> p x -> q x) -> All p l -> All q l
 72 |   mapProperty f []      = []
 73 |   mapProperty f (p::ps) = f p :: mapProperty f ps
 74 |
 75 |   public export
 76 |   zipPropertyWith : ({0 x : a} -> p x -> q x -> r x) ->
 77 |                     All p xs -> All q xs -> All r xs
 78 |   zipPropertyWith f []        []        = []
 79 |   zipPropertyWith f (px::pxs) (qx::qxs) = f px qx :: zipPropertyWith f pxs qxs
 80 |
 81 |   public export %inline
 82 |   imapProperty : (0 i : a -> Type) ->
 83 |                  (f : {0 x : _} -> i x => p x -> q x) ->
 84 |                  All i xs => All p xs -> All q xs
 85 |   imapProperty _ f @{ps} = zipPropertyWith (\_ => f) ps
 86 |
 87 |   public export
 88 |   forget : All {ne} (const a) b -> Lst ne a
 89 |   forget []      = []
 90 |   forget (x::xs) = x :: forget xs
 91 |
 92 |   public export
 93 |   all : ((x : a) -> Dec $ p x) -> (xs : Lst _ a) -> Dec $ All p xs
 94 |   all _ Nil = Yes Nil
 95 |   all p $ x::xs with (p x)
 96 |     all p $ _::_  | No npx = No $ \(px::_) => npx px
 97 |     all p $ x::xs | Yes px = case all p xs of
 98 |       Yes pxs => Yes $ px :: pxs
 99 |       No npxs => No $ \(_::pxs) => npxs pxs
100 |
101 |   public export
102 |   index : (idx : Fin xs.length) -> All p xs -> p (index idx xs)
103 |   index FZ     (p::_  ) = p
104 |   index (FS n) ( _::ps) = index n ps
105 |
106 | ||| Heterogeneous list
107 | public export
108 | HLst : Lst ne Type -> Type
109 | HLst = All id
110 |
111 | ----------------------------------------------------------
112 | --- Relationships between `All`, `Any` and other stuff ---
113 | ----------------------------------------------------------
114 |
115 | --- Relations throught `Not` ---
116 |
117 | export
118 | negAnyAll : {xs : Lst ne a} -> Not (Any p xs) -> All (Not . p) xs
119 | negAnyAll {xs=[]}   _ = []
120 | negAnyAll {xs=_::_} f = (f . Here) :: negAnyAll (f . There)
121 |
122 | export
123 | anyNegAll : Any (Not . p) xs -> Not (All p xs)
124 | anyNegAll (Here nnp) (p::_)  = nnp p
125 | anyNegAll (There np) (_::ps) = anyNegAll np ps
126 |
127 | export
128 | allNegAny : All (Not . p) xs -> Not (Any p xs)
129 | allNegAny []         p         = absurd p
130 | allNegAny (np::npxs) (Here p)  = absurd $ np p
131 | allNegAny (np::npxs) (There p) = allNegAny npxs p
132 |
133 | public export
134 | indexAll : Elem x xs -> All p xs -> p x
135 | indexAll  Here     $ p :: _  = p
136 | indexAll (There e) $ _ :: ps = indexAll e ps
137 |
138 | --- Relations between listwise `All` and elementwise `Subset` ---
139 |
140 | public export
141 | pushIn : (xs : Lst ne a) -> (0 _ : All p xs) -> Lst ne $ Subset a p
142 | pushIn []      []      = []
143 | pushIn (x::xs) (p::ps) = Element x p :: pushIn xs ps
144 |
145 | public export
146 | pullOut : (xs : Lst ne $ Subset a p) -> Subset (Lst ne a) (All p)
147 | pullOut []                  = Element [] []
148 | pullOut (Element x p :: xs) = let Element ss ps = pullOut xs in Element (x::ss) (p::ps)
149 |
150 | export
151 | pushInOutInverse : (xs : Lst ne a) -> (0 prf : All p xs) -> pullOut (pushIn xs prf) = Element xs prf
152 | pushInOutInverse []      []      = Refl
153 | pushInOutInverse (x::xs) (p::ps) = rewrite pushInOutInverse xs ps in Refl
154 |
155 | export
156 | pushOutInInverse : (xs : Lst ne $ Subset a p) -> uncurry Quantifiers.pushIn (pullOut xs) = xs
157 | pushOutInInverse [] = Refl
158 | pushOutInInverse (Element x p :: xs) with (pushOutInInverse xs)
159 |   pushOutInInverse (Element x p :: xs) | subprf with (pullOut xs)
160 |     pushOutInInverse (Element x p :: xs) | subprf | Element ss ps = rewrite subprf in Refl
161 |