module HERMIT.Shell.Externals where
import Control.Arrow
import Control.Monad (liftM)
import Data.Dynamic (fromDynamic)
import Data.List (intercalate)
import qualified Data.Map as M
import Data.Maybe (fromMaybe)
import Data.Monoid (mempty)
import HERMIT.External
import HERMIT.Kernel
import HERMIT.Kure
import HERMIT.Lemma
import HERMIT.Parser
import HERMIT.Plugin.Renderer
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
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 $ liftM Right . gc)
[ "garbage-collect all ASTs except for the initial and current AST" ]
, external "display" (CLSModify $ \ st -> do (er,st') <- runCLT st (showWindow Nothing)
return $ fmap (const st') er)
[ "redisplays current state" ]
, external "up" (Direction U)
[ "move to the parent node"]
, external "navigate" (CLSModify $ \ st -> return $ Right $ st { cl_nav = True })
[ "switch to navigate mode" ]
, external "command-line" (CLSModify $ \ st -> return $ Right $ st { cl_nav = False })
[ "switch to command line mode" ]
, external "set-window" (CLSModifyAndShow setWindow)
[ "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" (CLSModifyAndShow $ versionCmd Back)
[ "go back in the derivation" ] .+ VersionControl
, external "step" (CLSModifyAndShow $ versionCmd Step)
[ "step forward in the derivation" ] .+ VersionControl
, external "goto" (CLSModifyAndShow . versionCmd . Goto)
[ "goto a specific step in the derivation" ] .+ VersionControl
, external "goto" (CLSModifyAndShow . 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 -> CLSModifyAndShow $ \ st ->
case reads bStr of
[(b,"")] -> return $ Right $ setDiffOnly st b
_ -> return $ Left $ CLError "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 $ \ st ->
case reads bStr of
[(b,"")] -> return $ Right $ setFailHard st b
_ -> return $ Left $ CLError "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 $ \ st ->
case reads bStr of
[(b,"")] -> return $ Right $ setCoreLint st b
_ -> return $ Left $ CLError "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 -> CLSModifyAndShow $ \ st ->
case M.lookup name pp_dictionary of
Nothing -> return $ Left $ CLError $ "List of Pretty Printers: " ++ intercalate ", " (M.keys pp_dictionary)
Just pp -> return $ Right $ flip setPrettyOpts (cl_pretty_opts st) $ setPretty st pp)
[ "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 -> CLSModifyAndShow $ \ st ->
return $ Right $ setPrettyOpts st (updateWidthOption w (cl_pretty_opts st)))
["set the width of the screen"]
, external "set-pp-type" (\ str -> CLSModifyAndShow $ \ st ->
case reads str :: [(ShowOption,String)] of
[(opt,"")] -> return $ Right $ setPrettyOpts st (updateTypeShowOption opt (cl_pretty_opts st))
_ -> return $ Left $ CLError "valid arguments are Show, Abstract, and Omit")
["set how to show expression-level types (Show|Abstact|Omit)"]
, external "set-pp-coercion" (\ str -> CLSModifyAndShow $ \ st ->
case reads str :: [(ShowOption,String)] of
[(opt,"")] -> return $ Right $ setPrettyOpts st (updateCoShowOption opt (cl_pretty_opts st))
_ -> return $ Left $ CLError "valid arguments are Show, Abstract, and Omit")
["set how to show coercions (Show|Abstact|Omit)"]
, external "set-pp-uniques" (\ str -> CLSModifyAndShow $ \ st ->
case reads str of
[(b,"")] -> return $ Right $ setPrettyOpts st ((cl_pretty_opts st) { po_showUniques = b } )
_ -> return $ Left $ CLError "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 $ \st -> return $ Right $ st { cl_running_script = 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 :: CommandLineState -> IO CommandLineState
gc st = do
let k = cl_kernel st
cursor = cl_cursor st
asts <- listK k
mapM_ (deleteK k) [ ast | (ast,_,_) <- asts, ast `notElem` [cursor, firstAST] ]
return st
setWindow :: CommandLineState -> IO (Either CLException CommandLineState)
setWindow st = do
let ps = fromMaybe ([],mempty) (M.lookup (cl_cursor st) (cl_foci st))
return $ Right $ st { cl_window = pathStack2Path ps }
showRenderers :: QueryFun
showRenderers = message $ "set-renderer " ++ show (map fst shellRenderers)
versionCmd :: VersionCmd -> CommandLineState -> IO (Either CLException CommandLineState)
versionCmd whereTo st = do
all_asts <- listK (cl_kernel st)
case whereTo of
Goto ast ->
if ast `elem` [ ast' | (ast',_,_) <- all_asts ]
then return $ Right $ setCursor ast st
else return $ Left $ CLError $ "Cannot find AST #" ++ show ast ++ "."
GotoTag nm ->
case [ ast | (ast,nms) <- M.toList (cl_tags st), nm `elem` nms ] of
[] -> return $ Left $ CLError $ "No tag named: " ++ nm
(ast:_) -> return $ Right $ setCursor ast st
Tag nm ->
return $ Right $ st { cl_tags = M.insertWith (++) (cl_cursor st) [nm] (cl_tags st) }
Step -> do
let ns = [ (fromMaybe "unknown" msg, ast) | (ast,msg,Just p) <- all_asts, p == cl_cursor st ]
case ns of
[] -> return $ Left $ CLError "Cannot step forward (no more steps)."
[(cmd,ast)] -> do
putStrLn $ "step : " ++ cmd
return $ Right $ setCursor ast st
_ -> return $ Left $ CLError $ "Cannot step forward (multiple choices), use goto {"
++ intercalate "," (map (show.snd) ns) ++ "}"
Back -> do
let ns = [ (fromMaybe "unknown" msg, p) | (ast,msg,Just p) <- all_asts, ast == cl_cursor st ]
case ns of
[] -> return $ Left $ CLError "Cannot step backwards (no more steps)."
[(cmd,ast)] -> do
putStrLn $ "back, unstepping : " ++ cmd
return $ Right $ setCursor ast st
_ -> return $ Left $ CLError "Cannot step backwards (multiple choices, impossible!)."
showDerivationTree :: CommandLineState -> IO String
showDerivationTree st = do
all_asts <- listK (cl_kernel st)
let graph = [ (a,[fromMaybe "-- command missing!" b],c) | (c,b,Just a) <- all_asts ]
return $ unlines $ showRefactorTrail graph firstAST (cl_cursor st)
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 (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)