{- |
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