{- | Module : ./CMDL/ProcessScript.hs Description : process script commands Copyright : (c) Christian Maeder, DFKI GmbH 2009 License : GPLv2 or higher, see LICENSE.txt Maintainer : Christian.Maeder@dfki.de Stability : provisional Portability : portable -} module CMDL.ProcessScript where import Interfaces.Command import Interfaces.DataTypes import Driver.Options import CMDL.DataTypes import CMDL.DataTypesUtils import CMDL.Commands import CMDL.ParseProofScript as Parser import Common.Utils import Data.List import Control.Monad import System.IO import System.Exit import Static.GTheory import qualified Data.Map as Map import Common.AS_Annotation import Proofs.AbstractState import qualified Common.OrderedMap as OMap import Logic.Prover isNotDisproved :: G_theory -> Bool isNotDisproved :: G_theory -> Bool isNotDisproved G_theory {gTheorySens :: () gTheorySens = ThSens sentence (AnyComorphism, BasicProof) el} = [[BasicProof]] -> Bool checkListDisproved ([[BasicProof]] -> Bool) -> ([(String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))] -> [[BasicProof]]) -> [(String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))] -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . ((String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> [BasicProof]) -> [(String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))] -> [[BasicProof]] forall a b. (a -> b) -> [a] -> [b] map (((AnyComorphism, BasicProof) -> BasicProof) -> [(AnyComorphism, BasicProof)] -> [BasicProof] forall a b. (a -> b) -> [a] -> [b] map (AnyComorphism, BasicProof) -> BasicProof forall a b. (a, b) -> b snd ([(AnyComorphism, BasicProof)] -> [BasicProof]) -> ((String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> [(AnyComorphism, BasicProof)]) -> (String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> [BasicProof] forall b c a. (b -> c) -> (a -> b) -> a -> c . ThmStatus (AnyComorphism, BasicProof) -> [(AnyComorphism, BasicProof)] forall a. ThmStatus a -> [a] getThmStatus (ThmStatus (AnyComorphism, BasicProof) -> [(AnyComorphism, BasicProof)]) -> ((String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> ThmStatus (AnyComorphism, BasicProof)) -> (String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> [(AnyComorphism, BasicProof)] forall b c a. (b -> c) -> (a -> b) -> a -> c . SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> ThmStatus (AnyComorphism, BasicProof) forall s a. SenAttr s a -> a senAttr (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> ThmStatus (AnyComorphism, BasicProof)) -> ((String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))) -> (String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> ThmStatus (AnyComorphism, BasicProof) forall b c a. (b -> c) -> (a -> b) -> a -> c . ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))) -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) forall a. ElemWOrd a -> a OMap.ele (ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))) -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))) -> ((String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> (String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) forall b c a. (b -> c) -> (a -> b) -> a -> c . (String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))) -> ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))) forall a b. (a, b) -> b snd) ([(String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))] -> Bool) -> [(String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))] -> Bool forall a b. (a -> b) -> a -> b $ ThSens sentence (AnyComorphism, BasicProof) -> [(String, ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))] forall k a. Map k a -> [(k, a)] Map.toList ThSens sentence (AnyComorphism, BasicProof) el checkList :: [BasicProof] -> Bool checkList :: [BasicProof] -> Bool checkList [] = Bool False checkList (l :: BasicProof l : ls :: [BasicProof] ls) = case BasicProof l of BasicProof _ (ProofStatus _ b :: GoalStatus b _ _ _ _ _ _) -> case GoalStatus b of Disproved -> Bool True _ -> [BasicProof] -> Bool checkList [BasicProof] ls _ -> [BasicProof] -> Bool checkList [BasicProof] ls checkListDisproved :: [[BasicProof]] -> Bool checkListDisproved :: [[BasicProof]] -> Bool checkListDisproved = ([BasicProof] -> Bool) -> [[BasicProof]] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all (Bool -> Bool not (Bool -> Bool) -> ([BasicProof] -> Bool) -> [BasicProof] -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . [BasicProof] -> Bool checkList) cmdlProcessString :: FilePath -> Int -> String -> CmdlState -> IO (CmdlState, Maybe Command) cmdlProcessString :: String -> Int -> String -> CmdlState -> IO (CmdlState, Maybe Command) cmdlProcessString fp :: String fp l :: Int l ps :: String ps st :: CmdlState st = case String -> Int -> String -> Either String LitCommand parseSingleLine String fp Int l String ps of Left err :: String err -> (CmdlState, Maybe Command) -> IO (CmdlState, Maybe Command) forall (m :: * -> *) a. Monad m => a -> m a return (String -> Int -> CmdlState -> CmdlState genMsgAndCode String err 3 CmdlState st, Maybe Command forall a. Maybe a Nothing) Right c :: LitCommand c -> let cm :: CmdlCmdDescription cm = LitCommand -> CmdlCmdDescription Parser.command LitCommand c in (CmdlState -> (CmdlState, Maybe Command)) -> IO CmdlState -> IO (CmdlState, Maybe Command) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (\ nst :: CmdlState nst -> (CmdlState nst, Command -> Maybe Command forall a. a -> Maybe a Just (Command -> Maybe Command) -> Command -> Maybe Command forall a b. (a -> b) -> a -> b $ CmdlCmdDescription -> Command cmdDescription CmdlCmdDescription cm)) (IO CmdlState -> IO (CmdlState, Maybe Command)) -> IO CmdlState -> IO (CmdlState, Maybe Command) forall a b. (a -> b) -> a -> b $ CmdlCmdDescription -> CmdlState -> IO CmdlState execCmdlCmd CmdlCmdDescription cm CmdlState st -- sets the errorCode to 0 and then processes the string resetErrorAndProcString :: FilePath -> Int -> String -> CmdlState -> IO (CmdlState, Maybe Command) resetErrorAndProcString :: String -> Int -> String -> CmdlState -> IO (CmdlState, Maybe Command) resetErrorAndProcString fp :: String fp l :: Int l ps :: String ps st :: CmdlState st = String -> Int -> String -> CmdlState -> IO (CmdlState, Maybe Command) cmdlProcessString String fp Int l String ps (CmdlState -> IO (CmdlState, Maybe Command)) -> CmdlState -> IO (CmdlState, Maybe Command) forall a b. (a -> b) -> a -> b $ CmdlState -> CmdlState resetErrorCode CmdlState st execCmdlCmd :: CmdlCmdDescription -> CmdlState -> IO CmdlState execCmdlCmd :: CmdlCmdDescription -> CmdlState -> IO CmdlState execCmdlCmd cm :: CmdlCmdDescription cm = case CmdlCmdDescription -> CmdlCmdFnClasses cmdFn CmdlCmdDescription cm of CmdNoInput f :: CmdlState -> IO CmdlState f -> CmdlState -> IO CmdlState f CmdWithInput f :: String -> CmdlState -> IO CmdlState f -> String -> CmdlState -> IO CmdlState f (String -> CmdlState -> IO CmdlState) -> (Command -> String) -> Command -> CmdlState -> IO CmdlState forall b c a. (b -> c) -> (a -> b) -> a -> c . Command -> String cmdInputStr (Command -> CmdlState -> IO CmdlState) -> Command -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ CmdlCmdDescription -> Command cmdDescription CmdlCmdDescription cm cmdlProcessCmd :: Command -> CmdlState -> IO CmdlState cmdlProcessCmd :: Command -> CmdlState -> IO CmdlState cmdlProcessCmd c :: Command c = case (CmdlCmdDescription -> Bool) -> [CmdlCmdDescription] -> Maybe CmdlCmdDescription forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a find (Command -> Command -> Bool eqCmd Command c (Command -> Bool) -> (CmdlCmdDescription -> Command) -> CmdlCmdDescription -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . CmdlCmdDescription -> Command cmdDescription) [CmdlCmdDescription] getCommands of Nothing -> CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return (CmdlState -> IO CmdlState) -> (CmdlState -> CmdlState) -> CmdlState -> IO CmdlState forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> Int -> CmdlState -> CmdlState genMsgAndCode ("unknown command: " String -> String -> String forall a. [a] -> [a] -> [a] ++ Command -> String cmdNameStr Command c) 3 Just cm :: CmdlCmdDescription cm -> CmdlCmdDescription -> CmdlState -> IO CmdlState execCmdlCmd CmdlCmdDescription cm { cmdDescription :: Command cmdDescription = Command c } printCmdResult :: CmdlState -> IO CmdlState printCmdResult :: CmdlState -> IO CmdlState printCmdResult state :: CmdlState state = do let o :: CmdlMessage o = CmdlState -> CmdlMessage output CmdlState state ms :: String ms = CmdlMessage -> String outputMsg CmdlMessage o ws :: String ws = CmdlMessage -> String warningMsg CmdlMessage o es :: String es = CmdlMessage -> String errorMsg CmdlMessage o Bool -> IO () -> IO () forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless (String -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null String ms) (IO () -> IO ()) -> IO () -> IO () forall a b. (a -> b) -> a -> b $ String -> IO () putStrLn String ms Bool -> IO () -> IO () forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless (String -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null String ws) (IO () -> IO ()) -> (String -> IO ()) -> String -> IO () forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> IO () putStrLn (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ "Warning:\n" String -> String -> String forall a. [a] -> [a] -> [a] ++ String ws Bool -> IO () -> IO () forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless (String -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null String es) (IO () -> IO ()) -> (String -> IO ()) -> String -> IO () forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> IO () putStrLn (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ "Error:\n" String -> String -> String forall a. [a] -> [a] -> [a] ++ String es Handle -> IO () hFlush Handle stdout CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return CmdlState state { output :: CmdlMessage output = CmdlMessage emptyCmdlMessage } cmdlProcessScriptFile :: Bool -> FilePath -> CmdlState -> IO CmdlState cmdlProcessScriptFile :: Bool -> String -> CmdlState -> IO CmdlState cmdlProcessScriptFile doExit :: Bool doExit fp :: String fp st :: CmdlState st = do String str <- String -> IO String readFile String fp CmdlState s <- (CmdlState -> (String, Int) -> IO CmdlState) -> CmdlState -> [(String, Int)] -> IO CmdlState forall (t :: * -> *) (m :: * -> *) b a. (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b foldM (\ nst :: CmdlState nst (s :: String s, n :: Int n) -> do (cst :: CmdlState cst, _) <- String -> Int -> String -> CmdlState -> IO (CmdlState, Maybe Command) resetErrorAndProcString String fp Int n String s CmdlState nst CmdlState -> IO CmdlState printCmdResult CmdlState cst) CmdlState st ([(String, Int)] -> IO CmdlState) -> ([String] -> [(String, Int)]) -> [String] -> IO CmdlState forall b c a. (b -> c) -> (a -> b) -> a -> c . [String] -> [(String, Int)] forall a. [a] -> [(a, Int)] number ([String] -> IO CmdlState) -> [String] -> IO CmdlState forall a b. (a -> b) -> a -> b $ String -> [String] lines String str Bool -> IO () -> IO () forall (f :: * -> *). Applicative f => Bool -> f () -> f () when Bool doExit (IO () -> IO ()) -> IO () -> IO () forall a b. (a -> b) -> a -> b $ ExitCode -> IO () forall a. ExitCode -> IO a exitWith (ExitCode -> IO ()) -> ExitCode -> IO () forall a b. (a -> b) -> a -> b $ case IntState -> Maybe IntIState i_state (IntState -> Maybe IntIState) -> IntState -> Maybe IntIState forall a b. (a -> b) -> a -> b $ CmdlState -> IntState intState CmdlState s of Just x :: IntIState x -> let hd :: Int_NodeInfo hd : _ = IntIState -> [Int_NodeInfo] elements IntIState x in case Int_NodeInfo hd of Element list :: ProofState list _ -> if G_theory -> Bool isNotDisproved (ProofState -> G_theory currentTheory ProofState list) then CmdlState -> ExitCode getExitCode CmdlState s else Int -> ExitCode ExitFailure 4 Nothing -> CmdlState -> ExitCode getExitCode CmdlState s CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return CmdlState s -- | The function processes the file of instructions cmdlProcessFile :: Bool -> HetcatsOpts -> FilePath -> IO CmdlState cmdlProcessFile :: Bool -> HetcatsOpts -> String -> IO CmdlState cmdlProcessFile doExit :: Bool doExit opts :: HetcatsOpts opts file :: String file = do HetcatsOpts -> Int -> String -> IO () putIfVerbose HetcatsOpts opts 2 (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ "Processing hets proof file: " String -> String -> String forall a. [a] -> [a] -> [a] ++ String file CmdlState s <- Bool -> String -> CmdlState -> IO CmdlState cmdlProcessScriptFile Bool doExit String file (CmdlState -> IO CmdlState) -> CmdlState -> IO CmdlState forall a b. (a -> b) -> a -> b $ HetcatsOpts -> CmdlState emptyCmdlState HetcatsOpts opts Bool -> IO () -> IO () forall (f :: * -> *). Applicative f => Bool -> f () -> f () when Bool doExit (IO () -> IO ()) -> IO () -> IO () forall a b. (a -> b) -> a -> b $ ExitCode -> IO () forall a. ExitCode -> IO a exitWith (ExitCode -> IO ()) -> ExitCode -> IO () forall a b. (a -> b) -> a -> b $ CmdlState -> ExitCode getExitCode CmdlState s CmdlState -> IO CmdlState forall (m :: * -> *) a. Monad m => a -> m a return CmdlState s