diff --git a/src/Control/Lens.idr b/src/Control/Lens.idr index 5ddce24..d2970ef 100644 --- a/src/Control/Lens.idr +++ b/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 diff --git a/src/Control/Lens/Cons.idr b/src/Control/Lens/Cons.idr new file mode 100644 index 0000000..e790b2f --- /dev/null +++ b/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 + diff --git a/src/Data/List/Lens.idr b/src/Data/List/Lens.idr index 7dfe194..ad0f97c 100644 --- a/src/Data/List/Lens.idr +++ b/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 diff --git a/src/Data/Vect/Lens.idr b/src/Data/Vect/Lens.idr index b3337a9..f47ba31 100644 --- a/src/Data/Vect/Lens.idr +++ b/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_