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

Safe HaskellNone

Language.HERMIT.Monad

Contents

Synopsis

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.

newIdH :: String -> Type -> HermitM IdSource

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

newTyVarH :: String -> Kind -> HermitM TyVarSource

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

cloneVarH :: (String -> String) -> Var -> HermitM VarSource

This gives an new version of a Var, with the same info, and a new textual name.

Saving Definitions

type Label = StringSource

A label for individual definitions.

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.

getStash :: HermitM DefStashSource

Get the stash of saved definitions.

Messages

newtype HermitMEnv Source

A way of sending messages to top level

Constructors

HermitMEnv 

data DebugMessage Source

A message packet.

Constructors

DebugTick String 
DebugCore String HermitC Core

A postcard.