content: {- |
  Module      :  ./SoftFOL/ProveVampire.hs
  Description :  Interface to the Vampire theorem prover via MathServe.
  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 Vampire service, uses GUI.GenericATP.
  See <http://spass.mpi-sb.mpg.de/> for details on SPASS.
  
  -}
  
  module SoftFOL.ProveVampire (vampire, vampireCMDLautomaticBatch) 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.
  -}
  vampire :: Prover Sign Sentence SoftFOLMorphism () ProofTree
  vampire = (mkProverTemplate "Vampire" () vampireGUI)
    { proveCMDLautomaticBatch = Just vampireCMDLautomaticBatch }
  
  vampireHelpText :: String
  vampireHelpText =
    "No help yet available.\n" ++
    "email hets-devel@informatik.uni-bremen.de " ++
    "for more information.\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 = vampireHelpText,
        batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",
        fileExtensions = FileExtensions {problemOutput = ".tptp",
                                        proverOutput = ".vamp",
                                        theoryConfiguration = ".spcf"},
        runProver = runVampire,
        createProverOptions = extraOpts}
  
  -- ** GUI
  
  {- |
    Invokes the generic prover GUI. SPASS specific functions are omitted by
    data type ATPFunctions.
  -}
  vampireGUI :: 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
  vampireGUI thName th freedefs =
      genericATPgui (atpFun thName) True (proverName vampire) thName th
                   freedefs emptyProofTree
  
  -- ** command line function
  
  {- |
    Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
    automatic command line interface to the Vampire prover via MathServe.
    Vampire specific functions are omitted by data type ATPFunctions.
  -}
  vampireCMDLautomaticBatch ::
             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 -}
  vampireCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
                          thName defTS th freedefs =
      genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
          resultMVar (proverName vampire) thName
          (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
  
  {- |
    Runs the Vampire service.
  -}
  runVampire :: 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)
  runVampire sps cfg saveTPTP thName nGoal =
    Exception.catch (do
      prob <- showTPTPProblem thName sps nGoal $ extraOpts cfg ++
                                                   ["Requested prover: Vampire"]
      when saveTPTP
          (writeFile (thName ++ '_' : AS_Anno.senAttr nGoal ++ ".tptp") prob)
      mathServOut <- callMathServ
          MathServCall { mathServService = VampireService,
                        mathServOperation = TPTPProblem,
                        problem = prob,
                        proverTimeLimit = configTimeLimit cfg,
                        extraOptions = Just $ unwords $ extraOpts cfg}
      msResponse <- parseMathServOut mathServOut
      return (mapMathServResponse (getAxioms sps) msResponse cfg nGoal
             $ proverName vampire))
     $ excepToATPResult (proverName vampire) $ AS_Anno.senAttr nGoal
  