From 451d7b22333652069f2f7477404456f806056817 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 19 Oct 2023 14:57:35 -0400
Subject: [PATCH] Add IEach interface

---
 src/Control/Lens/Each.idr   | 23 +++++++++++++++++++++++
 src/Data/List/Lens.idr      |  4 ++++
 src/Data/SnocList/Lens.idr  |  4 ++++
 src/Data/SortedMap/Lens.idr | 14 ++++++++++++++
 src/Data/SortedSet/Lens.idr |  5 +++++
 src/Data/String/Lens.idr    |  4 ++++
 src/Data/Vect/Lens.idr      | 36 +++++++++++++++++-------------------
 7 files changed, 71 insertions(+), 19 deletions(-)

diff --git a/src/Control/Lens/Each.idr b/src/Control/Lens/Each.idr
index 3193db4..4919079 100644
--- a/src/Control/Lens/Each.idr
+++ b/src/Control/Lens/Each.idr
@@ -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
diff --git a/src/Data/List/Lens.idr b/src/Data/List/Lens.idr
index c8b9a82..7b39438 100644
--- a/src/Data/List/Lens.idr
+++ b/src/Data/List/Lens.idr
@@ -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
diff --git a/src/Data/SnocList/Lens.idr b/src/Data/SnocList/Lens.idr
index 86961c0..104ab9b 100644
--- a/src/Data/SnocList/Lens.idr
+++ b/src/Data/SnocList/Lens.idr
@@ -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
diff --git a/src/Data/SortedMap/Lens.idr b/src/Data/SortedMap/Lens.idr
index c9c2b9f..9028dae 100644
--- a/src/Data/SortedMap/Lens.idr
+++ b/src/Data/SortedMap/Lens.idr
@@ -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)}
diff --git a/src/Data/SortedSet/Lens.idr b/src/Data/SortedSet/Lens.idr
index e98e23e..dac3a46 100644
--- a/src/Data/SortedSet/Lens.idr
+++ b/src/Data/SortedSet/Lens.idr
@@ -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
diff --git a/src/Data/String/Lens.idr b/src/Data/String/Lens.idr
index 87541b7..d02d01d 100644
--- a/src/Data/String/Lens.idr
+++ b/src/Data/String/Lens.idr
@@ -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
diff --git a/src/Data/Vect/Lens.idr b/src/Data/Vect/Lens.idr
index 9ff08e7..df70777 100644
--- a/src/Data/Vect/Lens.idr
+++ b/src/Data/Vect/Lens.idr
@@ -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