
   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 | public export
  72 | Replaced : (vs : List a) -> Elem v vs -> (w : a) -> List a
  73 | Replaced (x :: xs) Here      w = w :: xs
  74 | Replaced (x :: xs) (There p) w = x :: Replaced xs p w
  75 | 
  76 | --------------------------------------------------------------------------------
  77 | --          Heterogeneous maps and traversals
  78 | --------------------------------------------------------------------------------
  79 | 
  80 | namespace Any
  81 |   public export %inline
  82 |   hmap : ({0 v : k} -> f v -> g v) -> Any f ks -> Any g ks
  83 |   hmap = mapProperty
  84 | 
  85 |   public export
  86 |   hzipWith :
  87 |        ({0 v : k} -> f v -> g v -> h v)
  88 |     -> All f ks
  89 |     -> Any g ks
  90 |     -> Any h ks
  91 |   hzipWith fun (v :: vs) (Here x)  = Here (fun v x)
  92 |   hzipWith fun (v :: vs) (There x) = There $ hzipWith fun vs x
  93 | 
  94 |   public export
  95 |   collapse : ({0 v : k} -> f v -> x) -> Any f ks -> x
  96 |   collapse g (Here v)  = g v
  97 |   collapse g (There v) = collapse g v
  98 | 
  99 |   public export %inline
 100 |   collapse' : Any (Prelude.const x) ks -> x
 101 |   collapse' = collapse id
 102 | 
 103 |   public export
 104 |   hsequence : Applicative f => Any (f . g) ks -> f (Any g ks)
 105 |   hsequence (Here x)  = Here <$> x
 106 |   hsequence (There x) = There <$> hsequence x
 107 | 
 108 |   export
 109 |   replace : (h : Has t ts) -> f s -> Any f ts -> Any f (Replaced ts h s)
 110 |   replace Here      v (Here x)  = Here v
 111 |   replace Here      v (There x) = There x
 112 |   replace (There p) v (Here x)  = Here x
 113 |   replace (There p) v (There x) = There $ replace p v x
 114 | 
 115 |   export
 116 |   update : (h : Has t ts) => (f t -> f s) -> Any f ts -> Any f (Replaced ts h s)
 117 |   update @{Here}    fun (Here x)  = Here (fun x)
 118 |   update @{Here}    fun (There x) = There x
 119 |   update @{There p} fun (Here x)  = Here x
 120 |   update @{There p} fun (There x) = There $ update fun x
 121 | 
 122 | namespace All
 123 |   public export %inline
 124 |   hmap : ({0 v : k} -> f v -> g v) -> All f ks -> All g ks
 125 |   hmap = mapProperty
 126 | 
 127 |   public export %inline
 128 |   hmapW : {ks : _} -> ((v : k) -> f v -> g v) -> All f ks -> All g ks
 129 |   hmapW {ks = []}    _ []      = []
 130 |   hmapW {ks = v::vs} g (x::xs) = g v x :: hmapW g xs
 131 | 
 132 |   public export
 133 |   hzipWith :
 134 |        ({0 v : k} -> f v -> g v -> h v)
 135 |     -> All f ks
 136 |     -> All g ks
 137 |     -> All h ks
 138 |   hzipWith fun (x :: xs) (y :: ys)  = fun x y :: hzipWith fun xs ys
 139 |   hzipWith fun []        []         = []
 140 | 
 141 |   public export
 142 |   hzipWithW :
 143 |        {ks : _}
 144 |     -> ((v : k) -> f v -> g v -> h v)
 145 |     -> All f ks
 146 |     -> All g ks
 147 |     -> All h ks
 148 |   hzipWithW {ks = v::vs} fun (x :: xs) (y :: ys)  = fun v x y :: hzipWithW fun xs ys
 149 |   hzipWithW {ks = []}    fun []        []         = []
 150 | 
 151 |   public export %inline
 152 |   happly : All (\x => f x -> g x) ks -> Any f ks -> Any g ks
 153 |   happly = hzipWith id
 154 | 
 155 |   public export %inline
 156 |   happly' : All (\x => f x -> t) ks -> Any f ks -> t
 157 |   happly' fs = collapse' . happly fs
 158 | 
 159 |   public export
 160 |   hfill : {ks : _} -> ((v : k) -> f v) -> All f ks
 161 |   hfill {ks = []}    g = []
 162 |   hfill {ks = v::vs} g = g v :: hfill g
 163 | 
 164 |   public export %inline
 165 |   hconst : {ks : _} -> t -> All (Prelude.const t) ks
 166 |   hconst = hfill . const
 167 | 
 168 |   public export
 169 |   hpure : All (Prelude.const ()) ks => ({0 v : k} -> f v) -> All f ks
 170 |   hpure @{[]}     fun = []
 171 |   hpure @{_ :: _} fun = fun :: hpure fun
 172 | 
 173 |   public export
 174 |   hfoldl : ({0 v : k} -> acc -> f v -> acc) -> acc -> All f ks -> acc
 175 |   hfoldl g x []        = x
 176 |   hfoldl g x (y :: ys) = hfoldl g (g x y) ys
 177 | 
 178 |   public export %inline
 179 |   hfoldMap : Monoid m => ({0 v : k} -> f v -> m) -> All f ks -> m
 180 |   hfoldMap g = hfoldl (\x,v => x <+> g v) neutral
 181 | 
 182 |   public export
 183 |   hsequence : Applicative f => All (f . g) ks -> f (All g ks)
 184 |   hsequence []      = pure []
 185 |   hsequence (x::xs) = [| x :: hsequence xs |]
 186 | 
 187 |   export
 188 |   replace : (h : Has t ts) -> f s -> All f ts -> All f (Replaced ts h s)
 189 |   replace Here      v (x::xs) = v :: xs
 190 |   replace (There p) v (x::xs) = x :: replace p v xs
 191 | 
 192 |   export
 193 |   update : (h : Has t ts) => (f t -> f s) -> All f ts -> All f (Replaced ts h s)
 194 |   update @{Here}    fun (x::xs) = fun x :: xs
 195 |   update @{There p} fun (x::xs) = x :: update fun xs
 196 | 
 197 | --------------------------------------------------------------------------------
 198 | --          Implementations
 199 | --------------------------------------------------------------------------------
 200 | 
 201 | %hint
 202 | allEq : All (Ord . p) xs => All (Eq . p) xs
 203 | allEq @{[]}     = []
 204 | allEq @{_ :: _} = %search :: allEq
 205 | 
 206 | export
 207 | All (Ord . p) xs => Ord (Any p xs) where
 208 |   compare @{_ :: _} (Here x)  (Here y)  = compare x y
 209 |   compare @{_ :: _} (There x) (There y) = compare x y
 210 |   compare           (Here _)  (There _) = LT
 211 |   compare           (There _) (Here _)  = GT
 212 |