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