Data.Type.Zipper

The list zipper data structure with a focused element (at the type-level).

Used for storing the registers and the instructions because of its performance benefits.

Documentation

data Zipper a where

Polymorphic list zipper.

Some functions that operate on Zippers are partial. Instead of having to mess with promoted Maybes and whatnot, this constructor represent an erroneous operation.

Constructors

Zip :: [a] -> a -> [a] -> Zipper a

Invalid :: Zipper a

type family FromList xs :: Zipper k

Construct `Zipper a` from `[a]`. The list must contain at least one element for the Zipper to be valid. The resulting Zipper focuses on the first element of the list, the tail of the list is found to the right.

Equations

FromList `[]` = Invalid

FromList (x : xs) = Zip `[]` x xs

type family Extract zipper :: k

Extract the focused element.

Equations

Extract (Zip p c n) = c

type family Replace zipper with :: Zipper k

Replace the focused element with a new one.

Equations

Replace (Zip p c n) with = Zip p with n

type family ToList zipper :: [k]

Create a list from the Zipper by appending together the left lift, the focused element and the right list in this order.

Equations

ToList (Zip `[]` e n) = e : n

ToList (Zip (p : ps) e n) = ToList (Zip ps p (e : n))

type family Left by zipper :: Zipper k

Shift the focus to the left

Equations

Left 0 z = z

Left n (Zip (p : prevs) cur next) = Left (n - 1) (Zip prevs p (cur : next))

Left n z = Invalid

type family Right by zipper :: Zipper k

Shift the focus to the right

Equations

Right 0 z = z

Right by (Zip prevs cur (n : next)) = Right (by - 1) (Zip (cur : prevs) n next)

Right n z = Invalid