Safe Haskell | None |
---|---|
Language | Haskell2010 |
- data HermitM a
- runHM :: HermitMEnv -> (HermitMResult a -> CoreM b) -> (String -> CoreM b) -> HermitM a -> CoreM b
- embedHermitM :: (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
- getHscEnv :: LiftCoreM m => m HscEnv
- runTcM :: (HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadIO m) => TcM a -> m a
- runDsM :: (HasDynFlags m, HasHermitMEnv m, LiftCoreM 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 :: DebugChan -> ModGuts -> Lemmas -> HermitMEnv
- getModGuts :: (HasHermitMEnv m, Monad m) => m ModGuts
- getDebugChan :: (HasHermitMEnv m, Monad m) => m DebugChan
- data KEnvMessage :: * where
- DebugTick :: String -> KEnvMessage
- DebugCore :: (LemmaContext c, ReadBindings c, ReadPath c Crumb) => String -> c -> LCoreTC -> KEnvMessage
- AddObligation :: HermitC -> LemmaName -> Lemma -> KEnvMessage
- sendKEnvMessage :: (HasHermitMEnv m, HasLemmas m, LiftCoreM m) => KEnvMessage -> 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.
runHM :: HermitMEnv -> (HermitMResult a -> CoreM b) -> (String -> CoreM b) -> HermitM a -> CoreM b Source
Eliminator for HermitM
.
embedHermitM :: (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.
HermitMResult | |
|
runTcM :: (HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadIO m) => TcM a -> m a Source
runDsM :: (HasDynFlags m, HasHermitMEnv m, LiftCoreM 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
getHermitMEnv :: m HermitMEnv Source
Get the HermitMEnv
mkEnv :: DebugChan -> ModGuts -> Lemmas -> HermitMEnv Source
getModGuts :: (HasHermitMEnv m, Monad m) => m ModGuts Source
Messages
getDebugChan :: (HasHermitMEnv m, Monad m) => m DebugChan Source
data KEnvMessage :: * where Source
A message packet.
DebugTick :: String -> KEnvMessage | |
DebugCore :: (LemmaContext c, ReadBindings c, ReadPath c Crumb) => String -> c -> LCoreTC -> KEnvMessage | |
AddObligation :: HermitC -> LemmaName -> Lemma -> KEnvMessage |
sendKEnvMessage :: (HasHermitMEnv m, HasLemmas m, LiftCoreM m) => KEnvMessage -> m () Source