Add IEach interface

This commit is contained in:
Kiana Sheibani 2023-10-19 14:57:35 -04:00
parent f2e172678a
commit 451d7b2233
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
7 changed files with 71 additions and 19 deletions

View file

@ -7,6 +7,7 @@ import Control.Lens.Iso
import Control.Lens.Lens
import Control.Lens.Optional
import Control.Lens.Traversal
import Control.Lens.Indexed
%default total
@ -24,6 +25,28 @@ interface Each s t a b | s where
||| containers that do not have a `Traversable` implementation.
each : Traversal s t a b
||| An interface for accessing every element of a container, providing an index.
|||
||| This can be thought of as a generalized version of `itraversed` for
||| containers that do not have a `Traversable` implementation.
public export
interface Each s t a b => IEach i s t a b | s where
||| Access every element of a container at the same time, providing an index.
|||
||| This can be thought of as a generalized version of `itraversed` for
||| containers that do not have a `Traversable` implementation.
ieach : IndexedTraversal i s t a b
public export
[Traversed] Traversable f => Each (f a) (f b) a b where
each = traversed
public export
[Ordinal] Num i => Each s t a b => IEach i s t a b where
ieach = iordinal each
public export
Each (Identity a) (Identity b) a b where

View file

@ -79,3 +79,7 @@ Snoc (List a) (List b) a b where
public export
Each (List a) (List b) a b where
each = traversed
public export
Num i => IEach i (List a) (List b) a b where
ieach = itraversed

View file

@ -79,3 +79,7 @@ Cons (SnocList a) (SnocList b) a b where
public export
Each (SnocList a) (SnocList b) a b where
each = traversed
public export
Num i => IEach i (SnocList a) (SnocList b) a b where
ieach = itraversed

View file

@ -30,3 +30,17 @@ atDep : DecEq k => {0 p : k -> Type} -> (x : k) ->
atDep {p} x = lens (lookupPrecise x) (\m => \case
Nothing => delete x m
Just v => insert x v m)
public export
Each (SortedMap k v) (SortedMap k w) v w where
each = traversed
public export
IEach k (SortedMap k v) (SortedMap k w) v w where
ieach = itraversal func
where
func : Applicative f => (k -> v -> f w) -> SortedMap k v -> f (SortedMap k w)
func f = map (cast {from = SortedDMap k (const w)})
. Dependent.traverse (f %search)
. cast {to = SortedDMap k (const v)}

View file

@ -6,6 +6,11 @@ import public Control.Lens
%default total
public export
each : Fold (SortedSet k) k
each = folding SortedSet.toList
public export
Ixed k () (SortedSet k) where
ix k = optional' (ignore . guard . contains k) const

View file

@ -58,3 +58,7 @@ Snoc String String Char Char where
public export
Each String String Char Char where
each = unpacked . traversed
public export
Num i => IEach i String String Char Char where
ieach = unpacked . itraversed

View file

@ -3,6 +3,7 @@ module Data.Vect.Lens
import Data.Vect
import public Control.Lens
import Data.Tuple.Lens
import Data.Profunctor.Traversing
%default total
@ -15,17 +16,23 @@ reversed = iso reverse reverse
public export
Ixed Nat a (Vect n a) where
ix n = optional' (ixMaybe n) (set n)
where
ixMaybe : forall n. Nat -> Vect n a -> Maybe a
ixMaybe _ [] = Nothing
ixMaybe Z (x :: _) = Just x
ixMaybe (S n) (_ :: xs) = ixMaybe n xs
ix = element
set : forall n. Nat -> Vect n a -> a -> Vect n a
set _ [] _ = []
set Z (_ :: xs) y = y :: xs
set (S n) (x :: xs) y = x :: set n xs y
public export
Ixed' Nat (Fin n) a (Vect n a) where
ix' n = lens (index n) (flip $ replaceAt n)
public export
Each (Vect n a) (Vect n b) a b where
each = traversed
public export
IEach (Fin n) (Vect n a) (Vect n b) a b where
ieach = itraversal func
where
func : forall n. Applicative f => (Fin n -> a -> f b) -> Vect n a -> f (Vect n b)
func f [] = pure []
func f (x :: xs) = [| f FZ x :: func (f . FS) xs |]
public export
@ -51,12 +58,3 @@ init_ = snoc_ . fst_
public export
last_ : Lens' (Vect (S n) a) a
last_ = snoc_ . snd_
public export
Ixed' Nat (Fin n) a (Vect n a) where
ix' n = lens (index n) (flip $ replaceAt n)
public export
Each (Vect n a) (Vect n b) a b where
each = traversed