{- |
Module      :  $Header$
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
