a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaederDescription : process script commands
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaederMaintainer : Christian.Maeder@dfki.de
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaederStability : provisional
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaederPortability : portable
f196ec1099fa1010eaa2f3c1c576c2e84e112eacLoredana Mihaela Diaconuimport qualified Data.Map as Map
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maederimport qualified Common.OrderedMap as OMap
f196ec1099fa1010eaa2f3c1c576c2e84e112eacLoredana Mihaela DiaconuisNotDisproved :: G_theory -> Bool
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian MaederisNotDisproved G_theory {gTheorySens = el} =
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder checkListDisproved . map
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder (map snd . getThmStatus . senAttr . OMap.ele . snd) $ Map.toList el
f196ec1099fa1010eaa2f3c1c576c2e84e112eacLoredana Mihaela DiaconucheckList :: [BasicProof] -> Bool
f196ec1099fa1010eaa2f3c1c576c2e84e112eacLoredana Mihaela DiaconucheckList [] = False
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian MaedercheckList (l : ls) = case l of
55ab20b85d8838544a83c1ef2e01e1f2b2da7496Eugen Kuksa BasicProof _ (ProofStatus _ b _ _ _ _ _ _) -> case b of
f196ec1099fa1010eaa2f3c1c576c2e84e112eacLoredana Mihaela Diaconu Disproved -> True
f196ec1099fa1010eaa2f3c1c576c2e84e112eacLoredana Mihaela Diaconu _ -> checkList ls
f196ec1099fa1010eaa2f3c1c576c2e84e112eacLoredana Mihaela Diaconu _ -> checkList ls
f196ec1099fa1010eaa2f3c1c576c2e84e112eacLoredana Mihaela DiaconucheckListDisproved :: [[BasicProof]] -> Bool
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian MaedercheckListDisproved = all (not . checkList)
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaedercmdlProcessString :: FilePath -> Int -> String -> CmdlState
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder -> IO (CmdlState, Maybe Command)
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaedercmdlProcessString fp l ps st = case parseSingleLine fp l ps of
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder Left err -> return (genMsgAndCode err 3 st, Nothing)
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder Right c -> let cm = Parser.command c in
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder fmap (\ nst -> (nst, Just $ cmdDescription cm)) $ execCmdlCmd cm st
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder-- sets the errorCode to 0 and then processes the string
d8a6d1101a0e3d09fb8f8566590cb209c103498aLoredana Mihaela DiaconuresetErrorAndProcString :: FilePath -> Int -> String -> CmdlState
d8a6d1101a0e3d09fb8f8566590cb209c103498aLoredana Mihaela Diaconu -> IO (CmdlState, Maybe Command)
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian MaederresetErrorAndProcString fp l ps st =
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder cmdlProcessString fp l ps $ resetErrorCode st
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaederexecCmdlCmd :: CmdlCmdDescription -> CmdlState -> IO CmdlState
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaederexecCmdlCmd cm =
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder case cmdFn cm of
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder CmdNoInput f -> f
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder CmdWithInput f -> f . cmdInputStr $ cmdDescription cm
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaedercmdlProcessCmd :: Command -> CmdlState -> IO CmdlState
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian MaedercmdlProcessCmd c = case find (eqCmd c . cmdDescription) getCommands of
d8a6d1101a0e3d09fb8f8566590cb209c103498aLoredana Mihaela Diaconu Nothing -> return . genMsgAndCode ("unknown command: " ++ cmdNameStr c) 3
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder Just cm -> execCmdlCmd cm { cmdDescription = c }
e4aeced5394758cc762e8817d031855cc1abb02cMarkus GrossprintCmdResult :: CmdlState -> IO CmdlState
e4aeced5394758cc762e8817d031855cc1abb02cMarkus GrossprintCmdResult state = do
e4aeced5394758cc762e8817d031855cc1abb02cMarkus Gross let o = output state
e4aeced5394758cc762e8817d031855cc1abb02cMarkus Gross ms = outputMsg o
e4aeced5394758cc762e8817d031855cc1abb02cMarkus Gross ws = warningMsg o
e4aeced5394758cc762e8817d031855cc1abb02cMarkus Gross es = errorMsg o
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder unless (null ms) $ putStrLn ms
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder unless (null ws) . putStrLn $ "Warning:\n" ++ ws
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder unless (null es) . putStrLn $ "Error:\n" ++ es
e4aeced5394758cc762e8817d031855cc1abb02cMarkus Gross hFlush stdout
e4aeced5394758cc762e8817d031855cc1abb02cMarkus Gross return state { output = emptyCmdlMessage }
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von SchroedercmdlProcessScriptFile :: Bool -> FilePath -> CmdlState -> IO CmdlState
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von SchroedercmdlProcessScriptFile doExit fp st = do
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder str <- readFile fp
d8a6d1101a0e3d09fb8f8566590cb209c103498aLoredana Mihaela Diaconu s <- foldM (\ nst (s, n) -> do
d8a6d1101a0e3d09fb8f8566590cb209c103498aLoredana Mihaela Diaconu (cst, _) <- resetErrorAndProcString fp n s nst
692ba5fae5e32e299f25a45dfb6caaa223e2e7d1Christian Maeder printCmdResult cst) st . number $ lines str
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder when doExit $ exitWith $ case i_state $ intState s of
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder Just x -> let hd : _ = elements x in case hd of
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder Element list _ -> if isNotDisproved (currentTheory list)
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder then getExitCode s
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder else ExitFailure 4
afe840fb938778fff70724bf8339cc4b77c5dfe8Christian Maeder Nothing -> getExitCode s
a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder-- | The function processes the file of instructions
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von SchroedercmdlProcessFile :: Bool -> HetcatsOpts -> FilePath -> IO CmdlState
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von SchroedercmdlProcessFile doExit opts file = do
6b7547c3dc5cef674d1a8f8c9f74d67f694a6188Christian Maeder putIfVerbose opts 2 $ "Processing hets proof file: " ++ file
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder s <- cmdlProcessScriptFile doExit file $ emptyCmdlState opts
0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder when doExit $ exitWith $ getExitCode s