hermit- Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone




The HERMIT Monad

runHM :: HermitMEnv -> DefStash -> (DefStash -> a -> CoreM b) -> (String -> CoreM b) -> HermitM a -> CoreM bSource

Eliminator for HermitM.

liftCoreM :: CoreM a -> HermitM aSource

CoreM can be lifted to HermitM.

newVarH :: String -> Type -> HermitM IdSource

Make a unique identifier for a specified type based on a provided name.

newTypeVarH :: String -> Kind -> HermitM TyVarSource

Make a unique type variable for a specified kind based on a provided name.

Saving Definitions

type Label = StringSource

A label for individual defintions.

type DefStash = Map Label CoreDefSource

A store of saved definitions.

saveDef :: Label -> CoreDef -> HermitM ()Source

Save a definition for future use.

lookupDef :: Label -> HermitM CoreDefSource

Lookup a previously saved definition.

newtype HermitMEnv Source

A way of sending messages to top level



data DebugMessage whereSource

A message packet.