Add optics for common types

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

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

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
+

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)

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'

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

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)