From e980b3602dee8992498bf09279919776a327302f Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Tue, 25 Apr 2023 12:39:52 -0400
Subject: [PATCH] Strengthen `Cons` and `Snoc` interfaces

---
 src/Control/Lens/Cons.idr | 25 ++++++++++++++++++++++++-
 src/Data/List/Lens.idr    | 22 +++++++++++++++-------
 src/Data/String/Lens.idr  | 19 ++++++++++++++++++-
 3 files changed, 57 insertions(+), 9 deletions(-)

diff --git a/src/Control/Lens/Cons.idr b/src/Control/Lens/Cons.idr
index 3937b27..01e0f02 100644
--- a/src/Control/Lens/Cons.idr
+++ b/src/Control/Lens/Cons.idr
@@ -4,6 +4,7 @@ import Data.Profunctor
 import Control.Lens.Optic
 import Control.Lens.Iso
 import Control.Lens.Prism
+import Control.Lens.Review
 import Control.Lens.Optional
 
 %default total
@@ -13,9 +14,15 @@ import Control.Lens.Optional
 ||| left side of a sequence.
 public export
 interface Cons s t a b | s where
-  ||| This is a prism that can attach or detach a value from the left side of a
+  ||| An isomorphism that can inspact the left side of a sequence.
+  consIso : Iso s t (Maybe (a, s)) (Maybe (b, t))
+
+  ||| A prism that can attach or detach a value from the left side of a
   ||| sequence.
   cons_ : Prism s t (a, s) (b, t)
+  cons_ = consIso . prism Just (\case
+    Nothing => Left Nothing
+    Just x => Right x)
 
 ||| Access the head (left-most element) of a sequence, if it is non-empty.
 public export
@@ -28,14 +35,25 @@ public export
 tail_ : Cons s s a a => Optional' s s
 tail_ @{_} @{MkIsOptional _} = cons_ . second
 
+||| Use a `Cons` implementation to construct an empty sequence.
+public export
+nil : Cons s s a a => s
+nil = review consIso Nothing
+
 
 ||| An interface that provides a way to detach and inspect elements from the
 ||| right side of a sequence.
 public export
 interface Snoc s t a b | s where
+  ||| An isomorphism that can inspact the right side of a sequence.
+  snocIso : Iso s t (Maybe (s, a)) (Maybe (t, b))
+
   ||| This is a prism that can attach or detach a value from the right side of a
   ||| sequence.
   snoc_ : Prism s t (s, a) (t, b)
+  snoc_ = snocIso . prism Just (\case
+    Nothing => Left Nothing
+    Just x => Right x)
 
 ||| Access all but the right-most element of a sequence, if it is non-empty.
 public export
@@ -46,3 +64,8 @@ init_ @{_} @{MkIsOptional _} = snoc_ . first
 public export
 last_ : Snoc s s a a => Optional' s a
 last_ @{_} @{MkIsOptional _} = snoc_ . second
+
+||| Use a `Snoc` implementation to construct an empty sequence.
+public export
+nil' : Snoc s s a a => s
+nil' = review snocIso Nothing
diff --git a/src/Data/List/Lens.idr b/src/Data/List/Lens.idr
index e17e632..483c95c 100644
--- a/src/Data/List/Lens.idr
+++ b/src/Data/List/Lens.idr
@@ -48,22 +48,30 @@ 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)
+  ix = element
 
 public export
 Cons (List a) (List b) a b where
+  consIso = iso (\case
+      [] => Nothing
+      x :: xs => Just (x,xs))
+    (maybe [] $ uncurry (::))
+
   cons_ = prism (uncurry (::)) (\case
     [] => Left []
     x :: xs => Right (x, xs))
 
+unsnoc : a -> List a -> (List a, a)
+unsnoc x [] = ([], x)
+unsnoc x (y :: xs) = mapFst (x ::) $ unsnoc y xs
+
 public export
 Snoc (List a) (List b) a b where
+  snocIso = iso (\case
+      [] => Nothing
+      x :: xs => Just $ unsnoc x xs)
+    (maybe [] $ uncurry snoc)
+
   snoc_ = prism (uncurry snoc) (\case
     [] => Left []
     x :: xs => Right $ unsnoc x xs)
-    where
-      unsnoc : a -> List a -> (List a, a)
-      unsnoc x [] = ([], x)
-      unsnoc x (y :: xs) = mapFst (x ::) $ unsnoc y xs
diff --git a/src/Data/String/Lens.idr b/src/Data/String/Lens.idr
index 9375427..ee4aaf1 100644
--- a/src/Data/String/Lens.idr
+++ b/src/Data/String/Lens.idr
@@ -26,6 +26,11 @@ public export
 packed : Iso' (List Char) String
 packed = iso pack unpack
 
+||| An isomorphism between a string and its reverse.
+public export
+reversed : Iso' String String
+reversed = involuted reverse
+
 
 public export
 Ixed Nat Char String where
@@ -33,8 +38,20 @@ Ixed Nat Char String where
 
 public export
 Cons String String Char Char where
+  consIso = iso strUncons (maybe "" $ uncurry strCons)
   cons_ = prism' (uncurry strCons) strUncons
 
+snoc : String -> Char -> String
+snoc s c = s ++ singleton c
+
+unsnoc : String -> Maybe (String, Char)
+unsnoc s =
+  case length s of
+    Z => Nothing
+    (S n) => Just (substr Z n s,
+                    assert_total $ strIndex s (cast n))
+
 public export
 Snoc String String Char Char where
-  snoc_ = unpacked . snoc_ . mappingFst packed
+  snocIso = iso unsnoc (maybe "" $ uncurry snoc)
+  snoc_ = prism' (uncurry snoc) unsnoc