{- |
Module      :  ./THF/SZSProver.hs
Description :  General Interface to a prover using SZS status messages
Copyright   :  (c) Jonathan von Schroeder, DFKI Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  non-portable (imports Prover)

Isabelle theorem prover for THF
-}

module THF.SZSProver
  ( createSZSProver
  , ProverType
  , ProverFuncs (..)
  ) where

import Logic.Prover

import THF.As (THFFormula)
import THF.Sign
import THF.ProverState
import THF.Sublogic

import Common.AS_Annotation as AS_Anno
import Common.Result
import Common.ProofTree
import Common.Utils (basename, timeoutCommand)
import Common.SZSOntology

import GUI.GenericATP

import Interfaces.GenericATPState

import Control.Monad (unless)
import qualified Control.Concurrent as Concurrent

import Proofs.BatchProcessing

import System.Directory

import Data.List
import Data.Maybe
import Data.Time (timeToTimeOfDay)
import Data.Time.Clock (secondsToDiffTime)


data ProverFuncs = ProverFuncs {
 ProverFuncs -> GenericConfig ProofTree -> Int
cfgTimeout :: GenericConfig ProofTree -> Int, -- in seconds
 ProverFuncs
-> Int
-> String
-> GenericConfig ProofTree
-> IO (String, [String])
proverCommand :: Int -> String -> GenericConfig ProofTree ->
                  IO (String, [String]),
 -- timeout -> problem file
 ProverFuncs -> String -> String -> String -> String
getMessage :: String -> String -> String -> String,
 -- result -> std out -> std err
 ProverFuncs -> String -> Maybe Int
getTimeUsed :: String -> Maybe Int -- in seconds
}

type ProverType = Prover SignTHF THFFormula MorphismTHF THFSl ProofTree

createSZSProver :: String -> String -> String -> ProverFuncs ->
                   ProverType
createSZSProver :: String -> String -> String -> ProverFuncs -> ProverType
createSZSProver bin :: String
bin name :: String
name hlp :: String
hlp d :: ProverFuncs
d = String
-> String
-> THFSl
-> (String
    -> Theory SignTHF THFFormula ProofTree
    -> [FreeDefMorphism THFFormula MorphismTHF]
    -> IO [ProofStatus ProofTree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory SignTHF THFFormula ProofTree
    -> [FreeDefMorphism THFFormula MorphismTHF]
    -> IO (ThreadId, MVar ()))
-> ProverType
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 String
bin String
name THFSl
tHF0
 (String
-> String
-> ProverFuncs
-> String
-> Theory SignTHF THFFormula ProofTree
-> [FreeDefMorphism THFFormula MorphismTHF]
-> IO [ProofStatus ProofTree]
proverGUI String
hlp String
name ProverFuncs
d)
 (String
-> String
-> ProverFuncs
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory SignTHF THFFormula ProofTree
-> [FreeDefMorphism THFFormula MorphismTHF]
-> IO (ThreadId, MVar ())
proverCMDLautomaticBatch String
hlp String
name ProverFuncs
d)

atpFun :: ProverFuncs
  -> String -- name
  -> String -- ^ theory name
  -> String -- help text
  -> ATPFunctions SignTHF THFFormula MorphismTHF ProofTree ProverStateTHF
atpFun :: ProverFuncs
-> String
-> String
-> String
-> ATPFunctions
     SignTHF THFFormula MorphismTHF ProofTree ProverStateTHF
atpFun d :: ProverFuncs
d name :: String
name _ hlp :: String
hlp = 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 SignTHF THFFormula MorphismTHF ProverStateTHF
initialProverState = InitialProverState SignTHF THFFormula MorphismTHF ProverStateTHF
initialProverStateTHF
  , atpTransSenName :: String -> String
atpTransSenName = String -> String
forall a. a -> a
id
  , atpInsertSentence :: ProverStateTHF -> Named THFFormula -> ProverStateTHF
atpInsertSentence = ProverStateTHF -> Named THFFormula -> ProverStateTHF
insertSentenceTHF
  , goalOutput :: ProverStateTHF -> Named THFFormula -> [String] -> IO String
goalOutput = ProverStateTHF -> Named THFFormula -> [String] -> IO String
showProblemTHF
  , proverHelpText :: String
proverHelpText = String
hlp
  , batchTimeEnv :: String
batchTimeEnv = "HETS_TPTP_BATCH_TIME_LIMIT"
  , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions {
      problemOutput :: String
problemOutput = ".p"
    , proverOutput :: String
proverOutput = ""
    , theoryConfiguration :: String
theoryConfiguration = "" }
  , runProver :: RunProver THFFormula ProofTree ProverStateTHF
runProver = ProverFuncs
-> String -> RunProver THFFormula ProofTree ProverStateTHF
runProverT ProverFuncs
d String
name
  , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts }

proverGUI :: String -- help text
    -> String -- name
    -> ProverFuncs
    -> String -- ^ theory name
    -> Theory SignTHF THFFormula ProofTree
    -> [FreeDefMorphism THFFormula MorphismTHF] -- ^ freeness constraints
    -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
proverGUI :: String
-> String
-> ProverFuncs
-> String
-> Theory SignTHF THFFormula ProofTree
-> [FreeDefMorphism THFFormula MorphismTHF]
-> IO [ProofStatus ProofTree]
proverGUI hlp :: String
hlp name :: String
name d :: ProverFuncs
d thName :: String
thName th :: Theory SignTHF THFFormula ProofTree
th freedefs :: [FreeDefMorphism THFFormula MorphismTHF]
freedefs =
    ATPFunctions
  SignTHF THFFormula MorphismTHF ProofTree ProverStateTHF
-> Bool
-> String
-> String
-> Theory SignTHF THFFormula ProofTree
-> [FreeDefMorphism THFFormula MorphismTHF]
-> 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 (ProverFuncs
-> String
-> String
-> String
-> ATPFunctions
     SignTHF THFFormula MorphismTHF ProofTree ProverStateTHF
atpFun ProverFuncs
d String
name String
thName String
hlp) Bool
True String
name String
thName Theory SignTHF THFFormula ProofTree
th
                  [FreeDefMorphism THFFormula MorphismTHF]
freedefs ProofTree
emptyProofTree

proverCMDLautomaticBatch
  :: String -- help
  -> String -- name
  -> ProverFuncs
  -> Bool -- ^ True means include proved theorems
  -> Bool -- ^ True means save problem file
  -> Concurrent.MVar (Result [ProofStatus ProofTree])
  -- ^ used to store the result of the batch run
  -> String -- ^ theory name
  -> TacticScript -- ^ default tactic script
  -> Theory SignTHF THFFormula ProofTree
  -- ^ theory consisting of a signature and sentences
  -> [FreeDefMorphism THFFormula MorphismTHF] -- ^ 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 -}
proverCMDLautomaticBatch :: String
-> String
-> ProverFuncs
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory SignTHF THFFormula ProofTree
-> [FreeDefMorphism THFFormula MorphismTHF]
-> IO (ThreadId, MVar ())
proverCMDLautomaticBatch hlp :: String
hlp name :: String
name d :: ProverFuncs
d inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus ProofTree])
resultMVar
                        thName :: String
thName defTS :: TacticScript
defTS th :: Theory SignTHF THFFormula ProofTree
th freedefs :: [FreeDefMorphism THFFormula MorphismTHF]
freedefs =
    ATPFunctions
  SignTHF THFFormula MorphismTHF ProofTree ProverStateTHF
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory SignTHF THFFormula ProofTree
-> [FreeDefMorphism THFFormula MorphismTHF]
-> 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 (ProverFuncs
-> String
-> String
-> String
-> ATPFunctions
     SignTHF THFFormula MorphismTHF ProofTree ProverStateTHF
atpFun ProverFuncs
d String
name String
thName String
hlp) Bool
inclProvedThs
        Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar String
name String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory SignTHF THFFormula ProofTree
th [FreeDefMorphism THFFormula MorphismTHF]
freedefs ProofTree
emptyProofTree

runProverT :: ProverFuncs
    -> String -- name
    -> ProverStateTHF
    -> GenericConfig ProofTree -- ^ configuration to use
    -> Bool -- ^ True means save THF file
    -> String -- ^ name of the theory in the DevGraph
    -> Named THFFormula -- ^ goal to prove
    -> IO (ATPRetval, GenericConfig ProofTree)
    -- ^ (retval, configuration with proof status and complete output)
runProverT :: ProverFuncs
-> String -> RunProver THFFormula ProofTree ProverStateTHF
runProverT d :: ProverFuncs
d name :: String
name pst :: ProverStateTHF
pst cfg :: GenericConfig ProofTree
cfg saveTHF :: Bool
saveTHF thName :: String
thName nGoal :: Named THFFormula
nGoal = do
    let tout :: Int
tout = ProverFuncs -> GenericConfig ProofTree -> Int
cfgTimeout ProverFuncs
d GenericConfig ProofTree
cfg
        tmpFileName :: String
tmpFileName = String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Named THFFormula -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named THFFormula
nGoal
    String
prob <- ProverStateTHF -> Named THFFormula -> [String] -> IO String
showProblemTHF ProverStateTHF
pst Named THFFormula
nGoal []
    Maybe (String, [String], Int)
runRes <- ProverFuncs
-> GenericConfig ProofTree
-> Int
-> Bool
-> String
-> String
-> IO (Maybe (String, [String], Int))
runProverProcess ProverFuncs
d GenericConfig ProofTree
cfg Int
tout Bool
saveTHF String
tmpFileName String
prob
    case Maybe (String, [String], Int)
runRes of
        Nothing -> (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
ATPTLimitExceeded, GenericConfig ProofTree
cfg
                        { proofStatus :: ProofStatus ProofTree
proofStatus =
                            (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus (Named THFFormula -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named THFFormula
nGoal)
                                            String
name ProofTree
emptyProofTree)
                                { usedTime :: TimeOfDay
usedTime =
                                   DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime (Integer -> DiffTime) -> Integer -> DiffTime
forall a b. (a -> b) -> a -> b
$
                                   Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
tout
                                , tacticScript :: TacticScript
tacticScript = String -> TacticScript
TacticScript
                                    (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
                                        { tsTimeLimit :: Int
tsTimeLimit = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg,
                                          tsExtraOpts :: [String]
tsExtraOpts = [] } }
                        , timeUsed :: TimeOfDay
timeUsed =
                           DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime (Integer -> DiffTime) -> Integer -> DiffTime
forall a b. (a -> b) -> a -> b
$
                           Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
tout })
        Just (exitCode :: String
exitCode, out :: [String]
out, tUsed :: Int
tUsed) ->
         let (err :: ATPRetval
err, retval :: ProofStatus ProofTree
retval) = case () of
                _ | String -> Bool
szsProved String
exitCode -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
provedStatus)
                _ | String -> Bool
szsDisproved String
exitCode -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
disProvedStatus)
                _ | String -> Bool
szsTimeout String
exitCode ->
                                    (ATPRetval
ATPTLimitExceeded, ProofStatus ProofTree
defaultProofStatus)
                _ | String -> Bool
szsStopped String
exitCode ->
                                    (ATPRetval
ATPBatchStopped, ProofStatus ProofTree
defaultProofStatus)
                _ ->
                                    (String -> ATPRetval
ATPError String
exitCode, ProofStatus ProofTree
defaultProofStatus)
             defaultProofStatus :: ProofStatus ProofTree
defaultProofStatus =
              (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus (Named THFFormula -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named THFFormula
nGoal) String
name ProofTree
emptyProofTree)
                       { usedTime :: TimeOfDay
usedTime =
                          DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime (Integer -> DiffTime) -> Integer -> DiffTime
forall a b. (a -> b) -> a -> b
$
                          Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
tUsed
                       , tacticScript :: TacticScript
tacticScript = String -> TacticScript
TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
                            { tsTimeLimit :: Int
tsTimeLimit = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg,
                              tsExtraOpts :: [String]
tsExtraOpts = [] } }
             disProvedStatus :: ProofStatus ProofTree
disProvedStatus = ProofStatus ProofTree
defaultProofStatus {goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved}
             provedStatus :: ProofStatus ProofTree
provedStatus = ProofStatus ProofTree
defaultProofStatus { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
                                              , usedAxioms :: [String]
usedAxioms = ProverStateTHF -> [String]
getAxioms ProverStateTHF
pst }
         in (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
err, GenericConfig ProofTree
cfg { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
retval
                         , resultOutput :: [String]
resultOutput = [String]
out
                         , timeUsed :: TimeOfDay
timeUsed =
                             DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime (Integer -> DiffTime) -> Integer -> DiffTime
forall a b. (a -> b) -> a -> b
$
                             Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
tUsed })

runProverProcess
    :: ProverFuncs
    -> GenericConfig ProofTree -- config
    -> Int -- ^ timeout time in seconds
    -> Bool -- ^ save problem
    -> String -- ^ filename without extension
    -> String -- ^ problem
    -> IO (Maybe (String, [String], Int))
runProverProcess :: ProverFuncs
-> GenericConfig ProofTree
-> Int
-> Bool
-> String
-> String
-> IO (Maybe (String, [String], Int))
runProverProcess d :: ProverFuncs
d cfg :: GenericConfig ProofTree
cfg tout :: Int
tout saveTHF :: Bool
saveTHF tmpFileName :: String
tmpFileName prob :: String
prob = do
    let tmpFile :: String
tmpFile = String -> String
basename String
tmpFileName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".p"
    String -> String -> IO ()
writeFile String
tmpFile String
prob
    (cmd :: String
cmd, args :: [String]
args) <- ProverFuncs
-> Int
-> String
-> GenericConfig ProofTree
-> IO (String, [String])
proverCommand ProverFuncs
d Int
tout String
tmpFile GenericConfig ProofTree
cfg
    Maybe (ExitCode, String, String)
mres <- Int -> String -> [String] -> IO (Maybe (ExitCode, String, String))
timeoutCommand Int
tout String
cmd [String]
args
    IO (Maybe (String, [String], Int))
-> ((ExitCode, String, String)
    -> IO (Maybe (String, [String], Int)))
-> Maybe (ExitCode, String, String)
-> IO (Maybe (String, [String], Int))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe (String, [String], Int) -> IO (Maybe (String, [String], Int))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, [String], Int)
forall a. Maybe a
Nothing) (\ (_, pout :: String
pout, perr :: String
perr) -> do
        let l :: [String]
l = String -> [String]
lines String
pout
            (res' :: String
res', _, tUsed :: Int
tUsed) = ProverFuncs -> [String] -> (String, Bool, Int)
parseOutput ProverFuncs
d [String]
l
            res :: String
res = ProverFuncs -> String -> String -> String -> String
getMessage ProverFuncs
d String
res' String
pout String
perr
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
saveTHF (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
tmpFile
        Maybe (String, [String], Int) -> IO (Maybe (String, [String], Int))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, [String], Int)
 -> IO (Maybe (String, [String], Int)))
-> Maybe (String, [String], Int)
-> IO (Maybe (String, [String], Int))
forall a b. (a -> b) -> a -> b
$ (String, [String], Int) -> Maybe (String, [String], Int)
forall a. a -> Maybe a
Just (String
res, [String]
l, Int
tUsed)) Maybe (ExitCode, String, String)
mres

-- parse the output and return the szsStatus and the used time.
parseOutput :: ProverFuncs -> [String] -> (String, Bool, Int)
  -- ^ (exit code, status found, used time ins ms)
parseOutput :: ProverFuncs -> [String] -> (String, Bool, Int)
parseOutput d :: ProverFuncs
d = ((String, Bool, Int) -> String -> (String, Bool, Int))
-> (String, Bool, Int) -> [String] -> (String, Bool, Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (String, Bool, Int) -> String -> (String, Bool, Int)
checkLine ("", Bool
False, -1) where
   checkLine :: (String, Bool, Int) -> String -> (String, Bool, Int)
checkLine (exCode :: String
exCode, stateFound :: Bool
stateFound, to :: Int
to) line :: String
line = case String -> Maybe String
getSZSStatusWord String
line of
        Just szsState :: String
szsState | Bool -> Bool
not Bool
stateFound -> (String
szsState, Bool
True, Int
to)
        _ -> case ProverFuncs -> String -> Maybe Int
getTimeUsed ProverFuncs
d String
line of
              Just secs :: Int
secs -> (String
exCode, Bool
stateFound, Int
secs)
              Nothing -> (String
exCode, Bool
stateFound, Int
to)

-- try to read the szs status from a given String
getSZSStatusWord :: String -> Maybe String
getSZSStatusWord :: String -> Maybe String
getSZSStatusWord line :: String
line =
    case String -> [String]
words (String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix "% SZS status" String
line) of
        [] -> Maybe String
forall a. Maybe a
Nothing
        w :: String
w : _ -> String -> Maybe String
forall a. a -> Maybe a
Just String
w