Compare commits
No commits in common. "da8f3a05e60673a0700765bdbfdd33f33cb8fd4f" and "63814e7809f4a0d868e18f8cb958cd0efad236a8" have entirely different histories.
da8f3a05e6
...
63814e7809
14
README.md
14
README.md
|
@ -3,14 +3,10 @@
|
||||||
This package provides utilities for working with lenses, prisms, traversals,
|
This package provides utilities for working with lenses, prisms, traversals,
|
||||||
and other optics in Idris. This library uses *profunctor optics*.
|
and other optics in Idris. This library uses *profunctor optics*.
|
||||||
|
|
||||||
## Comparison to Monocle
|
Eventually, this library will also include elaboration scripts to automatically
|
||||||
|
generate lenses for a particular datatype.
|
||||||
|
|
||||||
[Monocle](https://github.com/stefan-hoeck/idris2-monocle) is another Idris 2 library
|
## Comparisons
|
||||||
for lenses. That library represents lenses using a datatype, which is often less
|
|
||||||
efficient at run-time, but results in better error messages and is generally
|
|
||||||
simpler to understand.
|
|
||||||
|
|
||||||
## Comparisons to Non-Idris Libraries
|
|
||||||
|
|
||||||
This library is inspired by the Haskell libraries [lens](https://hackage.haskell.org/package/lens-5.2.2),
|
This library is inspired by the Haskell libraries [lens](https://hackage.haskell.org/package/lens-5.2.2),
|
||||||
[optics](https://hackage.haskell.org/package/optics) and [fresnel](https://hackage.haskell.org/package/fresnel),
|
[optics](https://hackage.haskell.org/package/optics) and [fresnel](https://hackage.haskell.org/package/fresnel),
|
||||||
|
@ -50,7 +46,3 @@ Or you can install using [pack](https://github.com/stefan-hoeck/idris2-pack):
|
||||||
pack install lens
|
pack install lens
|
||||||
```
|
```
|
||||||
|
|
||||||
## Thanks
|
|
||||||
|
|
||||||
Special thanks to [Stefan Höck](https://github.com/stefan-hoeck) for assistance
|
|
||||||
with writing elaboration scripts.
|
|
||||||
|
|
|
@ -1,5 +1,5 @@
|
||||||
package lens
|
package lens
|
||||||
version = 0.3.0
|
version = 0.2.0
|
||||||
|
|
||||||
brief = "Batteries-included profunctor optics"
|
brief = "Batteries-included profunctor optics"
|
||||||
|
|
||||||
|
|
|
@ -37,7 +37,7 @@ public export
|
||||||
||| `ix'`; for example, `Vect n a` uses `Nat` for `ix` and `Fin n` for `ix'`.
|
||| `ix'`; for example, `Vect n a` uses `Nat` for `ix` and `Fin n` for `ix'`.
|
||||||
public export
|
public export
|
||||||
interface Ixed i v a => Ixed' i i' v a | a where
|
interface Ixed i v a => Ixed' i i' v a | a where
|
||||||
||| A lens that infallibly accesses a value at a given index of a container.
|
||| An lens that infallibly accesses a value at a given index of a container.
|
||||||
ix' : i' -> Lens' a v
|
ix' : i' -> Lens' a v
|
||||||
|
|
||||||
||| An indexed version of `ix'`.
|
||| An indexed version of `ix'`.
|
||||||
|
|
|
@ -218,7 +218,7 @@ ianyOf = ifoldMapOf @{Any}
|
||||||
||| Return `True` if the element occurs in the focuses of the optic.
|
||| Return `True` if the element occurs in the focuses of the optic.
|
||||||
public export
|
public export
|
||||||
elemOf : Eq a => Fold s a -> a -> s -> Bool
|
elemOf : Eq a => Fold s a -> a -> s -> Bool
|
||||||
elemOf l = anyOf l . (==)
|
elemOf l = allOf l . (==)
|
||||||
|
|
||||||
||| Calculate the number of focuses of the optic.
|
||| Calculate the number of focuses of the optic.
|
||||||
public export
|
public export
|
||||||
|
@ -287,7 +287,7 @@ public export
|
||||||
preview : Fold s a -> s -> Maybe a
|
preview : Fold s a -> s -> Maybe a
|
||||||
preview = firstOf
|
preview = firstOf
|
||||||
|
|
||||||
export infixl 8 ^?, ^@?, ^., ^@.
|
infixl 8 ^?
|
||||||
|
|
||||||
||| Access the first focus value of an optic, returning `Nothing` if there are
|
||| Access the first focus value of an optic, returning `Nothing` if there are
|
||||||
||| no focuses.
|
||| no focuses.
|
||||||
|
@ -306,6 +306,8 @@ public export
|
||||||
ipreview : IndexedFold i s a -> s -> Maybe (i, a)
|
ipreview : IndexedFold i s a -> s -> Maybe (i, a)
|
||||||
ipreview = ifirstOf
|
ipreview = ifirstOf
|
||||||
|
|
||||||
|
infixl 8 ^@?
|
||||||
|
|
||||||
||| Access the first focus value and index of an indexed optic, returning Nothing
|
||| Access the first focus value and index of an indexed optic, returning Nothing
|
||||||
||| if there are no focuses.
|
||| if there are no focuses.
|
||||||
|||
|
|||
|
||||||
|
@ -336,6 +338,8 @@ public export
|
||||||
toListOf : Fold s a -> s -> List a
|
toListOf : Fold s a -> s -> List a
|
||||||
toListOf l = foldrOf l (::) []
|
toListOf l = foldrOf l (::) []
|
||||||
|
|
||||||
|
infixl 8 ^..
|
||||||
|
|
||||||
||| Return a list of all focuses of a fold.
|
||| Return a list of all focuses of a fold.
|
||||||
|||
|
|||
|
||||||
||| This is the operator form of `toListOf`.
|
||| This is the operator form of `toListOf`.
|
||||||
|
@ -349,6 +353,8 @@ public export
|
||||||
itoListOf : IndexedFold i s a -> s -> List (i, a)
|
itoListOf : IndexedFold i s a -> s -> List (i, a)
|
||||||
itoListOf l = ifoldrOf l ((::) .: (,)) []
|
itoListOf l = ifoldrOf l ((::) .: (,)) []
|
||||||
|
|
||||||
|
infixl 8 ^@..
|
||||||
|
|
||||||
||| Return a list of all focuses and indices of an indexed fold.
|
||| Return a list of all focuses and indices of an indexed fold.
|
||||||
|||
|
|||
|
||||||
||| This is the operator form of `itoListOf`.
|
||| This is the operator form of `itoListOf`.
|
||||||
|
|
|
@ -85,7 +85,8 @@ iview : IndexedGetter i s a -> s -> (i, a)
|
||||||
iview l = runForget $ l @{%search} @{Idxed} $ MkForget id
|
iview l = runForget $ l @{%search} @{Idxed} $ MkForget id
|
||||||
|
|
||||||
|
|
||||||
export infixl 8 ^., ^@.
|
infixl 8 ^.
|
||||||
|
infixl 8 ^@.
|
||||||
|
|
||||||
||| Access the focus value of an optic, particularly a `Getter`.
|
||| Access the focus value of an optic, particularly a `Getter`.
|
||||||
|||
|
|||
|
||||||
|
|
|
@ -93,7 +93,9 @@ icompose @{MkIsIso _} f l l' @{ind} =
|
||||||
l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p}
|
l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p}
|
||||||
. lmap (mapFst (uncurry f) . assocl) . indexed @{ind}
|
. lmap (mapFst (uncurry f) . assocl) . indexed @{ind}
|
||||||
|
|
||||||
export infixr 9 <.>, .>, <.
|
infixr 9 <.>
|
||||||
|
infixr 9 .>
|
||||||
|
infixr 9 <.
|
||||||
|
|
||||||
||| Compose two indexed optics, returning an optic indexed by a pair of indices.
|
||| Compose two indexed optics, returning an optic indexed by a pair of indices.
|
||||||
|||
|
|||
|
||||||
|
|
|
@ -139,15 +139,22 @@ fusing @{MkIsIso _} l = proextract . l . propure
|
||||||
-- Operators
|
-- Operators
|
||||||
------------------------------------------------------------------------------
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
export infixr 4 %%~, %%=, %%@~, %%@=
|
infixr 4 %%~; infix 4 %%=; infix 4 %%@~; infix 4 %%@=
|
||||||
|
|
||||||
export infixr 4 <%~, <%@~, <+~, <*~, <-~, </~, <||~, <&&~, <<+>~
|
infixr 4 <%~; infixr 4 <%@~; infixr 4 <+~; infixr 4 <*~; infixr 4 <-~
|
||||||
export infixr 4 <<%~, <<%@~, <<.~, <<?~, <<+~, <<*~, <<-~, <</~, <<||~, <<&&~, <<<+>~
|
infixr 4 </~; infixr 4 <||~; infixr 4 <&&~; infixr 4 <<+>~
|
||||||
|
|
||||||
export infix 4 <%=, <%@=, <+=, <*=, <-=, </=, <||=, <&&=, <<+>=
|
infixr 4 <<%~; infixr 4 <<%@~; infixr 4 <<.~; infixr 4 <<?~; infixr 4 <<+~
|
||||||
export infix 4 <<%=, <<%@=, <<.=, <<?=, <<+=, <<*=, <<-=, <</=, <<||=, <<&&=, <<<+>=
|
infixr 4 <<*~; infixr 4 <<-~; infixr 4 <</~; infixr 4 <<||~; infixr 4 <<&&~
|
||||||
|
infixr 4 <<<+>~
|
||||||
|
|
||||||
export infixr 1 <<<~
|
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 <<~
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
|
@ -396,8 +403,11 @@ 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 `(<~)` and `(<<~)` in that it also passes though
|
||| This is different from `(<~)` in that it also passes though the output of
|
||||||
||| the old value of the optic.
|
||| the action.
|
||||||
public export
|
public export
|
||||||
(<<<~) : MonadState s m => Lens s s a b -> m b -> m a
|
(<<~) : MonadState s m => Lens s s a b -> m b -> m b
|
||||||
(<<<~) l m = l <<.= !m
|
(<<~) l x = do
|
||||||
|
v <- x
|
||||||
|
modify $ l @{MkIsLens Function} (const v)
|
||||||
|
pure v
|
||||||
|
|
|
@ -66,7 +66,7 @@ public export
|
||||||
review : Review s a -> a -> s
|
review : Review s a -> a -> s
|
||||||
review l = reviews l id
|
review l = reviews l id
|
||||||
|
|
||||||
export infixr 8 ^$
|
infixr 8 ^$
|
||||||
|
|
||||||
||| Turn an optic around to inject a focus value into the larger data structure.
|
||| Turn an optic around to inject a focus value into the larger data structure.
|
||||||
||| This function takes a `Review`, which can also be a `Prism` or `Iso`.
|
||| This function takes a `Review`, which can also be a `Prism` or `Iso`.
|
||||||
|
|
|
@ -91,7 +91,7 @@ public export
|
||||||
over : Setter s t a b -> (a -> b) -> s -> t
|
over : Setter s t a b -> (a -> b) -> s -> t
|
||||||
over l = l @{MkIsSetter Function}
|
over l = l @{MkIsSetter Function}
|
||||||
|
|
||||||
export infixr 4 %~, %@~, .~, .@~
|
infixr 4 %~
|
||||||
|
|
||||||
||| Modify the focus or focuses of an optic.
|
||| Modify the focus or focuses of an optic.
|
||||||
|||
|
|||
|
||||||
|
@ -106,6 +106,8 @@ public export
|
||||||
iover : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t
|
iover : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t
|
||||||
iover l = l @{MkIsSetter Function} @{Idxed} . uncurry
|
iover l = l @{MkIsSetter Function} @{Idxed} . uncurry
|
||||||
|
|
||||||
|
infixr 4 %@~
|
||||||
|
|
||||||
||| Modify the focus or focuses of an indexed optic, having access to the index.
|
||| Modify the focus or focuses of an indexed optic, having access to the index.
|
||||||
|||
|
|||
|
||||||
||| This is the operator form of `iover`.
|
||| This is the operator form of `iover`.
|
||||||
|
@ -119,6 +121,8 @@ public export
|
||||||
set : Setter s t a b -> b -> s -> t
|
set : Setter s t a b -> b -> s -> t
|
||||||
set l = over l . const
|
set l = over l . const
|
||||||
|
|
||||||
|
infixr 4 .~
|
||||||
|
|
||||||
||| Set the focus or focuses of an optic to a constant value.
|
||| Set the focus or focuses of an optic to a constant value.
|
||||||
|||
|
|||
|
||||||
||| This is the operator form of `set`.
|
||| This is the operator form of `set`.
|
||||||
|
@ -132,6 +136,8 @@ public export
|
||||||
iset : IndexedSetter i s t a b -> (i -> b) -> s -> t
|
iset : IndexedSetter i s t a b -> (i -> b) -> s -> t
|
||||||
iset l = iover l . (const .)
|
iset l = iover l . (const .)
|
||||||
|
|
||||||
|
infix 4 .@~
|
||||||
|
|
||||||
||| Set the focus or focuses of an indexed optic, having access to the index.
|
||| Set the focus or focuses of an indexed optic, having access to the index.
|
||||||
|||
|
|||
|
||||||
||| This is the operator form of `iset`.
|
||| This is the operator form of `iset`.
|
||||||
|
@ -144,9 +150,13 @@ public export
|
||||||
-- More operators
|
-- More operators
|
||||||
------------------------------------------------------------------------------
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
export infixr 4 ?~, <.~, <?~, +~, *~, -~, /~, ||~, &&~, <+>~
|
infixr 4 ?~; infixr 4 <.~; infixr 4 <?~; infixr 4 +~; infixr 4 *~; infixr 4 -~
|
||||||
export infix 4 %=, %@=, .=, .@=, ?=, <.=, <?=, +=, *=, -=, //=, ||=, &&=, <+>=
|
infixr 4 /~; infixr 4 ||~; infixr 4 &&~; infixr 4 <+>~
|
||||||
export infix 1 <~, <<~
|
|
||||||
|
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 <+>=
|
||||||
|
|
||||||
|
|
||||||
||| Set the focus of an optic to `Just` a value.
|
||| Set the focus of an optic to `Just` a value.
|
||||||
public export
|
public export
|
||||||
|
@ -237,12 +247,12 @@ public export
|
||||||
||| Set within a state monad with pass-through.
|
||| Set within a state monad with pass-through.
|
||||||
public export
|
public export
|
||||||
(<.=) : MonadState s m => Setter s s a b -> b -> m b
|
(<.=) : MonadState s m => Setter s s a b -> b -> m b
|
||||||
(<.=) l x = (l .= x) $> x
|
(<.=) l x = (l .= x) >> pure x
|
||||||
|
|
||||||
||| Set to `Just` a value within a state monad with pass-through.
|
||| Set to `Just` a value within a state monad with pass-through.
|
||||||
public export
|
public export
|
||||||
(<?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m b
|
(<?=) : MonadState s m => Setter s s a (Maybe b) -> b -> m b
|
||||||
(<?=) l x = (l ?= x) $> x
|
(<?=) l x = (l ?= x) >> pure x
|
||||||
|
|
||||||
||| Add a constant value to the focus of an optic within a state monad.
|
||| Add a constant value to the focus of an optic within a state monad.
|
||||||
public export
|
public export
|
||||||
|
@ -293,11 +303,4 @@ 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 = l .= !m
|
(<~) l m = m >>= (l .=)
|
||||||
|
|
||||||
||| 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
|
|
||||||
|
|
|
@ -188,7 +188,7 @@ ifailover l = failover (l @{%search} @{Idxed}) . uncurry
|
||||||
|
|
||||||
partsOf_update : a -> State (List a) a
|
partsOf_update : a -> State (List a) a
|
||||||
partsOf_update x = get >>= \case
|
partsOf_update x = get >>= \case
|
||||||
x' :: xs' => put xs' $> x'
|
x' :: xs' => put xs' >> pure x'
|
||||||
[] => pure x
|
[] => pure x
|
||||||
|
|
||||||
||| Convert a traversal into a lens over a list of values.
|
||| Convert a traversal into a lens over a list of values.
|
||||||
|
@ -263,12 +263,12 @@ element : Traversable t => Nat -> Optional' (t a) a
|
||||||
element = elementOf traversed
|
element = elementOf traversed
|
||||||
|
|
||||||
|
|
||||||
||| Limit a traversal to its first `n` focuses.
|
||| Limit a traversal to its first n focuses.
|
||||||
public export
|
public export
|
||||||
taking : Nat -> Traversal s t a a -> Traversal s t a a
|
taking : Nat -> Traversal s t a a -> Traversal s t a a
|
||||||
taking n l = elementsOf l (< n)
|
taking n l = elementsOf l (< n)
|
||||||
|
|
||||||
||| Remove the first `n` focuses from a traversal.
|
||| Remove the first n focuses from a traversal.
|
||||||
public export
|
public export
|
||||||
dropping : Nat -> Traversal s t a a -> Traversal s t a a
|
dropping : Nat -> Traversal s t a a -> Traversal s t a a
|
||||||
dropping n l = elementsOf l (>= n)
|
dropping i l = elementsOf l (>= i)
|
||||||
|
|
|
@ -27,7 +27,7 @@ fromPointer k x (l, r) = l <>> (k,x) :: r
|
||||||
------------------------------------------------------------------------------
|
------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
export infix 9 @>
|
infix 9 @>
|
||||||
|
|
||||||
||| A simple type that represents a layer of the zipper as it moves downwards.
|
||| A simple type that represents a layer of the zipper as it moves downwards.
|
||||||
|||
|
|||
|
||||||
|
|
|
@ -1,51 +0,0 @@
|
||||||
module Data.List1.Lens
|
|
||||||
|
|
||||||
import Data.List1
|
|
||||||
import Data.Profunctor
|
|
||||||
import public Control.Lens
|
|
||||||
import Data.Tuple.Lens
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
||| An isomorphism between a list and its reverse.
|
|
||||||
public export
|
|
||||||
reversed : Iso (List1 a) (List1 b) (List1 a) (List1 b)
|
|
||||||
reversed = iso reverse reverse
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
cons_ : Iso (List1 a) (List1 b) (a, List a) (b, List b)
|
|
||||||
cons_ = iso (\(x:::xs) => (x,xs)) (uncurry (:::))
|
|
||||||
|
|
||||||
public export
|
|
||||||
head_ : Lens' (List1 a) a
|
|
||||||
head_ = cons_ . fst_
|
|
||||||
|
|
||||||
public export
|
|
||||||
tail_ : Lens' (List1 a) (List a)
|
|
||||||
tail_ = cons_ . snd_
|
|
||||||
|
|
||||||
public export
|
|
||||||
snoc_ : Iso (List1 a) (List1 b) (List a, a) (List b, b)
|
|
||||||
snoc_ = iso unsnoc (uncurry lappend . mapSnd singleton)
|
|
||||||
|
|
||||||
public export
|
|
||||||
init_ : Lens' (List1 a) (List a)
|
|
||||||
init_ = snoc_ . fst_
|
|
||||||
|
|
||||||
public export
|
|
||||||
last_ : Lens' (List1 a) a
|
|
||||||
last_ = snoc_ . snd_
|
|
||||||
|
|
||||||
|
|
||||||
public export
|
|
||||||
Ixed Nat a (List1 a) where
|
|
||||||
ix = element
|
|
||||||
|
|
||||||
public export
|
|
||||||
Each (List1 a) (List1 b) a b where
|
|
||||||
each = traversed
|
|
||||||
|
|
||||||
public export
|
|
||||||
Num i => IEach i (List1 a) (List1 b) a b where
|
|
||||||
ieach = itraversed
|
|
|
@ -19,7 +19,7 @@ Just_ = prism Just $ \case
|
||||||
Nothing => Left Nothing
|
Nothing => Left Nothing
|
||||||
Just x => Right x
|
Just x => Right x
|
||||||
|
|
||||||
export infixl 9 .?
|
infixl 9 .?
|
||||||
|
|
||||||
||| The composition `l .? l'` is equivalent to `l . Just_ . l'`.
|
||| The composition `l .? l'` is equivalent to `l . Just_ . l'`.
|
||||||
||| Useful for optics whose focus type is a `Maybe`, such as `at`.
|
||| Useful for optics whose focus type is a `Maybe`, such as `at`.
|
||||||
|
|
|
@ -5,11 +5,6 @@ import public Language.Reflection.Util
|
||||||
|
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
toField : Name -> Name
|
|
||||||
toField (NS ns nm) = NS ns (toField nm)
|
|
||||||
toField (UN (Basic nm)) = UN (Field nm)
|
|
||||||
toField nm = nm
|
|
||||||
|
|
||||||
parameters (o : LensOptions)
|
parameters (o : LensOptions)
|
||||||
lname : Name -> Name
|
lname : Name -> Name
|
||||||
lname n = UN $ Basic (o.fieldName $ nameStr n)
|
lname n = UN $ Basic (o.fieldName $ nameStr n)
|
||||||
|
@ -22,7 +17,7 @@ parameters (o : LensOptions)
|
||||||
|
|
||||||
ldef : BoundArg 0 RegularNamed -> Decl
|
ldef : BoundArg 0 RegularNamed -> Decl
|
||||||
ldef (BA x _ _) =
|
ldef (BA x _ _) =
|
||||||
let fld := toField $ argName x
|
let fld := argName x
|
||||||
nme := lname fld
|
nme := lname fld
|
||||||
u := update [ISetField [nameStr fld] `(y)] `(x)
|
u := update [ISetField [nameStr fld] `(y)] `(x)
|
||||||
in def nme [patClause (var nme) `(lens ~(var fld) $ \x,y => ~(u))]
|
in def nme [patClause (var nme) `(lens ~(var fld) $ \x,y => ~(u))]
|
||||||
|
|
Loading…
Reference in a new issue