Safe Haskell	None
Language	Haskell2010

Generics.MRSOP.Zipper

Contents

Primitives
Navigation
Interface

Description

Provides Zippers (aka One-hole contexts) for our universe.

Synopsis

data Loc :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> * where
- Loc :: IsNat ix => El fam ix -> Ctxs ki fam cs iy ix -> Loc ki fam cs iy
data Ctxs :: (kon -> *) -> [*] -> [[[Atom kon]]] -> Nat -> Nat -> * where
- CNil :: Ctxs ki fam cs ix ix
- Cons :: (IsNat ix, IsNat a, IsNat b) => Ctx ki fam (Lkup ix cs) b -> Ctxs ki fam cs a ix -> Ctxs ki fam cs a b
data Ctx :: (kon -> *) -> [*] -> [[Atom kon]] -> Nat -> * where
- Ctx :: Constr c n -> NPHole ki fam ix (Lkup n c) -> Ctx ki fam c ix
data NPHole :: (kon -> *) -> [*] -> Nat -> [Atom kon] -> * where
- H :: PoA ki (El fam) xs -> NPHole ki fam ix (I ix ': xs)
- T :: NA ki (El fam) x -> NPHole ki fam ix xs -> NPHole ki fam ix (x ': xs)
data NPHoleE :: (kon -> *) -> [*] -> [Atom kon] -> * where
- ExistsIX :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> NPHoleE ki fam xs
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
fillCtxs :: forall ix fam iy ki c. (IsNat ix, Family ki fam c) => El fam iy -> Ctxs ki fam c ix iy -> El fam ix
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 iy. SNat iy -> El fam iy -> El fam iy) -> 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.

Constructors

Loc :: IsNat ix => El fam ix -> Ctxs ki fam cs iy ix -> Loc ki fam cs iy

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.

Constructors

CNil :: Ctxs ki fam cs ix ix
Cons :: (IsNat ix, IsNat a, IsNat b) => Ctx ki fam (Lkup ix cs) b -> Ctxs ki fam cs a ix -> Ctxs ki fam cs a b

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.

Constructors

Ctx :: Constr c n -> NPHole ki fam ix (Lkup n c) -> Ctx ki fam c ix

data NPHole :: (kon -> *) -> [*] -> Nat -> [Atom kon] -> * where Source #

A NPHole ki fam ix prod is a recursive position of type ix in prod.

Constructors

H :: PoA ki (El fam) xs -> NPHole ki fam ix (I ix ': xs)
T :: NA ki (El fam) x -> NPHole ki fam ix xs -> NPHole ki fam ix (x ': xs)

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.

Constructors

ExistsIX :: IsNat ix => El fam ix -> NPHole ki fam ix xs -> NPHoleE ki fam xs

mkNPHole :: PoA ki (El fam) xs -> Maybe (NPHoleE ki fam xs) Source #

Given a PoA (product of atoms), returns a one with a hole in the first seen NA_I. Note that we need the NPHoleE with the existential because we don't know, a priori, what will be the type of such hole.

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.

fill :: IsNat ix => El fam ix -> Ctx ki fam c ix -> Rep ki (El fam) c Source #

Fills up a hole.

fillCtxs :: forall ix fam iy ki c. (IsNat ix, Family ki fam c) => El fam iy -> Ctxs ki fam c ix iy -> El fam ix Source #

Recursively fills a stack of holes however, the Family constraint ain't so nice. so we perhaps want to take zippers over a deep representation

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

leave :: (Family ki fam codes, IsNat ix) => Loc ki fam codes ix -> El fam ix Source #

Exits the zipper

update :: (Family ki fam codes, IsNat ix) => (forall iy. SNat iy -> El fam iy -> El fam iy) -> Loc ki fam codes ix -> Loc ki fam codes ix Source #

Updates the value in the hole.