| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Generics.MRSOP.Zipper
Contents
Description
Provides Zippers (aka One-hole contexts) for our universe.
- data Loc :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> * where
- data Ctxs :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> Nat -> * where
- data Ctx :: (kon -> *) -> [*] -> [[Atom kon]] -> Nat -> * where
- data NPHole :: (kon -> *) -> [*] -> Nat -> [Atom kon] -> * where
- data NPHoleE :: (kon -> *) -> [*] -> [Atom kon] -> * where
- mkNPHole :: PoA ki (El fam) xs -> Maybe (NPHoleE ki fam xs)
- fillNPHole :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> PoA ki (El fam) xs
- walkNPHole :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> Maybe (NPHoleE ki fam xs)
- first :: (forall ix. IsNat ix => El fam ix -> Ctx ki fam c ix -> a) -> Rep ki (El fam) c -> Maybe a
- fill :: IsNat ix => El fam ix -> Ctx ki fam c ix -> Rep ki (El fam) c
- next :: IsNat ix => (forall iy. IsNat iy => El fam iy -> Ctx ki fam c iy -> a) -> El fam ix -> Ctx ki fam c ix -> Maybe a
- down :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)
- up :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)
- right :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix)
- enter :: (Family ki fam codes, IsNat ix) => El fam ix -> Loc ki fam codes ix
- leave :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> El fam ix
- update :: (Family ki fam codes, IsNat ix) => (forall ix. SNat ix -> El fam ix -> El fam ix) -> Loc ki fam codes ix -> Loc ki fam codes ix
Documentation
data Loc :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> * where Source #
In a Zipper, a Location is a a pair of a one hole context
and whatever was supposed to be there. In a sums of products
fashion, it consists of a choice of constructor and
a position in the type of that constructor.
data Ctxs :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> Nat -> * where Source #
A Ctxs ki fam codes ix iy represents a value of type El fam ix
with a El fam iy-typed hole in it.
data Ctx :: (kon -> *) -> [*] -> [[Atom kon]] -> Nat -> * where Source #
A Ctx ki fam c ix is a choice of constructor for c
with a hole of type ix inside.
data NPHole :: (kon -> *) -> [*] -> Nat -> [Atom kon] -> * where Source #
A NPHole ki fam ix prod is a recursive position
of type ix in prod.
data NPHoleE :: (kon -> *) -> [*] -> [Atom kon] -> * where Source #
Existential abstraction; needed for walking the possible holes in a product. We must be able to hide the type.
fillNPHole :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> PoA ki (El fam) xs Source #
Given a hole and an element, put both together to form
the PoA again.
walkNPHole :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> Maybe (NPHoleE ki fam xs) Source #
Given an hole and an element, return the next hole, if any.
Primitives
first :: (forall ix. IsNat ix => El fam ix -> Ctx ki fam c ix -> a) -> Rep ki (El fam) c -> Maybe a Source #
Executes an action in the first hole within the given Rep value,
if such hole can be constructed.
next :: IsNat ix => (forall iy. IsNat iy => El fam iy -> Ctx ki fam c iy -> a) -> El fam ix -> Ctx ki fam c ix -> Maybe a Source #
Walks to the next hole and execute an action.
Navigation
down :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix) Source #
Move one layer deeper within the recursive structure.
up :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix) Source #
Move one layer upwards within the recursive structure
right :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> Maybe (Loc ki fam codes ix) Source #
More one hole to the right
Interface
enter :: (Family ki fam codes, IsNat ix) => El fam ix -> Loc ki fam codes ix Source #
Initializes the zipper