toki/idris2-lens
1
0
Fork 0
Code Issues Pull requests Activity

Update lens operators

Browse source
This commit is contained in:
Kiana Sheibani 2023-10-19 20:22:23 -04:00
parent 40fd0a3a3b
commit 1e6309237b
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
2 changed files with 15 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Control/Lens/Lens.idr
View file

@ -154,7 +154,7 @@ 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 <<||=; infix 4 <<&&=; infix 4 <<<+>= infix 4 <<-=; infix 4 <</=; infix 4 <<||=; infix 4 <<&&=; infix 4 <<<+>=
infixr 2 <<~ infixr 1 <<<~
public export public export
@ -403,11 +403,8 @@ public export
||| Run a monadic action and set the focus of an optic in state to the result. ||| 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 ||| This is different from `(<~)` and `(<<~)` in that it also passes though
||| the action. ||| the old value of the optic.
public export public export
(<<~) : MonadState s m => Lens s s a b -> m b -> m b (<<<~) : MonadState s m => Lens s s a b -> m b -> m a
(<<~) l x = do (<<<~) l m = l <<.= !m
v <- x
modify $ l @{MkIsLens Function} (const v)
pure v

11
src/Control/Lens/Setter.idr
View file

@ -157,6 +157,8 @@ 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 ||=
infix 4 &&=; infixr 4 <+>= infix 4 &&=; infixr 4 <+>=
infix 1 <~
infixr 1 <<~
||| Set the focus of an optic to `Just` a value. ||| Set the focus of an optic to `Just` a value.
public export public export
@ -303,4 +305,11 @@ public export
||| variable. ||| variable.
public export public export
(<~) : MonadState s m => Setter s s a b -> m b -> m () (<~) : MonadState s m => Setter s s a b -> m b -> m ()
(<~) l m = m >>= (l .=) (<~) l m = l .= !m
||| 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 => Setter s s a b -> m b -> m b
(<<~) l m = l <.= !m