hermit- Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone




HERMIT Bindings

data HermitBinding Source

HERMIT's representation of variable bindings.


BIND Int Bool CoreExpr

Binding depth, whether it is recursive, and the bound value (which cannot be inlined without checking for scoping issues).


For a lambda binding you only know the depth.

CASE Int CoreExpr (AltCon, [Id])

For case wildcard binders. First expr points to scrutinee, second to AltCon (which can be converted to Constructor or Literal).

hermitBindingDepth :: HermitBinding -> IntSource

Get the depth of a binding.

The HERMIT Context

data Context 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.

initContext :: ModGuts -> ContextSource

Create the initial HERMIT Context by providing a ModGuts.

(@@) :: Context -> Int -> ContextSource

Update the context by extending the stored AbsolutePath to a child.

addAltBindings :: [Id] -> Context -> ContextSource

Add the Ids bound by a DataCon in a case. Like lambda bindings, in that we know nothing about them, but all bound at the same depth, so we cannot just fold addLambdaBinding over the list.

addBinding :: CoreBind -> Context -> ContextSource

Add all bindings in a binding group to the Context.

addCaseBinding :: (Id, CoreExpr, CoreAlt) -> Context -> ContextSource

Add the bindings for a specific case alternative.

addLambdaBinding :: Id -> Context -> ContextSource

Add a binding that you know nothing about, except that it may shadow something. If so, do not worry about it here, just remember the binding and the depth. When we want to inline a value from the environment, we then check to see what is free in the inlinee, and see if any of the frees will stop the validity of the inlining.

hermitBindings :: Context -> Map Id HermitBindingSource

All (important) bindings in scope.

hermitDepth :: Context -> IntSource

The depth of the bindings.

hermitPath :: Context -> AbsolutePathSource

The AbsolutePath to the current node from the root.

hermitModGuts :: Context -> ModGutsSource

The ModGuts of the current module.

lookupHermitBinding :: Id -> Context -> Maybe HermitBindingSource

Lookup the binding for an identifier in a Context.

listBindings :: Context -> [Id]Source

List all the identifiers bound in the Context.

boundIn :: Id -> Context -> BoolSource

Determine if an identifier is bound in the Context.