| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
HERMIT.Monad
- data HermitM a
- runHM :: DebugChan -> HermitMEnv -> (HermitMResult a -> CoreM b) -> (String -> CoreM b) -> HermitM a -> CoreM b
- embedHermitM :: (HasDebugChan m, HasHermitMEnv m, HasLemmas m, HasStash m, LiftCoreM m) => HermitM a -> m a
- data HermitMEnv = HermitMEnv {}
- data HermitMResult a = HermitMResult {
- hResStash :: DefStash
- hResLemmas :: Lemmas
- hResult :: a
- class Monad m => LiftCoreM m where
- runTcM :: (HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadIO m) => TcM a -> m a
- runDsM :: (HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadIO m) => DsM a -> m a
- newtype RememberedName = RememberedName String
- type DefStash = Map RememberedName CoreDef
- saveDef :: (HasStash m, Monad m) => RememberedName -> CoreDef -> m ()
- lookupDef :: (HasStash m, Monad m) => RememberedName -> m CoreDef
- class HasStash m where
- data Equality = Equality [CoreBndr] CoreExpr CoreExpr
- newtype LemmaName = LemmaName String
- data Lemma = Lemma {}
- type Lemmas = Map LemmaName Lemma
- addLemma :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> m ()
- class HasHermitMEnv m where
- getHermitMEnv :: m HermitMEnv
- mkEnv :: ModGuts -> DefStash -> Lemmas -> HermitMEnv
- getModGuts :: (HasHermitMEnv m, Monad m) => m ModGuts
- class HasHscEnv m where
- class HasLemmas m where
- insertLemma :: LemmaName -> Lemma -> m ()
- getLemmas :: m Lemmas
- class HasDebugChan m where
- getDebugChan :: m (DebugMessage -> m ())
- data DebugMessage :: * where
- DebugTick :: String -> DebugMessage
- DebugCore :: (ReadBindings c, ReadPath c Crumb) => String -> c -> CoreTC -> DebugMessage
- sendDebugMessage :: (HasDebugChan m, Monad m) => DebugMessage -> m ()
The HERMIT Monad
The HERMIT monad is kept abstract.
It provides a reader for ModGuts, state for DefStash and Lemmas, and access to a debugging channel.
Instances
runHM :: DebugChan -> HermitMEnv -> (HermitMResult a -> CoreM b) -> (String -> CoreM b) -> HermitM a -> CoreM b Source
Eliminator for HermitM.
embedHermitM :: (HasDebugChan m, HasHermitMEnv m, HasLemmas m, HasStash m, LiftCoreM m) => HermitM a -> m a Source
Allow HermitM to be embedded in another monad with proper capabilities.
data HermitMEnv Source
The HermitM reader environment.
Constructors
| HermitMEnv | |
Fields
| |
data HermitMResult a Source
The HermitM result record.
Constructors
| HermitMResult | |
Fields
| |
runTcM :: (HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadIO m) => TcM a -> m a Source
runDsM :: (HasDynFlags m, HasHermitMEnv m, HasHscEnv m, MonadIO m) => DsM a -> m a Source
Saving Definitions
newtype RememberedName Source
A label for individual definitions. Use a newtype so we can tab-complete in shell.
Constructors
| RememberedName String |
type DefStash = Map RememberedName CoreDef Source
A store of saved definitions.
saveDef :: (HasStash m, Monad m) => RememberedName -> CoreDef -> m () Source
Save a definition for future use.
lookupDef :: (HasStash m, Monad m) => RememberedName -> m CoreDef Source
Lookup a previously saved definition.
Lemmas
An equality is represented as a set of universally quantified binders, and the LHS and RHS of the equality.
Instances
| Extern (RewriteH Equality) | |
| Extern (TransformH Equality String) | |
| type Box (RewriteH Equality) = RewriteEqualityBox | |
| type Box (TransformH Equality String) = TransformEqualityStringBox |
A name for lemmas. Use a newtype so we can tab-complete in shell.
An equality with a proven status.
addLemma :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> m () Source
Only adds a lemma if doesn't already exist.
Reader Information
class HasHermitMEnv m where Source
Instances
getModGuts :: (HasHermitMEnv m, Monad m) => m ModGuts Source
Writer Information
Messages
class HasDebugChan m where Source
Instances
data DebugMessage :: * where Source
A message packet.
Constructors
| DebugTick :: String -> DebugMessage | |
| DebugCore :: (ReadBindings c, ReadPath c Crumb) => String -> c -> CoreTC -> DebugMessage |
sendDebugMessage :: (HasDebugChan m, Monad m) => DebugMessage -> m () Source