0 | module Data.List.Fresh.Quantifiers
  1 |
  2 | import Data.List.Fresh
  3 | import Data.DPair
  4 | import Decidable.Equality
  5 | import Data.So
  6 |
  7 | %hide Builtin.infixr.(#)
  8 |
  9 | %default total
 10 |
 11 | namespace Any
 12 |   public export
 13 |   data Any : (0 p : a -> Type) -> FreshList a neq -> Type where
 14 |     Here  : {0 xs : FreshList a neq} -> {auto 0 fresh : x # xs}->
 15 |             (val : p x) -> Any p ((x :: xs) {fresh})
 16 |     There : {0 xs : FreshList a neq} -> {auto 0 fresh : x # xs}->
 17 |             (pos : Any p xs) -> Any p ((x :: xs) {fresh})
 18 |
 19 | export
 20 | Uninhabited (Any {neq} p []) where
 21 |   uninhabited _ impossible
 22 |
 23 | namespace All
 24 |   public export
 25 |   data All : (0 p : a -> Type) -> FreshList a neq -> Type where
 26 |     Nil : All p Nil
 27 |     (::) : {0 xs : FreshList a neq} -> (val : p x) ->
 28 |            {auto 0 fresh : x # xs} -> (vals : All p xs) ->
 29 |       All p ((x :: xs) {fresh})
 30 |
 31 | public export
 32 | lookupWithProof : {xs : FreshList a neq} -> (pos : Any p xs) -> (x : a ** p x)
 33 | lookupWithProof (Here  val) = (_ ** val)
 34 | lookupWithProof (There pos) = lookupWithProof pos
 35 |
 36 | public export
 37 | lookup : {xs : FreshList a neq} -> (pos : Any p xs) -> a
 38 | lookup = fst . lookupWithProof
 39 |
 40 | public export
 41 | remove : {xs : FreshList a neq} -> Any p xs -> FreshList a neq
 42 | 0 removeFreshness : {xs : FreshList a neq} -> (pos : Any p xs) ->
 43 |                     x # xs -> x # remove pos
 44 |
 45 | remove {xs =  _ :: xs}          (Here val)  = xs
 46 | remove {xs = (x :: xs) {fresh}} (There pos)
 47 |   = (x :: remove pos) {fresh = removeFreshness pos fresh}
 48 |
 49 | removeFreshness (Here val)  fresh = snd (soAnd fresh)
 50 | removeFreshness (There pos) fresh =
 51 |   let (neq, fresh) = soAnd fresh in
 52 |   andSo (neq, removeFreshness pos fresh)
 53 |
 54 | export infixr 4 !!
 55 |
 56 | public export
 57 | (!!) : (prfs : All p xs) -> (pos : Any q xs) -> p (lookup pos)
 58 | px :: pxs !! Here  val = px
 59 | px :: pxs !! There pos = pxs !! pos
 60 |
 61 | public export
 62 | (.toFreshList) : {xs : FreshList a neq} -> (rec : All p xs) ->
 63 |   FreshList (x : a ** p x) (neq `on` (.fst))
 64 | public export
 65 | 0 (.toFreshListFreshness) : {xs : FreshList a neq} -> (rec : All p xs) ->
 66 |   (y # xs) -> (y ** _) # rec.toFreshList
 67 |
 68 | [].toFreshList = []
 69 | ((val :: vals) {fresh}).toFreshList = ((_ ** val) :: vals.toFreshList)
 70 |   {fresh = vals.toFreshListFreshness fresh}
 71 |
 72 | []           .toFreshListFreshness y_fresh_xs  = Oh
 73 | (val :: vals).toFreshListFreshness y_fresh_xxs
 74 |   = let (y_fresh_val, y_fresh_vals) = soAnd y_fresh_xxs in
 75 |     andSo (y_fresh_val, vals.toFreshListFreshness y_fresh_vals)
 76 |
 77 | public export
 78 | traverse : {xs : FreshList a neq} ->
 79 |            Applicative f =>
 80 |            ((x : a) -> p x -> f (q x)) ->
 81 |            All {neq} p xs -> f (All {neq} q xs)
 82 | traverse act     []      = pure []
 83 | traverse act ((x :: xs)) = (\x, xs => x :: xs) <$> act _ x <*> traverse act xs
 84 |
 85 | public export
 86 | sequence : Applicative f => All {neq} (f . p) xs -> f (All {neq} p xs)
 87 | sequence [] = pure []
 88 | sequence (val :: vals) = (\x, xs => x :: xs) <$> val <*> sequence vals
 89 |
 90 | public export
 91 | any : (decide : (x : a) -> Dec $ p x) -> (xs : FreshList a neq) -> Dec (Any p xs)
 92 | any _ [] = No absurd
 93 | any decide (x :: xs) = case decide x of
 94 |   Yes prf   => Yes $ Here prf
 95 |   No not_x  => case any decide xs of
 96 |                  Yes prf    => Yes (There prf)
 97 |                  No  not_xs => No $ \case
 98 |                    Here val  => not_x val
 99 |                    There pos => not_xs pos
100 |
101 | public export
102 | isElem : DecEq a => (x : a) -> (xs : FreshList a neq) -> Dec (Any (x ===) xs)
103 | isElem x = any (decEq x)
104 |
105 | public export
106 | (.update) : Applicative f => {0 xs : FreshList a neq} -> (ps : All p xs) ->
107 |   (pos : Any q xs) ->
108 |   (action : p (lookup pos) -> f (p (lookup pos))) -> f (All p xs)
109 | (val :: vals).update (Here  _  ) action = (\x  => x   :: vals) <$> action val
110 | (val :: vals).update (There pos) action = (\xs => val :: xs  ) <$> vals.update pos action
111 |
112 | namespace Any
113 |
114 |   ||| Map a function
115 |   public export
116 |   map : {xs : FreshList a neq} -> ((x : a) -> p x -> q x) ->
117 |     Any p xs -> Any q xs
118 |   map f (Here px) = Here (f _ px)
119 |   map f (There p) = There (map f p)
120 |
121 | namespace All
122 |
123 |   ||| Map a function
124 |   public export
125 |   map : {xs : FreshList a neq} -> ((x : a) -> p x -> q x) ->
126 |     All p xs -> All q xs
127 |   map f [] = []
128 |   map f (px :: pxs) = f _ px :: map f pxs
129 |
130 |   ||| Map a function restricted to the support of the list
131 |   public export
132 |   mapSupport : ((pos : Any f xs) -> q (lookup pos)) -> All f xs -> All q xs
133 |   mapSupport g [] = []
134 |   mapSupport g (val :: vals)
135 |     = g (Here val) ::  mapSupport (\u => g $ There u) vals
136 |
137 | public export
138 | tabulate : {xs : FreshList a neq} -> (f : (x : a) -> p x) -> All p xs
139 | tabulate {xs =   []   } f = []
140 | tabulate {xs = x :: xs} f = f x :: tabulate f
141 |
142 | namespace All
143 |   public export
144 |   foldl : (f : b -> a -> b) -> b -> All {neq} (const a) xs -> b
145 |   foldl f x [] = x
146 |   foldl f x (val :: vals) = foldl f (x `f` val) vals
147 |
148 |   public export
149 |   foldr : (f : a -> b -> b) -> b -> All {neq} (const a) xs -> b
150 |   foldr f x [] = x
151 |   foldr f x (val :: vals) = (val `f` foldr f x vals)
152 |
153 | ------------------------------------------------------------------------
154 | -- Insertions
155 | -- All of these functions are essentially the same but they differ in
156 | -- their type in what is coming in and what is computed. Depending on
157 | -- the situation, one will be more convenient than the other.
158 | -- There is no silver bullet so we define these variations on the same
159 | -- function.
160 | ------------------------------------------------------------------------
161 |
162 | public export
163 | insertWith :
164 |   (f : (y : a) -> q y -> p y) ->
165 |   {xs : FreshList a neq} ->
166 |   (pos : Any q xs) -> All p (remove pos) -> All p xs
167 | insertWith f (Here qx)   pxs         = f _ qx :: pxs
168 | insertWith f (There pos) (py :: pxs) = py :: insertWith f pos pxs
169 |
170 | public export
171 | insertLookedup :
172 |   {xs : FreshList a neq} ->
173 |   (pos : Any q xs) -> p (lookup pos) -> All p (remove pos) -> All p xs
174 | insertLookedup (Here val)  px pxs         = px :: pxs
175 | insertLookedup (There pos) px (py :: pxs) = py :: insertLookedup pos px pxs
176 |