module HERMIT.Shell.Externals where
import Control.Arrow
import Control.Monad (liftM)
import Control.Monad.Reader (asks)
import Control.Monad.State (gets, modify)
import Data.Dynamic (fromDynamic)
import Data.List (intercalate)
import qualified Data.Map as M
import Data.Maybe (fromMaybe)
import HERMIT.External
import HERMIT.Kernel
import HERMIT.Kure
import HERMIT.Lemma
import HERMIT.Parser
import HERMIT.Plugin.Renderer
import HERMIT.Plugin.Types
import HERMIT.PrettyPrinter.Common
import HERMIT.Dictionary.Reasoning
import HERMIT.Shell.Dictionary
import HERMIT.Shell.KernelEffect
import HERMIT.Shell.Proof as Proof
import HERMIT.Shell.ScriptToRewrite
import HERMIT.Shell.ShellEffect
import HERMIT.Shell.Types
import Prelude.Compat
shell_externals :: [External]
shell_externals = map (.+ Shell)
[ external "resume" Resume
[ "stops HERMIT; resumes compile" ]
, external "abort" Abort
[ "hard UNIX-style exit; does not return to GHC; does not save" ]
, external "continue" Continue
[ "exits shell; resumes HERMIT" ]
, external "gc" Delete
[ "garbage-collect a given AST" ]
, external "gc" (CLSModify gc)
[ "garbage-collect all ASTs except for the initial and current AST" ]
, external "display" (CLSModify $ showWindowAlways Nothing)
[ "redisplays current state" ]
, external "up" (Direction U)
[ "move to the parent node"]
, external "navigate" (CLSModify $ modify $ \ st -> st { cl_nav = True })
[ "switch to navigate mode" ]
, external "command-line" (CLSModify $ modify $ \ st -> st { cl_nav = False })
[ "switch to command line mode" ]
, external "set-window" (CLSModify $ setWindow >> showWindow Nothing)
[ "fix the window to the current focus" ]
, external "top" (Direction T)
[ "move to root of current scope" ]
, external "log" (Inquiry showDerivationTree)
[ "go back in the derivation" ] .+ VersionControl
, external "back" (CLSModify $ versionCmd Back)
[ "go back in the derivation" ] .+ VersionControl
, external "step" (CLSModify $ versionCmd Step)
[ "step forward in the derivation" ] .+ VersionControl
, external "goto" (CLSModify . versionCmd . Goto)
[ "goto a specific step in the derivation" ] .+ VersionControl
, external "goto" (CLSModify . versionCmd . GotoTag)
[ "goto a specific step in the derivation by tag name" ] .+ VersionControl
, external "tag" (CLSModify . versionCmd . Tag)
[ "name the current step in the derivation" ] .+ VersionControl
, external "diff" Diff
[ "show diff of two ASTs" ] .+ VersionControl
, external "set-pp-diffonly" (\ bStr -> CLSModify $
case reads bStr of
[(b,"")] -> modify (\st -> st { cl_diffonly = b }) >> showWindow Nothing
_ -> fail "valid arguments are True and False" )
[ "set-pp-diffonly <True|False>; False by default"
, "print diffs rather than full code after a rewrite" ]
, external "set-fail-hard" (\ bStr -> CLSModify $
case reads bStr of
[(b,"")] -> modify $ \ st -> st { cl_failhard = b }
_ -> fail "valid arguments are True and False" )
[ "set-fail-hard <True|False>; False by default"
, "any rewrite failure causes compilation to abort" ]
, external "set-auto-corelint" (\ bStr -> CLSModify $
case reads bStr of
[(b,"")] -> modify $ flip setCoreLint b
_ -> fail "valid arguments are True and False" )
[ "set-auto-corelint <True|False>; False by default"
, "run core lint type-checker after every rewrite, reverting on failure" ]
, external "set-pp" (\ name -> CLSModify $
case M.lookup name pp_dictionary of
Nothing -> fail $ "List of Pretty Printers: " ++ intercalate ", " (M.keys pp_dictionary)
Just pp -> do modify $ \ st -> setPrettyOpts (setPretty st pp) (cl_pretty_opts st)
showWindow Nothing)
[ "set the pretty printer"
, "use 'set-pp ls' to list available pretty printers" ]
, external "set-pp-renderer" (PluginComp . changeRenderer)
[ "set the output renderer mode"]
, external "set-pp-renderer" showRenderers
[ "set the output renderer mode"]
,
external "dump" (\pp fp r w -> CLSModify (dump fp pp r w))
[ "dump <filename> <renderer> <width> - DEPRECATED"]
, external "dump" (\fp pp r w -> CLSModify (dump fp pp r w))
[ "dump <filename> <pretty-printer> <renderer> <width>"]
, external "dump-lemma" ((\nm fp pp r w -> getLemmaByNameT nm >>> liftPrettyH (pOptions pp) (ppLemmaT pp nm) >>> dumpT fp pp r w) :: LemmaName -> FilePath -> PrettyPrinter -> String -> Int -> TransformH LCoreTC ())
[ "Dump named lemma to a file."
, "dump-lemma <lemma-name> <filename> <pretty-printer> <renderer> <width>" ]
, external "dump-lemma" ((\pp nm fp r w -> getLemmaByNameT nm >>> liftPrettyH (pOptions pp) (ppLemmaT pp nm) >>> dumpT fp pp r w) :: PrettyPrinter -> LemmaName -> FilePath -> String -> Int -> TransformH LCoreTC ())
[ "Dump named lemma to a file."
, "dump-lemma <lemma-name> <filename> <pretty-printer> <renderer> <width>" ]
, external "set-pp-width" (\ w -> CLSModify $ do
modify $ \ st -> setPrettyOpts st (updateWidthOption w (cl_pretty_opts st))
showWindow Nothing)
["set the width of the screen"]
, external "set-pp-type" (\ str -> CLSModify $
case reads str :: [(ShowOption,String)] of
[(opt,"")] -> do modify $ \ st -> setPrettyOpts st (updateTypeShowOption opt (cl_pretty_opts st))
showWindow Nothing
_ -> fail "valid arguments are Show, Abstract, and Omit")
["set how to show expression-level types (Show|Abstact|Omit)"]
, external "set-pp-coercion" (\ str -> CLSModify $
case reads str :: [(ShowOption,String)] of
[(opt,"")] -> do modify $ \ st -> setPrettyOpts st (updateCoShowOption opt (cl_pretty_opts st))
showWindow Nothing
_ -> fail "valid arguments are Show, Abstract, and Omit")
["set how to show coercions (Show|Abstact|Omit)"]
, external "set-pp-uniques" (\ str -> CLSModify $
case reads str of
[(b,"")] -> do modify $ \ st -> setPrettyOpts st ((cl_pretty_opts st) { po_showUniques = b })
showWindow Nothing
_ -> fail "valid arguments are True and False")
["set whether uniques are printed with variable names"]
, external "{" BeginScope
["push current lens onto a stack"]
, external "}" EndScope
["pop a lens off a stack"]
, external "load" LoadFile
["load <script-name> <file-name> : load a HERMIT script from a file and save it under the specified name."]
, external "load-and-run" loadAndRun
["load-and-run <file-name> : load a HERMIT script from a file and run it immediately."]
, external "save" (SaveFile False)
["save <filename> : save the current complete derivation into a file."]
, external "save-verbose" (SaveFile True)
["save-verbose <filename> : save the current complete derivation into a file,"
,"including output of each command as a comment."]
, external "save-script" SaveScript
["save-script <filename> <script name> : save a loaded or manually defined script to a file." ]
, external "load-as-rewrite" (\ rewriteName fileName -> SeqMeta [LoadFile rewriteName fileName, ScriptToRewrite rewriteName rewriteName])
["load-as-rewrite <rewrite-name> <filepath> : load a HERMIT script from a file, and convert it to a rewrite."
,"Note that there are significant limitations on the commands the script may contain."] .+ Experiment .+ TODO
, external "script-to-rewrite" ScriptToRewrite
["script-to-rewrite <rewrite-name> <script-name> : create a new rewrite from a pre-loaded (or manually defined) HERMIT script."
,"Note that there are significant limitations on the commands the script may contain."] .+ Experiment .+ TODO
, external "define-script" DefineScript
["Define a new HERMIT script and bind it to a name."
,"Note that any names in the script will not be resolved until the script is *run*."
,"Example usage: define-script \"MyScriptName\" \"any-td beta-reduce ; let-subst ; bash\""]
, external "define-rewrite" (\ name str -> SeqMeta [DefineScript name str, ScriptToRewrite name name])
["Define a new HERMIT rewrite and bind it to a name."
,"Note that this also saves the input script under the same name."
,"Example usage: define-rewrite \"MyRewriteName\" \"let-subst >>> bash\""]
, external "run-script" RunScript
["Run a pre-loaded (or manually defined) HERMIT script."
,"Note that any names in the script will not be resolved until the script is *run*." ]
, external "display-scripts" displayScripts
["Display all loaded scripts."]
, external "stop-script" (CLSModify $ setRunningScript Nothing)
[ "Stop running the current script." ]
, external "possible-rewrites" (testAllT:: CommandLineState -> TransformH LCore String)
["Test all given set of rewrites to see if they succeed"] .+ Experiment
] ++ Proof.externals
gc :: CLT IO ()
gc = do
k <- asks pr_kernel
cursor <- gets cl_cursor
asts <- listK k
mapM_ (deleteK k) [ ast | (ast,_,_) <- asts, ast `notElem` [cursor, firstAST] ]
setWindow :: CLT IO ()
setWindow = modify $ \ st ->
let ps = fromMaybe ([],mempty) (M.lookup (cl_cursor st) (cl_foci st))
in st { cl_window = pathStack2Path ps }
showRenderers :: QueryFun
showRenderers = message $ "set-renderer " ++ show (map fst shellRenderers)
versionCmd :: VersionCmd -> CLT IO ()
versionCmd whereTo = do
k <- asks pr_kernel
all_asts <- listK k
case whereTo of
Goto ast ->
if ast `elem` [ ast' | (ast',_,_) <- all_asts ]
then modify (setCursor ast) >> showWindow Nothing
else fail $ "Cannot find AST #" ++ show ast ++ "."
GotoTag nm -> do
tags <- gets cl_tags
case [ ast | (ast,nms) <- M.toList tags, nm `elem` nms ] of
[] -> fail $ "No tag named: " ++ nm
(ast:_) -> modify (setCursor ast) >> showWindow Nothing
Tag nm -> do
modify $ \st -> st { cl_tags = M.insertWith (++) (cl_cursor st) [nm] (cl_tags st) }
cl_putStrLn $ "Tag: " ++ nm ++ " added."
Step -> do
cursor <- gets cl_cursor
let ns = [ (fromMaybe "unknown" msg, ast) | (ast,msg,Just p) <- all_asts, p == cursor ]
case ns of
[] -> fail "Cannot step forward (no more steps)."
[(cmd,ast)] -> do
cl_putStrLn $ "step : " ++ cmd
modify $ setCursor ast
showWindow Nothing
_ -> fail $ "Cannot step forward (multiple choices), use goto {"
++ intercalate "," (map (show.snd) ns) ++ "}"
Back -> do
cursor <- gets cl_cursor
let ns = [ (fromMaybe "unknown" msg, p) | (ast,msg,Just p) <- all_asts, ast == cursor ]
case ns of
[] -> fail "Cannot step backwards (no more steps)."
[(cmd,ast)] -> do
cl_putStrLn $ "back, unstepping : " ++ cmd
modify $ setCursor ast
showWindow Nothing
_ -> fail "Cannot step backwards (multiple choices, impossible!)."
showDerivationTree :: PluginReader -> CommandLineState -> IO String
showDerivationTree r s = do
let k = pr_kernel r
cursor = cl_cursor s
all_asts <- listK k
let graph = [ (a,[fromMaybe "-- command missing!" b],c) | (c,b,Just a) <- all_asts ]
return $ unlines $ showRefactorTrail graph firstAST cursor
showRefactorTrail :: (Eq a, Show a) => [(a,[String],a)] -> a -> a -> [String]
showRefactorTrail db a me =
case [ (b,c) | (a0,b,c) <- db, a == a0 ] of
[] -> [show' 3 a ++ " " ++ dot]
((b,c):bs) ->
[show' 3 a ++ " " ++ dot ++ (if not (null bs) then "->" else "") ] ++
[" " ++ "| " ++ txt | txt <- b ] ++
showRefactorTrail db c me ++
if null bs
then []
else [] :
showRefactorTrail [ (a',b',c') | (a',b',c') <- db
, not (a == a' && c == c')
] a me
where dot = if a == me then "*" else "o"
show' n x = replicate (n length (show a)) ' ' ++ show x
displayScripts :: QueryFun
displayScripts = Inquiry (const (return . showScripts . cl_scripts))
showScripts :: [(ScriptName,Script)] -> String
showScripts = concatMap (\ (name,script) -> name ++ ": " ++ unparseScript script ++ "\n\n")
testAllT :: CommandLineState -> TransformH LCore String
testAllT st = do
let es = cl_externals st
mbs = map (\d -> (externName d, fromDynamic (externDyn d) :: Maybe RewriteLCoreBox)) es
namedRewrites = [(name ,unbox boxedR) | (name, Just boxedR) <- mbs]
testRewrites False namedRewrites
testRewrites :: Bool-> [(ExternalName, RewriteH LCore)] -> TransformH LCore String
testRewrites debug rewrites = case debug of
True -> let list = mapM (\ (n,r) -> liftM (f n) (testM r)) rewrites
in liftM unlines list
False -> let list = mapM (\ (n,r) -> liftM (g n) (testM r)) rewrites
filtered = liftM (filter(\x -> snd x)) list
res = liftM (map (\ (n,b) -> f n b )) filtered
in liftM unlines res
where
f :: ExternalName -> Bool -> String
f x True = x++" would succeed."
f x False = x++" would fail."
g x y = (x,y)