From 783a1efe5e2b8b3c7f91ae7632105e2b0e847273 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 17 Apr 2023 13:27:33 -0400
Subject: [PATCH] Add optics for common types

---
 src/Control/Lens.idr     |  1 +
 src/Control/Lens/At.idr  | 36 +++++++++++++++++++++++++++++
 src/Data/Either/Lens.idr | 16 +++++++++++++
 src/Data/List/Lens.idr   | 50 ++++++++++++++++++++++++++++++++++++++++
 src/Data/Maybe/Lens.idr  | 24 +++++++++++++++++++
 src/Data/Tuple/Lens.idr  | 16 +++++++++++++
 src/Data/Vect/Lens.idr   | 31 +++++++++++++++++++++++++
 7 files changed, 174 insertions(+)
 create mode 100644 src/Control/Lens/At.idr
 create mode 100644 src/Data/Either/Lens.idr
 create mode 100644 src/Data/List/Lens.idr
 create mode 100644 src/Data/Maybe/Lens.idr
 create mode 100644 src/Data/Tuple/Lens.idr
 create mode 100644 src/Data/Vect/Lens.idr

diff --git a/src/Control/Lens.idr b/src/Control/Lens.idr
index 4771382..1f4d7a9 100644
--- a/src/Control/Lens.idr
+++ b/src/Control/Lens.idr
@@ -1,5 +1,6 @@
 module Control.Lens
 
+import public Control.Lens.At
 import public Control.Lens.Equality
 import public Control.Lens.Fold
 import public Control.Lens.Getter
diff --git a/src/Control/Lens/At.idr b/src/Control/Lens/At.idr
new file mode 100644
index 0000000..e7b0ad6
--- /dev/null
+++ b/src/Control/Lens/At.idr
@@ -0,0 +1,36 @@
+module Control.Lens.At
+
+import Control.Lens.Optic
+import Control.Lens.Lens
+import Control.Lens.Optional
+import Control.Lens.Traversal
+import Control.Lens.Setter
+
+%default total
+
+
+public export
+interface Ixed i v a | a where
+  ix : i -> Optional' a v
+
+public export
+[Function] Eq e => Ixed e a (e -> a) where
+  ix k = optional' (Just . ($ k)) (\f,x,k' => if k == k' then x else f k')
+
+
+public export
+interface Ixed i v a => Ixed' i i' v a | a where
+  ix' : i' -> Lens' a v
+
+public export
+[Function'] Eq e => Ixed' e e a (e -> a) using Function where
+  ix' k = lens ($ k) (\f,x,k' => if k == k' then x else f k')
+
+
+public export
+interface Ixed i v a => At i v a | a where
+  at : i -> Lens' a (Maybe v)
+
+public export
+sans : At i v a => i -> a -> a
+sans k = at k .~ Nothing
diff --git a/src/Data/Either/Lens.idr b/src/Data/Either/Lens.idr
new file mode 100644
index 0000000..66e43be
--- /dev/null
+++ b/src/Data/Either/Lens.idr
@@ -0,0 +1,16 @@
+module Data.Either.Lens
+
+import Data.Profunctor
+import public Control.Lens
+
+%default total
+
+
+public export
+Left_ : Prism (Either a c) (Either b c) a b
+Left_ @{MkIsPrism _} = left
+
+public export
+Right_ : Prism (Either c a) (Either c b) a b
+Right_ @{MkIsPrism _} = right
+
diff --git a/src/Data/List/Lens.idr b/src/Data/List/Lens.idr
new file mode 100644
index 0000000..8f9e013
--- /dev/null
+++ b/src/Data/List/Lens.idr
@@ -0,0 +1,50 @@
+module Data.List.Lens
+
+import Data.List
+import Data.Profunctor
+import public Control.Lens
+
+%default total
+
+
+stripPrefix : Eq a => List a -> List a -> Maybe (List a)
+stripPrefix [] ys = Just ys
+stripPrefix (_ :: _) [] = Nothing
+stripPrefix (x :: xs) (y :: ys) = guard (x == y) *> stripPrefix xs ys
+
+stripSuffix : Eq a => List a -> List a -> Maybe (List a)
+stripSuffix qs xs0 = go xs0 zs
+  where
+    drp : List a -> List a -> List a
+    drp (_::ps) (_::xs) = drp ps xs
+    drp [] xs = xs
+    drp _  [] = []
+
+    zs : List a
+    zs = drp qs xs0
+
+    go : List a -> List a -> Maybe (List a)
+    go (_::xs) (_::ys) = go xs ys
+    go xs [] = zipWith const xs0 zs <$ guard (xs == qs)
+    go [] _  = Nothing
+
+
+public export
+prefixed : Eq a => List a -> Prism' (List a) (List a)
+prefixed xs = prism' (xs ++) (stripPrefix xs)
+
+public export
+suffixed : Eq a => List a -> Prism' (List a) (List a)
+suffixed xs = prism' (++ xs) (stripSuffix xs)
+
+
+public export
+reversed : Iso (List a) (List b) (List a) (List b)
+reversed = iso reverse reverse
+
+
+public export
+Ixed Nat a (List a) where
+  ix n = optional' (getAt n) (\xs,x => case inBounds n xs of
+    Yes _ => replaceAt n x xs
+    No _ => xs)
diff --git a/src/Data/Maybe/Lens.idr b/src/Data/Maybe/Lens.idr
new file mode 100644
index 0000000..18f8847
--- /dev/null
+++ b/src/Data/Maybe/Lens.idr
@@ -0,0 +1,24 @@
+module Data.Maybe.Lens
+
+import Data.Maybe
+import Data.Profunctor
+import public Control.Lens
+
+%default total
+
+
+public export
+Nothing_ : Prism' (Maybe a) ()
+Nothing_ = prism' (const Nothing) (guard . isNothing)
+
+public export
+Just_ : Prism (Maybe a) (Maybe b) a b
+Just_ = prism Just $ \case
+  Nothing => Left Nothing
+  Just x => Right x
+
+infixl 9 .?
+
+public export
+(.?) : IsPrism p => Optic' p s t (Maybe a) (Maybe b) -> Optic' p a b a' b' -> Optic' p s t a' b'
+l .? l' = l . Just_ . l'
diff --git a/src/Data/Tuple/Lens.idr b/src/Data/Tuple/Lens.idr
new file mode 100644
index 0000000..20904fe
--- /dev/null
+++ b/src/Data/Tuple/Lens.idr
@@ -0,0 +1,16 @@
+module Data.Tuple.Lens
+
+import Data.Vect
+import Data.Profunctor
+import public Control.Lens
+
+%default total
+
+
+public export
+fst_ : Lens (a, c) (b, c) a b
+fst_ @{MkIsLens _} = first
+
+public export
+snd_ : Lens (c, a) (c, b) a b
+snd_ @{MkIsLens _} = second
diff --git a/src/Data/Vect/Lens.idr b/src/Data/Vect/Lens.idr
new file mode 100644
index 0000000..4116791
--- /dev/null
+++ b/src/Data/Vect/Lens.idr
@@ -0,0 +1,31 @@
+module Data.Vect.Lens
+
+import Data.Vect
+import Control.Lens
+
+%default total
+
+
+public export
+reversed : Iso (Vect n a) (Vect n b) (Vect n a) (Vect n b)
+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
+
+      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)