eflint-3.1.0.0: src/REPL.hs
{-# LANGUAGE LambdaCase #-}
module Main where
import Language.EFLINT.Spec
import Language.EFLINT.Explorer
import Language.EFLINT.Interpreter
import Language.EFLINT.Parse
import Language.EFLINT.Print (ppDeclSpec)
import Language.EFLINT.State
import Language.EFLINT.StaticEval
import Language.EFLINT.Options
import Language.EFLINT.Util
import Language.EFLINT.JSON(decode_json_file)
import qualified Language.Explorer.Pure as EI
import Control.Monad (forM_, foldM, when, unless)
import Control.Monad.Trans.Class (lift)
import Data.Char (isSpace)
import Data.List (isPrefixOf, isSuffixOf, (\\))
import qualified Data.Map as M
import qualified Data.Set as S
import Text.Read (readMaybe)
import System.IO.Error
import System.Environment
import System.Directory
import System.FilePath
import System.Console.Haskeline hiding (display)
-- the kind of explorer to use
init_explorer = init_tree_explorer
main = getArgs >>= arg_select
arg_select :: [String] -> IO ()
arg_select args = do
cdir <- getCurrentDirectory
let (files, flags') = span (not . (\a -> isPrefixOf "--" a || isPrefixOf "-" a)) args
opts <- run_options (["-i",cdir] ++ flags')
case files of
[] -> repl_without opts
[f] | ".eflint" `isSuffixOf` f -> repl_with opts f
[f] | ".json" `isSuffixOf` f -> repl_with opts f
_ -> putStrLn "Please provide: <NAME>.eflint <OPTIONS>"
repl_without :: Options -> IO ()
repl_without opts = compile_and_init opts emptySpec M.empty [] []
repl_with :: Options -> FilePath -> IO ()
repl_with opts fsrc = do
add_filepath fsrc opts
input_exists <- doesFileExist (fsrc ++ ".input")
when input_exists $
readFile (fsrc ++ ".input") >>= flip add_input opts . lines
add_include_path (takeDirectory fsrc) opts
add_include fsrc opts
case ".json" `isSuffixOf` fsrc of
True -> decode_json_file fsrc >>= \case
Left err -> putStrLn "could not parse JSON file:\n" >> putStrLn err
Right spec -> compile_and_init opts spec M.empty [] []
False -> do
fl <- readFile fsrc
case parse_component syn_directives_phrases fl of
Left err1 -> case parse_flint fl of
Left err2 -> do putStrLn "could not parse flint phrases:\n" >> putStrLn err1
putStrLn "could not parse flint spec:\n" >> putStrLn err2
Right (f,r,i,s) -> case find ignore_scenario opts of
True -> compile_and_init opts f r i []
False -> compile_and_init opts f r i s
Right ps -> init_with_phrases opts ps
compile_and_init :: Options -> Spec -> Refiner -> Initialiser -> Scenario -> IO ()
compile_and_init opts f r i s = case compile_all f r i s of
Right (spec',r',i',s') -> do
test <- is_in_test_mode opts
unless test $ do
let spec = refine_specification spec' r'
let state = make_initial_state spec i'
let explorer = init_explorer (Just (spec,state))
let ((_,c0),_,(sid, ctx)) = get_last_edge explorer (EI.currRef explorer)
verbosity opts Default $ display_commands
verbosity opts Default $ display_info opts [] c0 ctx
runInputT defaultSettings (repl opts explorer)
Left errs -> putStrLn "compilation errors:" >> putStrLn (unlines errs)
init_with_phrases :: Options -> [Either Directive Phrase] -> IO ()
init_with_phrases opts ps = do
let explorer = init_explorer Nothing
test <- is_in_test_mode opts
runInputT defaultSettings $ do
exp <- repl_directive_phrases opts ps explorer
unless test (repl opts exp)
repl :: Options -> Explorer -> InputT IO ()
repl opts exp = do
let (_, _, (sid, ctx)) = get_last_edge exp (EI.currRef exp)
maybeLine <- getInputLine ("#" ++ show sid ++ " > ")
case maybeLine of
Nothing -> return ()
Just input -> do
case span (not . isSpace) input of
(":choose", mint) -> repl_trigger ctx mint
(":jump", mint) -> revert_or_jump False mint sid
(":revert", mint) -> revert_or_jump True mint sid
(":display", _) -> lift (display ctx) >> continue exp
(":d", _) -> lift (display ctx) >> continue exp
(":spec", mty) -> lift (display_spec ctx mty) >> continue exp
(":session", _) -> outputStrLn (showTree exp) >> continue exp
(":s", _) -> outputStrLn (showTree exp) >> continue exp
(":options", _) -> lift (display_all_triggers ctx) >> continue exp
(":o", _) -> lift (display_all_triggers ctx) >> continue exp
(":help", _) -> lift display_commands >> continue exp
(":h", _) -> lift display_commands >> continue exp
(":quit", _) -> return ()
(":q", _) -> return ()
((':':mint),_) -> repl_trigger ctx mint
("#include", fp') -> repl_directive opts (Include fp) exp >>= continue
where fp = case readMaybe fp' of Nothing -> dropWhile isSpace fp'
Just str -> str
("#require", fp') -> repl_directive opts (Require fp) exp >>= continue
where fp = case readMaybe fp' of Nothing -> dropWhile isSpace fp'
Just str -> str
_ -> repl_recognize_phrase input
where continue = repl opts
repl_trigger ctx mint = case readMaybe (dropWhile isSpace mint) of
Just trig | trig <= length (rest_transitions ctx), trig > 0
-> repl_phrases opts emptyInput [PDo (fst $ map get_transition (rest_transitions ctx) !! (trig - 1))] exp >>= continue
_ -> lift display_commands >> continue exp
repl_recognize_phrase str = case parse_component syn_phrases str of
Left err -> outputStrLn err >> continue exp
Right ps -> repl_phrases opts emptyInput ps exp >>= continue
revert_or_jump destr mint sid = case readMaybe (dropWhile isSpace mint) of
Just sid' -> case run_ exp (Revert sid' destr) of
InvalidRevert -> outputStrLn ("state id " ++ show sid' ++ " unknown") >> continue exp
ResultTrans exp outs (old,_) (new,sid) ->
lift (display_info opts outs old new) >> continue exp
_ -> lift display_commands >> continue exp
repl_directive_phrases :: Options -> [Either Directive Phrase] -> Explorer -> InputT IO Explorer
repl_directive_phrases opts [] explorer = return explorer
repl_directive_phrases opts (edp:ps) explorer =
case edp of
Left d -> repl_directive opts d explorer >>= repl_directive_phrases opts ps
Right p -> repl_phrases opts emptyInput [p] explorer >>= repl_directive_phrases opts ps
where (_,_,(_,ctx)) = get_last_edge explorer (EI.currRef explorer)
isQuery phrase = case phrase of PQuery _ -> True
_ -> False
repl_phrases :: Options -> InputMap -> [Phrase] -> Explorer -> InputT IO Explorer
repl_phrases opts inpm phrases explorer =
repl_report opts inpm phrases (run_ explorer (Execute (convert_programs phrases) inpm)) explorer
repl_directive :: Options -> Directive -> Explorer -> InputT IO Explorer
repl_directive opts (Include fp) explorer = repl_import opts fp explorer
repl_directive opts (Require fp) explorer
| has_been_included fp opts = return explorer
| otherwise = repl_import opts fp explorer
repl_import :: Options -> FilePath -> Explorer -> InputT IO Explorer
repl_import opts fp explorer = do
let dirs = find include_paths opts
files <- lift $ find_included_file dirs fp
case files of
[] -> lift $ putStrLn ("could not find " ++ fp ++ " in " ++ show dirs) >> return explorer
(file:_) -> do
lift $ add_include_path (takeDirectory file) opts
lift $ add_include file opts
case ".json" `isSuffixOf` file of
True -> do
mspec <- lift (decode_json_file file)
case mspec of
Left err -> lift (putStrLn err) >> return explorer
Right spec -> lift (putStrLn "including .json files is no longer supported") >> return explorer --repl_directive_phrases opts [Right (PFrames spec)] explorer
False -> lift (catchIOError (Right <$> readFile file) handler) >>= \case
Left err -> lift (putStrLn err) >> return explorer
Right str -> case parse_component syn_directives_phrases str of
Left err -> lift (putStrLn err) >> return explorer
Right eps -> repl_directive_phrases opts eps explorer
where handler :: IOError -> IO (Either String a)
handler exc | isDoesNotExistError exc = return (Left ("unknown file: " ++ fp))
| isPermissionError exc = return (Left ("cannot read: " ++ fp))
| isAlreadyInUseError exc = return (Left ("in use: " ++ fp))
| otherwise = return (Left (show exc))
repl_report :: Options -> InputMap -> [Phrase] -> -- both used for re-execution in case of missing input
Response -> Explorer -> InputT IO Explorer
repl_report opts inpm phrases res exp = case res of
ResultTrans exp outs (old,_) (ctx,sid) -> case missing_inputs outs of
[] -> lift (verbosity opts TestMode (display_info opts outs old ctx)) >> return exp
ms -> do minpm <- foldM consider (Just inpm) ms
case minpm of Just inpm' -> repl_phrases opts inpm' phrases exp
Nothing -> return exp
where consider Nothing _ = return Nothing
consider (Just inpm) te@(_,d) = do
mass <- lift (consume_input opts)
let tryWith b = Just $ M.insert te b inpm
case mass of
Just b -> return (tryWith b)
Nothing -> do
lift $ putStrLn ("\nmissing truth-value for: " ++ ppTagged te)
lift $ putStrLn ("is this fact True or False?")
getInputLine "(True/False) > " >>= \case
Just s -> return $ tryWith (readAssignmentMaybe s)
Nothing -> return Nothing
InvalidRevert -> error "REPL.assert 1"
display_commands =
putStrLn "Available commands:\n\
\ :<INT> same as :choose <INT>\n\
\ :choose <INT> choose action or event trigger <INT>\n\
\ :force <INT> choose and force action or event trigger <INT>\n\
\ :revert <INT> revert to the configuration with id <INT>\n\
\ :display :d show all contents of the current configuration\n\
\ :spec pretty-print all type definitions\n\
\ :session :s show the history of the session\n\
\ :options :o show all actions & events, including disabled actions\n\
\ :help :h show these commands\n\
\ :quit :q end the exploration\n\
\ or just type a <PHRASE>"
display_info :: Options -> [Output] -> Config -> Config -> IO ()
display_info opts outs c0 cfg = do
verbosity opts TestMode $ display_errors (errors outs)
verbosity opts TestMode $ display_query_results (query_ress outs)
verbosity opts TestMode $ display_inst_query_results (inst_query_ress outs)
verbosity opts Default $ display_transitions (ex_triggers outs)
verbosity opts Default $ display_violations (violations outs)
verbosity opts Default $ display_new_types (M.keysSet $ decls $ cfg_spec c0) (M.keysSet $ decls $ cfg_spec cfg)
verbosity opts Default $ display_fact_changes (cfg_state c0) (cfg_state cfg)
verbosity opts Default $ display_new_invariants (invariants $ cfg_spec c0) (invariants $ cfg_spec cfg)
where display_query_results [] = return ()
display_query_results ress = mapM_ op ress
where op QuerySuccess = verbosity opts Default (putStrLn "query successful")
op QueryFailure = verbosity opts TestMode (putStrLn "query failed")
display_inst_query_results vss = forM_ vss $ \vs -> do mapM_ (putStrLn . ppTagged) vs
putStrLn ""
display_errors [] = return ()
display_errors errs = mapM_ op errs
where op (CompilationError err) = putStr err
op err = putStrLn (print_error err)
display_violations [] = return ()
display_violations vs = putStrLn "violations:" >> mapM_ op vs
where op (DutyViolation te) = putStrLn (" violated duty!: " ++ ppTagged te)
op (InvariantViolation d) = putStrLn (" violated invariant!: " ++ d)
op (TriggerViolation tinfo) = putStrLn (" disabled " ++ trans_type ++ ": " ++ ppTagged (trans_tagged tinfo))
where trans_type = if trans_is_action tinfo then "action" else "event"
display_transitions = mapM_ display_transition
display_transition trans = do
putStr ("executed transition: \n")
putStr (showTriggerTree trans)
display_fact_changes :: State -> State -> IO ()
display_fact_changes prev cur = do
display_facts "~" (S.toList (M.keysSet (contents prev) `S.difference` M.keysSet (contents cur)))
display_facts "-" (state_not_holds cur \\ state_not_holds prev)
display_facts "+" (state_holds cur \\ state_holds prev)
where display_facts pref fs = mapM_ op fs
where op f = putStrLn (pref ++ ppTagged f)
display_new_types :: S.Set DomId -> S.Set DomId -> IO ()
display_new_types prev cur = do
display_type_info "New type " (S.toList (cur `S.difference` prev))
display_type_info "Removed type " (S.toList (prev `S.difference` cur))
where display_type_info pref ts = mapM_ op ts
where op t = putStrLn (pref ++ t)
display_new_invariants :: S.Set DomId -> S.Set DomId -> IO ()
display_new_invariants prev cur = do
display_invariants "New invariant " (cur S.\\ prev)
display_invariants "Removed invariant " (prev S.\\ cur)
where display_invariants pref is = mapM_ op (S.toList is)
where op i = putStrLn (pref ++ i)
display_all_triggers :: Config -> IO ()
display_all_triggers cfg = display_triggers "" (map get_transition (rest_transitions cfg))
display_triggers str tes = display_triggers' tes
where display_triggers' [] = putStrLn ("no " ++ str ++ "actions or events")
display_triggers' tes = putStrLn (str ++ "actions & events:") >> mapM_ op (zip [1..] tes)
where op (i, (te,en)) = putStrLn (show i ++ ". " ++ ppTagged te ++ enabled)
where enabled | en = " (ENABLED)"
| otherwise = " (DISABLED)"
display :: Config -> IO ()
display cfg = putStrLn (show (cfg_state cfg))
display_spec :: Config -> String -> IO ()
display_spec ctx mty = case find_decl (cfg_spec ctx) ty of
Nothing -> forM_ (M.assocs (decls (cfg_spec ctx))) (putStrLn . uncurry ppDeclSpec)
Just tspec -> putStrLn (ppDeclSpec ty tspec)
where ty = dropWhile isSpace mty