Language.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.

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.

bindToIdExprs :: CoreBind -> [(Id, CoreExpr)]

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

Utilities

isCoArg :: CoreExpr -> Bool

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

exprTypeOrKind :: CoreExpr -> Type

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

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

Return the domain/codomain type of an endofunction expression.

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.

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 PathH

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 Core PathH)

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.