Generics.MRSOP.Zipper.Deep

Provides one-hole contexts for our universe, but over deep encoded datatypes. These are a bit easier to use computationally.

This module follows the very same structure as Zipper. Refer there for further documentation.

Documentation

data Ctxs (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where

Analogous to Ctxs

Constructors

Nil :: Ctxs ki codes ix ix

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

data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> Nat -> * where

Analogous to Ctx

Constructors

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

data NPHole (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> [Atom kon] -> * where

Analogous to NPHole, but uses a deep representation for generic values.

Constructors

H :: PoA ki (Fix ki codes) xs -> NPHole ki codes ix (I ix ': xs)

T :: NA ki (Fix ki codes) x -> NPHole ki codes ix xs -> NPHole ki codes ix (x ': xs)

getCtxsIx :: Ctxs ki codes iy ix -> Proxy ix

fillNPHole :: IsNat ix => Fix ki codes ix -> NPHole ki codes ix xs -> PoA ki (Fix ki codes) xs

Given a product with a hole in it, and an element, get back a product

dual of removeNPHole

fillCtxs :: IsNat ix => Fix ki codes iy -> Ctxs ki codes ix iy -> Fix ki codes ix

Given a value that fits in a context, fills the context hole.

fillCtx :: IsNat ix => Fix ki codes ix -> Ctx ki codes c ix -> Rep ki (Fix ki codes) c

removeCtxs :: (EqHO ki, IsNat ix) => Ctxs ki codes ix iy -> Fix ki codes ix -> Maybe (Fix ki codes iy)

Given a value and a context, tries to match to context in the value and, upon success, returns whatever overlaps with the hole.

removeCtx :: forall ix ki codes c. (EqHO ki, IsNat ix) => Rep ki (Fix ki codes) c -> Ctx ki codes c ix -> Maybe (Fix ki codes ix)

removeNPHole :: (EqHO ki, IsNat ix) => NPHole ki codes ix xs -> PoA ki (Fix ki codes) xs -> Maybe (Fix ki codes ix)