{- |
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 :: Prover Sign Sentence SoftFOLMorphism () ProofTree
vampire = (String
-> ()
-> (String
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence SoftFOLMorphism]
    -> IO [ProofStatus ProofTree])
-> Prover Sign Sentence SoftFOLMorphism () ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkProverTemplate "Vampire" () String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
vampireGUI)
  { proveCMDLautomaticBatch :: Maybe
  (Bool
   -> Bool
   -> MVar (Result [ProofStatus ProofTree])
   -> String
   -> TacticScript
   -> Theory Sign Sentence ProofTree
   -> [FreeDefMorphism Sentence SoftFOLMorphism]
   -> IO (ThreadId, MVar ()))
proveCMDLautomaticBatch = (Bool
 -> Bool
 -> MVar (Result [ProofStatus ProofTree])
 -> String
 -> TacticScript
 -> Theory Sign Sentence ProofTree
 -> [FreeDefMorphism Sentence SoftFOLMorphism]
 -> IO (ThreadId, MVar ()))
-> Maybe
     (Bool
      -> Bool
      -> MVar (Result [ProofStatus ProofTree])
      -> String
      -> TacticScript
      -> Theory Sign Sentence ProofTree
      -> [FreeDefMorphism Sentence SoftFOLMorphism]
      -> IO (ThreadId, MVar ()))
forall a. a -> Maybe a
Just Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
vampireCMDLautomaticBatch }

vampireHelpText :: String
vampireHelpText :: String
vampireHelpText =
  "No help yet available.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
  "email hets-devel@informatik.uni-bremen.de " String -> String -> String
forall a. [a] -> [a] -> [a]
++
  "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 :: String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun thName :: String
thName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> (String -> String)
-> (pst -> Named sentence -> pst)
-> (pst -> Named sentence -> [String] -> IO String)
-> String
-> String
-> FileExtensions
-> RunProver sentence proof_tree pst
-> (GenericConfig proof_tree -> [String])
-> ATPFunctions sign sentence morphism proof_tree pst
ATPFunctions
    { initialProverState :: InitialProverState Sign Sentence SoftFOLMorphism SoftFOLProverState
initialProverState = InitialProverState Sign Sentence SoftFOLMorphism SoftFOLProverState
spassProverState,
      atpTransSenName :: String -> String
atpTransSenName = String -> String
transSenName,
      atpInsertSentence :: SoftFOLProverState -> Named Sentence -> SoftFOLProverState
atpInsertSentence = SoftFOLProverState -> Named Sentence -> SoftFOLProverState
insertSentenceGen,
      goalOutput :: SoftFOLProverState -> Named Sentence -> [String] -> IO String
goalOutput = String
-> SoftFOLProverState -> Named Sentence -> [String] -> IO String
showTPTPProblem String
thName,
      proverHelpText :: String
proverHelpText = String
vampireHelpText,
      batchTimeEnv :: String
batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",
      fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions {problemOutput :: String
problemOutput = ".tptp",
                                      proverOutput :: String
proverOutput = ".vamp",
                                      theoryConfiguration :: String
theoryConfiguration = ".spcf"},
      runProver :: RunProver Sentence ProofTree SoftFOLProverState
runProver = RunProver Sentence ProofTree SoftFOLProverState
runVampire,
      createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
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 :: String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
vampireGUI thName :: String
thName th :: Theory Sign Sentence ProofTree
th freedefs :: [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs =
    ATPFunctions
  Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
-> Bool
-> String
-> String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> ProofTree
-> IO [ProofStatus ProofTree]
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui (String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun String
thName) Bool
True (Prover Sign Sentence SoftFOLMorphism () ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign Sentence SoftFOLMorphism () ProofTree
vampire) String
thName Theory Sign Sentence ProofTree
th
                 [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs ProofTree
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 :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
vampireCMDLautomaticBatch inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus ProofTree])
resultMVar
                        thName :: String
thName defTS :: TacticScript
defTS th :: Theory Sign Sentence ProofTree
th freedefs :: [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs =
    ATPFunctions
  Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> ProofTree
-> IO (ThreadId, MVar ())
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> String
-> ATPTacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO (ThreadId, MVar ())
genericCMDLautomaticBatch (String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun String
thName) Bool
inclProvedThs Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar (Prover Sign Sentence SoftFOLMorphism () ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign Sentence SoftFOLMorphism () ProofTree
vampire) String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory Sign Sentence ProofTree
th [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs ProofTree
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 :: RunProver Sentence ProofTree SoftFOLProverState
runVampire sps :: SoftFOLProverState
sps cfg :: GenericConfig ProofTree
cfg saveTPTP :: Bool
saveTPTP thName :: String
thName nGoal :: Named Sentence
nGoal =
  IO (ATPRetval, GenericConfig ProofTree)
-> (SomeException -> IO (ATPRetval, GenericConfig ProofTree))
-> IO (ATPRetval, GenericConfig ProofTree)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Exception.catch (do
    String
prob <- String
-> SoftFOLProverState -> Named Sentence -> [String] -> IO String
showTPTPProblem String
thName SoftFOLProverState
sps Named Sentence
nGoal ([String] -> IO String) -> [String] -> IO String
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                                                 ["Requested prover: Vampire"]
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveTPTP
        (String -> String -> IO ()
writeFile (String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Named Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
nGoal String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".tptp") String
prob)
    Either String String
mathServOut <- MathServCall -> IO (Either String String)
callMathServ
        MathServCall :: MathServServices
-> MathServOperationTypes
-> String
-> Int
-> Maybe String
-> MathServCall
MathServCall { mathServService :: MathServServices
mathServService = MathServServices
VampireService,
                      mathServOperation :: MathServOperationTypes
mathServOperation = MathServOperationTypes
TPTPProblem,
                      problem :: String
problem = String
prob,
                      proverTimeLimit :: Int
proverTimeLimit = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg,
                      extraOptions :: Maybe String
extraOptions = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg}
    Either String MathServResponse
msResponse <- Either String String -> IO (Either String MathServResponse)
parseMathServOut Either String String
mathServOut
    (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return ([String]
-> Either String MathServResponse
-> GenericConfig ProofTree
-> Named Sentence
-> String
-> (ATPRetval, GenericConfig ProofTree)
mapMathServResponse (SoftFOLProverState -> [String]
getAxioms SoftFOLProverState
sps) Either String MathServResponse
msResponse GenericConfig ProofTree
cfg Named Sentence
nGoal
           (String -> (ATPRetval, GenericConfig ProofTree))
-> String -> (ATPRetval, GenericConfig ProofTree)
forall a b. (a -> b) -> a -> b
$ Prover Sign Sentence SoftFOLMorphism () ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign Sentence SoftFOLMorphism () ProofTree
vampire))
   ((SomeException -> IO (ATPRetval, GenericConfig ProofTree))
 -> IO (ATPRetval, GenericConfig ProofTree))
-> (SomeException -> IO (ATPRetval, GenericConfig ProofTree))
-> IO (ATPRetval, GenericConfig ProofTree)
forall a b. (a -> b) -> a -> b
$ String
-> String
-> SomeException
-> IO (ATPRetval, GenericConfig ProofTree)
excepToATPResult (Prover Sign Sentence SoftFOLMorphism () ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign Sentence SoftFOLMorphism () ProofTree
vampire) (String
 -> SomeException -> IO (ATPRetval, GenericConfig ProofTree))
-> String
-> SomeException
-> IO (ATPRetval, GenericConfig ProofTree)
forall a b. (a -> b) -> a -> b
$ Named Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
nGoal