{- |
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 :: Prover Sign Sentence SoftFOLMorphism () ProofTree
mathServBroker = (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 String
brokerName () String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
mathServBrokerGUI)
  { 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 ())
mathServBrokerCMDLautomaticBatch }

mathServHelpText :: String
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 :: String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun thName :: String
thName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> TransSenName
-> (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 :: TransSenName
atpTransSenName = TransSenName
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
mathServHelpText,
      batchTimeEnv :: String
batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",
      fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions {problemOutput :: String
problemOutput = ".tptp",
                                      proverOutput :: String
proverOutput = ".spass",
                                      theoryConfiguration :: String
theoryConfiguration = ".spcf"},
      runProver :: RunProver Sentence ProofTree SoftFOLProverState
runProver = RunProver Sentence ProofTree SoftFOLProverState
runMSBroker,
      createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
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 :: String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
mathServBrokerGUI 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
False (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
mathServBroker) 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 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 :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
mathServBrokerCMDLautomaticBatch 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
mathServBroker) String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory Sign Sentence ProofTree
th [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs ProofTree
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 :: RunProver Sentence ProofTree SoftFOLProverState
runMSBroker 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]
++ ['[' Char -> TransSenName
forall a. a -> [a] -> [a]
: String
brokerName String -> TransSenName
forall a. [a] -> [a] -> [a]
++ "]"]
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveTPTP
        (String -> String -> IO ()
writeFile (String
thName String -> TransSenName
forall a. [a] -> [a] -> [a]
++ '_' Char -> TransSenName
forall a. a -> [a] -> [a]
: Named Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
nGoal String -> TransSenName
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
Broker,
                     mathServOperation :: MathServOperationTypes
mathServOperation = MathServOperationTypes
ProblemOpt,
                     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 = Maybe String
forall a. Maybe a
Nothing}
    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
mathServBroker))
   ((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
mathServBroker) (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