hermit-1.0.0.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone
LanguageHaskell2010

HERMIT.Core

Contents

Synopsis

Generic Data Type

data CoreProg Source

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 infixr 5

A binding group and the program it scopes over.

data CoreDef Source

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 

type CoreTickish = Tickish Id Source

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 Source

Syntactic Equality of programs.

bindSyntaxEq :: CoreBind -> CoreBind -> Bool Source

Syntactic Equality of binding groups.

defSyntaxEq :: CoreDef -> CoreDef -> Bool Source

Syntactic Equality of recursive definitions.

exprSyntaxEq :: CoreExpr -> CoreExpr -> Bool Source

Syntactic Equality of expressions.

altSyntaxEq :: CoreAlt -> CoreAlt -> Bool Source

Syntactic Equality of case alternatives.

typeSyntaxEq :: Type -> Type -> Bool Source

Syntactic Equality of Types.

coercionSyntaxEq :: Coercion -> Coercion -> Bool Source

Syntactic Equality of Coercions.

Alpha Equality

progAlphaEq :: CoreProg -> CoreProg -> Bool Source

Alpha equality of programs.

bindAlphaEq :: CoreBind -> CoreBind -> Bool Source

Alpha equality of binding groups.

defAlphaEq :: CoreDef -> CoreDef -> Bool Source

Alpha equality of recursive definitions.

exprAlphaEq :: CoreExpr -> CoreExpr -> Bool Source

Alpha equality of expressions.

altAlphaEq :: CoreAlt -> CoreAlt -> Bool Source

Alpha equality of case alternatives.

typeAlphaEq :: Type -> Type -> Bool Source

Alpha equality of types.

coercionAlphaEq :: Coercion -> Coercion -> Bool Source

Alpha equality of coercions.

Conversions to/from Core

defsToRecBind :: [CoreDef] -> CoreBind Source

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

defToIdExpr :: CoreDef -> (Id, CoreExpr) Source

Convert a definition to an identifier/expression pair.

progToBinds :: CoreProg -> [CoreBind] Source

Get the list of bindings in a program.

bindsToProg :: [CoreBind] -> CoreProg Source

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)] Source

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

Collecting variable bindings

progIds :: CoreProg -> [Id] Source

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

bindVars :: CoreBind -> [Var] Source

List all variables bound in a binding group.

defId :: CoreDef -> Id Source

Return the identifier bound by a recursive definition.

altVars :: CoreAlt -> [Var] Source

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. We do not use GHC's exprSomeFreeVars because it does not return the full set of free vars for a Var. It only returns the Var itself, rather than extendVarSet (freeVarsVar v) v like it should.

freeVarsProg :: CoreProg -> VarSet Source

Find all free variables in a program.

freeVarsBind :: CoreBind -> VarSet Source

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

freeVarsDef :: CoreDef -> VarSet Source

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

freeVarsExpr :: CoreExpr -> VarSet Source

Find all free variables in an expression.

freeVarsAlt :: CoreAlt -> VarSet Source

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

freeVarsVar :: Var -> VarSet Source

Find all free variables on a binder. Equivalent to idFreeVars, but safe to call on type bindings.

localFreeVarsAlt :: CoreAlt -> VarSet Source

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

freeVarsType :: Type -> TyVarSet Source

Find all free variables in a type.

freeVarsCoercion :: Coercion -> VarSet Source

Find all free variables in a coercion.

localFreeVarsExpr :: CoreExpr -> VarSet Source

Find all locally defined free variables in an expression.

freeIdsExpr :: CoreExpr -> IdSet Source

Find all free identifiers in an expression.

localFreeIdsExpr :: CoreExpr -> VarSet Source

Find all locally defined free identifiers in an expression.

Utilities

isCoArg :: CoreExpr -> Bool Source

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

exprKindOrType :: CoreExpr -> KindOrType Source

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 Source

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

endoFunTypeM :: MonadCatch m => Type -> m ([TyVar], Type) Source

Return the domain/codomain type of an endofunction type.

splitTyConAppM :: Monad m => Type -> m (TyCon, [Type]) Source

As splitTyConApp, catching failure in a monad.

splitFunTypeM :: MonadCatch m => Type -> m ([TyVar], Type, Type) Source

Get the quantified variables, domain, and codomain of a function type.

endoFunExprTypeM :: MonadCatch m => CoreExpr -> m ([TyVar], Type) Source

Return the domain/codomain type of an endofunction expression.

funExprArgResTypesM :: MonadCatch m => CoreExpr -> m ([TyVar], Type, Type) Source

Return the domain and codomain types of a function expression.

funExprsWithInverseTypes :: MonadCatch m => CoreExpr -> CoreExpr -> m (Type, Type) Source

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

appCount :: CoreExpr -> Int Source

Count the number of nested applications.

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

Map a function over the RHS of each case alternative.

substCoreAlt :: Var -> CoreExpr -> CoreAlt -> CoreAlt Source

Substitute all occurrences of a variable with an expression, in a case alternative.

substCoreExpr :: Var -> CoreExpr -> CoreExpr -> CoreExpr Source

Substitute all occurrences of a variable with an expression, in an expression.

betaReduceAll :: CoreExpr -> [CoreExpr] -> (CoreExpr, [CoreExpr]) Source

Beta-reduce as many lambda-binders as possible.

mkDataConApp :: [Type] -> DataCon -> [Var] -> CoreExpr Source

Build a constructor application. Accepts a list of types to which the type constructor is instantiated. Ex.

data T a b = C a b Int

Pseudocode:

mkDataConApp [a',b'] C [x,y,z] ==> C a' b' (x::a') (y::b') (z::Int) :: T a' b'

Crumbs

data Crumb Source

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

leftSibling :: Crumb -> Maybe Crumb Source

Converts a Crumb into the Crumb pointing to its left-sibling, if a such a Crumb exists. This is used for moving left in the shell.

rightSibling :: Crumb -> Maybe Crumb Source

Converts a Crumb into the Crumb pointing to its right-sibling, if a such a Crumb exists. This is used for moving right in the shell.