Safe Haskell	Safe
Language	Haskell2010

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

data Ctxs (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where
- 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
- 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
- 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
fillCtxs :: IsNat ix => Fix ki codes iy -> Ctxs ki codes ix iy -> Fix ki codes ix
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)
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)

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

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 #