{- |
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 :: Prover Sign Sentence SoftFOLMorphism () ProofTree
metisProver = String
-> String
-> ()
-> (String
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence SoftFOLMorphism]
    -> IO [ProofStatus ProofTree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence SoftFOLMorphism]
    -> IO (ThreadId, MVar ()))
-> Prover Sign Sentence SoftFOLMorphism () ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus proof_tree])
    -> String
    -> TacticScript
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkAutomaticProver "metis" "metis" () String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
metisGUI
  Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
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 :: 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 = ""
  , batchTimeEnv :: String
batchTimeEnv = ""
  , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions
      { problemOutput :: String
problemOutput = ".tptp"
      , proverOutput :: String
proverOutput = ".spass"
      , theoryConfiguration :: String
theoryConfiguration = "" }
  , runProver :: RunProver Sentence ProofTree SoftFOLProverState
runProver = RunProver Sentence ProofTree SoftFOLProverState
runMetis
  , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
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 :: String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
metisGUI 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
metisProver) 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 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 :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
metisProveCMDLautomaticBatch 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
metisProver) String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory Sign Sentence ProofTree
th [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs ProofTree
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 :: RunProver Sentence ProofTree SoftFOLProverState
runMetis sps :: SoftFOLProverState
sps cfg :: GenericConfig ProofTree
cfg saveTPTP :: Bool
saveTPTP thName :: String
thName nGoal :: Named Sentence
nGoal = do
  let saveFile :: String
saveFile = TransSenName
basename 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 <- String
-> SoftFOLProverState -> Named Sentence -> [String] -> IO String
showTPTPProblem String
thName SoftFOLProverState
sps Named Sentence
nGoal []
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveTPTP (String -> String -> IO ()
writeFile String
saveFile String
prob)
  String
timeTmpFile <- String -> String -> IO String
getTempFile String
prob String
saveFile
  HetsTime
start <- IO HetsTime
getHetsTime
  -- try timeout using perl
  (ex :: ExitCode
ex, out :: String
out, err :: String
err) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess "perl"
    ["-e", "alarm shift @ARGV; exec @ARGV"
    , Int -> String
forall a. Show a => a -> String
show (GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg), "metis", String
timeTmpFile] ""
  HetsTime
finish <- IO HetsTime
getHetsTime
  let executetime :: TimeOfDay
executetime = HetsTime -> HetsTime -> TimeOfDay
diffHetsTime HetsTime
finish HetsTime
start
      newCfg :: GenericConfig ProofTree
newCfg = GenericConfig ProofTree
cfg
        { timeUsed :: TimeOfDay
timeUsed = TimeOfDay
executetime
        , proofStatus :: ProofStatus ProofTree
proofStatus = (GenericConfig ProofTree -> ProofStatus ProofTree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig ProofTree
cfg) {usedTime :: TimeOfDay
usedTime = TimeOfDay
executetime}}
      finCfg :: GenericConfig ProofTree
finCfg = GenericConfig ProofTree
newCfg { resultOutput :: [String]
resultOutput = String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
out String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
err }
  String -> IO ()
removeFile String
timeTmpFile
  (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATPRetval, GenericConfig ProofTree)
 -> IO (ATPRetval, GenericConfig ProofTree))
-> (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall a b. (a -> b) -> a -> b
$ case ExitCode
ex of
         ExitSuccess ->
           ( ATPRetval
ATPSuccess
           , GenericConfig ProofTree
finCfg
             { proofStatus :: ProofStatus ProofTree
proofStatus = (GenericConfig ProofTree -> ProofStatus ProofTree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig ProofTree
finCfg)
               { usedAxioms :: [String]
usedAxioms = SoftFOLProverState -> [String]
getAxioms SoftFOLProverState
sps
               , goalStatus :: GoalStatus
goalStatus = String -> GoalStatus
getGoalStatus String
out }})
         ExitFailure e :: Int
e -> if Int
e Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 14 then
           ( ATPRetval
ATPTLimitExceeded
           , GenericConfig ProofTree
newCfg
               { timeLimitExceeded :: Bool
timeLimitExceeded = Bool
True
               , resultOutput :: [String]
resultOutput = ["TimeOut"] })
           else (String -> ATPRetval
ATPError String
err, GenericConfig ProofTree
finCfg)

-- | mapping from SZS Status to Goalstatus
getGoalStatus :: String -> GoalStatus
getGoalStatus :: String -> GoalStatus
getGoalStatus l :: String
l = let ll :: [String]
ll = String -> [String]
lines String
l in
  case (String -> Maybe String) -> [String] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "SZS status") [String]
ll of
  [] -> Reason -> GoalStatus
Open ([String] -> Reason
Reason [String]
ll)
  z :: [String]
z@(s :: String
s : _) -> case String -> [String]
words String
s of
    w :: String
w : _
      | String -> Bool
szsProved String
w -> Bool -> GoalStatus
Proved Bool
True
      | String -> Bool
szsDisproved String
w -> GoalStatus
Disproved
    _ -> Reason -> GoalStatus
Open ([String] -> Reason
Reason [String]
z)