diff --git a/src/Control/Lens.idr b/src/Control/Lens.idr index 1f4d7a9..5ddce24 100644 --- a/src/Control/Lens.idr +++ b/src/Control/Lens.idr @@ -4,6 +4,7 @@ import public Control.Lens.At import public Control.Lens.Equality import public Control.Lens.Fold import public Control.Lens.Getter +import public Control.Lens.Indexed import public Control.Lens.Iso import public Control.Lens.Lens import public Control.Lens.Optic diff --git a/src/Control/Lens/Fold.idr b/src/Control/Lens/Fold.idr index a23a31b..1d3a6bf 100644 --- a/src/Control/Lens/Fold.idr +++ b/src/Control/Lens/Fold.idr @@ -6,6 +6,7 @@ import Data.Profunctor.Costrong import Data.Profunctor.Traversing import Control.Applicative.Backwards import Control.Lens.Optic +import Control.Lens.Indexed import Control.Lens.OptionalFold import Control.Lens.Traversal @@ -39,7 +40,11 @@ foldToTraversal @{MkIsFold _} = MkIsTraversal %search ||| `Fold s a` is equivalent to `s -> List a`. public export 0 Fold : (s,a : Type) -> Type -Fold s a = Optic IsFold s s a a +Fold = Simple (Optic IsFold) + +public export +0 IndexedFold : (i,s,a : Type) -> Type +IndexedFold = Simple . IndexedOptic IsFold ------------------------------------------------------------------------------ @@ -68,6 +73,12 @@ public export folding : Foldable f => (s -> f a) -> Fold s a folding @{_} f @{MkIsFold _} = rphantom . contramapFst f . wander traverse_ +public export +ifolding : Foldable f => (s -> f (i, a)) -> IndexedFold i s a +ifolding @{_} f @{MkIsFold _} @{ind} = + rphantom . contramapFst f . wander traverse_ . indexed @{ind} + + ||| Reverse the order of a fold's focuses. public export backwards : Fold s a -> Fold s a @@ -98,18 +109,30 @@ public export foldMapOf : Monoid m => Fold s a -> (a -> m) -> s -> m foldMapOf l = runForget . l . MkForget +public export +ifoldMapOf : Monoid m => IndexedFold i s a -> (i -> a -> m) -> s -> m +ifoldMapOf l = runForget . l @{%search} @{Idxed} . MkForget . uncurry + ||| Combine the focuses of an optic using the provided function, starting from ||| the right. public export foldrOf : Fold s a -> (a -> acc -> acc) -> acc -> s -> acc foldrOf l = flip . foldMapOf @{MkMonoid @{MkSemigroup (.)} id} l +public export +ifoldrOf : IndexedFold i s a -> (i -> a -> acc -> acc) -> acc -> s -> acc +ifoldrOf l = flip . ifoldMapOf @{MkMonoid @{MkSemigroup (.)} id} l + ||| Combine the focuses of an optic using the provided function, starting from ||| the left. public export foldlOf : Fold s a -> (acc -> a -> acc) -> acc -> s -> acc foldlOf l = flip . foldMapOf @{MkMonoid @{MkSemigroup $ flip (.)} id} l . flip +public export +ifoldlOf : IndexedFold i s a -> (i -> acc -> a -> acc) -> acc -> s -> acc +ifoldlOf l = flip . ifoldMapOf @{MkMonoid @{MkSemigroup $ flip (.)} id} l . (flip .) + ||| Combine each focus value of an optic using a monoid structure. public export concatOf : Monoid m => Fold s m -> s -> m @@ -135,11 +158,21 @@ traverseOf_ l f = let _ = MkMonoid @{MkSemigroup (*>)} (pure ()) in foldMapOf l (ignore . f) +public export +itraverseOf_ : Applicative f => IndexedFold i s a -> (i -> a -> f b) -> s -> f () +itraverseOf_ l f = + let _ = MkMonoid @{MkSemigroup (*>)} (pure ()) + in ifoldMapOf l (ignore .: f) + ||| A version of `traverseOf_` with the arguments flipped. public export forOf_ : Applicative f => Fold s a -> s -> (a -> f b) -> f () forOf_ = flip . traverseOf_ +public export +iforOf_ : Applicative f => IndexedFold i s a -> s -> (i -> a -> f b) -> f () +iforOf_ = flip . itraverseOf_ + ||| The conjunction of an optic containing lazy boolean values. public export andOf : Fold s (Lazy Bool) -> s -> Bool @@ -179,12 +212,22 @@ public export firstOf : Fold s a -> s -> Maybe a firstOf l = foldMapOf l Just +public export +ifirstOf : IndexedFold i s a -> s -> Maybe (i, a) +ifirstOf l = runForget $ l @{%search} @{Idxed} $ MkForget Just + ||| Access the last focus value of an optic, returning `Nothing` if there are ||| no focuses. public export lastOf : Fold s a -> s -> Maybe a lastOf l = foldMapOf @{MkMonoid @{MkSemigroup $ flip (<+>)} neutral} l Just +public export +ilastOf : IndexedFold i s a -> s -> Maybe (i, a) +ilastOf l = + let _ = MkMonoid @{MkSemigroup $ flip (<+>)} neutral + in runForget $ l @{%search} @{Idxed} $ MkForget Just + ------------------------------------------------------------------------------ @@ -225,7 +268,18 @@ infixl 8 ^? ||| This is the operator form of `preview`. public export (^?) : s -> Fold s a -> Maybe a -(^?) s l = preview l s +(^?) x l = preview l x + + +public export +ipreview : IndexedFold i s a -> s -> Maybe (i, a) +ipreview = ifirstOf + +infixl 8 ^@? + +public export +(^@?) : s -> IndexedFold i s a -> Maybe (i, a) +(^@?) x l = ipreview l x ||| Convert a `Fold` into an `OptionalFold` that accesses the first focus element. @@ -235,6 +289,10 @@ public export pre : Fold s a -> OptionalFold s a pre = folding . preview +public export +ipre : IndexedFold i s a -> IndexedOptionalFold i s a +ipre = ifolding . ipreview + ||| Return a list of all focuses of a fold. public export @@ -249,3 +307,14 @@ infixl 8 ^.. public export (^..) : s -> Fold s a -> List a (^..) s l = toListOf l s + + +public export +itoListOf : IndexedFold i s a -> s -> List (i, a) +itoListOf l = ifoldrOf l ((::) .: (,)) [] + +infixl 8 ^@.. + +public export +(^@..) : s -> IndexedFold i s a -> List (i, a) +(^@..) x l = itoListOf l x diff --git a/src/Control/Lens/Getter.idr b/src/Control/Lens/Getter.idr index e498498..7f1a678 100644 --- a/src/Control/Lens/Getter.idr +++ b/src/Control/Lens/Getter.idr @@ -4,6 +4,7 @@ import Data.Bicontravariant import Data.Profunctor import Data.Profunctor.Costrong import Control.Lens.Optic +import Control.Lens.Indexed import Control.Lens.Lens %default total @@ -31,6 +32,10 @@ public export 0 Getter : (s,a : Type) -> Type Getter = Simple (Optic IsGetter) +public export +0 IndexedGetter : (i,s,a : Type) -> Type +IndexedGetter = Simple . IndexedOptic IsGetter + ------------------------------------------------------------------------------ -- Utilities for getters @@ -42,6 +47,10 @@ public export to : (s -> a) -> Getter s a to f @{MkIsGetter _} = lmap f . rphantom +public export +ito : (s -> (i, a)) -> IndexedGetter i s a +ito f @{MkIsGetter _} @{ind} = lmap f . rphantom . indexed @{ind} + ||| Construct a getter that always returns a constant value. public export like : a -> Getter s a @@ -50,7 +59,7 @@ like = to . const ||| Access the value of an optic and apply a function to it, returning the result. public export -views : Getter s a -> (a -> r) -> (s -> r) +views : Getter s a -> (a -> r) -> s -> r views l = runForget . l . MkForget ||| Access the focus value of an optic, particularly a `Getter`. @@ -58,8 +67,17 @@ public export view : Getter s a -> s -> a view l = views l id +public export +iviews : IndexedGetter i s a -> (i -> a -> r) -> s -> r +iviews l = runForget . l @{%search} @{Idxed} . MkForget . uncurry + +public export +iview : IndexedGetter i s a -> s -> (i, a) +iview l = runForget $ l @{%search} @{Idxed} $ MkForget id + infixl 8 ^. +infixl 8 ^@. ||| Access the focus value of an optic, particularly a `Getter`. ||| @@ -67,3 +85,7 @@ infixl 8 ^. public export (^.) : s -> Getter s a -> a (^.) x l = view l x + +public export +(^@.) : s -> IndexedGetter i s a -> (i, a) +(^@.) x l = iview l x diff --git a/src/Control/Lens/Indexed.idr b/src/Control/Lens/Indexed.idr new file mode 100644 index 0000000..813837c --- /dev/null +++ b/src/Control/Lens/Indexed.idr @@ -0,0 +1,33 @@ +module Control.Lens.Indexed + +import Data.Profunctor +import Control.Lens.Optic +import Control.Lens.Iso + +%default total + + +public export +interface Indexable i (0 p, p' : Type -> Type -> Type) | p, p' where + indexed : p' a b -> p (i, a) b + + +-- Non-indexed use (default) +public export +IsIso p => Indexable i p p where + indexed @{MkIsIso _} = lmap snd + +-- Indexed use +public export +[Idxed] Indexable i p (p . (i,)) where + indexed = id + + +public export +0 IndexedOptic' : (Type -> Type -> Type) -> (i,s,t,a,b : Type) -> Type +IndexedOptic' p i s t a b = forall p'. Indexable i p p' => p' a b -> p s t + +public export +0 IndexedOptic : ((Type -> Type -> Type) -> Type) -> (i,s,t,a,b : Type) -> Type +IndexedOptic constr i s t a b = + forall p,p'. constr p => Indexable i p p' => p' a b -> p s t diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr index 6bd158d..2a4bfb7 100644 --- a/src/Control/Lens/Lens.idr +++ b/src/Control/Lens/Lens.idr @@ -4,6 +4,7 @@ import Data.Profunctor import Data.Profunctor.Yoneda import Control.Monad.State import Control.Lens.Optic +import Control.Lens.Indexed import Control.Lens.Equality import Control.Lens.Iso @@ -48,6 +49,14 @@ public export 0 Lens' : (s,a : Type) -> Type Lens' = Simple Lens +public export +0 IndexedLens : (i,s,t,a,b : Type) -> Type +IndexedLens = IndexedOptic IsLens + +public export +0 IndexedLens' : (i,s,a : Type) -> Type +IndexedLens' = Simple . IndexedLens + ------------------------------------------------------------------------------ -- Utilities for lenses @@ -63,6 +72,16 @@ public export lens : (get : s -> a) -> (set : s -> b -> t) -> Lens s t a b lens get set @{MkIsLens _} = dimap (\x => (x, get x)) (uncurry set) . second +public export +ilens : (get : s -> (i, a)) -> (set : s -> b -> t) -> IndexedLens i s t a b +ilens get set @{_} @{ind} = lens get set . indexed @{ind} + + +public export +withIndex : i -> Lens s t a b -> IndexedLens i s t a b +withIndex i l @{MkIsLens _} @{ind} = l . lmap (i,) . indexed @{ind} + + ||| Extract getter and setter functions from a lens. public export getLens : Lens s t a b -> (s -> a, s -> b -> t) @@ -83,8 +102,8 @@ withLens l f = uncurry f (getLens l) ||| `Void` vacuously "contains" a value of any other type. public export -devoid : Lens Void Void a b -devoid @{MkIsLens _} = dimap absurd snd . first +devoid : IndexedLens i Void Void a b +devoid @{MkIsLens _} = ilens absurd const ||| All values contain a unit. public export @@ -114,18 +133,19 @@ fusing @{MkIsIso _} l = proextract . l . propure -- Operators ------------------------------------------------------------------------------ -infixr 4 %%~; infix 4 %%= +infixr 4 %%~; infix 4 %%=; infix 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 <= infixr 2 <<~ @@ -139,12 +159,26 @@ public export (%%=) : MonadState s m => Lens s s a b -> (a -> (r, b)) -> m r (%%=) = (state . (swap .)) .: (%%~) +public export +(%%@~) : Functor f => IndexedLens i s t a b -> (i -> a -> f b) -> s -> f t +(%%@~) l = applyStar . l {p=Star f} @{%search} @{Idxed} + . MkStar . uncurry + +public export +(%%@=) : MonadState s m => IndexedLens i s s a b -> (i -> 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 +||| Modify a value with pass-through, having access to the index. +public export +(<%@~) : IndexedLens i s t a b -> (i -> 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) @@ -195,6 +229,10 @@ public export (<<%~) : Lens s t a b -> (a -> b) -> s -> (a, t) (<<%~) l f = l %%~ (\x => (x, f x)) +||| Modify the value of an indexed lens and return the old value. +(<<%@~) : IndexedLens i s t a b -> (i -> a -> b) -> s -> (a, t) +(<<%@~) l f = l %%@~ (\i,x => (x, f i x)) + ||| Set the value of a lens and return the old value. public export (<<.~) : Lens s t a b -> b -> s -> (a, t) @@ -256,6 +294,11 @@ public export (<%=) : MonadState s m => Lens s s a b -> (a -> b) -> m b (<%=) = (state . (swap .)) .: (<%~) +||| Modify within a state monad with pass-through, having access to the index. +public export +(<%@=) : MonadState s m => IndexedLens i s s a b -> (i -> 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 @@ -297,6 +340,11 @@ public export (<<%=) : MonadState s m => Lens s s a b -> (a -> b) -> m a (<<%=) = (state . (swap .)) .: (<<%~) +||| Modify the value of an indexed lens into state and return the old value. +public export +(<<%@=) : MonadState s m => IndexedLens i s s a b -> (i -> 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 diff --git a/src/Control/Lens/Optic.idr b/src/Control/Lens/Optic.idr index 3947389..ee44137 100644 --- a/src/Control/Lens/Optic.idr +++ b/src/Control/Lens/Optic.idr @@ -1,5 +1,6 @@ module Control.Lens.Optic +import Data.Tensor import Data.Profunctor %default total @@ -17,3 +18,4 @@ Optic' p s t a b = p a b -> p s t public export 0 Optic : ((Type -> Type -> Type) -> Type) -> (s,t,a,b : Type) -> Type Optic constr s t a b = forall p. constr p => Optic' p s t a b + diff --git a/src/Control/Lens/Optional.idr b/src/Control/Lens/Optional.idr index c9ddb69..79caccb 100644 --- a/src/Control/Lens/Optional.idr +++ b/src/Control/Lens/Optional.idr @@ -2,6 +2,7 @@ module Control.Lens.Optional import Data.Profunctor import Control.Lens.Optic +import Control.Lens.Indexed import Control.Lens.Lens import Control.Lens.Prism @@ -38,6 +39,14 @@ public export 0 Optional' : (s,a : Type) -> Type Optional' = Simple Optional +public export +0 IndexedOptional : (i,s,t,a,b : Type) -> Type +IndexedOptional = IndexedOptic IsOptional + +public export +0 IndexedOptional' : (i,s,a : Type) -> Type +IndexedOptional' = Simple . IndexedOptional + ------------------------------------------------------------------------------ -- Utilities for Optionals @@ -61,10 +70,19 @@ public export optional' : (s -> Maybe a) -> (s -> b -> s) -> Optional s s a b optional' prj = optional (\x => maybe (Left x) Right (prj x)) +public export +ioptional : (s -> Either t (i, a)) -> (s -> b -> t) -> IndexedOptional i s t a b +ioptional prj set @{_} @{ind} = optional prj set . indexed @{ind} + +public export +ioptional' : (s -> Maybe (i, a)) -> (s -> b -> s) -> IndexedOptional i s s a b +ioptional' prj = ioptional (\x => maybe (Left x) Right (prj x)) + + ||| The trivial optic that has no focuses. public export -ignored : Optional s s a b -ignored = optional' (const Nothing) const +ignored : IndexedOptional i s s a b +ignored = ioptional' (const Nothing) const ||| Extract projection and setter functions from an optional. @@ -93,5 +111,5 @@ withOptional l f = uncurry f (getOptional l) ||| Retrieve the focus value of an optional, or allow its type to change if there ||| is no focus. public export -matching : Prism s t a b -> s -> Either t a -matching = snd . getPrism +matching : Optional s t a b -> s -> Either t a +matching = fst . getOptional diff --git a/src/Control/Lens/OptionalFold.idr b/src/Control/Lens/OptionalFold.idr index 3e599c5..13858f6 100644 --- a/src/Control/Lens/OptionalFold.idr +++ b/src/Control/Lens/OptionalFold.idr @@ -4,6 +4,7 @@ import Data.Bicontravariant import Data.Profunctor import Data.Profunctor.Costrong import Control.Lens.Optic +import Control.Lens.Indexed import Control.Lens.Optional import Control.Lens.Getter @@ -35,6 +36,10 @@ public export 0 OptionalFold : (s,a : Type) -> Type OptionalFold = Simple (Optic IsOptFold) +public export +0 IndexedOptionalFold : (i,s,a : Type) -> Type +IndexedOptionalFold = Simple . IndexedOptic IsOptFold + ------------------------------------------------------------------------------ -- Utilities for OptionalFolds @@ -47,6 +52,12 @@ folding : (s -> Maybe a) -> OptionalFold s a folding f @{MkIsOptFold _} = contrabimap (\x => maybe (Left x) Right (f x)) Left . right +public export +ifolding : (s -> Maybe (i, a)) -> IndexedOptionalFold i s a +ifolding f @{MkIsOptFold _} @{ind} = + contrabimap (\x => maybe (Left x) Right (f x)) Left . right . indexed @{ind} + + ||| Construct an `OptionalFold` that can be used to filter the focuses ||| of another optic. ||| diff --git a/src/Control/Lens/Prism.idr b/src/Control/Lens/Prism.idr index 7228e88..5a5980b 100644 --- a/src/Control/Lens/Prism.idr +++ b/src/Control/Lens/Prism.idr @@ -2,6 +2,7 @@ module Control.Lens.Prism import Data.Profunctor import Control.Lens.Optic +import Control.Lens.Indexed import Control.Lens.Iso %default total @@ -37,6 +38,14 @@ public export 0 Prism' : (s,a : Type) -> Type Prism' = Simple Prism +public export +0 IndexedPrism : (i,s,t,a,b : Type) -> Type +IndexedPrism = IndexedOptic IsPrism + +public export +0 IndexedPrism' : (i,s,a : Type) -> Type +IndexedPrism' = Simple . IndexedPrism + ------------------------------------------------------------------------------ -- Utilities for prisms @@ -53,6 +62,14 @@ public export prism' : (b -> s) -> (s -> Maybe a) -> Prism s s a b prism' inj prj = prism inj (\x => maybe (Left x) Right (prj x)) +public export +iprism : (b -> t) -> (s -> Either t (i, a)) -> IndexedPrism i s t a b +iprism inj prj @{_} @{ind} = prism inj prj . indexed @{ind} + +public export +iprism' : (b -> s) -> (s -> Maybe (i, a)) -> IndexedPrism i s s a b +iprism' inj prj = iprism inj (\x => maybe (Left x) Right (prj x)) + ||| Extract injection and projection functions from a prism. public export diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr index ed63e73..d63d74e 100644 --- a/src/Control/Lens/Setter.idr +++ b/src/Control/Lens/Setter.idr @@ -7,6 +7,7 @@ import Data.Profunctor.Traversing import Data.Profunctor.Mapping import Control.Monad.State import Control.Lens.Optic +import Control.Lens.Indexed import Control.Lens.Traversal %default total @@ -44,6 +45,14 @@ public export 0 Setter' : (s,a : Type) -> Type Setter' = Simple Setter +public export +0 IndexedSetter : (i,s,t,a,b : Type) -> Type +IndexedSetter = IndexedOptic IsSetter + +public export +0 IndexedSetter' : (i,s,a : Type) -> Type +IndexedSetter' = Simple . IndexedSetter + ------------------------------------------------------------------------------ -- Utilities for setters @@ -55,6 +64,10 @@ public export sets : ((a -> b) -> s -> t) -> Setter s t a b sets f @{MkIsSetter _} = roam f +public export +isets : ((i -> a -> b) -> s -> t) -> IndexedSetter i s t a b +isets f @{MkIsSetter _} @{ind} = roam (f . curry) . indexed @{ind} + ||| Derive a setter from a `Functor` implementation. public export mapped : Functor f => Setter (f a) (f b) a b @@ -81,6 +94,17 @@ public export (%~) = over +public export +iover : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t +iover l = l @{MkIsSetter Function} @{Idxed} . uncurry + +infixr 4 %@~ + +public export +(%@~) : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t +(%@~) = iover + + ||| Set the focus or focuses of an optic to a constant value. public export set : Setter s t a b -> b -> s -> t @@ -96,15 +120,27 @@ public export (.~) = set +public export +iset : IndexedSetter i s t a b -> (i -> b) -> s -> t +iset l = iover l . (const .) + +infix 4 .@~ + +public export +(.@~) : IndexedSetter i s t a b -> (i -> b) -> s -> t +(.@~) = iset + + ------------------------------------------------------------------------------ --- Operators +-- More operators ------------------------------------------------------------------------------ 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 = infixr 4 <~ @@ -175,11 +211,19 @@ public export (%=) : MonadState s m => Setter s s a b -> (a -> b) -> m () (%=) = modify .: over +public export +(%@=) : MonadState s m => IndexedSetter i s s a b -> (i -> a -> b) -> m () +(%@=) = modify .: iover + ||| Set the focus of an optic within a state monad. public export (.=) : MonadState s m => Setter s s a b -> b -> m () (.=) = modify .: set +public export +(.@=) : MonadState s m => IndexedSetter i s s a b -> (i -> b) -> m () +(.@=) = modify .: iset + ||| 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 () diff --git a/src/Control/Lens/Traversal.idr b/src/Control/Lens/Traversal.idr index 72287a6..112a658 100644 --- a/src/Control/Lens/Traversal.idr +++ b/src/Control/Lens/Traversal.idr @@ -1,12 +1,13 @@ module Control.Lens.Traversal import Control.Monad.State -import Data.Zippable +import Data.List import Data.Profunctor import Data.Profunctor.Traversing import Control.Applicative.Backwards import Control.Applicative.Indexing import Control.Lens.Optic +import Control.Lens.Indexed import Control.Lens.Optional import Control.Lens.Lens import Control.Lens.Prism @@ -39,17 +40,37 @@ public export 0 Traversal' : (s,a : Type) -> Type Traversal' = Simple Traversal +public export +0 IndexedTraversal : (i,s,t,a,b : Type) -> Type +IndexedTraversal = IndexedOptic IsTraversal + +public export +0 IndexedTraversal' : (i,s,a : Type) -> Type +IndexedTraversal' = Simple . IndexedTraversal + ------------------------------------------------------------------------------ -- Utilities for traversals ------------------------------------------------------------------------------ +public export +iordinal : Traversal s t a b -> IndexedTraversal Nat s t a b +iordinal l @{MkIsTraversal _} @{ind} = wander (func . curry) . indexed @{ind} + where + func : forall f. Applicative f => (Nat -> a -> f b) -> s -> f t + func = indexing $ applyStar . l . MkStar {f = Indexing f} + + ||| Derive a traversal from a `Traversable` implementation. public export traversed : Traversable t => Traversal (t a) (t b) a b traversed @{_} @{MkIsTraversal _} = traverse' +public export +itraversed : Traversable t => IndexedTraversal Nat (t a) (t b) a b +itraversed = iordinal traversed + ||| Contstruct a traversal over a `Bitraversable` container with matching types. public export both : Bitraversable t => Traversal (t a a) (t b b) a b @@ -71,10 +92,18 @@ public export traverseOf : Applicative f => Traversal s t a b -> (a -> f b) -> s -> f t traverseOf l = applyStar . l . MkStar {f} +public export +itraverseOf : Applicative f => IndexedTraversal i s t a b -> (i -> a -> f b) -> s -> f t +itraverseOf l = traverseOf (l @{%search} @{Idxed}) . uncurry + ||| A version of `traverseOf` but with the arguments flipped. public export forOf : Applicative f => Traversal s t a b -> s -> (a -> f b) -> f t -forOf l = flip $ traverseOf l +forOf = flip . traverseOf + +public export +iforOf : Applicative f => IndexedTraversal i s t a b -> s -> (i -> a -> f b) -> f t +iforOf = flip . itraverseOf ||| Evaluate each computation within the traversal and collect the results. public export @@ -128,6 +157,16 @@ failover l f x = (b, y) = traverseOf l ((True,) . f) x in guard b $> y +public export +ifailover : Alternative f => IndexedTraversal i s t a b -> (i -> a -> b) -> s -> f t +ifailover l = failover (l @{%search} @{Idxed}) . uncurry + + +partsOf_update : a -> State (List a) a +partsOf_update x = get >>= \case + x' :: xs' => put xs' >> pure x' + [] => pure x + ||| 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 @@ -136,12 +175,12 @@ failover l f x = 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 + (flip evalState . traverseOf l partsOf_update) + +public export +ipartsOf : IndexedTraversal i s t a a -> IndexedLens (List i) s t (List a) (List a) +ipartsOf l = ilens (unzip . (runForget $ l @{%search} @{Idxed} $ MkForget pure)) + (flip evalState . itraverseOf l (const partsOf_update)) ||| Construct an optional that focuses on the first value of a traversal. diff --git a/src/Data/Either/Lens.idr b/src/Data/Either/Lens.idr index 66e43be..81ca516 100644 --- a/src/Data/Either/Lens.idr +++ b/src/Data/Either/Lens.idr @@ -14,3 +14,13 @@ public export Right_ : Prism (Either c a) (Either c b) a b Right_ @{MkIsPrism _} = right + +public export +chosen : IndexedLens (Either () ()) (Either a a) (Either b b) a b +chosen = ilens + (\case + Left x => (Left (), x) + Right x => (Right (), x)) + (\case + Left _ => Left + Right _ => Right) diff --git a/src/Data/Tuple/Lens.idr b/src/Data/Tuple/Lens.idr index 20904fe..a3cfcf1 100644 --- a/src/Data/Tuple/Lens.idr +++ b/src/Data/Tuple/Lens.idr @@ -14,3 +14,12 @@ fst_ @{MkIsLens _} = first public export snd_ : Lens (c, a) (c, b) a b snd_ @{MkIsLens _} = second + + +public export +ifst_ : IndexedLens i (a, i) (b, i) a b +ifst_ = ilens swap (flip $ mapFst . const) + +public export +isnd_ : IndexedLens i (i, a) (i, b) a b +isnd_ = ilens id (flip $ mapSnd . const)