content: {- |
  Module      :  ./SoftFOL/ProveMathServ.hs
  Description :  Interface for the MathServe broker.
  Copyright   :  (c) Rene Wagner, Klaus Luettich, Rainer Grabbe,
                     Uni Bremen 2005-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  needs POSIX
  
  Interface for the MathServe broker which calls different ATP systems,
  uses GUI.GenericATP.
  
  -}
  
  {-
      To do:
      - check why an internal error during batch mode running does not invoke
        an error window. Also the proving won't stop.
  -}
  
  module SoftFOL.ProveMathServ
    ( mathServBroker
    , mathServBrokerCMDLautomaticBatch
    ) where
  
  import Logic.Prover
  
  import SoftFOL.Sign
  import SoftFOL.Translate
  import SoftFOL.MathServMapping
  import SoftFOL.MathServParsing
  import SoftFOL.ProverState
  
  import qualified Common.AS_Annotation as AS_Anno
  import qualified Common.Result as Result
  import Common.ProofTree
  
  import Control.Monad (when)
  import qualified Control.Concurrent as Concurrent
  import qualified Control.Exception as Exception
  
  import GUI.GenericATP
  import Interfaces.GenericATPState
  import Proofs.BatchProcessing
  
  -- * Prover implementation
  
  {- |
    The Prover implementation. First runs the batch prover (with graphical
    feedback), then starts the GUI prover.
  -}
  mathServBroker :: Prover Sign Sentence SoftFOLMorphism () ProofTree
  mathServBroker = (mkProverTemplate brokerName () mathServBrokerGUI)
    { proveCMDLautomaticBatch = Just mathServBrokerCMDLautomaticBatch }
  
  mathServHelpText :: String
  mathServHelpText =
    "No help for MathServ available.\n"
  
  -- * Main prover functions
  
  -- ** Utility functions
  
  {- |
    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 = mathServHelpText,
        batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",
        fileExtensions = FileExtensions {problemOutput = ".tptp",
                                        proverOutput = ".spass",
                                        theoryConfiguration = ".spcf"},
        runProver = runMSBroker,
        createProverOptions = extraOpts}
  
  -- ** GUI
  
  {- |
    Invokes the generic prover GUI. SoftFOL specific functions are omitted by
    data type ATPFunctions.
  -}
  mathServBrokerGUI :: 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
  mathServBrokerGUI thName th freedefs =
      genericATPgui (atpFun thName) False (proverName mathServBroker) thName th
                    freedefs emptyProofTree
  
  -- ** command line function
  
  {- |
    Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
    automatic command line interface to the MathServe Broker.
    MathServ specific functions are omitted by data type ATPFunctions.
  -}
  mathServBrokerCMDLautomaticBatch ::
             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 -}
  mathServBrokerCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
                          thName defTS th freedefs =
      genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
          resultMVar (proverName mathServBroker) thName
          (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
  
  
  {- |
    Runs the MathServ broker and returns GUI proof status and prover
    configuration with  proof status and complete prover output.
  -}
  runMSBroker :: 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)
  runMSBroker sps cfg saveTPTP thName nGoal =
    Exception.catch (do
      prob <- showTPTPProblem thName sps nGoal $ extraOpts cfg
              ++ ['[' : brokerName ++ "]"]
      when saveTPTP
          (writeFile (thName ++ '_' : AS_Anno.senAttr nGoal ++ ".tptp") prob)
      mathServOut <- callMathServ
          MathServCall {mathServService = Broker,
                       mathServOperation = ProblemOpt,
                       problem = prob,
                       proverTimeLimit = configTimeLimit cfg,
                       extraOptions = Nothing}
      msResponse <- parseMathServOut mathServOut
      return (mapMathServResponse (getAxioms sps) msResponse cfg nGoal $
              proverName mathServBroker))
     $ excepToATPResult (proverName mathServBroker) $ AS_Anno.senAttr nGoal
  