hermit-1.0.1: src/HERMIT/Shell/Types.hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module HERMIT.Shell.Types where
import Control.Arrow
import Control.Concurrent.STM
import Control.Monad
import Control.Monad.Error.Class (MonadError(..))
import qualified Control.Monad.Fail as Fail (MonadFail(..))
import Control.Monad.IO.Class (MonadIO(..))
import Control.Monad.Reader (MonadReader(..), ReaderT(..), asks)
import Control.Monad.State (MonadState(..), StateT(..), gets, modify)
import Control.Monad.Trans.Class (MonadTrans(..))
import Control.Monad.Trans.Except (ExceptT(..), runExceptT)
import Data.Dynamic
import qualified Data.Map as M
import Data.Maybe (fromMaybe, isJust)
import HERMIT.Context
import HERMIT.Core
import HERMIT.Dictionary.Reasoning hiding (externals)
import HERMIT.External
import qualified HERMIT.GHC as GHC
import HERMIT.Kernel
import HERMIT.Kure
import HERMIT.Lemma
import HERMIT.Monad
import HERMIT.Parser
import HERMIT.PrettyPrinter.Common
import HERMIT.PrettyPrinter.Glyphs
import HERMIT.Plugin.Display
import HERMIT.Plugin.Renderer
import HERMIT.Plugin.Types
import System.Console.Haskeline hiding (catch, display)
import System.Console.Terminal.Size (Window(..), size)
import System.IO (Handle, stdout)
import qualified Text.PrettyPrint.MarkedHughesPJ as PP
----------------------------------------------------------------------------------
data QueryFun :: * -> * where
QueryString :: Injection a LCoreTC => TransformH a String -> QueryFun String
QueryGlyphs :: Injection a LCoreTC => TransformH a Glyphs -> QueryFun Glyphs
QueryPrettyH :: Injection a LCoreTC => PrettyH a -> QueryFun ()
Diff :: AST -> AST -> QueryFun ()
Inquiry :: (PluginReader -> CommandLineState -> IO String) -> QueryFun ()
QueryUnit :: Injection a LCoreTC => TransformH a () -> QueryFun ()
QueryA :: (Typeable a, Injection c LCoreTC)
=> TransformH c a -> QueryFun a
message :: String -> QueryFun ()
message = Inquiry . const . const . return
data QueryFunBox where
QueryFunBox :: Typeable a => QueryFun a -> QueryFunBox
instance Typeable a => Extern (QueryFun a) where
type Box (QueryFun _a) = QueryFunBox
box = QueryFunBox
unbox (QueryFunBox i) =
case cast i of
Just res -> res
Nothing -> error "Extern -- unbox: casting of query function failed."
performQuery :: (MonadCatch m, CLMonad m) => QueryFun a -> ExprH -> m a
performQuery qf expr = go qf
where cm = Changed $ unparseExprH expr
go (QueryString q) =
do str <- prefixFailMsg "Query failed: " (queryInContext (promoteT q) cm)
putStrToConsole str
return str
go (QueryGlyphs q) = do
res@(Glyphs gs) <- prefixFailMsg "Query failed: " $ queryInContext (promoteT q) cm
sequence_ [ liftIO $ withStyle sty txt
| Glyph txt sty <- gs
]
liftIO $ putStr "\n"
return res
go (QueryPrettyH q) = do
st <- get
doc <- prefixFailMsg "Query failed: " $ queryInContext (liftPrettyH (pOptions (cl_pretty st)) $ promoteT q) cm
liftIO $ cl_render st stdout (cl_pretty_opts st) (Right doc)
go (Inquiry f) = ask >>= \env -> get >>= liftIO . f env >>= putStrToConsole
go (Diff ast1 ast2) = do
k <- asks pr_kernel
st <- get
all_asts <- listK k
let getCmds ast
| ast == ast1 = []
| otherwise = case [ (p,msg) | (to,msg,Just p) <- all_asts, to == ast ] of
[(ast',msg)] -> fromMaybe "-- unknown command!" msg : getCmds ast'
_ -> ["error: history broken!"] -- should be impossible
cl_putStrLn "Commands:"
cl_putStrLn "========="
cl_putStrLn $ unlines $ reverse $ getCmds ast2
doc1 <- ppWholeProgram ast1
doc2 <- ppWholeProgram ast2
r <- diffDocH (cl_pretty st) doc1 doc2
cl_putStrLn "Diff:"
cl_putStrLn "====="
cl_putStr r
go (QueryUnit q) = do
-- TODO: Again, we may want a quiet version of the kernel_env
let str = unparseExprH expr
modFailMsg (\ err -> str ++ " [exception: " ++ err ++ "]") $ queryInContext (promoteT q) cm
putStrToConsole $ str ++ " [correct]"
go (QueryA q) = do
let str = unparseExprH expr
res <- modFailMsg (\ err -> str ++ " [exception: " ++ err ++ "]") $
queryInContext (promoteT q) cm
putStrToConsole $ str ++ " [correct]"
return res
ppWholeProgram :: (CLMonad m, MonadCatch m) => AST -> m DocH
ppWholeProgram ast = do
st <- get
k <- asks pr_kernel
d <- queryK k
(extractT $ pathT [ModGuts_Prog] $ liftPrettyH (cl_pretty_opts st) $ pLCoreTC $ cl_pretty st)
Never
(cl_kernel_env st) ast
return $ snd d -- discard new AST, assuming pp won't create one
----------------------------------------------------------------------------------
type TagName = String
data VersionCmd = Back -- back (up) the derivation tree
| Step -- down one step; assumes only one choice
| Goto AST -- goto a specific AST
| GotoTag TagName -- goto a specific AST, by tag name
| Tag TagName -- tag the current AST with a name
deriving Show
----------------------------------------------------------------------------------
data CLException = CLAbort
| CLResume AST
| CLContinue CommandLineState -- TODO: needed?
| CLError String
abort :: MonadError CLException m => m a
abort = throwError CLAbort
resume :: MonadError CLException m => AST -> m a
resume = throwError . CLResume
continue :: MonadError CLException m => CommandLineState -> m a
continue = throwError . CLContinue
rethrowCLE :: CLException -> PluginM a
rethrowCLE CLAbort = throwError PAbort
rethrowCLE (CLResume sast) = throwError (PResume sast)
rethrowCLE (CLContinue s) = put (cl_pstate s) >> return (error "CLContinue cannot return a value")
rethrowCLE (CLError msg) = throwError (PError msg)
rethrowPE :: MonadError CLException m => PException -> m a
rethrowPE PAbort = throwError CLAbort
rethrowPE (PResume sast) = throwError (CLResume sast)
rethrowPE (PError msg) = throwError (CLError msg)
----------------------------------------------------------------------------------
-- | This type is similiar to PluginM, except that its exception and state types are
-- supersets of those for PluginM, and it is a transformer. There are two functions:
-- `clm` and `pluginM` for converting between the two. The reason we do this is to obtain
-- a clean separation of plugin state from commandline state without nesting state
-- transformers. Nesting StateT leads to a lot of awkward lifting and manual state
-- management in the command line code.
--
-- NB: an alternative to monad transformers, like Oleg's Extensible Effects, might be useful here.
newtype CLT m a = CLT { unCLT :: ExceptT CLException (ReaderT PluginReader (StateT CommandLineState m)) a }
deriving (Functor, Applicative, MonadIO, MonadError CLException,
MonadState CommandLineState, MonadReader PluginReader)
-- Adapted from System.Console.Haskeline.MonadException, which hasn't provided an instance for ExceptT yet
instance MonadException m => MonadException (ExceptT e m) where
controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
run' = RunIO (fmap ExceptT . run . runExceptT)
in fmap runExceptT $ f run'
instance MonadException m => MonadException (CLT m) where
controlIO f = CLT $ controlIO $ \(RunIO run) -> let run' = RunIO (fmap CLT . run . unCLT)
in fmap unCLT $ f run'
-- This is copied verbatim from Haskeline, which provides an instance for strict State only.
-- This allows lazy State to enjoy the same benefits.
instance MonadException m => MonadException (StateT s m) where
controlIO f = StateT $ \s -> controlIO $ \(RunIO run) -> let
run' = RunIO (fmap (StateT . const) . run . flip runStateT s)
in fmap (flip runStateT s) $ f run'
type CLMonad m = (MonadIO m, MonadState CommandLineState m, MonadReader PluginReader m, MonadError CLException m)
instance MonadTrans CLT where
-- lift :: Monad m => m a -> CLT m a
lift = CLT . lift . lift . lift
-- TODO: type CLM = CLT IO
-- | Our own custom instance of Monad for CLT so we don't have to depend on
-- newtype deriving to do the right thing for fail.
instance Monad m => Monad (CLT m) where
return = CLT . return
(CLT m) >>= k = CLT (m >>= unCLT . k)
fail = Fail.fail
instance Monad m => Fail.MonadFail (CLT m) where
fail = CLT . throwError . CLError
-- | Run a CLT computation.
runCLT :: PluginReader -> CommandLineState -> CLT m a -> m (Either CLException a, CommandLineState)
runCLT r s = flip runStateT s . flip runReaderT r . runExceptT . unCLT
-- | Lift a CLT IO computation into a computation in an arbitrary CLMonad.
clm2clt :: CLMonad m => CLT IO a -> m a
clm2clt m = do
st <- get
env <- ask
(ea, st') <- liftIO (runCLT env st m)
either throwError (\r -> put st' >> return r) ea
-- | Lift a CLM computation into the PluginM monad.
clm :: CLT IO a -> PluginM a
clm m = do
s <- mkCLS
env <- ask
(er,s') <- liftIO $ runCLT env s m
case er of
Left err -> rethrowCLE err
Right r -> put (cl_pstate s') >> return r
-- | Lift a PluginM computation into the CLM monad.
pluginM :: CLMonad m => PluginM a -> m a
pluginM m = do
s <- get
env <- ask
(er,ps) <- liftIO $ runPluginT env (cl_pstate s) m
case er of
Left err -> rethrowPE err
Right r -> put (s { cl_pstate = ps }) >> return r
instance Monad m => MonadCatch (CLT m) where
-- law: fail msg `catchM` f == f msg
-- catchM :: m a -> (String -> m a) -> m a
catchM m f = do
st <- get
env <- ask
(er,st') <- lift $ runCLT env st m
case er of
Left err -> case err of
CLError msg -> f msg
other -> throwError other -- rethrow abort/resume/continue
Right v -> put st' >> return v
----------------------------------------------------------------------------------
-- Session-local issues; things that are never saved (except the PluginState).
data CommandLineState = CommandLineState
{ cl_pstate :: PluginState -- ^ Access to the enclosing plugin state. This is propagated back
-- to the plugin after the CLT computation ends. We do it this way
-- because nested StateT is a pain.
, cl_height :: Int -- ^ console height, in lines
, cl_scripts :: [(ScriptName,Script)]
, cl_nav :: Bool -- ^ keyboard input the nav panel
, cl_foci :: M.Map AST PathStack -- ^ focus assigned to each AST
, cl_tags :: M.Map AST [String] -- ^ list of tags on an AST
, cl_proofstack :: M.Map AST [ProofTodo] -- ^ stack of todos for the proof shell
, cl_window :: PathH -- ^ path to beginning of window, always a prefix of focus path in kernel
, cl_externals :: [External] -- ^ Currently visible externals
, cl_running_script :: Maybe Script -- ^ Nothing = no script running, otherwise the remaining script commands
, cl_safety :: Safety -- ^ which level of safety we are running in
, cl_templemmas :: TVar [(HermitC,LemmaName,Lemma)] -- ^ updated by kernel env with temporary obligations
, cl_failhard :: Bool -- ^ Any exception will cause an abort.
, cl_diffonly :: Bool -- ^ Print diffs instead of full focus.
}
type PathStack = ([LocalPathH], LocalPathH)
data ProofTodo = Unproven
{ ptName :: LemmaName -- ^ lemma we are proving
, ptLemma :: Lemma
, ptContext :: HermitC -- ^ context in which lemma is being proved
, ptPath :: PathStack -- ^ path into lemma to focus on
}
data Safety = StrictSafety | NormalSafety | NoSafety
deriving (Read, Show, Eq)
filterSafety :: Safety -> [External] -> [External]
filterSafety NoSafety = id
filterSafety NormalSafety = filter ((Unsafe `notElem`) . externTags)
filterSafety StrictSafety = filter ((`notElem` ["assume"]) . externName) . filterSafety NormalSafety
-- TODO: currently, we only prevent assuming proofs in strict mode
-- it would probably be better to explicitly tag every command allowed
-- in strict safety mode with the 'Safe' tag, then change this to:
-- filterSafety StrictSafety = filter ((Safe `elem`) . externTags)
-- To ease the pain of nested records, define some boilerplate here.
cl_corelint :: CommandLineState -> Bool
cl_corelint = ps_corelint . cl_pstate
setCoreLint :: CommandLineState -> Bool -> CommandLineState
setCoreLint st b = st { cl_pstate = (cl_pstate st) { ps_corelint = b } }
cl_cursor :: CommandLineState -> AST
cl_cursor = ps_cursor . cl_pstate
setCursor :: AST -> CommandLineState -> CommandLineState
setCursor sast st = st { cl_pstate = (cl_pstate st) { ps_cursor = sast } }
cl_kernel_env :: CommandLineState -> KernelEnv
cl_kernel_env s = do
let KernelEnv f = mkKernelEnv (cl_pstate s)
KernelEnv $ \ msg ->
case msg of
AddObligation c nm l@(Lemma _ NotProven Obligation) | cl_safety s /= NoSafety ->
liftIO $ atomically $ modifyTVar' (cl_templemmas s) ((c,nm,l):)
_ -> f msg
cl_pretty :: CommandLineState -> PrettyPrinter
cl_pretty = ps_pretty . cl_pstate
setPretty :: CommandLineState -> PrettyPrinter -> CommandLineState
setPretty st pp = st { cl_pstate = (cl_pstate st) { ps_pretty = pp } }
cl_pretty_opts :: CommandLineState -> PrettyOptions
cl_pretty_opts = pOptions . cl_pretty
setPrettyOpts :: CommandLineState -> PrettyOptions -> CommandLineState
setPrettyOpts st po = setPretty st $ (cl_pretty st) { pOptions = po }
cl_render :: CommandLineState -> (Handle -> PrettyOptions -> Either String DocH -> IO ())
cl_render = ps_render . cl_pstate
-- | Create default CommandLineState from PluginState.
-- Note: the dictionary (cl_dict) will be empty, and should be populated if needed.
mkCLS :: PluginM CommandLineState
mkCLS = do
ps <- get
(w,h) <- liftIO getTermDimensions
tlv <- liftIO (newTVarIO [])
let st = CommandLineState { cl_pstate = ps
, cl_height = h
, cl_scripts = []
, cl_nav = False
, cl_foci = M.empty
, cl_tags = M.empty
, cl_proofstack = M.empty
, cl_window = mempty
, cl_externals = [] -- Note, empty dictionary.
, cl_running_script = Nothing
, cl_safety = NormalSafety
, cl_templemmas = tlv
, cl_failhard = False
, cl_diffonly = False
}
return $ setPrettyOpts st $ (cl_pretty_opts st) { po_width = w }
-- | Returns the (width, height) of the terminal HERMIT is running in.
-- If it can't figure it out, it uses a default of (80, 25).
getTermDimensions :: IO (Int, Int)
getTermDimensions = do
Window h w <- fromMaybe (Window 25 80) <$> size
return (w, h)
newtype CLSBox = CLSBox CommandLineState
instance Extern CommandLineState where
type Box CommandLineState = CLSBox
unbox (CLSBox st) = st
box = CLSBox
type ScriptName = String
-- tick counter
tick :: TVar (M.Map String Int) -> String -> IO Int
tick var msg = atomically $ do
m <- readTVar var
let c = case M.lookup msg m of
Nothing -> 1
Just x -> x + 1
writeTVar var (M.insert msg c m)
return c
cl_putStr :: CLMonad m => String -> m ()
cl_putStr = pluginM . ps_putStr
cl_putStrLn :: CLMonad m => String -> m ()
cl_putStrLn = pluginM . ps_putStrLn
isRunningScript :: MonadState CommandLineState m => m Bool
isRunningScript = liftM isJust $ gets cl_running_script
setRunningScript :: MonadState CommandLineState m => Maybe Script -> m ()
setRunningScript ms = modify $ \st -> st { cl_running_script = ms }
-- TODO: rename?
putStrToConsole :: CLMonad m => String -> m ()
putStrToConsole str = ifM isRunningScript (return ()) (cl_putStrLn str)
------------------------------------------------------------------------------
pathStack2Path :: ([LocalPath crumb], LocalPath crumb) -> Path crumb
pathStack2Path (ps,p) = concat $ reverse (map snocPathToPath (p:ps))
-- | A primitive means of denoting navigation of a tree (within a local scope).
data Direction = U -- ^ Up
| T -- ^ Top
deriving (Eq, Show)
pathStackToLens :: (Injection a g, Walker HermitC g) => [LocalPathH] -> LocalPathH -> LensH a g
pathStackToLens ps p = injectL >>> pathL (pathStack2Path (ps,p))
getPathStack :: CLMonad m => m ([LocalPathH], LocalPathH)
getPathStack = do
st <- get
return $ fromMaybe ([],mempty) (M.lookup (cl_cursor st) (cl_foci st))
getFocusPath :: CLMonad m => m PathH
getFocusPath = liftM pathStack2Path getPathStack
addFocusT :: (Injection a g, Walker HermitC g, CLMonad m) => TransformH g b -> m (TransformH a b)
addFocusT t = do
(base, rel) <- getPathStack
return $ focusT (pathStackToLens base rel) t
addFocusR :: (Injection a g, Walker HermitC g, CLMonad m) => RewriteH g -> m (RewriteH a)
addFocusR r = do
(base, rel) <- getPathStack
return $ focusR (pathStackToLens base rel) r
------------------------------------------------------------------------------
addAST :: CLMonad m => AST -> m ()
addAST ast = do
copyProofStack ast
copyPathStack ast
modify $ setCursor ast
modifyLocalPath :: (MonadCatch m, CLMonad m) => (LocalPathH -> LocalPathH) -> ExprH -> m ()
modifyLocalPath f expr = do
ps <- getProofStackEmpty
k <- asks pr_kernel
(kEnv,ast) <- gets (cl_kernel_env &&& cl_cursor)
case ps of
todo@(Unproven _ (Lemma q _ _) c _) : todos -> do
let (base, rel) = ptPath todo
rel' = f rel
requireDifferent rel rel'
(ast',()) <- queryK k (constT
(applyT
(setFailMsg "invalid path."
(focusT (pathStackToLens base rel' :: LensH Clause LCoreTC) successT))
c q))
(Always $ unparseExprH expr) kEnv ast
addAST ast'
let todo' = todo { ptPath = (base, rel') }
modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) (todo':todos) (cl_proofstack st) }
_ -> do
(base, rel) <- getPathStack
let rel' = f rel
requireDifferent rel rel'
-- we are testing paths, so the sum type matters
(ast',()) <- queryK k (setFailMsg "invalid path."
(focusT (pathStackToLens base rel' :: LensH GHC.ModGuts CoreTC) successT))
(Always $ unparseExprH expr) kEnv ast
addAST ast'
modify $ \ st -> st { cl_foci = M.insert (cl_cursor st) (base, rel') (cl_foci st) }
requireDifferent :: Monad m => LocalPathH -> LocalPathH -> m ()
requireDifferent p1 p2 = when (p1 == p2) $ fail "path unchanged, nothing to do."
copyPathStack :: CLMonad m => AST -> m ()
copyPathStack ast = do
(base, rel) <- getPathStack
modify $ \ st -> st { cl_foci = M.insert ast (base, rel) (cl_foci st) }
copyProofStack :: CLMonad m => AST -> m ()
copyProofStack ast = modify $ \ st -> let newStack = fromMaybe [] $ M.lookup (cl_cursor st) (cl_proofstack st)
in st { cl_proofstack = M.insert ast newStack (cl_proofstack st) }
pushProofStack :: CLMonad m => ProofTodo -> m ()
pushProofStack todo = modify $ \ st -> st { cl_proofstack = M.insertWith (++) (cl_cursor st) [todo] (cl_proofstack st) }
popProofStack :: CLMonad m => m ProofTodo
popProofStack = do
t : ts <- getProofStack
modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) ts (cl_proofstack st) }
return t
announceUnprovens :: (MonadCatch m, CLMonad m) => m ()
announceUnprovens = do
(c,m) <- queryInFocus (contextT &&& getLemmasT :: TransformH LCore (HermitC,Lemmas)) Never
sf <- gets cl_safety
case sf of
StrictSafety -> do
let ls = [ nl | nl@(_,Lemma _ p u) <- M.toList m, p `elem` [NotProven, Assumed], u /= NotUsed ]
forM_ ls $ \ nl@(nm,_) -> do
cl_putStrLn $ "Fatal: Lemma " ++ show nm ++ " has not been proven, but was used."
printLemma stdout c mempty nl
unless (null ls) abort -- don't finish if this happens
NormalSafety -> do
let np = [ nl | nl@(_,Lemma _ NotProven u) <- M.toList m, u /= NotUsed ]
forM_ np $ \ nl@(nm,_) -> do
cl_putStrLn $ "Fatal: Lemma " ++ show nm ++ " has not been proven, but was used."
printLemma stdout c mempty nl
unless (null np) abort -- don't finish if this happens
let as = [ nl | nl@(_,Lemma _ Assumed u) <- M.toList m, u /= NotUsed ]
forM_ as $ \ nl@(nm,_) -> do
cl_putStrLn $ "Warning: Lemma " ++ show nm ++ " was assumed but not proven."
printLemma stdout c mempty nl
NoSafety -> return ()
-- | Always returns a non-empty list.
getProofStack :: CLMonad m => m [ProofTodo]
getProofStack = do
todos <- getProofStackEmpty
case todos of
[] -> fail "No lemma currently being proved."
_ -> return todos
getProofStackEmpty :: CLMonad m => m [ProofTodo]
getProofStackEmpty = do
(ps, ast) <- gets (cl_proofstack &&& cl_cursor)
maybe (return []) return $ M.lookup ast ps
------------------------------------------------------------------------------
fixWindow :: CLMonad m => m ()
fixWindow = do
-- check to make sure new path is still inside window
focusPath <- getFocusPath
-- move the window in two cases:
-- 1. window path is not prefix of focus path
-- 2. window path is empty (since at the top level we only show type sigs)
{- when (not (isPrefixOf (cl_window st) focusPath) || null (cl_window st))
$ put $ st { cl_window = focusPath } -}
modify $ \ st -> st { cl_window = focusPath } -- TODO: temporary until we figure out a better highlight interface
{-
getWindow :: (MonadCatch m, CLMonad m) => m DocH
getWindow = do
render <- gets (ps_render . cl_pstate)
printWindowAlways Nothing
-- restore the state
modify (\ s -> s { cl_pstate = (cl_pstate s) { ps_render = render }})
return undefined
-}
-- printWindow only calls display if a script is not running
printWindow :: (MonadCatch m, CLMonad m) => Maybe Handle -> m ()
printWindow = ifM isRunningScript (return ()) . printWindowAlways
-- always prints the current view. This a wrapper around 'display'.
printWindowAlways :: (MonadCatch m, CLMonad m) => Maybe Handle -> m ()
printWindowAlways mbh = do
(ps,(ast,(pp,render))) <- gets (cl_proofstack &&& cl_cursor &&& cl_pretty &&& (ps_render . cl_pstate))
let h = fromMaybe stdout mbh
pStr = render h (pOptions pp) . Left
case M.lookup ast ps of
Just (Unproven _ l c p : _) -> printLemma h c p ("Goal:",l)
_ -> do st <- get
if cl_diffonly st
then do
k <- asks pr_kernel
all_asts <- listK k
let kEnv = cl_kernel_env st
ast' = head $ [ cur | (cur, _, Just p) <- all_asts, p == ast ] ++ [ast]
ppOpts = cl_pretty_opts st
q <- addFocusT $ liftPrettyH ppOpts $ pLCoreTC pp
(_,doc1) <- queryK k q Never kEnv ast
(_,doc2) <- queryK k q Never kEnv ast'
diffDocH pp doc1 doc2 >>= liftIO . pStr -- TODO
else fixWindow >> gets cl_window >>= pluginM . printDisplay mbh . Just --TODO
-- always prints the current view. This a wrapper around 'display'.
showWindow :: (MonadCatch m, CLMonad m) => m DocH
showWindow = do
(ps,(ast,_)) <- gets (cl_proofstack &&& cl_cursor &&& cl_pretty &&& (ps_render . cl_pstate))
case M.lookup ast ps of
Just (Unproven _ l c p : _) -> showLemma c p ("Goal:",l)
_ -> fixWindow >> gets cl_window >>= pluginM . showDisplay . Just --TODO
printLemma :: (MonadCatch m, CLMonad m)
=> Handle -> HermitC -> PathStack -> (LemmaName,Lemma) -> m ()
printLemma h c p (nm,lm) = do -- TODO
doc' <- showLemma c p (nm,lm)
st <- get
liftIO $ cl_render st h (cl_pretty_opts st) (Right doc')
showLemma :: (MonadCatch m, CLMonad m)
=> HermitC -> PathStack -> (LemmaName,Lemma) -> m DocH
showLemma c p (nm,Lemma q _ _) = do -- TODO
(pp,opts) <- gets (cl_pretty &&& cl_pretty_opts)
as <- queryInContext ((liftPrettyH opts $ do
m <- getAntecedents <$> contextT
ds <- forM (M.toList m) $ \(n',l') -> return l' >>> ppLemmaT pp n'
if M.null m
then return []
else return $ PP.text "Assumed lemmas: " : ds
) :: TransformH LCoreTC [DocH]) Never
doc <- queryInFocus ((constT $ applyT (extractT (liftPrettyH (pOptions pp) (pathT (pathStack2Path p) (pLCoreTC pp)))) c q) :: TransformH Core DocH) Never
return $ PP.vcat $ as ++ [PP.text (show nm) PP.$+$ PP.nest 2 doc]
------------------------------------------------------------------------------
queryInFocus :: (Walker HermitC g, Injection GHC.ModGuts g, MonadCatch m, CLMonad m)
=> TransformH g b -> CommitMsg -> m b
queryInFocus t msg = do
q <- addFocusT t
st <- get
k <- asks pr_kernel
(ast', r) <- queryK k q msg (cl_kernel_env st) (cl_cursor st)
addAST ast'
return r
-- meant to be used inside queryInFocus
inProofFocusT :: ProofTodo -> TransformH LCoreTC b -> TransformH Core b
inProofFocusT (Unproven _ (Lemma q _ _) c ps) t =
contextfreeT $ applyT (return q >>> extractT (pathT (pathStack2Path ps) t)) c
inProofFocusR :: ProofTodo -> RewriteH LCoreTC -> TransformH Core Clause
inProofFocusR (Unproven _ (Lemma q _ _) c ps) rr =
contextfreeT $ applyT (return q >>> extractR (pathR (pathStack2Path ps) rr)) c
-- TODO: better name
queryInContext :: forall b m. (MonadCatch m, CLMonad m) => TransformH LCoreTC b -> CommitMsg -> m b
queryInContext tr cm = do
ps <- getProofStackEmpty
case ps of
todo@(Unproven {}) : _
-> {- GHC.trace "in proof context" $ -} queryInFocus (inProofFocusT todo tr) cm
_ -> {- GHC.trace "in modguts context" $ -} queryInFocus (extractT tr :: TransformH CoreTC b) cm