Define cons and snoc optics

src/Control/Lens.idr

@@ -1,6 +1,7 @@
 module Control.Lens
 
 import public Control.Lens.At
+import public Control.Lens.Cons
 import public Control.Lens.Equality
 import public Control.Lens.Fold
 import public Control.Lens.Getter

src/Control/Lens/Cons.idr

@@ -0,0 +1,36 @@
+module Control.Lens.Cons
+
+import Data.Profunctor
+import Control.Lens.Optic
+import Control.Lens.Iso
+import Control.Lens.Prism
+import Control.Lens.Optional
+
+%default total
+
+
+public export
+interface Cons s t a b | s where
+  cons_ : Prism s t (a, s) (b, t)
+
+public export
+head_ : Cons s s a a => Optional' s a
+head_ @{_} @{MkIsOptional _} = cons_ . first
+
+public export
+tail_ : Cons s s a a => Optional' s s
+tail_ @{_} @{MkIsOptional _} = cons_ . second
+
+
+public export
+interface Snoc s t a b | s where
+  snoc_ : Prism s t (s, a) (t, b)
+
+public export
+init_ : Snoc s s a a => Optional' s s
+init_ @{_} @{MkIsOptional _} = snoc_ . first
+
+public export
+last_ : Snoc s s a a => Optional' s a
+last_ @{_} @{MkIsOptional _} = snoc_ . second
+

src/Data/List/Lens.idr

@@ -51,3 +51,20 @@ 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)
+
+
+public export
+Cons (List a) (List b) a b where
+  cons_ = prism (uncurry (::)) (\case
+    [] => Left []
+    x :: xs => Right (x, xs))
+
+public export
+Snoc (List a) (List b) a b where
+  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

src/Data/Vect/Lens.idr

@@ -1,7 +1,8 @@
 module Data.Vect.Lens
 
 import Data.Vect
-import Control.Lens
+import public Control.Lens
+import Data.Tuple.Lens
 
 %default total
 
@@ -30,3 +31,28 @@ Ixed Nat a (Vect n a) where
 public export
 Ixed' Nat (Fin n) a (Vect n a) where
   ix' n = lens (index n) (flip $ replaceAt n)
+
+
+public export
+cons_ : Iso (Vect (S n) a) (Vect (S n) b) (a, Vect n a) (b, Vect n b)
+cons_ = iso (\(x :: xs) => (x,xs)) (uncurry (::))
+
+public export
+head_ : Lens' (Vect (S n) a) a
+head_ = cons_ . fst_
+
+public export
+tail_ : Lens' (Vect (S n) a) (Vect n a)
+tail_ = cons_ . snd_
+
+public export
+snoc_ : Iso (Vect (S n) a) (Vect (S n) b) (Vect n a, a) (Vect n b, b)
+snoc_ = iso unsnoc (uncurry snoc)
+
+public export
+init_ : Lens' (Vect (S n) a) (Vect n a)
+init_ = snoc_ . fst_
+
+public export
+last_ : Lens' (Vect (S n) a) a
+last_ = snoc_ . snd_