content: {- |
  Module      :  ./SoftFOL/ProveMetis.hs
  Copyright   :  (c) Christian Maeder, DFKI GmbH 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (ATP GUI)
  
  call metis prover
  -}
  
  module SoftFOL.ProveMetis
    ( metisProver
    , metisProveCMDLautomaticBatch
    ) where
  
  import Common.AS_Annotation as AS_Anno
  import Common.ProofTree
  import Common.Timing
  import Common.Utils
  import Common.SZSOntology
  import qualified Common.Result as Result
  
  import qualified Control.Concurrent as Concurrent
  import Control.Monad
  
  import Data.List
  import Data.Maybe
  
  import GUI.GenericATP
  
  import Interfaces.GenericATPState
  
  import Logic.Prover
  
  import Proofs.BatchProcessing
  
  import SoftFOL.ProverState
  import SoftFOL.Sign
  import SoftFOL.Translate
  
  import System.Directory
  import System.Exit
  
  -- | The Prover implementation.
  metisProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree
  metisProver = mkAutomaticProver "metis" "metis" () metisGUI
    metisProveCMDLautomaticBatch
  
  {- |
    Record for prover specific functions. This is used by both GUI and command
    line interface.
  -}
  atpFun :: String -- ^ theory name
    -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
  atpFun thName = ATPFunctions
    { initialProverState = spassProverState
    , atpTransSenName = transSenName
    , atpInsertSentence = insertSentenceGen
    , goalOutput = showTPTPProblem thName
    , proverHelpText = ""
    , batchTimeEnv = ""
    , fileExtensions = FileExtensions
        { problemOutput = ".tptp"
        , proverOutput = ".spass"
        , theoryConfiguration = "" }
    , runProver = runMetis
    , createProverOptions = extraOpts }
  
  
  {- |
    Invokes the generic prover GUI.
  -}
  metisGUI :: String -- ^ theory name
             -> Theory Sign Sentence ProofTree
             {- ^ theory consisting of a SoftFOL.Sign.Sign
             and a list of Named SoftFOL.Sign.Sentence -}
             -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
             -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
  metisGUI thName th freedefs =
      genericATPgui (atpFun thName) True (proverName metisProver) thName th
                    freedefs emptyProofTree
  
  
  -- ** command line function
  
  {- |
    Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
    automatic command line interface to the Metis prover.
  -}
  
  metisProveCMDLautomaticBatch ::
             Bool -- ^ True means include proved theorems
          -> Bool -- ^ True means save problem file
          -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
             -- ^ used to store the result of the batch run
          -> String -- ^ theory name
          -> TacticScript -- ^ default tactic script
          -> Theory Sign Sentence ProofTree {- ^ theory consisting of a
             'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence' -}
          -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
          -> IO (Concurrent.ThreadId, Concurrent.MVar ())
             {- ^ fst: identifier of the batch thread for killing it
             snd: MVar to wait for the end of the thread -}
  metisProveCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
                          thName defTS th freedefs =
      genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
          resultMVar (proverName metisProver) thName
          (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
  
  
  runMetis :: SoftFOLProverState
             {- ^ logical part containing the input Sign and axioms and possibly
             goals that have been proved earlier as additional axioms -}
             -> GenericConfig ProofTree -- ^ configuration to use
             -> Bool -- ^ True means save TPTP file
             -> String -- ^ name of the theory in the DevGraph
             -> AS_Anno.Named SPTerm -- ^ goal to prove
             -> IO (ATPRetval, GenericConfig ProofTree)
             -- ^ (retval, configuration with proof status and complete output)
  runMetis sps cfg saveTPTP thName nGoal = do
    let saveFile = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".tptp"
    prob <- showTPTPProblem thName sps nGoal []
    when saveTPTP (writeFile saveFile prob)
    timeTmpFile <- getTempFile prob saveFile
    start <- getHetsTime
    -- try timeout using perl
    (ex, out, err) <- executeProcess "perl"
      ["-e", "alarm shift @ARGV; exec @ARGV"
      , show (configTimeLimit cfg), "metis", timeTmpFile] ""
    finish <- getHetsTime
    let executetime = diffHetsTime finish start
        newCfg = cfg
          { timeUsed = executetime
          , proofStatus = (proofStatus cfg) {usedTime = executetime}}
        finCfg = newCfg { resultOutput = lines $ out ++ err }
    removeFile timeTmpFile
    return $ case ex of
           ExitSuccess ->
             ( ATPSuccess
             , finCfg
               { proofStatus = (proofStatus finCfg)
                 { usedAxioms = getAxioms sps
                 , goalStatus = getGoalStatus out }})
           ExitFailure e -> if e == 14 then
             ( ATPTLimitExceeded
             , newCfg
                 { timeLimitExceeded = True
                 , resultOutput = ["TimeOut"] })
             else (ATPError err, finCfg)
  
  -- | mapping from SZS Status to Goalstatus
  getGoalStatus :: String -> GoalStatus
  getGoalStatus l = let ll = lines l in
    case mapMaybe (stripPrefix "SZS status") ll of
    [] -> Open (Reason ll)
    z@(s : _) -> case words s of
      w : _
        | szsProved w -> Proved True
        | szsDisproved w -> Disproved
      _ -> Open (Reason z)
  