HERMIT.Kure.Universes

Universes

data Core

Core is a KURE universe for traversing GHC Core, excluding types and coercions. Core = ModGuts + CoreProg + CoreBind + CoreDef + CoreExpr + CoreAlt

Constructors

GutsCore ModGuts

The module.

ProgCore CoreProg

A program (a telescope of top-level binding groups).

BindCore CoreBind

A binding group.

DefCore CoreDef

A recursive definition.

ExprCore CoreExpr

An expression.

AltCore CoreAlt

A case alternative.

Instances

(ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, HasEmptyContext c) => Walker c Core

Walking over modules, programs, binding groups, definitions, expressions and case alternatives.

Injection ModGuts Core

Injection CoreExpr Core

Injection CoreBind Core

Injection CoreAlt Core

Injection CoreDef Core

Injection CoreProg Core

Injection Core LCoreTC

Injection Core LCore

Injection Core CoreTC

data TyCo

TyCo is a KURE universe for traversing types and coercions. TyCo = Type + Coercion

Constructors

TypeCore Type

A type.

CoercionCore Coercion

A coercion.

Instances

(ExtendPath c Crumb, ReadPath c Crumb, AddBindings c) => Walker c TyCo

Walking over types and coercions.

Injection Coercion TyCo

Injection Type TyCo

Injection TyCo LCoreTC

Injection TyCo CoreTC

data LCore

LCore is a KURE universe for traversing HERMIT lemmas and the Core expressions they contain. Types and coercions are not traversed (for that, use LCoreTC). LCore = Core + Quantified + Clause

Constructors

LQuantified Quantified

LClause Clause

LCore Core

Instances

(AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadPath c Crumb) => Walker c LCore

Walking over modules, programs, binding groups, definitions, expressions, case alternatives, lemma quantifiers and lemma clauses.

Injection ModGuts LCore

Injection CoreExpr LCore

Injection CoreBind LCore

Injection CoreAlt LCore

Injection CoreDef LCore

Injection CoreProg LCore

Injection Clause LCore

Injection Quantified LCore

Injection LCore LCoreTC

Injection Core LCore

Extern [RewriteH LCore]

Extern (BiRewriteH LCore)

Extern (RewriteH LCore)

Extern (PrettyH LCore)

Extern (TransformH LCoreTC LCore)

Extern (TransformH LCore String)

Extern (TransformH LCore ())

Extern (TransformH LCore LocalPathH)

Extern (TransformH LCore DocH)

type Box [RewriteH LCore] = RewriteLCoreListBox

type Box (BiRewriteH LCore) = BiRewriteLCoreBox

type Box (RewriteH LCore) = RewriteLCoreBox

type Box (PrettyH LCore) = PrettyHLCoreBox

type Box (TransformH LCoreTC LCore) = TransformLCoreTCLCoreBox

type Box (TransformH LCore String) = TransformLCoreStringBox

type Box (TransformH LCore ()) = TransformLCoreUnitBox

type Box (TransformH LCore LocalPathH) = TransformLCorePathBox

type Box (TransformH LCore DocH) = TransformLCoreDocHBox

data LCoreTC

LCoreTC is a KURE universe for traversing HERMIT lemmas and the Core expressions they contain. Unlike LCore, types and coercions are also traversed. LCore = LCore + TyCo

Constructors

LTCCore LCore

LTCTyCo TyCo

Instances

(AddBindings c, ExtendPath c Crumb, HasEmptyContext c, ReadPath c Crumb) => Walker c LCoreTC

Walking over modules, programs, binding groups, definitions, expressions, case alternatives, types, coercions, lemma quantifiers and lemma clauses.

Injection ModGuts LCoreTC

Injection CoreExpr LCoreTC

Injection CoreBind LCoreTC

Injection CoreAlt LCoreTC

Injection Coercion LCoreTC

Injection Type LCoreTC

Injection CoreDef LCoreTC

Injection CoreProg LCoreTC

Injection Clause LCoreTC

Injection Quantified LCoreTC

Injection LCore LCoreTC

Injection CoreTC LCoreTC

Injection TyCo LCoreTC

Injection Core LCoreTC

Extern [RewriteH LCoreTC]

Extern (BiRewriteH LCoreTC)

Extern (RewriteH LCoreTC)

Extern (PrettyH LCoreTC)

Extern (TransformH LCoreTC String)

Extern (TransformH LCoreTC ())

Extern (TransformH LCoreTC LocalPathH)

Extern (TransformH LCoreTC LCore)

Extern (TransformH LCoreTC DocH)

type Box [RewriteH LCoreTC] = RewriteLCoreTCListBox

type Box (BiRewriteH LCoreTC) = BiRewriteLCoreTCBox

type Box (RewriteH LCoreTC) = RewriteLCoreTCBox

type Box (PrettyH LCoreTC) = PrettyHLCoreTCBox

type Box (TransformH LCoreTC String) = TransformLCoreTCStringBox

type Box (TransformH LCoreTC ()) = TransformLCoreTCUnitBox

type Box (TransformH LCoreTC LocalPathH) = TransformLCoreTCPathBox

type Box (TransformH LCoreTC LCore) = TransformLCoreTCLCoreBox

type Box (TransformH LCoreTC DocH) = TransformLCoreTCDocHBox

data CoreTC

Core is a KURE universe for traversing GHC Core, including types and coercions. CoreTC = Core + TyCo

Constructors

Core Core

TyCo TyCo

Instances

(ExtendPath c Crumb, ReadPath c Crumb, AddBindings c, HasEmptyContext c) => Walker c CoreTC

Walking over modules, programs, binding groups, definitions, expressions, case alternatives, types and coercions.

Injection ModGuts CoreTC

Injection CoreExpr CoreTC

Injection CoreBind CoreTC

Injection CoreAlt CoreTC

Injection Coercion CoreTC

Injection Type CoreTC

Injection CoreDef CoreTC

Injection CoreProg CoreTC

Injection CoreTC LCoreTC

Injection TyCo CoreTC

Injection Core CoreTC

Equality

Syntactic Equality

coreSyntaxEq :: Core -> Core -> Bool

Syntactic equality of Core fragments.

tyCoSyntaxEq :: TyCo -> TyCo -> Bool

Syntactic equality of TyCo fragments.

coreTCSyntaxEq :: CoreTC -> CoreTC -> Bool

Syntactic equality of CoreTC fragments.

lcoreSyntaxEq :: LCore -> LCore -> Bool

Syntactic equality of LCore fragments.

lcoreTCSyntaxEq :: LCoreTC -> LCoreTC -> Bool

Syntactic equality of LCoreTC fragments.

Alpha Equality

coreAlphaEq :: Core -> Core -> Bool

Alpha equality of Core fragments.

tyCoAlphaEq :: TyCo -> TyCo -> Bool

Alpha equality of TyCo fragments.

coreTCAlphaEq :: CoreTC -> CoreTC -> Bool

Alpha equality of CoreTC fragments.

Collecting Free Variables

freeVarsCore :: Core -> VarSet

Find all free variables in a Core node.

freeVarsTyCo :: TyCo -> VarSet

Find all free variables in a TyCo node.

freeVarsCoreTC :: CoreTC -> VarSet

Find all free variables in a CoreTC node.

Promotion Combinators

Transform Promotions

promoteModGutsT :: (Monad m, Injection ModGuts g) => Transform c m ModGuts b -> Transform c m g b

Promote a translate on ModGuts.

promoteProgT :: (Monad m, Injection CoreProg g) => Transform c m CoreProg b -> Transform c m g b

Promote a translate on CoreProg.

promoteBindT :: (Monad m, Injection CoreBind g) => Transform c m CoreBind b -> Transform c m g b

Promote a translate on CoreBind.

promoteDefT :: (Monad m, Injection CoreDef g) => Transform c m CoreDef b -> Transform c m g b

Promote a translate on CoreDef.

promoteExprT :: (Monad m, Injection CoreExpr g) => Transform c m CoreExpr b -> Transform c m g b

Promote a translate on CoreExpr.

promoteAltT :: (Monad m, Injection CoreAlt g) => Transform c m CoreAlt b -> Transform c m g b

Promote a translate on CoreAlt.

promoteTypeT :: (Monad m, Injection Type g) => Transform c m Type b -> Transform c m g b

Promote a translate on Type.

promoteCoercionT :: (Monad m, Injection Coercion g) => Transform c m Coercion b -> Transform c m g b

Promote a translate on Coercion.

promoteQuantifiedT :: (Monad m, Injection Quantified g) => Transform c m Quantified b -> Transform c m g b

Promote a translate on Quantified.

promoteClauseT :: (Monad m, Injection Clause g) => Transform c m Clause b -> Transform c m g b

Promote a translate on Clause.

promoteCoreT :: (Monad m, Injection Core g) => Transform c m Core b -> Transform c m g b

Promote a translate on Core.

promoteLCoreT :: (Monad m, Injection LCore g) => Transform c m LCore b -> Transform c m g b

Promote a translate on LCore.

promoteCoreTCT :: (Monad m, Injection CoreTC g) => Transform c m CoreTC b -> Transform c m g b

Promote a translate on CoreTC.

Rewrite Promotions

promoteModGutsR :: (Monad m, Injection ModGuts g) => Rewrite c m ModGuts -> Rewrite c m g

Promote a rewrite on ModGuts.

promoteProgR :: (Monad m, Injection CoreProg g) => Rewrite c m CoreProg -> Rewrite c m g

Promote a rewrite on CoreProg.

promoteBindR :: (Monad m, Injection CoreBind g) => Rewrite c m CoreBind -> Rewrite c m g

Promote a rewrite on CoreBind.

promoteDefR :: (Monad m, Injection CoreDef g) => Rewrite c m CoreDef -> Rewrite c m g

Promote a rewrite on CoreDef.

promoteExprR :: (Monad m, Injection CoreExpr g) => Rewrite c m CoreExpr -> Rewrite c m g

Promote a rewrite on CoreExpr.

promoteAltR :: (Monad m, Injection CoreAlt g) => Rewrite c m CoreAlt -> Rewrite c m g

Promote a rewrite on CoreAlt.

promoteTypeR :: (Monad m, Injection Type g) => Rewrite c m Type -> Rewrite c m g

Promote a rewrite on Type.

promoteCoercionR :: (Monad m, Injection Coercion g) => Rewrite c m Coercion -> Rewrite c m g

Promote a rewrite on Coercion.

promoteQuantifiedR :: (Monad m, Injection Quantified g) => Rewrite c m Quantified -> Rewrite c m g

Promote a rewrite on Quantified.

promoteClauseR :: (Monad m, Injection Clause g) => Rewrite c m Clause -> Rewrite c m g

Promote a rewrite on Clause.

promoteCoreR :: (Monad m, Injection Core g) => Rewrite c m Core -> Rewrite c m g

Promote a rewrite on Core.

promoteLCoreR :: (Monad m, Injection LCore g) => Rewrite c m LCore -> Rewrite c m g

Promote a rewrite on Core.

promoteCoreTCR :: (Monad m, Injection CoreTC g) => Rewrite c m CoreTC -> Rewrite c m g

Promote a rewrite on CoreTC.

BiRewrite Promotions

promoteExprBiR :: (Monad m, Injection CoreExpr g) => BiRewrite c m CoreExpr -> BiRewrite c m g

Promote a bidirectional rewrite on CoreExpr.