module HERMIT.Shell.KernelEffect
( KernelEffect(..)
, performKernelEffect
, applyRewrite
, setPath
) where
import Control.Arrow
import Control.Monad.State
import qualified Data.Map as M
import Data.Monoid
import Data.Typeable
import HERMIT.Context
import HERMIT.Dictionary
import HERMIT.External
import HERMIT.Kernel
import HERMIT.Kure
import HERMIT.Lemma
import HERMIT.Parser
import HERMIT.Shell.Types
data KernelEffect = Direction Direction
| BeginScope
| EndScope
| Delete AST
deriving Typeable
instance Extern KernelEffect where
type Box KernelEffect = KernelEffect
box i = i
unbox i = i
performKernelEffect :: (MonadCatch m, CLMonad m) => ExprH -> KernelEffect -> m ()
performKernelEffect e = \case
Direction d -> goUp d e
BeginScope -> beginScope e
EndScope -> endScope e
Delete sast -> deleteAST sast
applyRewrite :: (MonadCatch m, CLMonad m) => RewriteH LCoreTC -> ExprH -> m ()
applyRewrite rr expr = do
ps <- getProofStackEmpty
let str = unparseExprH expr
case ps of
todo@(Unproven {}) : todos -> do
q' <- queryInFocus (inProofFocusR todo (promoteR rr) >>> (contextfreeT (applyT lintQuantifiedT (ptContext todo)) >> idR) :: TransformH Core Quantified) (Always str)
let todo' = todo { ptLemma = (ptLemma todo) { lemmaQ = q' } }
modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) (todo':todos) (cl_proofstack st) }
_ -> do
(k,(kEnv,(ast,cl))) <- gets (cl_kernel &&& cl_kernel_env &&& cl_cursor &&& cl_corelint)
rr' <- addFocusR (extractR rr :: RewriteH CoreTC)
ast' <- prefixFailMsg "Rewrite failed:" $ applyK k rr' (Always str) kEnv ast
when cl $ do
warns <- liftM snd (queryK k lintModuleT Never kEnv ast')
`catchM` (\ errs -> deleteK k ast' >> fail errs)
putStrToConsole warns
addAST ast'
ifM isRunningScript (return ()) (showWindow Nothing)
setPath :: (Injection a LCoreTC, MonadCatch m, CLMonad m) => TransformH a LocalPathH -> ExprH -> m ()
setPath t expr = do
p <- prefixFailMsg "Cannot find path: " $ queryInContext (promoteT t) Never
modifyLocalPath (<> p) expr
ifM isRunningScript (return ()) (showWindow Nothing)
goUp :: (MonadCatch m, CLMonad m) => Direction -> ExprH -> m ()
goUp T expr = modifyLocalPath (const mempty) expr
goUp U expr = do
(_,rel) <- getPathStack
case rel of
SnocPath [] -> fail "cannot move up, at root of scope."
SnocPath (_:cs) -> modifyLocalPath (const $ SnocPath cs) expr
ifM isRunningScript (return ()) (showWindow Nothing)
beginScope :: (MonadCatch m, CLMonad m) => ExprH -> m ()
beginScope expr = do
ps <- getProofStackEmpty
let logExpr = do
(k,ast) <- gets (cl_kernel &&& cl_cursor)
tellK k (unparseExprH expr) ast
case ps of
[] -> do
(base, rel) <- getPathStack
addAST =<< logExpr
modify $ \ st -> st { cl_foci = M.insert (cl_cursor st) (rel : base, mempty) (cl_foci st) }
Unproven nm l c ls (base,p) : todos -> do
addAST =<< logExpr
let todos' = Unproven nm l c ls (p : base, mempty) : todos
modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) todos' (cl_proofstack st) }
_ -> fail "beginScope: impossible case!"
ifM isRunningScript (return ()) (showWindow Nothing)
endScope :: (MonadCatch m, CLMonad m) => ExprH -> m ()
endScope expr = do
ps <- getProofStackEmpty
let logExpr = do
(k,ast) <- gets (cl_kernel &&& cl_cursor)
tellK k (unparseExprH expr) ast
case ps of
[] -> do
(base, _) <- getPathStack
case base of
[] -> fail "no scope to end."
(rel:base') -> do
addAST =<< logExpr
modify $ \ st -> st { cl_foci = M.insert (cl_cursor st) (base', rel) (cl_foci st) }
Unproven nm l c ls (base,_) : todos -> do
case base of
[] -> fail "no scope to end."
(p:base') -> do
addAST =<< logExpr
let todos' = Unproven nm l c ls (base', p) : todos
modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) todos' (cl_proofstack st) }
_ -> fail "endScope: impossible case!"
ifM isRunningScript (return ()) (showWindow Nothing)
deleteAST :: (MonadCatch m, CLMonad m) => AST -> m ()
deleteAST ast = gets cl_kernel >>= flip deleteK ast