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

Safe HaskellNone

Language.HERMIT.Context

Contents

Synopsis

HERMIT Contexts

The Standard Context

data HermitC Source

The HERMIT context, containing all bindings in scope and the current location in the AST. The bindings here are lazy by choice, so that we can avoid the cost of building the context if we never use it.

initHermitC :: ModGuts -> HermitCSource

Create the initial HERMIT HermitC by providing a ModGuts.

Bindings

data HermitBindingSite Source

HERMIT's representation of variable bindings. Bound expressions cannot be inlined without checking for shadowing issues (using the depth information).

Constructors

REC CoreExpr 
NONREC CoreExpr 
LAM 
CASEALT 
FORALL 
CASEWILD CoreExpr (AltCon, [Var])

We store both the scrutinised expression, and the case alternative AltCon (which can be converted to Constructor or Literal) and variables.

type BindingDepth = IntSource

The depth of a binding. Used, for example, to detect shadowing when inlining.

hermitBindingSiteExpr :: HermitBindingSite -> Maybe CoreExprSource

Retrieve the expression in a HermitBindingSite, if there is one.

hermitBindingExpr :: HermitBinding -> Maybe CoreExprSource

Retrieve the expression in a HermitBinding, if there is one.

Adding bindings to contexts

class AddBindings c whereSource

A class of contexts that can have HERMIT bindings added to them.

Methods

addHermitBindings :: [(Var, HermitBindingSite)] -> c -> cSource

Add a complete set of parrallel bindings to the context. (Parallel bindings occur in recursive let bindings and case alternatives.) This can also be used for solitary bindings (e.g. lambdas). Bindings are added in parallel sets to help with shadowing issues.

Instances

AddBindings HermitC 
AddBindings PrettyC 
AddBindings (SnocPath crumb)

Here the bindings are just discarded.

addBindingGroup :: AddBindings c => CoreBind -> c -> cSource

Add all bindings in a binding group to a context.

addLambdaBinding :: AddBindings c => Var -> c -> cSource

Add a lambda bound variable to a context. All that is known is the variable, which may shadow something. If so, we don't worry about that here, it is instead checked during inlining.

addAltBindings :: AddBindings c => [Var] -> c -> cSource

Add the variables bound by a DataCon in a case. They are all bound at the same depth.

addCaseWildBinding :: AddBindings c => (Id, CoreExpr, CoreAlt) -> c -> cSource

Add a wildcard binding for a specific case alternative.

addForallBinding :: AddBindings c => TyVar -> c -> cSource

Add a universally quantified type variable to a context.

Reading bindings from the context

class BoundVars c whereSource

A class of contexts that stores the set of variables in scope that have been bound during the traversal.

Methods

boundVars :: c -> Set VarSource

boundIn :: ReadBindings c => Var -> c -> BoolSource

Determine if a variable is bound in a context.

findBoundVars :: BoundVars c => Name -> c -> [Var]Source

List all variables bound in the context that match the given name.

class BoundVars c => ReadBindings c whereSource

A class of contexts from which HERMIT bindings can be retrieved.

lookupHermitBinding :: ReadBindings c => Var -> c -> Maybe HermitBindingSource

Lookup the binding for a variable in a context.

Accessing the Global Reader Environment from the context

class HasGlobalRdrEnv c whereSource

A class of contexts that store the Global Reader Environment.

Accessing GHC rewrite rules from the context

class HasCoreRules c whereSource

A class of contexts that store GHC rewrite rules.