Document new features

This commit is contained in:
Kiana Sheibani 2023-04-24 10:02:32 -04:00
parent 32b6962be7
commit bf3ef35b63
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
4 changed files with 80 additions and 10 deletions

View file

@ -9,28 +9,40 @@ import Control.Lens.Optional
%default total %default total
||| An interface that provides a way to detach and inspect elements from the
||| left side of a sequence.
public export public export
interface Cons s t a b | s where interface Cons s t a b | s where
||| This is a prism that can attach or detach a value from the left side of a
||| sequence.
cons_ : Prism s t (a, s) (b, t) cons_ : Prism s t (a, s) (b, t)
||| Access the head (left-most element) of a sequence, if it is non-empty.
public export public export
head_ : Cons s s a a => Optional' s a head_ : Cons s s a a => Optional' s a
head_ @{_} @{MkIsOptional _} = cons_ . first head_ @{_} @{MkIsOptional _} = cons_ . first
||| Access the tail (all but the left-most element) of a sequence, if it is
||| non-empty.
public export public export
tail_ : Cons s s a a => Optional' s s tail_ : Cons s s a a => Optional' s s
tail_ @{_} @{MkIsOptional _} = cons_ . second tail_ @{_} @{MkIsOptional _} = cons_ . second
||| An interface that provides a way to detach and inspect elements from the
||| right side of a sequence.
public export public export
interface Snoc s t a b | s where interface Snoc s t a b | s where
||| This is a prism that can attach or detach a value from the right side of a
||| sequence.
snoc_ : Prism s t (s, a) (t, b) snoc_ : Prism s t (s, a) (t, b)
||| Access all but the right-most element of a sequence, if it is non-empty.
public export public export
init_ : Snoc s s a a => Optional' s s init_ : Snoc s s a a => Optional' s s
init_ @{_} @{MkIsOptional _} = snoc_ . first init_ @{_} @{MkIsOptional _} = snoc_ . first
||| Access the last (right-most) element of a sequence, if it is non-empty.
public export public export
last_ : Snoc s s a a => Optional' s a last_ : Snoc s s a a => Optional' s a
last_ @{_} @{MkIsOptional _} = snoc_ . second last_ @{_} @{MkIsOptional _} = snoc_ . second

View file

@ -13,6 +13,8 @@ import Control.Lens
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
||| The pointer stores the values on the current layer other than the focused one,
||| indirectly pointing to the focused value.
Pointer : (i, a : Type) -> Type Pointer : (i, a : Type) -> Type
Pointer i a = (SnocList (i, a), List (i, a)) Pointer i a = (SnocList (i, a), List (i, a))
@ -26,30 +28,51 @@ fromPointer k x (l, r) = l <>> (k,x) :: r
infix 9 @> infix 9 @>
||| A simple type that represents a layer of the zipper as it moves downwards.
|||
||| It also carries an index for that particular layer, if an indexed lens was
||| used to create it.
public export public export
data ZipLayer : Type where data ZipLayer : Type where
(@>) : (i, a : Type) -> ZipLayer (@>) : (i, a : Type) -> ZipLayer
||| Get the type from a layer of a zipper.
public export public export
getTy : ZipLayer -> Type getTy : ZipLayer -> Type
getTy (_ @> a) = a getTy (_ @> a) = a
||| The coil keeps track of the data not being focused on by the zipper, and
||| allows the final value to be repackaged at the end.
data Coil : List ZipLayer -> Type -> Type -> Type where data Coil : List ZipLayer -> Type -> Type -> Type where
Nil : Coil [] i a Nil : Coil [] i a
Cons : Pointer j s -> j -> (List (i, a) -> s) -> Cons : Pointer j s -> j -> (List (i, a) -> s) ->
Coil hs j s -> Coil (j @> s :: hs) i a Coil hs j s -> Coil (j @> s :: hs) i a
||| A zipper is a temporary data structure that can be "opened" on a particular
||| value, and allows one to move through its structure and operate on any
||| part of it.
||| A zipper can be opened from *any* value using `zipper`.
|||
||| Rather than being defined for a particular data structure, this zipper type
||| uses lenses to traverse through its value. The zipper can be moved down
||| through a traversal or lens, up out of one, or left and right between the
||| focuses of a traversal.
|||
||| You can use `rezip` to repackage the zipper back into a regular value.
export export
data Zipper : List ZipLayer -> Type -> Type -> Type where data Zipper : List ZipLayer -> Type -> Type -> Type where
MkZipper : Coil hs i a -> Pointer i a -> i -> a -> Zipper hs i a MkZipper : Coil hs i a -> Pointer i a -> i -> a -> Zipper hs i a
||| Open a zipper from a value.
export export
zipper : a -> Zipper [] () a zipper : a -> Zipper [] () a
zipper x = MkZipper Nil ([<], []) () x zipper x = MkZipper Nil ([<], []) () x
||| A lens that points to the current focus of the zipper.
export export
focus : IndexedLens' i (Zipper hs i a) a focus : IndexedLens' i (Zipper hs i a) a
focus = ilens (\(MkZipper _ _ i x) => (i, x)) focus = ilens (\(MkZipper _ _ i x) => (i, x))
@ -61,35 +84,37 @@ focus = ilens (\(MkZipper _ _ i x) => (i, x))
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
||| Move up a layer of the zipper.
export export
upward : Zipper (j @> s :: hs) i a -> Zipper hs j s upward : Zipper (j @> s :: hs) i a -> Zipper hs j s
upward (MkZipper (Cons p j k coil) q i x) = upward (MkZipper (Cons p j k coil) q i x) =
MkZipper coil p j $ k $ fromPointer i x q MkZipper coil p j $ k $ fromPointer i x q
||| Perform an action on a zipper, but leave the zipper's state unchanged if the
||| action fails.
|||
||| This is intended to be used as `tug rightward`, `tug leftward`, etc.
export export
tug : (a -> Maybe a) -> a -> a tug : (a -> Maybe a) -> a -> a
tug f x = fromMaybe x (f x) tug f x = fromMaybe x (f x)
||| Move right one value in the current layer. This will fail if already at the
||| rightmost value.
export export
rightward : Alternative f => Zipper hs i a -> f (Zipper hs i a) rightward : Alternative f => Zipper hs i a -> f (Zipper hs i a)
rightward (MkZipper _ (_, []) _ _) = empty rightward (MkZipper _ (_, []) _ _) = empty
rightward (MkZipper coil (l, (j,y) :: r) i x) = rightward (MkZipper coil (l, (j,y) :: r) i x) =
pure $ MkZipper coil (l :< (i,x), r) j y pure $ MkZipper coil (l :< (i,x), r) j y
||| Move left one value in the current layer. This will fail if already at the
||| leftmost value.
export export
leftward : Alternative f => Zipper hs i a -> f (Zipper hs i a) leftward : Alternative f => Zipper hs i a -> f (Zipper hs i a)
leftward (MkZipper _ ([<], _) _ _) = empty leftward (MkZipper _ ([<], _) _ _) = empty
leftward (MkZipper coil (l :< (j,y), r) i x) = leftward (MkZipper coil (l :< (j,y), r) i x) =
pure $ MkZipper coil (l, (i,x) :: r) j y pure $ MkZipper coil (l, (i,x) :: r) j y
export ||| Move to the rightmost value in the current layer.
leftmost : Zipper hs i a -> Zipper hs i a
leftmost (MkZipper coil p i x) =
case fromPointer i x p of
(j,y) :: xs => MkZipper coil ([<], xs) j y
-- Too lazy to prove this impossible for now
[] => assert_total $ idris_crash "Unreachable"
export export
rightmost : Zipper hs i a -> Zipper hs i a rightmost : Zipper hs i a -> Zipper hs i a
rightmost (MkZipper coil (l,r) i x) = rightmost (MkZipper coil (l,r) i x) =
@ -98,7 +123,19 @@ rightmost (MkZipper coil (l,r) i x) =
-- Too lazy to prove this impossible for now -- Too lazy to prove this impossible for now
[<] => assert_total $ idris_crash "Unreachable" [<] => assert_total $ idris_crash "Unreachable"
||| Move to the leftmost value in the current layer.
export
leftmost : Zipper hs i a -> Zipper hs i a
leftmost (MkZipper coil p i x) =
case fromPointer i x p of
(j,y) :: xs => MkZipper coil ([<], xs) j y
-- Too lazy to prove this impossible for now
[] => assert_total $ idris_crash "Unreachable"
||| Move downward through an indexed lens.
|||
||| This cannot fail, since a lens always contains a value.
export export
idownward : IndexedLens' i s a -> Zipper hs j s -> Zipper (j @> s :: hs) i a idownward : IndexedLens' i s a -> Zipper hs j s -> Zipper (j @> s :: hs) i a
idownward l (MkZipper coil p j y) = idownward l (MkZipper coil p j y) =
@ -108,6 +145,9 @@ idownward l (MkZipper coil p j y) =
go : List a -> s go : List a -> s
go ls = set (partsOf l) ls y go ls = set (partsOf l) ls y
||| Move downward through a lens.
|||
||| This cannot fail, since a lens always contains a value.
export export
downward : Lens' s a -> Zipper hs j s -> Zipper (j @> s :: hs) () a downward : Lens' s a -> Zipper hs j s -> Zipper (j @> s :: hs) () a
downward l (MkZipper coil p i x) = downward l (MkZipper coil p i x) =
@ -116,6 +156,10 @@ downward l (MkZipper coil p i x) =
go : List a -> s go : List a -> s
go ls = set (partsOf l) ls x go ls = set (partsOf l) ls x
||| Move downward through an indexed traversal. This will fail if the traversal
||| has no focuses.
|||
||| If the traversal has multiple values, the zipper will focus on the leftmost one.
export export
iwithin : Alternative f => IndexedTraversal' i s a -> Zipper hs j s -> f (Zipper (j @> s :: hs) i a) iwithin : Alternative f => IndexedTraversal' i s a -> Zipper hs j s -> f (Zipper (j @> s :: hs) i a)
iwithin l (MkZipper coil p j y) = iwithin l (MkZipper coil p j y) =
@ -126,6 +170,10 @@ iwithin l (MkZipper coil p j y) =
go : List a -> s go : List a -> s
go ls = set (partsOf l) ls y go ls = set (partsOf l) ls y
||| Move downward through a traversal. This will fail if the traversal has no
||| focuses.
|||
||| If the traversal has multiple values, the zipper will focus on the leftmost one.
export export
within : Alternative f => Traversal' s a -> Zipper hs j s -> f (Zipper (j @> s :: hs) Nat a) within : Alternative f => Traversal' s a -> Zipper hs j s -> f (Zipper (j @> s :: hs) Nat a)
within = iwithin . iordinal within = iwithin . iordinal
@ -135,6 +183,7 @@ recoil : Coil hs i a -> List (i, a) -> getTy $ last (i @> a :: hs)
recoil Nil xs = assert_total $ case xs of (_,x) :: _ => x recoil Nil xs = assert_total $ case xs of (_,x) :: _ => x
recoil (Cons p i f coil) xs = recoil coil $ fromPointer i (f xs) p recoil (Cons p i f coil) xs = recoil coil $ fromPointer i (f xs) p
||| Close a zipper, repackaging it back into a value of its original type.
export export
rezip : Zipper hs i a -> getTy $ last (i @> a :: hs) rezip : Zipper hs i a -> getTy $ last (i @> a :: hs)
rezip (MkZipper coil p i x) = recoil coil $ fromPointer i x p rezip (MkZipper coil p i x) = recoil coil $ fromPointer i x p

View file

@ -52,7 +52,6 @@ Ixed Nat a (List a) where
Yes _ => replaceAt n x xs Yes _ => replaceAt n x xs
No _ => xs) No _ => xs)
public export public export
Cons (List a) (List b) a b where Cons (List a) (List b) a b where
cons_ = prism (uncurry (::)) (\case cons_ = prism (uncurry (::)) (\case

View file

@ -8,10 +8,20 @@ import Data.List.Lens
%default total %default total
||| An isomorphism between a string and a list of characters.
|||
||| ```idris
||| unpacked = from packed
||| ```
public export public export
unpacked : Iso' String (List Char) unpacked : Iso' String (List Char)
unpacked = iso unpack pack unpacked = iso unpack pack
||| An isomorphism between a list of characters and a string.
|||
||| ```idris
||| packed = from unpacked
||| ```
public export public export
packed : Iso' (List Char) String packed : Iso' (List Char) String
packed = iso pack unpack packed = iso pack unpack