module HERMIT.Monad
(
HermitM
, runHM
, embedHermitM
, HermitMEnv
, HermitMResult(..)
, LiftCoreM(..)
, getHscEnv
, runTcM
, runDsM
, HasLemmas(..)
, addLemma
, findLemma
, insertLemma
, deleteLemma
, HasHermitMEnv(..)
, mkEnv
, getModGuts
, getDebugChan
, KEnvMessage(..)
, sendKEnvMessage
) where
import Prelude.Compat hiding (lookup)
import Control.Monad
import Control.Monad.IO.Class
import Data.Map
import Language.KURE
import HERMIT.Core
import HERMIT.Context
import HERMIT.GHC
import HERMIT.GHC.Typechecker
import HERMIT.Kure.Universes
import HERMIT.Lemma
data HermitMEnv = HermitMEnv { hEnvChanged :: Bool
, hEnvDebug :: DebugChan
, hEnvModGuts :: ModGuts
, hEnvLemmas :: Lemmas
}
type DebugChan = KEnvMessage -> HermitM ()
mkEnv :: DebugChan -> ModGuts -> Lemmas -> HermitMEnv
mkEnv = HermitMEnv False
data HermitMResult a = HermitMResult { hResChanged :: Bool
, hResLemmas :: Lemmas
, hResult :: a
}
changedResult :: Lemmas -> a -> HermitMResult a
changedResult = HermitMResult True
mkResult :: HermitMEnv -> a -> HermitMResult a
mkResult env = HermitMResult (hEnvChanged env) (hEnvLemmas env)
newtype HermitM a = HermitM { runHermitM :: HermitMEnv -> CoreM (KureM (HermitMResult a)) }
runHM :: HermitMEnv
-> (HermitMResult a -> CoreM b)
-> (String -> CoreM b)
-> HermitM a
-> CoreM b
runHM env success failure ma = runHermitM ma env >>= runKureM success failure
embedHermitM :: (HasHermitMEnv m, HasLemmas m, LiftCoreM m) => HermitM a -> m a
embedHermitM hm = do
env <- getHermitMEnv
r <- liftCoreM (runHermitM hm env) >>= runKureM return fail
when (hResChanged r) $ forM_ (toList (hResLemmas r)) $ uncurry insertLemma
return $ hResult r
instance Functor HermitM where
fmap :: (a -> b) -> HermitM a -> HermitM b
fmap = liftM
instance Applicative HermitM where
pure :: a -> HermitM a
pure = return
(<*>) :: HermitM (a -> b) -> HermitM a -> HermitM b
(<*>) = ap
instance Monad HermitM where
return :: a -> HermitM a
return a = HermitM $ \ env -> return (return (mkResult env a))
(>>=) :: HermitM a -> (a -> HermitM b) -> HermitM b
(HermitM gcm) >>= f =
HermitM $ \ env -> gcm env >>= runKureM (\ (HermitMResult c ls a) ->
let env' = env { hEnvChanged = c, hEnvLemmas = ls }
in runHermitM (f a) env')
(return . fail)
fail :: String -> HermitM a
fail msg = HermitM $ const $ return $ fail msg
instance MonadCatch HermitM where
catchM :: HermitM a -> (String -> HermitM a) -> HermitM a
(HermitM gcm) `catchM` f = HermitM $ \ env -> gcm env >>= runKureM (return.return)
(\ msg -> runHermitM (f msg) env)
instance MonadIO HermitM where
liftIO :: IO a -> HermitM a
liftIO = liftCoreM . liftIO
instance MonadUnique HermitM where
getUniqueSupplyM :: HermitM UniqSupply
getUniqueSupplyM = liftCoreM getUniqueSupplyM
instance MonadThings HermitM where
lookupThing :: Name -> HermitM TyThing
lookupThing nm = runTcM $ tcLookupGlobal nm
instance HasDynFlags HermitM where
getDynFlags :: HermitM DynFlags
getDynFlags = liftCoreM getDynFlags
class HasHermitMEnv m where
getHermitMEnv :: m HermitMEnv
instance HasHermitMEnv HermitM where
getHermitMEnv = HermitM $ \ env -> return $ return $ mkResult env env
getModGuts :: (HasHermitMEnv m, Monad m) => m ModGuts
getModGuts = liftM hEnvModGuts getHermitMEnv
getDebugChan :: (HasHermitMEnv m, Monad m) => m DebugChan
getDebugChan = liftM hEnvDebug getHermitMEnv
sendKEnvMessage :: (HasHermitMEnv m, HasLemmas m, LiftCoreM m) => KEnvMessage -> m ()
sendKEnvMessage msg = getDebugChan >>= embedHermitM . ($ msg)
class HasLemmas m where
getLemmas :: m Lemmas
putLemmas :: Lemmas -> m ()
instance HasLemmas HermitM where
getLemmas = HermitM $ \ env -> return $ return $ mkResult env (hEnvLemmas env)
putLemmas m = HermitM $ \ _ -> return $ return $ changedResult m ()
insertLemma :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> m ()
insertLemma nm l = getLemmas >>= putLemmas . insert nm l
addLemma :: (HasLemmas m, Monad m) => LemmaName -> Lemma -> m ()
addLemma nm l = do
ls <- getLemmas
maybe (insertLemma nm l) (\ _ -> return ()) (lookup nm ls)
findLemma :: (HasLemmas m, Monad m) => LemmaName -> m Lemma
findLemma nm = do
r <- liftM (lookup nm) getLemmas
maybe (fail $ "lemma does not exist: " ++ show nm) return r
deleteLemma :: (HasLemmas m, Monad m) => LemmaName -> m ()
deleteLemma nm = getLemmas >>= putLemmas . delete nm
class Monad m => LiftCoreM m where
liftCoreM :: CoreM a -> m a
instance LiftCoreM HermitM where
liftCoreM coreM = HermitM $ \ env -> coreM >>= return . return . mkResult env
getHscEnv :: LiftCoreM m => m HscEnv
getHscEnv = liftCoreM getHscEnvCoreM
data KEnvMessage :: * where
DebugTick :: String -> KEnvMessage
DebugCore :: (LemmaContext c, ReadBindings c, ReadPath c Crumb) => String -> c -> LCoreTC -> KEnvMessage
AddObligation :: HermitC -> LemmaName -> Lemma -> KEnvMessage
runTcM :: (HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadIO m) => TcM a -> m a
runTcM m = do
env <- getHscEnv
dflags <- getDynFlags
guts <- getModGuts
(msgs, mr) <- liftIO $ initTcFromModGuts env guts HsSrcFile False m
let showMsgs (warns, errs) = showSDoc dflags $ vcat
$ text "Errors:" : pprErrMsgBag errs
++ text "Warnings:" : pprErrMsgBag warns
maybe (fail $ showMsgs msgs) return mr
runDsM :: (HasDynFlags m, HasHermitMEnv m, LiftCoreM m, MonadIO m) => DsM a -> m a
runDsM = runTcM . initDsTc