diff --git a/lens.ipkg b/lens.ipkg index 9e56c0a..d58b97d 100644 --- a/lens.ipkg +++ b/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 diff --git a/src/Data/SnocList/Lens.idr b/src/Data/SnocList/Lens.idr new file mode 100644 index 0000000..86961c0 --- /dev/null +++ b/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 diff --git a/src/Data/SortedMap/Lens.idr b/src/Data/SortedMap/Lens.idr new file mode 100644 index 0000000..c9c2b9f --- /dev/null +++ b/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) diff --git a/src/Data/SortedSet/Lens.idr b/src/Data/SortedSet/Lens.idr new file mode 100644 index 0000000..e98e23e --- /dev/null +++ b/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) diff --git a/src/Data/Stream/Lens.idr b/src/Data/Stream/Lens.idr new file mode 100644 index 0000000..2d45565 --- /dev/null +++ b/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) diff --git a/src/Data/String/Lens.idr b/src/Data/String/Lens.idr index ee61913..87541b7 100644 --- a/src/Data/String/Lens.idr +++ b/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