content: {- |
  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 {gTheorySens = el} =
    checkListDisproved . map
    (map snd . getThmStatus . senAttr . OMap.ele . snd) $ Map.toList el
  
  checkList :: [BasicProof] -> Bool
  checkList [] = False
  checkList (l : ls) = case l of
              BasicProof _ (ProofStatus _ b _ _ _ _ _ _) -> case b of
                Disproved -> True
                _ -> checkList ls
              _ -> checkList ls
  
  checkListDisproved :: [[BasicProof]] -> Bool
  checkListDisproved = all (not . checkList)
  
  cmdlProcessString :: FilePath -> Int -> String -> CmdlState
    -> IO (CmdlState, Maybe Command)
  cmdlProcessString fp l ps st = case parseSingleLine fp l ps of
    Left err -> return (genMsgAndCode err 3 st, Nothing)
    Right c -> let cm = Parser.command c in
         fmap (\ nst -> (nst, Just $ cmdDescription cm)) $ execCmdlCmd cm st
  
  -- sets the errorCode to 0 and then processes the string
  resetErrorAndProcString :: FilePath -> Int -> String -> CmdlState
    -> IO (CmdlState, Maybe Command)
  resetErrorAndProcString fp l ps st =
    cmdlProcessString fp l ps $ resetErrorCode st
  
  execCmdlCmd :: CmdlCmdDescription -> CmdlState -> IO CmdlState
  execCmdlCmd cm =
    case cmdFn cm of
      CmdNoInput f -> f
      CmdWithInput f -> f . cmdInputStr $ cmdDescription cm
  
  cmdlProcessCmd :: Command -> CmdlState -> IO CmdlState
  cmdlProcessCmd c = case find (eqCmd c . cmdDescription) getCommands of
    Nothing -> return . genMsgAndCode ("unknown command: " ++ cmdNameStr c) 3
    Just cm -> execCmdlCmd cm { cmdDescription = c }
  
  printCmdResult :: CmdlState -> IO CmdlState
  printCmdResult state = do
    let o = output state
        ms = outputMsg o
        ws = warningMsg o
        es = errorMsg o
    unless (null ms) $ putStrLn ms
    unless (null ws) . putStrLn $ "Warning:\n" ++ ws
    unless (null es) . putStrLn $ "Error:\n" ++ es
    hFlush stdout
    return state { output = emptyCmdlMessage }
  
  cmdlProcessScriptFile :: Bool -> FilePath -> CmdlState -> IO CmdlState
  cmdlProcessScriptFile doExit fp st = do
    str <- readFile fp
    s <- foldM (\ nst (s, n) -> do
        (cst, _) <- resetErrorAndProcString fp n s nst
        printCmdResult cst) st . number $ lines str
    when doExit $ exitWith $ case i_state $ intState s of
      Just x -> let hd : _ = elements x in case hd of
        Element list _ -> if isNotDisproved (currentTheory list)
            then getExitCode s
            else ExitFailure 4
      Nothing -> getExitCode s
    return s
  
  
  -- | The function processes the file of instructions
  cmdlProcessFile :: Bool -> HetcatsOpts -> FilePath -> IO CmdlState
  cmdlProcessFile doExit opts file = do
    putIfVerbose opts 2 $ "Processing hets proof file: " ++ file
    s <- cmdlProcessScriptFile doExit file $ emptyCmdlState opts
    when doExit $ exitWith $ getExitCode s
    return s
  