generics-mrsop-2.0.0: Generic Programming with Mutually Recursive Sums of Products.

Safe HaskellSafe
LanguageHaskell2010

Generics.MRSOP.Zipper.Deep

Description

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.

Synopsis

Documentation

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

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 Source #

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 Source #

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 Source #

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

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 Source #

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 Source #

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

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) Source #

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