HERMIT.Kure

KURE

All the required functionality of KURE is exported here, so other modules do not need to import KURE directly.

module Language.KURE

module Language.KURE.BiTransform

module Language.KURE.Lens

module Language.KURE.ExtendableContext

module Language.KURE.Pathfinder

Sub-Modules

module HERMIT.Kure.Universes

Synonyms

type TransformH a b = Transform HermitC HermitM a b

type RewriteH a = Rewrite HermitC HermitM a

type BiRewriteH a = BiRewrite HermitC HermitM a

type LensH a b = Lens HermitC HermitM a b

type PathH = Path Crumb

Utilities

inContextM :: c -> Transform c m () a -> m a

Congruence combinators

Modguts

modGutsT :: (ExtendPath c Crumb, HasEmptyContext c, Monad m) => Transform c m CoreProg a -> (ModGuts -> a -> b) -> Transform c m ModGuts b

Transform a module. Slightly different to the other congruence combinators: it passes in all of the original to the reconstruction function.

modGutsR :: (ExtendPath c Crumb, HasEmptyContext c, Monad m) => Rewrite c m CoreProg -> Rewrite c m ModGuts

Rewrite the CoreProg child of a module.

Program

progNilT :: Monad m => b -> Transform c m CoreProg b

Transform an empty list.

progConsT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m CoreBind a1 -> Transform c m CoreProg a2 -> (a1 -> a2 -> b) -> Transform c m CoreProg b

Transform a program of the form: (CoreBind : CoreProg)

progConsAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite all children of a program of the form: (CoreBind : CoreProg)

progConsAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite any children of a program of the form: (CoreBind : CoreProg)

progConsOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite one child of a program of the form: (CoreBind : CoreProg)

Binding Groups

nonRecT :: (ExtendPath c Crumb, Monad m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreBind b

Transform a binding group of the form: NonRec Var CoreExpr

nonRecAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind

Rewrite all children of a binding group of the form: NonRec Var CoreExpr

nonRecAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind

Rewrite any children of a binding group of the form: NonRec Var CoreExpr

nonRecOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreBind

Rewrite one child of a binding group of the form: NonRec Var CoreExpr

recT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Transform c m CoreDef a) -> ([a] -> b) -> Transform c m CoreBind b

Transform a binding group of the form: Rec [CoreDef]

recAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind

Rewrite all children of a binding group of the form: Rec [CoreDef]

recAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind

Rewrite any children of a binding group of the form: Rec [CoreDef]

recOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreBind

Rewrite one child of a binding group of the form: Rec [CoreDef]

Recursive Definitions

defT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Id a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreDef b

Transform a recursive definition of the form: Def Id CoreExpr

defAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef

Rewrite all children of a recursive definition of the form: Def Id CoreExpr

defAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef

Rewrite any children of a recursive definition of the form: Def Id CoreExpr

defOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Id -> Rewrite c m CoreExpr -> Rewrite c m CoreDef

Rewrite one child of a recursive definition of the form: Def Id CoreExpr

Case Alternatives

altT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m AltCon a1 -> (Int -> Transform c m Var a2) -> Transform c m CoreExpr a3 -> (a1 -> [a2] -> a3 -> b) -> Transform c m CoreAlt b

Transform a case alternative of the form: (AltCon, [Var], CoreExpr)

altAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt

Rewrite all children of a case alternative of the form: (AltCon, Id, CoreExpr)

altAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt

Rewrite any children of a case alternative of the form: (AltCon, Id, CoreExpr)

altOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m AltCon -> (Int -> Rewrite c m Var) -> Rewrite c m CoreExpr -> Rewrite c m CoreAlt

Rewrite one child of a case alternative of the form: (AltCon, Id, CoreExpr)

Expressions

varT :: (ExtendPath c Crumb, Monad m) => Transform c m Id b -> Transform c m CoreExpr b

Transform an expression of the form: Var Id

varR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Id -> Rewrite c m CoreExpr

Rewrite the Id child in an expression of the form: Var Id

litT :: (ExtendPath c Crumb, Monad m) => Transform c m Literal b -> Transform c m CoreExpr b

Transform an expression of the form: Lit Literal

litR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Literal -> Rewrite c m CoreExpr

Rewrite the Literal child in an expression of the form: Lit Literal

appT :: (ExtendPath c Crumb, Monad m) => Transform c m CoreExpr a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b

Transform an expression of the form: App CoreExpr CoreExpr

appAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: App CoreExpr CoreExpr

appAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: App CoreExpr CoreExpr

appOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: App CoreExpr CoreExpr

lamT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Lam Var CoreExpr

lamAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Lam Var CoreExpr

lamAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Lam Var CoreExpr

lamOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: Lam Var CoreExpr

letT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m CoreBind a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Let CoreBind CoreExpr

letAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Let CoreBind CoreExpr

letAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Let CoreBind CoreExpr

letOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreBind -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: Let CoreBind CoreExpr

caseT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m CoreExpr e -> Transform c m Id w -> Transform c m Type ty -> (Int -> Transform c m CoreAlt alt) -> (e -> w -> ty -> [alt] -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Case CoreExpr Id Type [CoreAlt]

caseAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> Rewrite c m CoreAlt) -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Case CoreExpr Id Type [CoreAlt]

caseAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> Rewrite c m CoreAlt) -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Case CoreExpr Id Type [CoreAlt]

caseOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> Rewrite c m CoreAlt) -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: Case CoreExpr Id Type [CoreAlt]

castT :: (ExtendPath c Crumb, Monad m) => Transform c m CoreExpr a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Cast CoreExpr Coercion

castAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Cast CoreExpr Coercion

castAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Cast CoreExpr Coercion

castOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Coercion -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: Cast CoreExpr Coercion

tickT :: (ExtendPath c Crumb, Monad m) => Transform c m CoreTickish a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Tick CoreTickish CoreExpr

tickAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Tick CoreTickish CoreExpr

tickAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Tick CoreTickish CoreExpr

tickOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m CoreTickish -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Tick CoreTickish CoreExpr

typeT :: (ExtendPath c Crumb, Monad m) => Transform c m Type b -> Transform c m CoreExpr b

Transform an expression of the form: Type Type

typeR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m CoreExpr

Rewrite the Type child in an expression of the form: Type Type

coercionT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion b -> Transform c m CoreExpr b

Transform an expression of the form: Coercion Coercion

coercionR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m CoreExpr

Rewrite the Coercion child in an expression of the form: Coercion Coercion

Composite Congruence Combinators

defOrNonRecT :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m g b

Transform a definition of the form NonRec Var CoreExpr or Def Id CoreExpr

defOrNonRecAllR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g

Rewrite all children of a definition of the form NonRec Var CoreExpr or Def Id CoreExpr

defOrNonRecAnyR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g

Rewrite any children of a definition of the form NonRec Var CoreExpr or Def Id CoreExpr

defOrNonRecOneR :: (Injection CoreBind g, Injection CoreDef g, ExtendPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m g

Rewrite one child of a definition of the form NonRec Var CoreExpr or Def Id CoreExpr

recDefT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Transform c m Id a1, Transform c m CoreExpr a2)) -> ([(a1, a2)] -> b) -> Transform c m CoreBind b

Transform a binding group of the form: Rec [(Id, CoreExpr)]

recDefAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind

Rewrite all children of a binding group of the form: Rec [(Id, CoreExpr)]

recDefAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind

Rewrite any children of a binding group of the form: Rec [(Id, CoreExpr)]

recDefOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreBind

Rewrite one child of a binding group of the form: Rec [(Id, CoreExpr)]

letNonRecT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> Transform c m CoreExpr a3 -> (a1 -> a2 -> a3 -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Let (NonRec Var CoreExpr) CoreExpr

letNonRecAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Let (NonRec Var CoreExpr) CoreExpr

letNonRecAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Let (NonRec Var CoreExpr) CoreExpr

letNonRecOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: Let (NonRec Var CoreExpr) CoreExpr

letRecT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Transform c m CoreDef a1) -> Transform c m CoreExpr a2 -> ([a1] -> a2 -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Let (Rec [CoreDef]) CoreExpr

letRecAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Let (Rec [CoreDef]) CoreExpr

letRecAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Let (Rec [CoreDef]) CoreExpr

letRecOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: Let (Rec [CoreDef]) CoreExpr

letRecDefT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Transform c m Id a1, Transform c m CoreExpr a2)) -> Transform c m CoreExpr a3 -> ([(a1, a2)] -> a3 -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Let (Rec [(Id, CoreExpr)]) CoreExpr

letRecDefAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Let (Rec [(Id, CoreExpr)]) CoreExpr

letRecDefAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Let (Rec [(Id, CoreExpr)]) CoreExpr

letRecDefOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: Let (Rec [(Id, CoreExpr)]) CoreExpr

consNonRecT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Var a1 -> Transform c m CoreExpr a2 -> Transform c m CoreProg a3 -> (a1 -> a2 -> a3 -> b) -> Transform c m CoreProg b

Transform a program of the form: (NonRec Var CoreExpr) : CoreProg

consNonRecAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite all children of an expression of the form: (NonRec Var CoreExpr) : CoreProg

consNonRecAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite any children of an expression of the form: (NonRec Var CoreExpr) : CoreProg

consNonRecOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m CoreExpr -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite one child of an expression of the form: (NonRec Var CoreExpr) : CoreProg

consRecT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Transform c m CoreDef a1) -> Transform c m CoreProg a2 -> ([a1] -> a2 -> b) -> Transform c m CoreProg b

Transform an expression of the form: (Rec [CoreDef]) : CoreProg

consRecAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite all children of an expression of the form: (Rec [CoreDef]) : CoreProg

consRecAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite any children of an expression of the form: (Rec [CoreDef]) : CoreProg

consRecOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreDef) -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite one child of an expression of the form: (Rec [CoreDef]) : CoreProg

consRecDefT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Transform c m Id a1, Transform c m CoreExpr a2)) -> Transform c m CoreProg a3 -> ([(a1, a2)] -> a3 -> b) -> Transform c m CoreProg b

Transform an expression of the form: (Rec [(Id, CoreExpr)]) : CoreProg

consRecDefAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite all children of an expression of the form: (Rec [(Id, CoreExpr)]) : CoreProg

consRecDefAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite any children of an expression of the form: (Rec [(Id, CoreExpr)]) : CoreProg

consRecDefOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> (Rewrite c m Id, Rewrite c m CoreExpr)) -> Rewrite c m CoreProg -> Rewrite c m CoreProg

Rewrite one child of an expression of the form: (Rec [(Id, CoreExpr)]) : CoreProg

caseAltT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m CoreExpr sc -> Transform c m Id w -> Transform c m Type ty -> (Int -> (Transform c m AltCon con, Int -> Transform c m Var v, Transform c m CoreExpr rhs)) -> (sc -> w -> ty -> [(con, [v], rhs)] -> b) -> Transform c m CoreExpr b

Transform an expression of the form: Case CoreExpr Id Type [(AltCon, [Var], CoreExpr)]

caseAltAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> (Rewrite c m AltCon, Int -> Rewrite c m Var, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr

Rewrite all children of an expression of the form: Case CoreExpr Id Type [(AltCon, [Var], CoreExpr)]

caseAltAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> (Rewrite c m AltCon, Int -> Rewrite c m Var, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr

Rewrite any children of an expression of the form: Case CoreExpr Id Type [(AltCon, [Var], CoreExpr)]

caseAltOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m CoreExpr -> Rewrite c m Id -> Rewrite c m Type -> (Int -> (Rewrite c m AltCon, Int -> Rewrite c m Var, Rewrite c m CoreExpr)) -> Rewrite c m CoreExpr

Rewrite one child of an expression of the form: Case CoreExpr Id Type [(AltCon, [Var], CoreExpr)]

Recursive Composite Congruence Combinators

progBindsT :: forall c m a b. (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Transform c m CoreBind a) -> ([a] -> b) -> Transform c m CoreProg b

Transform all top-level binding groups in a program.

progBindsAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreBind) -> Rewrite c m CoreProg

Rewrite all top-level binding groups in a program.

progBindsAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreBind) -> Rewrite c m CoreProg

Rewrite any top-level binding groups in a program.

progBindsOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => (Int -> Rewrite c m CoreBind) -> Rewrite c m CoreProg

Rewrite any top-level binding groups in a program.

Types

tyVarT :: (ExtendPath c Crumb, Monad m) => Transform c m TyVar b -> Transform c m Type b

Transform a type of the form: TyVarTy TyVar

tyVarR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyVar -> Rewrite c m Type

Rewrite the TyVar child of a type of the form: TyVarTy TyVar

litTyT :: (ExtendPath c Crumb, Monad m) => Transform c m TyLit b -> Transform c m Type b

Transform a type of the form: LitTy TyLit

litTyR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyLit -> Rewrite c m Type

Rewrite the TyLit child of a type of the form: LitTy TyLit

appTyT :: (ExtendPath c Crumb, Monad m) => Transform c m Type a1 -> Transform c m Type a2 -> (a1 -> a2 -> b) -> Transform c m Type b

Transform a type of the form: AppTy Type Type

appTyAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type

Rewrite all children of a type of the form: AppTy Type Type

appTyAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type

Rewrite any children of a type of the form: AppTy Type Type

appTyOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type

Rewrite one child of a type of the form: AppTy Type Type

funTyT :: (ExtendPath c Crumb, Monad m) => Transform c m Type a1 -> Transform c m Type a2 -> (a1 -> a2 -> b) -> Transform c m Type b

Transform a type of the form: FunTy Type Type

funTyAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type

Rewrite all children of a type of the form: FunTy Type Type

funTyAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type

Rewrite any children of a type of the form: FunTy Type Type

funTyOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Type -> Rewrite c m Type -> Rewrite c m Type

Rewrite one child of a type of the form: FunTy Type Type

forAllTyT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m Var a1 -> Transform c m Type a2 -> (a1 -> a2 -> b) -> Transform c m Type b

Transform a type of the form: ForAllTy Var Type

forAllTyAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type

Rewrite all children of a type of the form: ForAllTy Var Type

forAllTyAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type

Rewrite any children of a type of the form: ForAllTy Var Type

forAllTyOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m Var -> Rewrite c m Type -> Rewrite c m Type

Rewrite one child of a type of the form: ForAllTy Var Type

tyConAppT :: (ExtendPath c Crumb, Monad m) => Transform c m TyCon a1 -> (Int -> Transform c m KindOrType a2) -> (a1 -> [a2] -> b) -> Transform c m Type b

Transform a type of the form: TyConApp TyCon [KindOrType]

tyConAppAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type

Rewrite all children of a type of the form: TyConApp TyCon [KindOrType]

tyConAppAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type

Rewrite any children of a type of the form: TyConApp TyCon [KindOrType]

tyConAppOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m KindOrType) -> Rewrite c m Type

Rewrite one child of a type of the form: TyConApp TyCon [KindOrType]

Coercions

reflT :: (ExtendPath c Crumb, Monad m) => Transform c m Type a1 -> (Role -> a1 -> b) -> Transform c m Coercion b

Transform a coercion of the form: Refl Role Type

reflR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Type -> Rewrite c m Coercion

Rewrite the Type child of a coercion of the form: Refl Role Type

tyConAppCoT :: (ExtendPath c Crumb, Monad m) => Transform c m TyCon a1 -> (Int -> Transform c m Coercion a2) -> (Role -> a1 -> [a2] -> b) -> Transform c m Coercion b

Transform a coercion of the form: TyConAppCo Role TyCon [Coercion]

tyConAppCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion

Rewrite all children of a coercion of the form: TyConAppCo TyCon [Coercion]

tyConAppCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion

Rewrite any children of a coercion of the form: TyConAppCo TyCon [Coercion]

tyConAppCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m TyCon -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion

Rewrite one child of a coercion of the form: TyConAppCo TyCon [Coercion]

appCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b

Transform a coercion of the form: AppCo Coercion Coercion

appCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite all children of a coercion of the form: AppCo Coercion Coercion

appCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite any children of a coercion of the form: AppCo Coercion Coercion

appCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite one child of a coercion of the form: AppCo Coercion Coercion

forAllCoT :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Transform c m TyVar a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b

Transform a coercion of the form: ForAllCo TyVar Coercion

forAllCoAllR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, Monad m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite all children of a coercion of the form: ForAllCo TyVar Coercion

forAllCoAnyR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite any children of a coercion of the form: ForAllCo TyVar Coercion

forAllCoOneR :: (ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, MonadCatch m) => Rewrite c m TyVar -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite one child of a coercion of the form: ForAllCo TyVar Coercion

coVarCoT :: (ExtendPath c Crumb, Monad m) => Transform c m CoVar b -> Transform c m Coercion b

Transform a coercion of the form: CoVarCo CoVar

coVarCoR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoVar -> Rewrite c m Coercion

Rewrite the CoVar child of a coercion of the form: CoVarCo CoVar

axiomInstCoT :: (ExtendPath c Crumb, Monad m) => Transform c m (CoAxiom Branched) a1 -> Transform c m BranchIndex a2 -> (Int -> Transform c m Coercion a3) -> (a1 -> a2 -> [a3] -> b) -> Transform c m Coercion b

Transform a coercion of the form: AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]

axiomInstCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m (CoAxiom Branched) -> Rewrite c m BranchIndex -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion

Rewrite all children of a coercion of the form: AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]

axiomInstCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m (CoAxiom Branched) -> Rewrite c m BranchIndex -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion

Rewrite any children of a coercion of the form: AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]

axiomInstCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m (CoAxiom Branched) -> Rewrite c m BranchIndex -> (Int -> Rewrite c m Coercion) -> Rewrite c m Coercion

Rewrite one child of a coercion of the form: AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]

symCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion b -> Transform c m Coercion b

Transform a coercion of the form: SymCo Coercion

symCoR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite the Coercion child of a coercion of the form: SymCo Coercion

transCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b

Transform a coercion of the form: TransCo Coercion Coercion

transCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite all children of a coercion of the form: TransCo Coercion Coercion

transCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite any children of a coercion of the form: TransCo Coercion Coercion

transCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite one child of a coercion of the form: TransCo Coercion Coercion

nthCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Int a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b

Transform a coercion of the form: NthCo Int Coercion

nthCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite all children of a coercion of the form: NthCo Int Coercion

nthCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite any children of a coercion of the form: NthCo Int Coercion

nthCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Int -> Rewrite c m Coercion -> Rewrite c m Coercion

Rewrite one child of a coercion of the form: NthCo Int Coercion

instCoT :: (ExtendPath c Crumb, Monad m) => Transform c m Coercion a1 -> Transform c m Type a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b

Transform a coercion of the form: InstCo Coercion Type

instCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion

Rewrite all children of a coercion of the form: InstCo Coercion Type

instCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion

Rewrite any children of a coercion of the form: InstCo Coercion Type

instCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m Coercion -> Rewrite c m Type -> Rewrite c m Coercion

Rewrite one child of a coercion of the form: InstCo Coercion Type

lrCoT :: (ExtendPath c Crumb, Monad m) => Transform c m LeftOrRight a1 -> Transform c m Coercion a2 -> (a1 -> a2 -> b) -> Transform c m Coercion b

Transform a coercion of the form: LRCo LeftOrRight Coercion

lrCoAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m LeftOrRight -> Rewrite c m Coercion -> Rewrite c m Coercion

Transform all children of a coercion of the form: LRCo LeftOrRight Coercion

lrCoAnyR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m LeftOrRight -> Rewrite c m Coercion -> Rewrite c m Coercion

Transform any children of a coercion of the form: LRCo LeftOrRight Coercion

lrCoOneR :: (ExtendPath c Crumb, MonadCatch m) => Rewrite c m LeftOrRight -> Rewrite c m Coercion -> Rewrite c m Coercion

Transform one child of a coercion of the form: LRCo LeftOrRight Coercion

Lemmas

conjT :: (ExtendPath c Crumb, Monad m) => Transform c m Clause a1 -> Transform c m Clause a2 -> (a1 -> a2 -> b) -> Transform c m Clause b

Transform a clause of the form: Conj Clause Clause

conjAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Clause -> Rewrite c m Clause -> Rewrite c m Clause

Rewrite all children of a clause of the form: : Conj Clause Clause

disjT :: (ExtendPath c Crumb, Monad m) => Transform c m Clause a1 -> Transform c m Clause a2 -> (a1 -> a2 -> b) -> Transform c m Clause b

Transform a clause of the form: Disj Clause Clause

disjAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m Clause -> Rewrite c m Clause -> Rewrite c m Clause

Rewrite all children of a clause of the form: : Disj Clause Clause

implT :: (ExtendPath c Crumb, LemmaContext c, Monad m) => Transform c m Clause a1 -> Transform c m Clause a2 -> (LemmaName -> a1 -> a2 -> b) -> Transform c m Clause b

Transform a clause of the form: Impl LemmaName Clause Clause

implAllR :: (ExtendPath c Crumb, LemmaContext c, Monad m) => Rewrite c m Clause -> Rewrite c m Clause -> Rewrite c m Clause

Rewrite all children of a clause of the form: : Impl Clause Clause

equivT :: (ExtendPath c Crumb, Monad m) => Transform c m CoreExpr a1 -> Transform c m CoreExpr a2 -> (a1 -> a2 -> b) -> Transform c m Clause b

Transform a clause of the form: Equiv CoreExpr CoreExpr

equivAllR :: (ExtendPath c Crumb, Monad m) => Rewrite c m CoreExpr -> Rewrite c m CoreExpr -> Rewrite c m Clause

Rewrite all children of a clause of the form: : Equiv CoreExpr CoreExpr

forallT :: (ExtendPath c Crumb, AddBindings c, ReadPath c Crumb, Monad m) => Transform c m [CoreBndr] a1 -> Transform c m Clause a2 -> (a1 -> a2 -> b) -> Transform c m Clause b

Transform a clause of the form: Forall '[CoreBndr]' Clause

forallR :: (ExtendPath c Crumb, AddBindings c, ReadPath c Crumb, Monad m) => Rewrite c m [CoreBndr] -> Rewrite c m Clause -> Rewrite c m Clause

Rewrite the a clause of the form: Forall '[CoreBndr]' Clause

Applicative

(<$>) :: Monad m => (a -> b) -> m a -> m b

(<*>) :: Monad m => m (a -> b) -> m a -> m b