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

Safe HaskellNone
LanguageHaskell2010

HERMIT.Context

Contents

Synopsis

HERMIT Contexts

Path Synonyms

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.

Instances

HasEmptyContext HermitC

The |HermitC| empty context has an initial depth of 0, an empty path, and no bindings nor rules.

HasCoreRules HermitC 
ReadBindings HermitC 
BoundVars HermitC 
AddBindings HermitC 
ExtendPath HermitC Crumb

Extend the AbsolutePath stored in the HERMIT context.

ReadPath HermitC Crumb

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

Extern [RewriteH LCoreTC] 
Extern [RewriteH LCore] 
Extern (BiRewriteH LCoreTC) 
Extern (BiRewriteH LCore) 
Extern (RewriteH LCoreTC) 
Extern (RewriteH LCore) 
Extern (RewriteH Equality) 
Extern (TransformH LCoreTC String) 
Extern (TransformH LCoreTC ()) 
Extern (TransformH LCoreTC LocalPathH) 
Extern (TransformH LCoreTC LCore) 
Extern (TransformH LCoreTC DocH) 
Extern (TransformH LCore String) 
Extern (TransformH LCore ()) 
Extern (TransformH LCore LocalPathH) 
Extern (TransformH LCore DocH) 
Extern (TransformH Equality String) 
Extern (TransformH Equality ()) 
type Box [RewriteH LCoreTC] = RewriteLCoreTCListBox 
type Box [RewriteH LCore] = RewriteLCoreListBox 
type Box (BiRewriteH LCoreTC) = BiRewriteLCoreTCBox 
type Box (BiRewriteH LCore) = BiRewriteLCoreBox 
type Box (RewriteH LCoreTC) = RewriteLCoreTCBox 
type Box (RewriteH LCore) = RewriteLCoreBox 
type Box (RewriteH Equality) 
type Box (TransformH LCoreTC String) = TransformLCoreTCStringBox 
type Box (TransformH LCoreTC ()) = TransformLCoreTCUnitBox 
type Box (TransformH LCoreTC LocalPathH) = TransformLCoreTCPathBox 
type Box (TransformH LCoreTC LCore) = TransformLCoreTCLCoreBox 
type Box (TransformH LCoreTC DocH) = TransformLCoreTCDocHBox 
type Box (TransformH LCore String) = TransformLCoreStringBox 
type Box (TransformH LCore ()) = TransformLCoreUnitBox 
type Box (TransformH LCore LocalPathH) = TransformLCorePathBox 
type Box (TransformH LCore DocH) = TransformLCoreDocHBox 
type Box (TransformH Equality String) 
type Box (TransformH Equality ()) 

topLevelHermitC :: ModGuts -> HermitC Source

A special HERMIT context intended for use only when focussed on ModGuts. All top-level bindings are considered to be in scope at depth 0.

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

LAM

A lambda-bound variable.

NONREC CoreExpr

A non-recursive binding of an expression.

REC CoreExpr

A recursive binding that does not depend on the current expression (i.e. we're not in the binding group of that binding).

SELFREC

A recursive binding of a superexpression of the current node (i.e. we're in the RHS of that binding).

MUTUALREC CoreExpr

A recursive binding that is mutually recursive with the binding under consideration (i.e. we're in another definition in the same recursive binding group.).

CASEALT

A variable bound in a case alternative.

CASEBINDER CoreExpr (AltCon, [Var])

A case binder. We store both the scrutinised expression, and the case alternative AltCon and variables.

FORALL

A universally quantified type variable.

TOPLEVEL CoreExpr

A special case. When we're focussed on ModGuts, we treat all top-level bindings as being in scope at depth 0.

type BindingDepth = Int Source

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

hermitBindingSiteExpr :: HermitBindingSite -> KureM CoreExpr Source

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

hermitBindingExpr :: HermitBinding -> KureM CoreExpr Source

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

Adding bindings to contexts

class AddBindings c where Source

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

Methods

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

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)

The bindings are just discarded.

(AddBindings c, AddBindings e) => AddBindings (ExtendContext c e)

The bindings are added to the base context and the extra context.

addBindingGroup :: (AddBindings c, ReadPath c Crumb) => CoreBind -> c -> c Source

Add all bindings in a binding group to a context.

addDefBinding :: (AddBindings c, ReadPath c Crumb) => Id -> c -> c Source

Add the binding for a recursive definition currently under examination. Note that because the expression may later be modified, the context only records the identifier, not the expression.

addDefBindingsExcept :: (AddBindings c, ReadPath c Crumb) => Int -> [(Id, CoreExpr)] -> c -> c Source

Add a list of recursive bindings to the context, except the nth binding in the list. The idea is to exclude the definition being descended into.

addLambdaBinding :: (AddBindings c, ReadPath c Crumb) => Var -> c -> c Source

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, ReadPath c Crumb) => [Var] -> c -> c Source

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

addCaseBinderBinding :: (AddBindings c, ReadPath c Crumb) => (Id, CoreExpr, CoreAlt) -> c -> c Source

Add the case binder for a specific case alternative.

addForallBinding :: (AddBindings c, ReadPath c Crumb) => TyVar -> c -> c Source

Add a universally quantified type variable to a context.

Reading bindings from the context

class BoundVars c where Source

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

Methods

boundVars :: c -> VarSet Source

boundIn :: ReadBindings c => Var -> c -> Bool Source

Determine if a variable is bound in a context.

findBoundVars :: BoundVars c => (Var -> Bool) -> c -> VarSet Source

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

class BoundVars c => ReadBindings c where Source

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

lookupHermitBinding :: (ReadBindings c, Monad m) => Var -> c -> m HermitBinding Source

Lookup the binding for a variable in a context.

lookupHermitBindingDepth :: (ReadBindings c, Monad m) => Var -> c -> m BindingDepth Source

Lookup the depth of a variable's binding in a context.

lookupHermitBindingSite :: (ReadBindings c, Monad m) => Var -> BindingDepth -> c -> m HermitBindingSite Source

Lookup the binding for a variable in a context, ensuring it was bound at the specified depth.

inScope :: BoundVars c => c -> Var -> Bool Source

Determine whether a variable is in scope.

Accessing GHC rewrite rules from the context

class HasCoreRules c where Source

A class of contexts that store GHC rewrite rules.

An empty Context

class HasEmptyContext c where Source

A class of contexts that provide an empty context.

Methods

setEmptyContext :: c -> c Source

Instances

HasEmptyContext HermitC

The |HermitC| empty context has an initial depth of 0, an empty path, and no bindings nor rules.

HasEmptyContext PrettyC 
HasEmptyContext c => HasEmptyContext (ExtendContext c (LocalPath Crumb))