Safe Haskell | None |
---|---|
Language | Haskell2010 |
- type AbsolutePathH = AbsolutePath Crumb
- type LocalPathH = LocalPath Crumb
- data HermitC
- topLevelHermitC :: ModGuts -> HermitC
- toHermitC :: (HasCoreRules c, LemmaContext c, ReadBindings c, ReadPath c Crumb) => c -> HermitC
- data HermitBindingSite
- type BindingDepth = Int
- data HermitBinding
- hbDepth :: HermitBinding -> BindingDepth
- hbSite :: HermitBinding -> HermitBindingSite
- hbPath :: HermitBinding -> AbsolutePathH
- hermitBindingSiteExpr :: HermitBindingSite -> KureM CoreExpr
- hermitBindingSummary :: HermitBinding -> String
- hermitBindingExpr :: HermitBinding -> KureM CoreExpr
- class AddBindings c where
- addHermitBindings :: [(Var, HermitBindingSite, AbsolutePathH)] -> c -> c
- addBindingGroup :: (AddBindings c, ReadPath c Crumb) => CoreBind -> c -> c
- addDefBinding :: (AddBindings c, ReadPath c Crumb) => Id -> c -> c
- addDefBindingsExcept :: (AddBindings c, ReadPath c Crumb) => Int -> [(Id, CoreExpr)] -> c -> c
- addLambdaBinding :: (AddBindings c, ReadPath c Crumb) => Var -> c -> c
- addAltBindings :: (AddBindings c, ReadPath c Crumb) => [Var] -> c -> c
- addCaseBinderBinding :: (AddBindings c, ReadPath c Crumb) => (Id, CoreExpr, CoreAlt) -> c -> c
- addForallBinding :: (AddBindings c, ReadPath c Crumb) => TyVar -> c -> c
- class BoundVars c where
- boundIn :: ReadBindings c => Var -> c -> Bool
- findBoundVars :: BoundVars c => (Var -> Bool) -> c -> VarSet
- class BoundVars c => ReadBindings c where
- hermitDepth :: c -> BindingDepth
- hermitBindings :: c -> Map Var HermitBinding
- lookupHermitBinding :: (ReadBindings c, Monad m) => Var -> c -> m HermitBinding
- lookupHermitBindingDepth :: (ReadBindings c, Monad m) => Var -> c -> m BindingDepth
- lookupHermitBindingSite :: (ReadBindings c, Monad m) => Var -> BindingDepth -> c -> m HermitBindingSite
- inScope :: BoundVars c => c -> Var -> Bool
- class HasCoreRules c where
- hermitCoreRules :: c -> [CoreRule]
- class LemmaContext c where
- addAntecedent :: LemmaName -> Lemma -> c -> c
- getAntecedents :: c -> Lemmas
- class HasEmptyContext c where
- setEmptyContext :: c -> c
HERMIT Contexts
Path Synonyms
type AbsolutePathH = AbsolutePath Crumb Source
type LocalPathH = LocalPath Crumb Source
The Standard Context
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.
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.
toHermitC :: (HasCoreRules c, LemmaContext c, ReadBindings c, ReadPath c Crumb) => c -> HermitC Source
Build a HermitC out of any context that has the capabilities.
Bindings
data HermitBindingSite Source
HERMIT's representation of variable bindings. Bound expressions cannot be inlined without checking for shadowing issues (using the depth information).
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 |
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.
data HermitBinding Source
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.
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.
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.
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.
hermitDepth :: c -> BindingDepth Source
hermitBindings :: c -> Map Var HermitBinding Source
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.
Accessing GHC rewrite rules from the context
class HasCoreRules c where Source
A class of contexts that store GHC rewrite rules.
hermitCoreRules :: c -> [CoreRule] Source
Accessing temporary lemmas in scope
class LemmaContext c where Source
A class of contexts that can store local Lemmas as we descend past implications.
addAntecedent :: LemmaName -> Lemma -> c -> c Source
getAntecedents :: c -> Lemmas Source
An empty Context
class HasEmptyContext c where Source
A class of contexts that provide an empty context.
setEmptyContext :: c -> c Source
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)) |