From 5fdd7192b19f206f512dc66cb98bed0707e17e93 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sat, 15 Apr 2023 21:44:56 -0400
Subject: [PATCH] Add operators

---
 src/Control/Lens/Lens.idr      | 250 +++++++++++++++++++++++++++++++++
 src/Control/Lens/Setter.idr    | 171 ++++++++++++++++++++++
 src/Control/Lens/Traversal.idr |  16 +++
 3 files changed, 437 insertions(+)

diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr
index 76de836..6bd158d 100644
--- a/src/Control/Lens/Lens.idr
+++ b/src/Control/Lens/Lens.idr
@@ -2,6 +2,7 @@ module Control.Lens.Lens
 
 import Data.Profunctor
 import Data.Profunctor.Yoneda
+import Control.Monad.State
 import Control.Lens.Optic
 import Control.Lens.Equality
 import Control.Lens.Iso
@@ -107,3 +108,252 @@ alongside l l' =
 public export
 fusing : IsIso p => Optic' (Yoneda p) s t a b -> Optic' p s t a b
 fusing @{MkIsIso _} l = proextract . l . propure
+
+
+------------------------------------------------------------------------------
+-- Operators
+------------------------------------------------------------------------------
+
+infixr 4 %%~; infix 4 %%=
+
+infixr 4 <%~; infixr 4 <+~; infixr 4 <*~; infixr 4 <-~; infixr 4 </~
+infixr 4 <||~; infixr 4 <&&~; infixr 4 <<+>~
+
+infixr 4 <<%~; infixr 4 <<.~; infixr 4 <<?~; infixr 4 <<+~; infixr 4 <<*~
+infixr 4 <<-~; infixr 4 <</~; infixr 4 <<||~; infixr 4 <<&&~; infixr 4 <<<+>~
+
+infix 4 <%=; infix 4 <+=; infix 4 <*=; infix 4 <-=; infix 4 </=
+infix 4 <||=; infix 4 <&&=; infix 4 <<+>=
+
+infix 4 <<%=; infix 4 <<.=; infix 4 <<?=; infix 4 <<+=; infix 4 <<*=
+infix 4 <<-=; infix 4 <</=; infix 4 <<||=; infix 4 <<&&=; infix 4 <<<+>=
+
+infixr 2 <<~
+
+
+public export
+(%%~) : Functor f => Lens s t a b -> (a -> f b) -> s -> f t
+(%%~) l = applyStar . l . MkStar {f}
+
+public export
+(%%=) : MonadState s m => Lens s s a b -> (a -> (r, b)) -> m r
+(%%=) = (state . (swap .)) .: (%%~)
+
+
+||| Modify a value with pass-through.
+public export
+(<%~) : Lens s t a b -> (a -> b) -> s -> (b, t)
+(<%~) l f = l %%~ (\x => (x,x)) . f
+
+||| Add a value to the lens with pass-through.
+public export
+(<+~) : Num a => Lens s t a a -> a -> s -> (a, t)
+(<+~) l = (<%~) l . (+)
+
+||| Multiply the lens by a value with pass-through.
+public export
+(<*~) : Num a => Lens s t a a -> a -> s -> (a, t)
+(<*~) l = (<%~) l . (*)
+
+||| Subtract a value from the lens with pass-through.
+public export
+(<-~) : Neg a => Lens s t a a -> a -> s -> (a, t)
+(<-~) l = (<%~) l . flip (-)
+
+||| Divide the lens by a value with pass-through.
+public export
+(</~) : Fractional a => Lens s t a a -> a -> s -> (a, t)
+(</~) l = (<%~) l . flip (/)
+
+||| Logically OR the lens with a constant value with pass-through.
+|||
+||| Like (||) and (||~), this operator takes a lazy second argument.
+public export
+(<||~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)
+(<||~) l = (<%~) l . flip (||)
+
+||| Logically AND the lens with a constant value with pass-through.
+|||
+||| Like (&&) and (&&~), this operator takes a lazy second argument.
+public export
+(<&&~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)
+(<&&~) l = (<%~) l . flip (&&)
+
+||| Modify an lens's focus with the semigroup/monoid operator with pass-through.
+|||
+||| The constant value is applied to the focus from the right:
+||| ```
+||| l <<+>~ x = l <%~ (<+> x)
+||| ```
+public export
+(<<+>~) : Semigroup a => Lens s t a a -> a -> s -> (a, t)
+(<<+>~) l = (<%~) l . flip (<+>)
+
+
+||| Modify the value of a lens and return the old value.
+public export
+(<<%~) : Lens s t a b -> (a -> b) -> s -> (a, t)
+(<<%~) l f = l %%~ (\x => (x, f x))
+
+||| Set the value of a lens and return the old value.
+public export
+(<<.~) : Lens s t a b -> b -> s -> (a, t)
+(<<.~) l x = l %%~ (,x)
+
+||| Set a lens to `Just` a value and return the old value.
+public export
+(<<?~) : Lens s t a (Maybe b) -> b -> s -> (a, t)
+(<<?~) l = (<<.~) l . Just
+
+||| Add a constant value to a lens's focus and return the old value.
+public export
+(<<+~) : Num a => Lens s t a a -> a -> s -> (a, t)
+(<<+~) l = (<<%~) l . (+)
+
+||| Multiply a lens's focus by a constant value and return the old value.
+public export
+(<<*~) : Num a => Lens s t a a -> a -> s -> (a, t)
+(<<*~) l = (<<%~) l . (*)
+
+||| Subtract a constant value from a lens's focus and return the old value.
+public export
+(<<-~) : Neg a => Lens s t a a -> a -> s -> (a, t)
+(<<-~) l = (<%~) l . flip (-)
+
+||| Divide a lens's focus by a constant value and return the old value.
+public export
+(<</~) : Fractional a => Lens s t a a -> a -> s -> (a, t)
+(<</~) l = (<<%~) l . flip (/)
+
+||| Logically OR a lens's focus by a constant value and return the old value.
+|||
+||| Like (||) and (||~), this operator takes a lazy second argument.
+public export
+(<<||~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)
+(<<||~) l = (<<%~) l . flip (||)
+
+||| Logically AND a lens's focus by a constant value and return the old value.
+|||
+||| Like (&&) and (&&~), this operator takes a lazy second argument.
+public export
+(<<&&~) : Lens s t Bool Bool -> Lazy Bool -> s -> (Bool, t)
+(<<&&~) l = (<<%~) l . flip (&&)
+
+||| Modify a lens's focus using the semigroup/monoid operator and return the
+||| old value.
+|||
+||| The constant value is applied to the focus from the right:
+||| ```
+||| l <<<+>~ x = l <<%~ (<+> x)
+||| ```
+public export
+(<<<+>~) : Semigroup a => Lens s t a a -> a -> s -> (a, t)
+(<<<+>~) l = (<<%~) l . flip (<+>)
+
+
+||| Modify within a state monad with pass-through.
+public export
+(<%=) : MonadState s m => Lens s s a b -> (a -> b) -> m b
+(<%=) = (state . (swap .)) .: (<%~)
+
+||| Add a value to the lens into state with pass-through.
+public export
+(<+=) : Num a => MonadState s m => Lens' s a -> a -> m a
+(<+=) = (state . (swap .)) .: (<+~)
+
+||| Multiply a lens's focus into state by a constant value with pass-through.
+public export
+(<*=) : Num a => MonadState s m => Lens' s a -> a -> m a
+(<*=) = (state . (swap .)) .: (<*~)
+
+||| Subtract a value from the lens into state with pass-through.
+public export
+(<-=) : Neg a => MonadState s m => Lens' s a -> a -> m a
+(<-=) = (state . (swap .)) .: (<-~)
+
+||| Divide a lens's focus into state by a constant value with pass-through.
+public export
+(</=) : Fractional a => MonadState s m => Lens' s a -> a -> m a
+(</=) = (state . (swap .)) .: (</~)
+
+||| Logically OR a lens's focus into state with a constant value with pass-through.
+public export
+(<||=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool
+(<||=) = (state . (swap .)) .: (<||~)
+
+||| Logically AND a lens's focus into state with a constant value with pass-through.
+public export
+(<&&=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool
+(<&&=) = (state . (swap .)) .: (<&&~)
+
+||| Modify a lens's focus into state using a semigroup operation with pass-through.
+public export
+(<<+>=) : MonadState s m => Semigroup a => Lens' s a -> a -> m a
+(<<+>=) = (state . (swap .)) .: (<<+>~)
+
+
+||| Modify the value of a lens into state and return the old value.
+public export
+(<<%=) : MonadState s m => Lens s s a b -> (a -> b) -> m a
+(<<%=) = (state . (swap .)) .: (<<%~)
+
+||| Set the value of a lens into state and return the old value.
+public export
+(<<.=) : MonadState s m => Lens s s a b -> b -> m a
+(<<.=) = (state . (swap .)) .: (<<.~)
+
+||| Set a lens into state to `Just` a value and return the old value.
+public export
+(<<?=) : MonadState s m => Lens s s a (Maybe b) -> b -> m a
+(<<?=) = (state . (swap .)) .: (<<?~)
+
+||| Add a value to the lens into state and return the old value.
+public export
+(<<+=) : Num a => MonadState s m => Lens' s a -> a -> m a
+(<<+=) = (state . (swap .)) .: (<<+~)
+
+||| Multiply a lens's focus into state by a constant value and return the old
+||| value.
+public export
+(<<*=) : Num a => MonadState s m => Lens' s a -> a -> m a
+(<<*=) = (state . (swap .)) .: (<<*~)
+
+||| Subtract a value from the lens into state and return the old value.
+public export
+(<<-=) : Neg a => MonadState s m => Lens' s a -> a -> m a
+(<<-=) = (state . (swap .)) .: (<<-~)
+
+||| Divide a lens's focus into state by a constant value and return the old
+||| value.
+public export
+(<</=) : Fractional a => MonadState s m => Lens' s a -> a -> m a
+(<</=) = (state . (swap .)) .: (<</~)
+
+||| Logically OR a lens's focus into state with a constant value and return the
+||| old value.
+public export
+(<<||=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool
+(<<||=) = (state . (swap .)) .: (<<||~)
+
+||| Logically AND a lens's focus into state with a constant value and return the
+||| old value.
+public export
+(<<&&=) : MonadState s m => Lens s s Bool Bool -> Lazy Bool -> m Bool
+(<<&&=) = (state . (swap .)) .: (<<&&~)
+
+||| Modify a lens's focus into state using a semigroup operation and return the
+||| old value.
+public export
+(<<<+>=) : MonadState s m => Semigroup a => Lens' s a -> a -> m a
+(<<<+>=) = (state . (swap .)) .: (<<<+>~)
+
+
+||| Run a monadic action and set the focus of an optic in state to the result.
+||| This is different from `(<~)` in that it also passes though the output of
+||| the action.
+public export
+(<<~) : MonadState s m => Lens s s a b -> m b -> m b
+(<<~) l x = do
+  v <- x
+  modify $ l @{MkIsLens Function} (const v)
+  pure v
diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr
index 7f5618f..ed63e73 100644
--- a/src/Control/Lens/Setter.idr
+++ b/src/Control/Lens/Setter.idr
@@ -5,6 +5,7 @@ import Data.Profunctor
 import Data.Profunctor.Costrong
 import Data.Profunctor.Traversing
 import Data.Profunctor.Mapping
+import Control.Monad.State
 import Control.Lens.Optic
 import Control.Lens.Traversal
 
@@ -70,7 +71,177 @@ public export
 over : Setter s t a b -> (a -> b) -> s -> t
 over l = l @{MkIsSetter Function}
 
+infixr 4 %~
+
+||| Modify the focus or focuses of an optic.
+|||
+||| This is the operator form of `over`.
+public export
+(%~) : Setter s t a b -> (a -> b) -> s -> t
+(%~) = over
+
+
 ||| Set the focus or focuses of an optic to a constant value.
 public export
 set : Setter s t a b -> b -> s -> t
 set l = over l . const
+
+infixr 4 .~
+
+||| Set the focus or focuses of an optic to a constant value.
+|||
+||| This is the operator form of `set`.
+public export
+(.~) : Setter s t a b -> b -> s -> t
+(.~) = set
+
+
+------------------------------------------------------------------------------
+-- Operators
+------------------------------------------------------------------------------
+
+infixr 4 ?~; infixr 4 <.~; infixr 4 <?~; infixr 4 +~; infixr 4 *~; infixr 4 -~
+infixr 4 /~; infixr 4 ||~; infixr 4 &&~; infixr 4 <+>~
+
+infix 4 %=; infix 4 .=; infix 4 ?=; infix 4 <.=; infix 4 <?=; infix 4 +=
+infix 4 *=; infix 4 -=; infix 4 /=; infix 4 ||=; infix 4 &&=; infixr 4 <+>=
+
+infixr 4 <~
+
+
+||| Set the focus of an optic to `Just` a value.
+public export
+(?~) : Setter s t a (Maybe b) -> b -> s -> t
+(?~) l = set l . Just
+
+||| Set a value with pass-through.
+public export
+(<.~) : Setter s t a b -> b -> s -> (b, t)
+(<.~) l x = (x,) . set l x
+
+||| Set `Just` a value with pass-through.
+public export
+(<?~) : Setter s t a (Maybe b) -> b -> s -> (b, t)
+(<?~) l x = (x,) . (?~) l x
+
+
+||| Add a constant value to the focus of an optic.
+public export
+(+~) : Num a => Setter s t a a -> a -> s -> t
+(+~) l = over l . (+)
+
+||| Multiply the focus of an optic by a constant value.
+public export
+(*~) : Num a => Setter s t a a -> a -> s -> t
+(*~) l = over l . (*)
+
+||| Subtract a constant value from the focus of an optic.
+public export
+(-~) : Neg a => Setter s t a a -> a -> s -> t
+(-~) l = over l . flip (-)
+
+||| Divide the focus of an optic by a constant value.
+public export
+(/~) : Fractional a => Setter s t a a -> a -> s -> t
+(/~) l = over l . flip (/)
+
+||| Logically OR the focus of an optic with a constant value.
+|||
+||| Like `(||)`, this operator takes a lazy second argument.
+public export
+(||~) : Setter s t Bool Bool -> Lazy Bool -> s -> t
+(||~) l = over l . flip (||)
+
+||| Logically AND the focus of an optic with a constant value.
+|||
+||| Like `(&&)`, this operator takes a lazy second argument.
+public export
+(&&~) : Setter s t Bool Bool -> Lazy Bool -> s -> t
+(&&~) l = over l . flip (&&)
+
+||| Modify the focus of an optic using the semigroup/monoid operator.
+|||
+||| The constant value is applied to the focus from the right:
+||| ```idris
+||| l <+>~ x = over l (<+> x)
+||| ```
+public export
+(<+>~) : Semigroup a => Setter s t a a -> a -> s -> t
+(<+>~) l = over l . flip (<+>)
+
+
+||| Modify the focus of an optic within a state monad.
+public export
+(%=) : MonadState s m => Setter s s a b -> (a -> b) -> m ()
+(%=) = modify .: over
+
+||| Set the focus of an optic within a state monad.
+public export
+(.=) : MonadState s m => Setter s s a b -> b -> m ()
+(.=) = modify .: set
+
+||| Set the focus of an optic within a state monad to `Just` a value.
+public export
+(?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m ()
+(?=) = modify .: (?~)
+
+||| Set within a state monad with pass-through.
+public export
+(<.=) : MonadState s m => Setter s s a b -> b -> m b
+(<.=) l x = (l .= x) >> pure x
+
+||| Set to `Just` a value within a state monad with pass-through.
+public export
+(<?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m b
+(<?=) l x = (l ?= x) >> pure x
+
+||| Add a constant value to the focus of an optic within a state monad.
+public export
+(+=) : Num a => MonadState s m => Setter' s a -> a -> m ()
+(+=) = modify .: (+~)
+
+||| Multiply the focus of an optic into state by a constant value.
+public export
+(*=) : Num a => MonadState s m => Setter' s a -> a -> m ()
+(*=) = modify .: (*~)
+
+||| Subtract a constant value from the focus of an optic within a state monad.
+public export
+(-=) : Neg a => MonadState s m => Setter' s a -> a -> m ()
+(-=) = modify .: (-~)
+
+||| Divide the focus of an optic into state by a constant value.
+public export
+(//=) : Fractional a => MonadState s m => Setter' s a -> a -> m ()
+(//=) = modify .: (/~)
+
+||| Logically OR the focus of an optic into state with a constant value.
+|||
+||| Like `(||)`, this operator takes a lazy second argument.
+public export
+(||=) : MonadState s m => Setter' s Bool -> Lazy Bool -> m ()
+(||=) = modify .: (||~)
+
+||| Logically AND the focus of an optic into state with a constant value.
+|||
+||| Like `(&&)`, this operator takes a lazy second argument.
+public export
+(&&=) : MonadState s m => Setter' s Bool -> Lazy Bool -> m ()
+(&&=) = modify .: (&&~)
+
+||| Modify the focus of an optic into state using the semigroup/monoid operator.
+|||
+||| The constant value is applied to the focus from the right.
+public export
+(<+>=) : Semigroup a => MonadState s m => Setter' s a -> a -> m ()
+(<+>=) = modify .: (<+>~)
+
+
+||| Run a monadic action and set the focus of an optic in state to the result.
+|||
+||| This can be thought of as a variation on the do-notation pseudo-operator (<-),
+||| storing the result of a computation within state instead of in a local
+||| variable.
+public export
+(<~) : MonadState s m => Setter s s a b -> m b -> m ()
+(<~) l m = m >>= (l .=)
diff --git a/src/Control/Lens/Traversal.idr b/src/Control/Lens/Traversal.idr
index 1715ca7..72287a6 100644
--- a/src/Control/Lens/Traversal.idr
+++ b/src/Control/Lens/Traversal.idr
@@ -8,6 +8,7 @@ import Control.Applicative.Backwards
 import Control.Applicative.Indexing
 import Control.Lens.Optic
 import Control.Lens.Optional
+import Control.Lens.Lens
 import Control.Lens.Prism
 
 %default total
@@ -127,6 +128,21 @@ failover l f x =
       (b, y) = traverseOf l ((True,) . f) x
   in  guard b $> y
 
+||| Convert a traversal into a lens over a list of values.
+|||
+||| Note that this is only a true lens if the invariant of the list's length is
+||| maintained. You should avoid mapping `over` this lens with a function that
+||| changes the list's length.
+public export
+partsOf : Traversal s t a a -> Lens s t (List a) (List a)
+partsOf l = lens (runForget $ l $ MkForget pure)
+                  (flip evalState . traverseOf l update)
+  where
+    update : a -> State (List a) a
+    update x = get >>= \case
+      x' :: xs' => put xs' >> pure x'
+      []        => pure x
+
 
 ||| Construct an optional that focuses on the first value of a traversal.
 |||