ProcessScript.hs revision 04857331be117d4e2215d866c309a17bd9a7e15c
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederDescription : process script commands
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2009
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : Christian.Maeder@dfki.de
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : provisional
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability : portable
ebcaad207cafc89eeb49d431f40de2ef4c48411cChristian Maederimport qualified Data.Map as Map
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederisNotDisproved :: G_theory -> Bool
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederisNotDisproved G_theory {gTheorySens = el} = checkListDisproved $ Data.List.map ((Data.List.map snd) .getThmStatus .
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder senAttr . ele . snd) $ Map.toList el
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercheckList :: [BasicProof] -> Bool
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercheckList [] = False
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercheckList (l : ls) = case l of
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder BasicProof _ (ProofStatus _ b _ _ _ _ _) -> case b of
38775225cf810f5895cc03b4acbcfe8f84f2513aChristian Maeder Disproved -> True
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder _ -> checkList ls
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder _ -> checkList ls
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercheckListDisproved :: [[BasicProof]] -> Bool
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercheckListDisproved [] = True
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian MaedercheckListDisproved (l : ls) = if checkList l then False
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder else checkListDisproved ls
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercmdlProcessString :: FilePath -> Int -> String -> CmdlState
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder -> IO (CmdlState, Maybe Command)
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedercmdlProcessString fp l ps st = case parseSingleLine fp l ps of
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Left err -> do
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder return (genMsgAndCode err 3 st, Nothing)
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Right c -> let cm = Parser.command c in
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder fmap (\ nst -> (nst, Just $ cmdDescription cm)) $ execCmdlCmd cm st
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder--sets the errorCode to 0 and then processes the string
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederresetErrorAndProcString :: FilePath -> Int -> String -> CmdlState
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder -> IO (CmdlState, Maybe Command)
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederresetErrorAndProcString fp l ps st = cmdlProcessString fp l ps $ resetErrorCode st
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederexecCmdlCmd :: CmdlCmdDescription -> CmdlState -> IO CmdlState
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederexecCmdlCmd cm =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder case cmdFn cm of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder CmdNoInput f -> f
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder CmdWithInput f -> f . cmdInputStr $ cmdDescription cm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedercmdlProcessCmd :: Command -> CmdlState -> IO CmdlState
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedercmdlProcessCmd c = case find (eqCmd c . cmdDescription) getCommands of
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Nothing -> return . genMsgAndCode ("unknown command: " ++ cmdNameStr c) 3
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Just cm -> execCmdlCmd cm { cmdDescription = c }
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederprintCmdResult :: CmdlState -> IO CmdlState
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederprintCmdResult state = do
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder let o = output state
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ms = outputMsg o
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder ws = warningMsg o
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder es = errorMsg o
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder unless (Data.List.null ms) $ putStrLn ms
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder unless (Data.List.null ws) . putStrLn $ "Warning:\n" ++ ws
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder unless (Data.List.null es) . putStrLn $ "Error:\n" ++ es
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder hFlush stdout
7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder return state { output = emptyCmdlMessage }
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedercmdlProcessScriptFile :: Bool -> FilePath -> CmdlState -> IO CmdlState
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedercmdlProcessScriptFile doExit fp st = do
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder str <- readFile fp
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder s <- foldM (\ nst (s, n) -> do
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (cst, _) <- resetErrorAndProcString fp n s nst
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder printCmdResult cst) st . number $ lines str
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder case i_state $ intState s of
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Just x -> case head $ elements x of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Element list _ -> when doExit $ if isNotDisproved (currentTheory list)
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder then exitWith $ getExitCode s
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder else exitWith $ ExitFailure 4
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder Nothing -> when doExit $ exitWith $ getExitCode s
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- | The function processes the file of instructions
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedercmdlProcessFile :: Bool -> HetcatsOpts -> FilePath -> IO CmdlState
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedercmdlProcessFile doExit opts file = do
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder putIfVerbose opts 2 $ "Processing hets proof file: " ++ file
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder s <- cmdlProcessScriptFile doExit file $ emptyCmdlState opts
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder when doExit $ exitWith $ getExitCode s