HERMIT.Kure.SumTypes

Sum Types

data Core

Core is a sum type for use by KURE. 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 CoreTC

Extern [RewriteH Core]

Extern (BiRewriteH Core)

Extern (RewriteH Core)

Extern (TransformH Core String)

Extern (TransformH Core ())

Extern (TransformH Core LocalPathH)

type Box [RewriteH Core] = RewriteCoreListBox

type Box (BiRewriteH Core) = BiRewriteCoreBox

type Box (RewriteH Core) = RewriteCoreBox

type Box (TransformH Core String) = TransformCoreStringBox

type Box (TransformH Core ()) = TransformCoreCheckBox

type Box (TransformH Core LocalPathH) = TransformCorePathBox

data TyCo

TyCo is a sum type for use by KURE. 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 CoreTC

data CoreTC

CoreTC is a sum type for use by KURE. 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 and case alternatives.

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 TyCo CoreTC

Injection Core CoreTC

Extern (RewriteH CoreTC)

Extern (TransformDocH CoreTC)

Extern (TransformH CoreTC String)

Extern (TransformH CoreTC ())

Extern (TransformH CoreTC LocalPathH)

type Box (RewriteH CoreTC) = RewriteCoreTCBox

type Box (TransformDocH CoreTC) = TransformCoreTCDocHBox

type Box (TransformH CoreTC String) = TransformCoreTCStringBox

type Box (TransformH CoreTC ()) = TransformCoreTCCheckBox

type Box (TransformH CoreTC LocalPathH) = TransformCoreTCPathBox

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.

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.

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.

BiRewrite Promotions

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

Promote a bidirectional rewrite on CoreExpr.