
   0 | module Control.Lens.Lens
   1 | 
   2 | import Data.Profunctor
   3 | import Data.Profunctor.Yoneda
   4 | import Control.Monad.State
   5 | import Control.Lens.Optic
   6 | import Control.Lens.Indexed
   7 | import Control.Lens.Equality
   8 | import Control.Lens.Iso
   9 | 
  10 | %default total
  11 | 
  12 | 
  13 | ------------------------------------------------------------------------------
  14 | -- Type definitions
  15 | ------------------------------------------------------------------------------
  16 | 
  17 | 
  18 | public export
  19 | record IsLens p where
  20 |   constructor MkIsLens
  21 |   runIsLens : Strong p
  22 | 
  23 | export %hint
  24 | lensToIso : IsLens p => IsIso p
  25 | lensToIso @{MkIsLens _} = MkIsIso %search
  26 | 
  27 | export %hint
  28 | indexedLens : IsLens p => IsLens (Indexed i p)
  29 | indexedLens @{MkIsLens _} = MkIsLens %search
  30 | 
  31 | 
  32 | ||| A *lens* is a functional reference to a value within a larger data structure.
  33 | ||| Lenses allow one to access or modify the value that they reference, called
  34 | ||| the "focus" or "focus element".
  35 | |||
  36 | ||| For example, the lens `fst_` from `Data.Tuple.Lens` focuses on the first
  37 | ||| element of a pair. It has the type:
  38 | |||
  39 | ||| ```idris
  40 | ||| fst_ : Lens (a, c) (b, c) a b
  41 | ||| ```
  42 | |||
  43 | ||| The types `s, t` correspond to the type of the outside data structure, and
  44 | ||| `a, b` correspond to the type of the focus element. Two of each type is
  45 | ||| provided to allow for operations that change the type of the focus.
  46 | public export
  47 | 0 Lens : (s,t,a,b : Type) -> Type
  48 | Lens = Optic IsLens
  49 | 
  50 | ||| `Lens'` is the `Simple` version of `Lens`.
  51 | public export
  52 | 0 Lens' : (s,a : Type) -> Type
  53 | Lens' = Simple Lens
  54 | 
  55 | ||| An indexed lens allows access to the index of a focus while setting it.
  56 | |||
  57 | ||| Any indexed lens can be coerced into a regular lens and used in normal lens
  58 | ||| functions, but there are also special functions that take indexed lenses
  59 | ||| (i.e. `iover` instead of `over`).
  60 | public export
  61 | 0 IndexedLens : (i,s,t,a,b : Type) -> Type
  62 | IndexedLens = IndexedOptic IsLens
  63 | 
  64 | ||| `IndexedLens'` is the `Simple` version of `IndexedLens`.
  65 | public export
  66 | 0 IndexedLens' : (i,s,a : Type) -> Type
  67 | IndexedLens' = Simple . IndexedLens
  68 | 
  69 | 
  70 | ------------------------------------------------------------------------------
  71 | -- Utilities for lenses
  72 | ------------------------------------------------------------------------------
  73 | 
  74 | 
  75 | ||| Construct a lens given getter and setter functions.
  76 | |||
  77 | ||| @ get The getter function
  78 | ||| @ set The setter function, where the first argument is the data structure
  79 | ||| to modify and the second argument is the new focus value
  80 | public export
  81 | lens : (get : s -> a) -> (set : s -> b -> t) -> Lens s t a b
  82 | lens get set @{MkIsLens _} = dimap (\x => (x, get x)) (uncurry set) . second
  83 | 
  84 | ||| Construct an indexed lens given getter and setter functions.
  85 | public export
  86 | ilens : (get : s -> (i, a)) -> (set : s -> b -> t) -> IndexedLens i s t a b
  87 | ilens get set @{_} @{ind} = lens get set . indexed @{ind}
  88 | 
  89 | 
  90 | ||| Extract getter and setter functions from a lens.
  91 | public export
  92 | getLens : Lens s t a b -> (s -> a, s -> b -> t)
  93 | getLens l = l @{MkIsLens strong} (id, const id)
  94 |   where
  95 |     Profunctor (\x,y => (x -> a, x -> b -> y)) where
  96 |       dimap f g (get, set) = (get . f, (g .) . set . f)
  97 | 
  98 |     [strong] GenStrong Pair (\x,y => (x -> a, x -> b -> y)) where
  99 |       strongl (get, set) = (get . fst, \(a,c),b => (set a b, c))
 100 |       strongr (get, set) = (get . snd, \(c,a),b => (c, set a b))
 101 | 
 102 | ||| Extract getter and setter functions from a lens.
 103 | public export
 104 | withLens : Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r
 105 | withLens l f = uncurry f (getLens l)
 106 | 
 107 | 
 108 | ||| `Void` vacuously "contains" a value of any other type.
 109 | public export
 110 | devoid : IndexedLens i Void t a b
 111 | devoid = ilens absurd absurd
 112 | 
 113 | ||| All values contain a unit.
 114 | public export
 115 | united : Lens' a ()
 116 | united @{MkIsLens _} = dimap ((),) snd . first
 117 | 
 118 | ||| Create a lens that operates on pairs from two other lenses.
 119 | public export
 120 | alongside : Lens s t a b -> Lens s' t' a' b' -> Lens (s, s') (t, t') (a, a') (b, b')
 121 | alongside l l' =
 122 |   let (get1, set1) = getLens l
 123 |       (get2, set2) = getLens l'
 124 |   in lens (bimap get1 get2) (uncurry bimap . bimap set1 set2)
 125 | 
 126 | 
 127 | 
 128 | ||| Optimize a composition of optics by fusing their uses of `dimap` into one.
 129 | |||
 130 | ||| This function exploits the Yoneda lemma. `fusing (a . b)` is essentially
 131 | ||| equivalent to `a . b`, but the former will only call `dimap` once.
 132 | public export
 133 | fusing : IsIso p => Optic' (Yoneda p) s t a b -> Optic' p s t a b
 134 | fusing @{MkIsIso _} l = proextract . l . propure
 135 | 
 136 | 
 137 | ------------------------------------------------------------------------------
 138 | -- Operators
 139 | ------------------------------------------------------------------------------
 140 | 
 141 | export infixr 4 %%~, %%=, %%@~, %%@=
 142 | 
 143 | export infixr 4 <%~, <%@~, <+~, <*~, <-~, </~, <||~, <&&~, <<+>~
 144 | export infixr 4 <<%~, <<%@~, <<.~, <<?~, <<+~, <<*~, <<-~, <</~, <<||~, <<&&~, <<<+>~
 145 | 
 146 | export infix 4 <%=, <%@=, <+=, <*=, <-=, </=, <||=, <&&=, <<+>=
 147 | export infix 4 <<%=, <<%@=, <<.=, <<?=, <<+=, <<*=, <<-=, <</=, <<||=, <<&&=, <<<+>=
 148 | 
 149 | export infixr 1 <<<~
 150 | 
 151 | 
 152 | public export
 153 | (%%~) : Functor f => Lens s t a b -> (a -> f b) -> s -> f t
 154 | (%%~) l = applyStar . l . MkStar {f}
 155 | 
 156 | public export
 157 | (%%=) : MonadState s m => Lens s s a b -> (a -> (r, b)) -> m r
 158 | (%%=) = (state . (swap .)) .: (%%~)
 159 | 
 160 | public export
 161 | (%%@~) : Functor f => IndexedLens i s t a b -> (i -> a -> f b) -> s -> f t
 162 | (%%@~) l = applyStar . l {p=Star f} @{%search} @{Idxed}
 163 |             . MkStar . uncurry
 164 | 
 165 | public export
 166 | (%%@=) : MonadState s m => IndexedLens i s s a b -> (i -> a -> (r, b)) -> m r
 167 | (%%@=) = (state . (swap .)) .: (%%@~)
 168 | 
 169 | 
 170 | ||| Modify a value with pass-through.
 171 | public export
 172 | (<%~) : Lens s t a b -> (a -> b) -> s -> (b, t)
 173 | (<%~) l f = l %%~ (\x => (x,x)) . f
 174 | 
 175 | ||| Modify a value with pass-through, having access to the index.
 176 | public export
 177 | (<%@~) : IndexedLens i s t a b -> (i -> a -> b) -> s -> (b, t)
 178 | (<%@~) l f = l %%@~ (\x => (x,x)) .: f
 179 | 
 180 | ||| Add a value to the lens with pass-through.
 181 | public export
 182 | (<+~) : Num a => Lens s t a a -> a -> s -> (a, t)
 183 | (<+~) l = (<%~) l . (+)
 184 | 
 185 | ||| Multiply the lens by a value with pass-through.
 186 | public export
 187 | (<*~) : Num a => Lens s t a a -> a -> s -> (a, t)
 188 | (<*~) l = (<%~) l . (*)
 189 | 
 190 | ||| Subtract a value from the lens with pass-through.
 191 | public export
 192 | (<-~) : Neg a => Lens s t a a -> a -> s -> (a, t)
 193 | (<-~) l = (<%~) l . flip (-)
 194 | 
 195 | ||| Divide the lens by a value with pass-through.
 196 | public export
 197 | (</~) : Fractional a => Lens s t a a -> a -> s -> (a, t)
 198 | (</~) l = (<%~) l . flip (/)
 199 | 
 200 | ||| Logically OR the lens with a constant value with pass-through.
 201 | |||
 202 | ||| Like (||) and (||~), this operator takes a lazy second argument.
 203 | public export
 204 | (<||~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)
 205 | (<||~) l = (<%~) l . flip (||)
 206 | 
 207 | ||| Logically AND the lens with a constant value with pass-through.
 208 | |||
 209 | ||| Like (&&) and (&&~), this operator takes a lazy second argument.
 210 | public export
 211 | (<&&~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)
 212 | (<&&~) l = (<%~) l . flip (&&)
 213 | 
 214 | ||| Modify an lens's focus with the semigroup/monoid operator with pass-through.
 215 | |||
 216 | ||| The constant value is applied to the focus from the right:
 217 | ||| ```
 218 | ||| l <<+>~ x = l <%~ (<+> x)
 219 | ||| ```
 220 | public export
 221 | (<<+>~) : Semigroup a => Lens s t a a -> a -> s -> (a, t)
 222 | (<<+>~) l = (<%~) l . flip (<+>)
 223 | 
 224 | 
 225 | ||| Modify the value of a lens and return the old value.
 226 | public export
 227 | (<<%~) : Lens s t a b -> (a -> b) -> s -> (a, t)
 228 | (<<%~) l f = l %%~ (\x => (x, f x))
 229 | 
 230 | ||| Modify the value of an indexed lens and return the old value.
 231 | (<<%@~) : IndexedLens i s t a b -> (i -> a -> b) -> s -> (a, t)
 232 | (<<%@~) l f = l %%@~ (\i,x => (x, f i x))
 233 | 
 234 | ||| Set the value of a lens and return the old value.
 235 | public export
 236 | (<<.~) : Lens s t a b -> b -> s -> (a, t)
 237 | (<<.~) l x = l %%~ (,x)
 238 | 
 239 | ||| Set a lens to `Just` a value and return the old value.
 240 | public export
 241 | (<<?~) : Lens s t a (Maybe b) -> b -> s -> (a, t)
 242 | (<<?~) l = (<<.~) l . Just
 243 | 
 244 | ||| Add a constant value to a lens's focus and return the old value.
 245 | public export
 246 | (<<+~) : Num a => Lens s t a a -> a -> s -> (a, t)
 247 | (<<+~) l = (<<%~) l . (+)
 248 | 
 249 | ||| Multiply a lens's focus by a constant value and return the old value.
 250 | public export
 251 | (<<*~) : Num a => Lens s t a a -> a -> s -> (a, t)
 252 | (<<*~) l = (<<%~) l . (*)
 253 | 
 254 | ||| Subtract a constant value from a lens's focus and return the old value.
 255 | public export
 256 | (<<-~) : Neg a => Lens s t a a -> a -> s -> (a, t)
 257 | (<<-~) l = (<%~) l . flip (-)
 258 | 
 259 | ||| Divide a lens's focus by a constant value and return the old value.
 260 | public export
 261 | (<</~) : Fractional a => Lens s t a a -> a -> s -> (a, t)
 262 | (<</~) l = (<<%~) l . flip (/)
 263 | 
 264 | ||| Logically OR a lens's focus by a constant value and return the old value.
 265 | |||
 266 | ||| Like (||) and (||~), this operator takes a lazy second argument.
 267 | public export
 268 | (<<||~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)
 269 | (<<||~) l = (<<%~) l . flip (||)
 270 | 
 271 | ||| Logically AND a lens's focus by a constant value and return the old value.
 272 | |||
 273 | ||| Like (&&) and (&&~), this operator takes a lazy second argument.
 274 | public export
 275 | (<<&&~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)
 276 | (<<&&~) l = (<<%~) l . flip (&&)
 277 | 
 278 | ||| Modify a lens's focus using the semigroup/monoid operator and return the
 279 | ||| old value.
 280 | |||
 281 | ||| The constant value is applied to the focus from the right:
 282 | ||| ```
 283 | ||| l <<<+>~ x = l <<%~ (<+> x)
 284 | ||| ```
 285 | public export
 286 | (<<<+>~) : Semigroup a => Lens s t a a -> a -> s -> (a, t)
 287 | (<<<+>~) l = (<<%~) l . flip (<+>)
 288 | 
 289 | 
 290 | ||| Modify within a state monad with pass-through.
 291 | public export
 292 | (<%=) : MonadState s m => Lens s s a b -> (a -> b) -> m b
 293 | (<%=) = (state . (swap .)) .: (<%~)
 294 | 
 295 | ||| Modify within a state monad with pass-through, having access to the index.
 296 | public export
 297 | (<%@=) : MonadState s m => IndexedLens i s s a b -> (i -> a -> b) -> m b
 298 | (<%@=) = (state . (swap .)) .: (<%@~)
 299 | 
 300 | ||| Add a value to the lens into state with pass-through.
 301 | public export
 302 | (<+=) : Num a => MonadState s m => Lens' s a -> a -> m a
 303 | (<+=) = (state . (swap .)) .: (<+~)
 304 | 
 305 | ||| Multiply a lens's focus into state by a constant value with pass-through.
 306 | public export
 307 | (<*=) : Num a => MonadState s m => Lens' s a -> a -> m a
 308 | (<*=) = (state . (swap .)) .: (<*~)
 309 | 
 310 | ||| Subtract a value from the lens into state with pass-through.
 311 | public export
 312 | (<-=) : Neg a => MonadState s m => Lens' s a -> a -> m a
 313 | (<-=) = (state . (swap .)) .: (<-~)
 314 | 
 315 | ||| Divide a lens's focus into state by a constant value with pass-through.
 316 | public export
 317 | (</=) : Fractional a => MonadState s m => Lens' s a -> a -> m a
 318 | (</=) = (state . (swap .)) .: (</~)
 319 | 
 320 | ||| Logically OR a lens's focus into state with a constant value with pass-through.
 321 | public export
 322 | (<||=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool
 323 | (<||=) = (state . (swap .)) .: (<||~)
 324 | 
 325 | ||| Logically AND a lens's focus into state with a constant value with pass-through.
 326 | public export
 327 | (<&&=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool
 328 | (<&&=) = (state . (swap .)) .: (<&&~)
 329 | 
 330 | ||| Modify a lens's focus into state using a semigroup operation with pass-through.
 331 | public export
 332 | (<<+>=) : MonadState s m => Semigroup a => Lens' s a -> a -> m a
 333 | (<<+>=) = (state . (swap .)) .: (<<+>~)
 334 | 
 335 | 
 336 | ||| Modify the value of a lens into state and return the old value.
 337 | public export
 338 | (<<%=) : MonadState s m => Lens s s a b -> (a -> b) -> m a
 339 | (<<%=) = (state . (swap .)) .: (<<%~)
 340 | 
 341 | ||| Modify the value of an indexed lens into state and return the old value.
 342 | public export
 343 | (<<%@=) : MonadState s m => IndexedLens i s s a b -> (i -> a -> b) -> m a
 344 | (<<%@=) = (state . (swap .)) .: (<<%@~)
 345 | 
 346 | ||| Set the value of a lens into state and return the old value.
 347 | public export
 348 | (<<.=) : MonadState s m => Lens s s a b -> b -> m a
 349 | (<<.=) = (state . (swap .)) .: (<<.~)
 350 | 
 351 | ||| Set a lens into state to `Just` a value and return the old value.
 352 | public export
 353 | (<<?=) : MonadState s m => Lens s s a (Maybe b) -> b -> m a
 354 | (<<?=) = (state . (swap .)) .: (<<?~)
 355 | 
 356 | ||| Add a value to the lens into state and return the old value.
 357 | public export
 358 | (<<+=) : Num a => MonadState s m => Lens' s a -> a -> m a
 359 | (<<+=) = (state . (swap .)) .: (<<+~)
 360 | 
 361 | ||| Multiply a lens's focus into state by a constant value and return the old
 362 | ||| value.
 363 | public export
 364 | (<<*=) : Num a => MonadState s m => Lens' s a -> a -> m a
 365 | (<<*=) = (state . (swap .)) .: (<<*~)
 366 | 
 367 | ||| Subtract a value from the lens into state and return the old value.
 368 | public export
 369 | (<<-=) : Neg a => MonadState s m => Lens' s a -> a -> m a
 370 | (<<-=) = (state . (swap .)) .: (<<-~)
 371 | 
 372 | ||| Divide a lens's focus into state by a constant value and return the old
 373 | ||| value.
 374 | public export
 375 | (<</=) : Fractional a => MonadState s m => Lens' s a -> a -> m a
 376 | (<</=) = (state . (swap .)) .: (<</~)
 377 | 
 378 | ||| Logically OR a lens's focus into state with a constant value and return the
 379 | ||| old value.
 380 | public export
 381 | (<<||=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool
 382 | (<<||=) = (state . (swap .)) .: (<<||~)
 383 | 
 384 | ||| Logically AND a lens's focus into state with a constant value and return the
 385 | ||| old value.
 386 | public export
 387 | (<<&&=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool
 388 | (<<&&=) = (state . (swap .)) .: (<<&&~)
 389 | 
 390 | ||| Modify a lens's focus into state using a semigroup operation and return the
 391 | ||| old value.
 392 | public export
 393 | (<<<+>=) : MonadState s m => Semigroup a => Lens' s a -> a -> m a
 394 | (<<<+>=) = (state . (swap .)) .: (<<<+>~)
 395 | 
 396 | 
 397 | ||| Run a monadic action and set the focus of an optic in state to the result.
 398 | ||| This is different from `(<~)` and `(<<~)` in that it also passes though
 399 | ||| the old value of the optic.
 400 | public export
 401 | (<<<~) : MonadState s m => Lens s s a b -> m b -> m a
 402 | (<<<~) l m = l <<.= !m
 403 |