HERMIT.Core

Generic Data Type

data CoreProg

A program is a telescope of nested binding groups. That is, each binding scopes over the remainder of the program. In GHC Core, programs are encoded as [CoreBind]. This data type is isomorphic.

Constructors

ProgNil

An empty program.

ProgCons CoreBind CoreProg

A binding group and the program it scopes over.

Instances

Injection CoreProg CoreTC

Injection CoreProg Core

data CoreDef

A (potentially recursive) definition is an identifier and an expression. In GHC Core, recursive definitions are encoded as (Id, CoreExpr) pairs. This data type is isomorphic.

Constructors

Def Id CoreExpr

Instances

Injection CoreDef CoreTC

Injection CoreDef Core

type CoreTickish = Tickish Id

Unlike everything else, there is no synonym for Tickish Id provided by GHC, so we define one.

Equality

We define both syntactic equality and alpha equality.

Syntactic Equality

progSyntaxEq :: CoreProg -> CoreProg -> Bool

Syntactic Equality of programs.

bindSyntaxEq :: CoreBind -> CoreBind -> Bool

Syntactic Equality of binding groups.

defSyntaxEq :: CoreDef -> CoreDef -> Bool

Syntactic Equality of recursive definitions.

exprSyntaxEq :: CoreExpr -> CoreExpr -> Bool

Syntactic Equality of expressions.

altSyntaxEq :: CoreAlt -> CoreAlt -> Bool

Syntactic Equality of case alternatives.

typeSyntaxEq :: Type -> Type -> Bool

Syntactic Equality of Types.

coercionSyntaxEq :: Coercion -> Coercion -> Bool

Syntactic Equality of Coercions.

Alpha Equality

progAlphaEq :: CoreProg -> CoreProg -> Bool

Alpha equality of programs.

bindAlphaEq :: CoreBind -> CoreBind -> Bool

Alpha equality of binding groups.

defAlphaEq :: CoreDef -> CoreDef -> Bool

Alpha equality of recursive definitions.

exprAlphaEq :: CoreExpr -> CoreExpr -> Bool

Alpha equality of expressions.

altAlphaEq :: CoreAlt -> CoreAlt -> Bool

Alpha equality of case alternatives.

typeAlphaEq :: Type -> Type -> Bool

Alpha equality of types.

coercionAlphaEq :: Coercion -> Coercion -> Bool

Alpha equality of coercions.

Conversions to/from Core

defsToRecBind :: [CoreDef] -> CoreBind

Convert a list of recursive definitions into an (isomorphic) recursive binding group.

defToIdExpr :: CoreDef -> (Id, CoreExpr)

Convert a definition to an identifier/expression pair.

progToBinds :: CoreProg -> [CoreBind]

Get the list of bindings in a program.

bindsToProg :: [CoreBind] -> CoreProg

Build a program from a list of bindings. Note that bindings earlier in the list are considered scope over bindings later in the list.

bindToVarExprs :: CoreBind -> [(Var, CoreExpr)]

Extract the list of identifier/expression pairs from a binding group.

Collecting variable bindings

progIds :: CoreProg -> [Id]

List all identifiers bound at the top-level in a program.

bindVars :: CoreBind -> [Var]

List all variables bound in a binding group.

defId :: CoreDef -> Id

Return the identifier bound by a recursive definition.

altVars :: CoreAlt -> [Var]

List the variables bound by a case alternative.

Collecting free variables

The GHC Function exprFreeVars defined in CoreFVs only returns *locally-defined* free variables. In HERMIT, this is typically not what we want, so we define our own functions. We reuse some of the functionality in CoreFVs, but alas much of it is not exposed, so we have to reimplement some of it.

freeVarsProg :: CoreProg -> VarSet

Find all free variables in a program.

freeVarsBind :: CoreBind -> VarSet

Find all free identifiers in a binding group, which excludes any variables bound in the group.

freeVarsDef :: CoreDef -> VarSet

Find all free variables is a recursive definition, which excludes the bound variable.

freeVarsExpr :: CoreExpr -> VarSet

Find all free variables in an expression.

freeVarsAlt :: CoreAlt -> VarSet

Find all free variables in a case alternative, which excludes any variables bound in the alternative.

freeVarsType :: Type -> TyVarSet

Find all free variables in a type.

freeVarsCoercion :: Coercion -> VarSet

Find all free variables in a coercion.

localFreeVarsExpr :: CoreExpr -> VarSet

Find all locally defined free variables in an expression.

freeIdsExpr :: CoreExpr -> IdSet

Find all free identifiers in an expression.

localFreeIdsExpr :: CoreExpr -> VarSet

Find all locally defined free identifiers in an expression.

Utilities

isCoArg :: CoreExpr -> Bool

Returns True iff the expression is a Coercion expression at its top level.

exprKindOrType :: CoreExpr -> KindOrType

GHC's exprType function throws an error if applied to a Type. This function returns the Kind of a Type, but otherwise behaves as exprType.

exprTypeM :: Monad m => CoreExpr -> m Type

GHC's exprType function throws an error if applied to a Type. This function catches that case as failure in an arbitrary monad.

endoFunType :: Monad m => CoreExpr -> m Type

Return the domain/codomain type of an endofunction expression.

splitFunTypeM :: Monad m => Type -> m (Type, Type)

Return the domain and codomain types of a function type, if it is a function type.

funArgResTypes :: Monad m => CoreExpr -> m (Type, Type)

Return the domain and codomain types of a function expression.

funsWithInverseTypes :: MonadCatch m => CoreExpr -> CoreExpr -> m (Type, Type)

Check two expressions have types a -> b and b -> a, returning (a,b).

appCount :: CoreExpr -> Int

Count the number of nested applications.

mapAlts :: (CoreExpr -> CoreExpr) -> [CoreAlt] -> [CoreAlt]

Map a function over the RHS of each case alternative.

Crumbs

data Crumb

Crumbs record a path through the tree, using descriptive constructor names.

Constructors

ModGuts_Prog

ProgCons_Head

ProgCons_Tail

NonRec_RHS

NonRec_Var

Rec_Def Int

Def_Id

Def_RHS

Var_Id

Lit_Lit

App_Fun

App_Arg

Lam_Var

Lam_Body

Let_Bind

Let_Body

Case_Scrutinee

Case_Binder

Case_Type

Case_Alt Int

Cast_Expr

Cast_Co

Tick_Tick

Tick_Expr

Type_Type

Co_Co

Alt_Con

Alt_Var Int

Alt_RHS

TyVarTy_TyVar

LitTy_TyLit

AppTy_Fun

AppTy_Arg

TyConApp_TyCon

TyConApp_Arg Int

FunTy_Dom

FunTy_CoDom

ForAllTy_Var

ForAllTy_Body

Refl_Type

TyConAppCo_TyCon

TyConAppCo_Arg Int

AppCo_Fun

AppCo_Arg

ForAllCo_TyVar

ForAllCo_Body

CoVarCo_CoVar

AxiomInstCo_Axiom

AxiomInstCo_Index

AxiomInstCo_Arg Int

UnsafeCo_Left

UnsafeCo_Right

SymCo_Co

TransCo_Left

TransCo_Right

NthCo_Int

NthCo_Co

InstCo_Co

InstCo_Type

LRCo_LR

LRCo_Co

Instances

Eq Crumb

Read Crumb

Show Crumb

Extern Crumb

Extern LocalPathH

ExtendPath HermitC Crumb

Extend the AbsolutePath stored in the HERMIT context.

ExtendPath PrettyC Crumb

ReadPath HermitC Crumb

Retrieve the AbsolutePath to the current node, from the HERMIT context.

ReadPath PrettyC Crumb

Extern (TranslateH CoreTC LocalPathH)

Extern (TranslateH Core LocalPathH)

showCrumbs :: [Crumb] -> String

deprecatedLeftSibling :: Crumb -> Maybe Crumb

Converts a Crumb into the Crumb pointing to its left-sibling, if a such a Crumb exists. This is for backwards compatibility purposes with the old Int representation.

deprecatedRightSibling :: Crumb -> Maybe Crumb

Converts a Crumb into the Crumb pointing to its right-sibling, if a such a Crumb exists. This is for backwards compatibility purposes with the old Int representation.