Compare commits

..

10 commits

Author SHA1 Message Date
Kiana Sheibani da8f3a05e6
Fix typo 2024-06-29 01:55:20 -04:00
Kiana Sheibani 60231f4a2b
Add export declaration to fixities 2024-06-29 01:55:19 -04:00
Kiana Sheibani 6d7153496d
Merge pull request #2 from crumbtoo/main
Use postfix field projections in elab script
2024-06-28 21:00:42 -04:00
Madeleine Sydney 61acb58a22 Derive lenses without prefix_record_projections 2024-06-27 20:38:43 -06:00
Kiana Sheibani 253467ebae
Fix definition of elemOf 2024-01-29 21:44:54 -05:00
Kiana Sheibani a7152cd582
Combine fixity declarations
Apparently this is something you can do? I wasn't aware of it,
but it's very useful!
2023-11-04 20:58:54 -04:00
Kiana Sheibani 1e6309237b
Update lens operators 2023-10-19 20:22:23 -04:00
Kiana Sheibani 40fd0a3a3b
Add lenses for List1 2023-10-19 19:57:39 -04:00
Kiana Sheibani aabe5a94d0
Update version to 0.3.0 2023-10-19 16:23:53 -04:00
Kiana Sheibani d2ebddeab7
Update README 2023-10-19 16:23:05 -04:00
14 changed files with 105 additions and 63 deletions

View file

@ -3,10 +3,14 @@
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*.
Eventually, this library will also include elaboration scripts to automatically ## Comparison to Monocle
generate lenses for a particular datatype.
## Comparisons [Monocle](https://github.com/stefan-hoeck/idris2-monocle) is another Idris 2 library
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),
@ -46,3 +50,7 @@ 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.

View file

@ -1,5 +1,5 @@
package lens package lens
version = 0.2.0 version = 0.3.0
brief = "Batteries-included profunctor optics" brief = "Batteries-included profunctor optics"

View file

@ -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
||| An lens that infallibly accesses a value at a given index of a container. ||| A 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'`.

View file

@ -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 = allOf l . (==) elemOf l = anyOf 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
infixl 8 ^? export 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,8 +306,6 @@ 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.
||| |||
@ -338,8 +336,6 @@ 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`.
@ -353,8 +349,6 @@ 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`.

View file

@ -85,8 +85,7 @@ iview : IndexedGetter i s a -> s -> (i, a)
iview l = runForget $ l @{%search} @{Idxed} $ MkForget id iview l = runForget $ l @{%search} @{Idxed} $ MkForget id
infixl 8 ^. export infixl 8 ^., ^@.
infixl 8 ^@.
||| Access the focus value of an optic, particularly a `Getter`. ||| Access the focus value of an optic, particularly a `Getter`.
||| |||

View file

@ -93,9 +93,7 @@ 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}
infixr 9 <.> export 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.
||| |||

View file

@ -139,22 +139,15 @@ fusing @{MkIsIso _} l = proextract . l . propure
-- Operators -- Operators
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
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 infixr 4 <<%~, <<%@~, <<.~, <<?~, <<+~, <<*~, <<-~, <</~, <<||~, <<&&~, <<<+>~
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 <<<+>~
infix 4 <%=; infix 4 <%@=; infix 4 <+=; infix 4 <*=; infix 4 <-=; infix 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 <<<+>=
infixr 2 <<~
public export public export
@ -403,11 +396,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

View file

@ -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
infixr 8 ^$ export 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`.

View file

@ -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}
infixr 4 %~ export infixr 4 %~, %@~, .~, .@~
||| Modify the focus or focuses of an optic. ||| Modify the focus or focuses of an optic.
||| |||
@ -106,8 +106,6 @@ 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`.
@ -121,8 +119,6 @@ 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`.
@ -136,8 +132,6 @@ 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`.
@ -150,13 +144,9 @@ public export
-- More operators -- More operators
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
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 %=, %@=, .=, .@=, ?=, <.=, <?=, +=, *=, -=, //=, ||=, &&=, <+>=
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
@ -247,12 +237,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) >> pure x (<.=) l x = (l .= x) $> 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) >> pure x (<?=) l x = (l ?= x) $> 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
@ -303,4 +293,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

View file

@ -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' >> pure x' x' :: xs' => put xs' $> 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 i l = elementsOf l (>= i) dropping n l = elementsOf l (>= n)

View file

@ -27,7 +27,7 @@ fromPointer k x (l, r) = l <>> (k,x) :: r
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
infix 9 @> export 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.
||| |||

51
src/Data/List1/Lens.idr Normal file
View file

@ -0,0 +1,51 @@
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

View file

@ -19,7 +19,7 @@ Just_ = prism Just $ \case
Nothing => Left Nothing Nothing => Left Nothing
Just x => Right x Just x => Right x
infixl 9 .? export 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`.

View file

@ -5,6 +5,11 @@ 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)
@ -17,7 +22,7 @@ parameters (o : LensOptions)
ldef : BoundArg 0 RegularNamed -> Decl ldef : BoundArg 0 RegularNamed -> Decl
ldef (BA x _ _) = ldef (BA x _ _) =
let fld := argName x let fld := toField $ 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))]