0 | module Data.List.Quantifiers.Extra
  1 |
  2 | import public Data.List.Elem
  3 | import public Data.List.Quantifiers
  4 |
  5 | %default total
  6 |
  7 | ||| Just like `HList` is an alias for `All id`, this is an
  8 | ||| alias for `Any id`.
  9 | public export
 10 | 0 HSum : List Type -> Type
 11 | HSum = Any id
 12 |
 13 | ||| Proof that a value is present in a list. This is
 14 | ||| just an alias for `Data.List.Elem` with a name that's
 15 | ||| sometimes more fitting.
 16 | public export
 17 | 0 Has : (v : a) -> (vs : List a) -> Type
 18 | Has = Elem
 19 |
 20 | ||| Removes an element from a list. This is used to
 21 | ||| calculate the list of effects after a single effect
 22 | ||| was properly handled.
 23 | public export
 24 | 0 (-) : (ts : List a) -> (v : a) -> (prf : Has v ts) => List a
 25 | (-) (_ :: vs)      _ @{Here}    = vs
 26 | (-) (y :: x :: xs) v @{There k} = y :: (-) (x :: xs) v
 27 |
 28 | ||| Inject a value into a `Any f ts`.
 29 | public export
 30 | inject : (prf : Has t ts) => f t -> Any f ts
 31 | inject @{Here}    v = Here v
 32 | inject @{There _} v = There $ inject v
 33 |
 34 | ||| Injects a heterogeneous sum into a larger one.
 35 | public export
 36 | widen : All (`Has` ts) ss => Any f ss -> Any f ts
 37 | widen @{_::_} (Here v)  = inject v
 38 | widen @{_::_} (There v) = widen v
 39 |
 40 | ||| Tries to extract a value from a `Any f ts`.
 41 | public export
 42 | project : (0 t : k) -> (prf : Has t ts) => Any f ts -> Maybe (f t)
 43 | project t @{Here}    (Here v)  = Just v
 44 | project t @{There p} (There v) = project t @{p} v
 45 | project t _                    = Nothing
 46 |
 47 | ||| Tries to extract a value from a `Any f ts`.
 48 | public export %inline
 49 | project' : (prf : Has t ts) => Any f ts -> Maybe (f t)
 50 | project' = project t
 51 |
 52 | ||| Extracts the only possible value from a unary sum.
 53 | public export %inline
 54 | project1 : Any f [t] -> f t
 55 | project1 (Here v)  = v
 56 | project1 (There _) impossible
 57 |
 58 | ||| Extract one of the values from an `Any f ts`.
 59 | public export
 60 | decomp :
 61 |      {0 t      : k}
 62 |   -> {0 ts     : List k}
 63 |   -> {auto prf : Has t ts}
 64 |   -> Any f ts
 65 |   -> Either (Any f (ts - t)) (f t)
 66 | decomp @{Here}                       (Here v)  = Right v
 67 | decomp @{Here}                       (There v) = Left $ v
 68 | decomp @{There _} {ts = _ :: _ :: _} (Here v)  = Left $ Here v
 69 | decomp @{There _} {ts = _ :: _ :: _} (There v) = mapFst There $ decomp v
 70 |
 71 | --------------------------------------------------------------------------------
 72 | --          Heterogeneous maps and traversals
 73 | --------------------------------------------------------------------------------
 74 |
 75 | namespace Any
 76 |   public export %inline
 77 |   hmap : ({0 v : k} -> f v -> g v) -> Any f ks -> Any g ks
 78 |   hmap = mapProperty
 79 |
 80 |   public export
 81 |   hzipWith :
 82 |        ({0 v : k} -> f v -> g v -> h v)
 83 |     -> All f ks
 84 |     -> Any g ks
 85 |     -> Any h ks
 86 |   hzipWith fun (v :: vs) (Here x)  = Here (fun v x)
 87 |   hzipWith fun (v :: vs) (There x) = There $ hzipWith fun vs x
 88 |
 89 |   public export
 90 |   collapse : ({0 v : k} -> f v -> x) -> Any f ks -> x
 91 |   collapse g (Here v)  = g v
 92 |   collapse g (There v) = collapse g v
 93 |
 94 |   public export %inline
 95 |   collapse' : Any (Prelude.const x) ks -> x
 96 |   collapse' = collapse id
 97 |
 98 |   public export
 99 |   hsequence : Applicative f => Any (f . g) ks -> f (Any g ks)
100 |   hsequence (Here x)  = Here <$> x
101 |   hsequence (There x) = There <$> hsequence x
102 |
103 | namespace All
104 |   public export %inline
105 |   hmap : ({0 v : k} -> f v -> g v) -> All f ks -> All g ks
106 |   hmap = mapProperty
107 |
108 |   public export %inline
109 |   hmapW : {ks : _} -> ((v : k) -> f v -> g v) -> All f ks -> All g ks
110 |   hmapW {ks = []}    _ []      = []
111 |   hmapW {ks = v::vs} g (x::xs) = g v x :: hmapW g xs
112 |
113 |   public export
114 |   hzipWith :
115 |        ({0 v : k} -> f v -> g v -> h v)
116 |     -> All f ks
117 |     -> All g ks
118 |     -> All h ks
119 |   hzipWith fun (x :: xs) (y :: ys)  = fun x y :: hzipWith fun xs ys
120 |   hzipWith fun []        []         = []
121 |
122 |   public export
123 |   hzipWithW :
124 |        {ks : _}
125 |     -> ((v : k) -> f v -> g v -> h v)
126 |     -> All f ks
127 |     -> All g ks
128 |     -> All h ks
129 |   hzipWithW {ks = v::vs} fun (x :: xs) (y :: ys)  = fun v x y :: hzipWithW fun xs ys
130 |   hzipWithW {ks = []}    fun []        []         = []
131 |
132 |   public export %inline
133 |   happly : All (\x => f x -> g x) ks -> Any f ks -> Any g ks
134 |   happly = hzipWith id
135 |
136 |   public export %inline
137 |   happly' : All (\x => f x -> t) ks -> Any f ks -> t
138 |   happly' fs = collapse' . happly fs
139 |
140 |   public export
141 |   hfill : {ks : _} -> ((v : k) -> f v) -> All f ks
142 |   hfill {ks = []}    g = []
143 |   hfill {ks = v::vs} g = g v :: hfill g
144 |
145 |   public export %inline
146 |   hconst : {ks : _} -> t -> All (Prelude.const t) ks
147 |   hconst = hfill . const
148 |
149 |   public export
150 |   hpure : All (Prelude.const ()) ks => ({0 v : k} -> f v) -> All f ks
151 |   hpure @{[]}     fun = []
152 |   hpure @{_ :: _} fun = fun :: hpure fun
153 |
154 |   public export
155 |   hfoldl : ({0 v : k} -> acc -> f v -> acc) -> acc -> All f ks -> acc
156 |   hfoldl g x []        = x
157 |   hfoldl g x (y :: ys) = hfoldl g (g x y) ys
158 |
159 |   public export %inline
160 |   hfoldMap : Monoid m => ({0 v : k} -> f v -> m) -> All f ks -> m
161 |   hfoldMap g = hfoldl (\x,v => x <+> g v) neutral
162 |
163 |   public export
164 |   hsequence : Applicative f => All (f . g) ks -> f (All g ks)
165 |   hsequence []      = pure []
166 |   hsequence (x::xs) = [| x :: hsequence xs |]
167 |
168 | --------------------------------------------------------------------------------
169 | --          Implementations
170 | --------------------------------------------------------------------------------
171 |
172 | %hint
173 | allEq : All (Ord . p) xs => All (Eq . p) xs
174 | allEq @{[]}     = []
175 | allEq @{_ :: _} = %search :: allEq
176 |
177 | export
178 | All (Ord . p) xs => Ord (Any p xs) where
179 |   compare @{_ :: _} (Here x)  (Here y)  = compare x y
180 |   compare @{_ :: _} (There x) (There y) = compare x y
181 |   compare           (Here _)  (There _) = LT
182 |   compare           (There _) (Here _)  = GT
183 |