Control.Zipper

A system for type-safe, traversal-based zippers into arbitrary datatypes.

Definitions

data ZipLayer : Type

  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.

Totality: total
Visibility: public export
Constructor: 

(@>) : Type -> Type -> ZipLayer

getTy : ZipLayer -> Type

  Get the type from a layer of a zipper.

Totality: total
Visibility: public export

data Zipper : List ZipLayer -> Type -> Type -> Type

  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.

Totality: total
Visibility: export
Constructor: 

MkZipper : Coil hs i a -> Pointer i a -> i -> a -> Zipper hs i a

zipper : a -> Zipper [] () a

  Open a zipper from a value.

Totality: total
Visibility: export

focus : IndexedLens' i (Zipper hs i a) a

  A lens that points to the current focus of the zipper.

Totality: total
Visibility: export

upward : Zipper ((j @> s) :: hs) i a -> Zipper hs j s

  Move up a layer of the zipper.

Totality: total
Visibility: export

tug : (a -> Maybe a) -> a -> a

  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.

Totality: total
Visibility: export

rightward : Alternative f => Zipper hs i a -> f (Zipper hs i a)

  Move right one value in the current layer. This will fail if already at the
  rightmost value.

Totality: total
Visibility: export

leftward : Alternative f => Zipper hs i a -> f (Zipper hs i a)

  Move left one value in the current layer. This will fail if already at the
  leftmost value.

Totality: total
Visibility: export

rightmost : Zipper hs i a -> Zipper hs i a

  Move to the rightmost value in the current layer.

Totality: total
Visibility: export

leftmost : Zipper hs i a -> Zipper hs i a

  Move to the leftmost value in the current layer.

Totality: total
Visibility: export

idownward : IndexedLens' i s a -> Zipper hs j s -> Zipper ((j @> s) :: hs) i a

  Move downward through an indexed lens.
  
  This cannot fail, since a lens always contains a value.

Totality: total
Visibility: export

downward : Lens' s a -> Zipper hs j s -> Zipper ((j @> s) :: hs) () a

  Move downward through a lens.
  
  This cannot fail, since a lens always contains a value.

Totality: total
Visibility: export

iwithin : Alternative f => IndexedTraversal' i s a -> Zipper hs j s -> f (Zipper ((j @> s) :: hs) i a)

  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.

Totality: total
Visibility: export

within : Alternative f => Traversal' s a -> Zipper hs j s -> f (Zipper ((j @> s) :: hs) Nat a)

  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.

Totality: total
Visibility: export

rezip : Zipper hs i a -> getTy (last ((i @> a) :: hs))

  Close a zipper, repackaging it back into a value of its original type.

Totality: total
Visibility: export