Add more lens modules for datatypes

lens.ipkg

@@ -16,6 +16,7 @@ modules = Control.Applicative.Backwards,
           Control.Applicative.Indexing,
           Control.Lens.At,
           Control.Lens.Cons,
+          Control.Lens.Each,
           Control.Lens.Equality,
           Control.Lens.Fold,
           Control.Lens.Getter,
@@ -35,6 +36,9 @@ modules = Control.Applicative.Backwards,
           Data.Either.Lens,
           Data.List.Lens,
           Data.Maybe.Lens,
+          Data.SnocList.Lens,
+          Data.SortedMap.Lens,
+          Data.SortedSet.Lens,
           Data.String.Lens,
           Data.Tuple.Lens,
           Data.Vect.Lens

src/Data/SnocList/Lens.idr

@@ -0,0 +1,81 @@
+module Data.SnocList.Lens
+
+import Data.Zippable
+import Data.SnocList
+import Data.Profunctor
+import public Control.Lens
+
+%default total
+
+
+stripPrefix : Eq a => SnocList a -> SnocList a -> Maybe (SnocList a)
+stripPrefix qs xs0 = go xs0 zs
+  where
+    drp : SnocList a -> SnocList a -> SnocList a
+    drp (ps :< _) (xs :< _) = drp ps xs
+    drp [<] xs = xs
+    drp _  [<] = [<]
+
+    zs : SnocList a
+    zs = drp qs xs0
+
+    go : SnocList a -> SnocList a -> Maybe (SnocList a)
+    go (xs :< _) (ys :< _) = go xs ys
+    go xs [<] = zipWith const xs0 zs <$ guard (xs == qs)
+    go [<] _  = Nothing
+
+stripSuffix : Eq a => SnocList a -> SnocList a -> Maybe (SnocList a)
+stripSuffix [<] ys = Just ys
+stripSuffix (_ :< _) [<] = Nothing
+stripSuffix (xs :< x) (ys :< y) = guard (x == y) *> stripSuffix xs ys
+
+
+||| A prism that strips a prefix from a snoclist of values.
+public export
+prefixed : Eq a => SnocList a -> Prism' (SnocList a) (SnocList a)
+prefixed xs = prism' (xs ++) (stripPrefix xs)
+
+||| A prism that strips a suffix from a snoclist of values.
+public export
+suffixed : Eq a => SnocList a -> Prism' (SnocList a) (SnocList a)
+suffixed xs = prism' (++ xs) (stripSuffix xs)
+
+||| An isomorphism between a snoclist and its reverse.
+public export
+reversed : Iso (SnocList a) (SnocList b) (SnocList a) (SnocList b)
+reversed = iso reverse reverse
+
+
+public export
+Ixed Nat a (SnocList a) where
+  ix = element
+
+public export
+Snoc (SnocList a) (SnocList b) a b where
+  snocIso = iso (\case
+      [<] => Nothing
+      xs :< x => Just (xs,x))
+    (maybe [<] $ uncurry (:<))
+
+  snoc_ = prism (uncurry (:<)) (\case
+    [<] => Left [<]
+    xs :< x => Right (xs,x))
+
+uncons : SnocList a -> a -> (a, SnocList a)
+uncons [<] x = (x, [<])
+uncons (ys :< y) x = mapSnd (:< x) $ uncons ys y
+
+public export
+Cons (SnocList a) (SnocList b) a b where
+  consIso = iso (\case
+      [<] => Nothing
+      xs :< x => Just $ uncons xs x)
+    (maybe [<] $ uncurry cons)
+
+  cons_ = prism (uncurry cons) (\case
+    [<] => Left [<]
+    xs :< x => Right $ uncons xs x)
+
+public export
+Each (SnocList a) (SnocList b) a b where
+  each = traversed

src/Data/SortedMap/Lens.idr

@@ -0,0 +1,32 @@
+module Data.SortedMap.Lens
+
+import Decidable.Equality
+import Data.SortedMap.Dependent
+import Data.SortedMap
+import public Control.Lens
+
+%default total
+
+
+public export
+Ixed k v (SortedMap k v) where
+  ix k = optional' (lookup k) (flip $ insert k)
+
+public export
+At k v (SortedMap k v) where
+  at k = lens (lookup k) (flip $ \case
+    Nothing => delete k
+    Just v => insert k v)
+
+
+public export
+ixDep : DecEq k => {0 p : k -> Type} -> (x : k) ->
+          Optional' (SortedDMap k p) (p x)
+ixDep {p} x = optional' (lookupPrecise x) (\m,v => insert x v m)
+
+public export
+atDep : DecEq k => {0 p : k -> Type} -> (x : k) ->
+          Lens' (SortedDMap k p) (Maybe $ p x)
+atDep {p} x = lens (lookupPrecise x) (\m => \case
+  Nothing => delete x m
+  Just v => insert x v m)

src/Data/SortedSet/Lens.idr

@@ -0,0 +1,17 @@
+module Data.SortedSet.Lens
+
+import Data.SortedSet
+import public Control.Lens
+
+%default total
+
+
+public export
+Ixed k () (SortedSet k) where
+  ix k = optional' (ignore . guard . contains k) const
+
+public export
+At k () (SortedSet k) where
+  at k = lens (ignore . guard . contains k) (flip $ \case
+    Nothing => delete k
+    Just _ => insert k)

src/Data/Stream/Lens.idr

@@ -0,0 +1,47 @@
+module Data.Stream.Lens
+
+import Data.Stream
+import public Control.Lens
+import Data.Tuple.Lens
+
+%default total
+
+
+replaceList : List a -> Stream a -> Stream a
+replaceList [] ys = ys
+replaceList (x :: xs) (_ :: ys) = x :: replaceList xs ys
+
+replaceAt : Nat -> a -> Stream a -> Stream a
+replaceAt Z x (_ :: ys) = x :: ys
+replaceAt (S n) x (y :: ys) = y :: replaceAt n x ys
+
+
+public export
+cons_ : Iso (Stream a) (Stream b) (a, Stream a) (b, Stream b)
+cons_ = iso (\(x::xs) => (x,xs)) (\(x,xs) => x::xs)
+
+public export
+head_ : Lens' (Stream a) a
+head_ = cons_ . fst_
+
+public export
+tail_ : Lens' (Stream a) (Stream a)
+tail_ = cons_ . snd_
+
+
+public export
+taken' : Nat -> Lens' (Stream a) (List a)
+taken' n = lens (take n) (flip replaceList)
+
+public export
+taken : Nat -> Traversal' (Stream a) a
+taken n = taken' n . traversed
+
+
+public export
+Ixed Nat a (Stream a) where
+  ix n = lens (index n) (flip $ replaceAt n)
+
+public export
+Ixed' Nat Nat a (Stream a) where
+  ix' n = lens (index n) (flip $ replaceAt n)

src/Data/String/Lens.idr

@@ -1,7 +1,6 @@
 module Data.String.Lens
 
 import Data.String
-import Data.Profunctor
 import public Control.Lens
 import Data.List.Lens