| 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, LiftCoreM m) => HermitM a -> m a
- data HermitMEnv
- data HermitMResult a = HermitMResult {
- hResChanged :: Bool
- 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
- class HasLemmas m where
- addLemma :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> m ()
- findLemma :: (HasLemmas m, Monad m) => LemmaName -> m Lemma
- insertLemma :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> m ()
- deleteLemma :: (HasLemmas m, Monad m) => LemmaName -> m ()
- class HasHermitMEnv m where
- getHermitMEnv :: m HermitMEnv
- mkEnv :: ModGuts -> Lemmas -> HermitMEnv
- getModGuts :: (HasHermitMEnv m, Monad m) => m ModGuts
- class HasHscEnv m where
- class HasDebugChan m where
- getDebugChan :: m (DebugMessage -> m ())
- data DebugMessage :: * where
- DebugTick :: String -> DebugMessage
- DebugCore :: (ReadBindings c, ReadPath c Crumb) => String -> c -> LCoreTC -> 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 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, LiftCoreM m) => HermitM a -> m a Source
Allow HermitM to be embedded in another monad with proper capabilities.
data HermitMEnv Source
The HermitM environment.
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
Lemmas
addLemma :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> m () Source
Only adds a lemma if doesn't already exist.
findLemma :: (HasLemmas m, Monad m) => LemmaName -> m Lemma Source
Find a lemma by name. Fails if lemma does not exist.
insertLemma :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> m () Source
Insert or replace a lemma.
deleteLemma :: (HasLemmas m, Monad m) => LemmaName -> m () Source
Reader Information
class HasHermitMEnv m where Source
Instances
mkEnv :: ModGuts -> Lemmas -> HermitMEnv Source
getModGuts :: (HasHermitMEnv m, Monad m) => m ModGuts Source
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 -> LCoreTC -> DebugMessage |
sendDebugMessage :: (HasDebugChan m, Monad m) => DebugMessage -> m () Source