{- |
Module      :  ./SoftFOL/ProveDarwin.hs
Description :  Interface to the TPTP theorem prover via Darwin.
Copyright   :  (c) Heng Jiang, Uni Bremen 2004-2007
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

Interface for the Darwin service, uses GUI.GenericATP.
See <http://spass.mpi-sb.mpg.de/> for details on SPASS, and
<http://combination.cs.uiowa.edu/Darwin/> for Darwin.
-}

module SoftFOL.ProveDarwin
  ( darwinProver
  , darwinCMDLautomaticBatch
  , darwinConsChecker
  , runDarwinProcess
  , ProverBinary (..)
  , darwinExe
  , proverBinary
  , tptpProvers
  , eproverOpts
  ) where

-- preliminary hacks for display of CASL models
import Logic.Prover

import SoftFOL.Sign
import SoftFOL.Translate
import SoftFOL.ProverState
import SoftFOL.EProver

import Common.AS_Annotation as AS_Anno
import qualified Common.Result as Result
import Common.ProofTree
import Common.ProverTools
import Common.SZSOntology
import Common.Utils

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

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

import System.Directory
import System.Process (waitForProcess, runInteractiveCommand,
                       runProcess, terminateProcess)
import System.IO (hGetContents, openFile, hClose, IOMode (WriteMode))

import Control.Exception as Exception

import GUI.GenericATP
import Interfaces.GenericATPState
import Proofs.BatchProcessing

import qualified Data.Map as Map
import qualified Data.Set as Set

-- * Prover implementation

data ProverBinary = Darwin | DarwinFD | EDarwin | EProver | Leo | IProver
  deriving (Int -> ProverBinary
ProverBinary -> Int
ProverBinary -> [ProverBinary]
ProverBinary -> ProverBinary
ProverBinary -> ProverBinary -> [ProverBinary]
ProverBinary -> ProverBinary -> ProverBinary -> [ProverBinary]
(ProverBinary -> ProverBinary)
-> (ProverBinary -> ProverBinary)
-> (Int -> ProverBinary)
-> (ProverBinary -> Int)
-> (ProverBinary -> [ProverBinary])
-> (ProverBinary -> ProverBinary -> [ProverBinary])
-> (ProverBinary -> ProverBinary -> [ProverBinary])
-> (ProverBinary -> ProverBinary -> ProverBinary -> [ProverBinary])
-> Enum ProverBinary
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: ProverBinary -> ProverBinary -> ProverBinary -> [ProverBinary]
$cenumFromThenTo :: ProverBinary -> ProverBinary -> ProverBinary -> [ProverBinary]
enumFromTo :: ProverBinary -> ProverBinary -> [ProverBinary]
$cenumFromTo :: ProverBinary -> ProverBinary -> [ProverBinary]
enumFromThen :: ProverBinary -> ProverBinary -> [ProverBinary]
$cenumFromThen :: ProverBinary -> ProverBinary -> [ProverBinary]
enumFrom :: ProverBinary -> [ProverBinary]
$cenumFrom :: ProverBinary -> [ProverBinary]
fromEnum :: ProverBinary -> Int
$cfromEnum :: ProverBinary -> Int
toEnum :: Int -> ProverBinary
$ctoEnum :: Int -> ProverBinary
pred :: ProverBinary -> ProverBinary
$cpred :: ProverBinary -> ProverBinary
succ :: ProverBinary -> ProverBinary
$csucc :: ProverBinary -> ProverBinary
Enum, ProverBinary
ProverBinary -> ProverBinary -> Bounded ProverBinary
forall a. a -> a -> Bounded a
maxBound :: ProverBinary
$cmaxBound :: ProverBinary
minBound :: ProverBinary
$cminBound :: ProverBinary
Bounded)

tptpProvers :: [ProverBinary]
tptpProvers :: [ProverBinary]
tptpProvers = [ProverBinary
forall a. Bounded a => a
minBound .. ProverBinary
forall a. Bounded a => a
maxBound]

proverBinary :: ProverBinary -> String
proverBinary :: ProverBinary -> String
proverBinary b :: ProverBinary
b = ProverBinary -> String
darwinExe ProverBinary
b String -> String -> String
forall a. [a] -> [a] -> [a]
++
  case ProverBinary
b of
    Darwin -> "-non-fd"
    _ -> ""

darwinExe :: ProverBinary -> String
darwinExe :: ProverBinary -> String
darwinExe b :: ProverBinary
b = case ProverBinary
b of
  Darwin -> "darwin"
  DarwinFD -> "darwin"
  EDarwin -> "e-darwin"
  EProver -> "eprover"
  Leo -> "leo"
  IProver -> "iproveropt"

{- | The Prover implementation. First runs the batch prover (with
  graphical feedback), then starts the GUI prover. -}
darwinProver
  :: ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree
darwinProver :: ProverBinary -> Prover Sign Sentence SoftFOLMorphism () ProofTree
darwinProver b :: ProverBinary
b =
  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 (ProverBinary -> String
darwinExe ProverBinary
b) (ProverBinary -> String
proverBinary ProverBinary
b) () (ProverBinary
-> String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
darwinGUI ProverBinary
b)
  ((Bool
  -> Bool
  -> MVar (Result [ProofStatus ProofTree])
  -> String
  -> TacticScript
  -> Theory Sign Sentence ProofTree
  -> [FreeDefMorphism Sentence SoftFOLMorphism]
  -> IO (ThreadId, MVar ()))
 -> Prover Sign Sentence SoftFOLMorphism () 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 a b. (a -> b) -> a -> b
$ ProverBinary
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
darwinCMDLautomaticBatchAux ProverBinary
b

darwinConsChecker
  :: ProverBinary -> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
darwinConsChecker :: ProverBinary
-> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
darwinConsChecker b :: ProverBinary
b =
  (String
-> String
-> ()
-> (String
    -> TacticScript
    -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
    -> [FreeDefMorphism Sentence SoftFOLMorphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
forall sublogics sign sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
mkUsableConsChecker (ProverBinary -> String
darwinExe ProverBinary
b) (ProverBinary -> String
proverBinary ProverBinary
b) () ((String
  -> TacticScript
  -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
  -> [FreeDefMorphism Sentence SoftFOLMorphism]
  -> IO (CCStatus ProofTree))
 -> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree)
-> (String
    -> TacticScript
    -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
    -> [FreeDefMorphism Sentence SoftFOLMorphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
forall a b. (a -> b) -> a -> b
$ ProverBinary
-> String
-> TacticScript
-> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (CCStatus ProofTree)
consCheck ProverBinary
b)
  { ccNeedsTimer :: Bool
ccNeedsTimer = Bool
False }

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: ProverBinary  -- ^ the actual binary
  -> String -- ^ theory name
  -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun :: ProverBinary
-> String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun b :: ProverBinary
b 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 = "no help for darwin available"
  , 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 = ProverBinary -> RunProver Sentence ProofTree SoftFOLProverState
runDarwin ProverBinary
b
  , 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.
-}
darwinGUI
  :: ProverBinary -- ^ the actual binary
  -> String -- ^ theory name
  -> Theory Sign Sentence ProofTree
  -- ^ theory consisting of a signature and sentences
  -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
  -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
darwinGUI :: ProverBinary
-> String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO [ProofStatus ProofTree]
darwinGUI b :: ProverBinary
b 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 (ProverBinary
-> String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun ProverBinary
b String
thName) Bool
True (ProverBinary -> String
proverBinary ProverBinary
b) 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 Darwin prover.
  Darwin specific functions are omitted by data type ATPFunctions.
-}
darwinCMDLautomaticBatch
  :: 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 signature and sentences
  -> [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 -}
darwinCMDLautomaticBatch :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
darwinCMDLautomaticBatch = ProverBinary
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
darwinCMDLautomaticBatchAux ProverBinary
Darwin

darwinCMDLautomaticBatchAux
  :: ProverBinary -- ^ the actual binary
  -> 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 signature and sentences
  -> [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 -}
darwinCMDLautomaticBatchAux :: ProverBinary
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (ThreadId, MVar ())
darwinCMDLautomaticBatchAux b :: ProverBinary
b 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 (ProverBinary
-> String
-> ATPFunctions
     Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
atpFun ProverBinary
b String
thName) Bool
inclProvedThs Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar (ProverBinary -> String
proverBinary ProverBinary
b) String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory Sign Sentence ProofTree
th [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs ProofTree
emptyProofTree

-- * Main prover functions

eproverOpts :: String -> String
eproverOpts :: String -> String
eproverOpts verb :: String
verb = "-xAuto -tAuto --tptp3-format " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
verb
  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " --memory-limit=2048 --soft-cpu-limit="

extras :: ProverBinary -> Bool -> String -> String
extras :: ProverBinary -> Bool -> String -> String
extras b :: ProverBinary
b cons :: Bool
cons tl :: String
tl = let
  tOut :: String
tOut = " -to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl
  darOpt :: String
darOpt = "-pc false"
  fdOpt :: String
fdOpt = String
darOpt String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
cons then " -pmtptp true" else "") String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -fd true"
  in case ProverBinary
b of
    EProver -> String -> String
eproverOpts (if Bool
cons then "-s" else "") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl
    Leo -> "-t " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl
    Darwin -> String
darOpt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tOut
    DarwinFD -> String
fdOpt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tOut
    EDarwin -> String
fdOpt String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -eq Axioms" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tOut
    IProver -> "--time_out_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl String -> String -> String
forall a. [a] -> [a] -> [a]
++ " --sat_mode true"

{- | Runs the Darwin service. The tactic script only contains a string for the
  time limit. -}
consCheck
  :: ProverBinary
  -> String
  -> TacticScript
  -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
  -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
  -> IO (CCStatus ProofTree)
consCheck :: ProverBinary
-> String
-> TacticScript
-> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
-> [FreeDefMorphism Sentence SoftFOLMorphism]
-> IO (CCStatus ProofTree)
consCheck b :: ProverBinary
b thName :: String
thName (TacticScript tl :: String
tl) tm :: TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
tm freedefs :: [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs = case TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
-> Theory Sign Sentence ProofTree
forall sign sen mor proof_tree.
TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
tTarget TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
tm of
    Theory sig :: Sign
sig nSens :: ThSens Sentence (ProofStatus ProofTree)
nSens -> do
        let proverStateI :: SoftFOLProverState
proverStateI = InitialProverState Sign Sentence SoftFOLMorphism SoftFOLProverState
spassProverState Sign
sig (ThSens Sentence (ProofStatus ProofTree) -> [Named Sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens Sentence (ProofStatus ProofTree)
nSens) [FreeDefMorphism Sentence SoftFOLMorphism]
freedefs
        String
prob <- String -> SoftFOLProverState -> [String] -> IO String
showTPTPProblemM String
thName SoftFOLProverState
proverStateI []
        (exitCode :: String
exitCode, out :: [String]
out, tUsed :: Int
tUsed) <-
          String
-> Bool -> String -> String -> String -> IO (String, [String], Int)
runDarwinProcess (ProverBinary -> String
darwinExe ProverBinary
b) Bool
False (ProverBinary -> Bool -> String -> String
extras ProverBinary
b Bool
True String
tl) String
thName String
prob
        let outState :: CCStatus ProofTree
outState = CCStatus :: forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
CCStatus
               { ccResult :: Maybe Bool
ccResult = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
               , ccProofTree :: ProofTree
ccProofTree = String -> ProofTree
ProofTree (String -> ProofTree) -> String -> ProofTree
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
exitCode String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
out
               , ccUsedTime :: TimeOfDay
ccUsedTime = 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 }
        CCStatus ProofTree -> IO (CCStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (CCStatus ProofTree -> IO (CCStatus ProofTree))
-> CCStatus ProofTree -> IO (CCStatus ProofTree)
forall a b. (a -> b) -> a -> b
$ if String -> Bool
szsProved String
exitCode then CCStatus ProofTree
outState else
                    CCStatus ProofTree
outState
                    { ccResult :: Maybe Bool
ccResult = if String -> Bool
szsDisproved String
exitCode then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                                 else Maybe Bool
forall a. Maybe a
Nothing }

runDarwinProcess
  :: String -- ^ binary name
  -> Bool -- ^ save problem
  -> String -- ^ options
  -> String -- ^ filename without extension
  -> String -- ^ problem
  -> IO (String, [String], Int)
runDarwinProcess :: String
-> Bool -> String -> String -> String -> IO (String, [String], Int)
runDarwinProcess bin :: String
bin saveTPTP :: Bool
saveTPTP options :: String
options tmpFileName :: String
tmpFileName prob :: String
prob = do
  let tmpFile :: String
tmpFile = String -> String
basename String
tmpFileName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".tptp"
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveTPTP (String -> String -> IO ()
writeFile String
tmpFile String
prob)
  Bool
noProg <- String -> IO Bool
missingExecutableInPath String
bin
  if Bool
noProg then
    (String, [String], Int) -> IO (String, [String], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
bin String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found. Check your $PATH", [], -1)
    else do
    String
timeTmpFile <- String -> String -> IO String
getTempFile String
prob String
tmpFile
    (_, pout :: String
pout, perr :: String
perr) <-
      String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
bin (String -> [String]
words String
options [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
timeTmpFile]) ""
    let l :: [String]
l = String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
pout String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
perr
        (res :: String
res, _, tUsed :: Int
tUsed) = [String] -> (String, Bool, Int)
parseOutput [String]
l
    String -> IO ()
removeFile String
timeTmpFile
    (String, [String], Int) -> IO (String, [String], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
res, [String]
l, Int
tUsed)

mkGraph :: String -> IO ()
mkGraph :: String -> IO ()
mkGraph f :: String
f = do
 String
fContent <- String -> IO String
readFile String
f
 let fLines :: [String]
fLines = String -> [String]
lines String
fContent
 let ((p_set :: Set String
p_set, (cs :: [(String, String)]
cs, axs :: [(String, String)]
axs)), res :: Maybe String
res) =
      ((Set String, ([(String, String)], [(String, String)]))
 -> ProofStep
 -> (Set String, ([(String, String)], [(String, String)])))
-> (Set String, ([(String, String)], [(String, String)]))
-> [String]
-> ((Set String, ([(String, String)], [(String, String)])),
    Maybe String)
forall a.
(a -> ProofStep -> a) -> a -> [String] -> (a, Maybe String)
processProof ((Set String -> ProofStep -> Set String)
-> (([(String, String)], [(String, String)])
    -> ProofStep -> ([(String, String)], [(String, String)]))
-> (Set String, ([(String, String)], [(String, String)]))
-> ProofStep
-> (Set String, ([(String, String)], [(String, String)]))
forall a b c.
(a -> b -> a) -> (c -> b -> c) -> (a, c) -> b -> (a, c)
zipF Set String -> ProofStep -> Set String
proofInfo ((([(String, String)], [(String, String)])
  -> ProofStep -> ([(String, String)], [(String, String)]))
 -> (Set String, ([(String, String)], [(String, String)]))
 -> ProofStep
 -> (Set String, ([(String, String)], [(String, String)])))
-> (([(String, String)], [(String, String)])
    -> ProofStep -> ([(String, String)], [(String, String)]))
-> (Set String, ([(String, String)], [(String, String)]))
-> ProofStep
-> (Set String, ([(String, String)], [(String, String)]))
forall a b. (a -> b) -> a -> b
$ ([(String, String)] -> ProofStep -> [(String, String)])
-> ([(String, String)] -> ProofStep -> [(String, String)])
-> ([(String, String)], [(String, String)])
-> ProofStep
-> ([(String, String)], [(String, String)])
forall a b c.
(a -> b -> a) -> (c -> b -> c) -> (a, c) -> b -> (a, c)
zipF [(String, String)] -> ProofStep -> [(String, String)]
conjectures [(String, String)] -> ProofStep -> [(String, String)]
axioms)
       (Set String
forall a. Set a
Set.empty, ([], [])) ([String]
 -> ((Set String, ([(String, String)], [(String, String)])),
     Maybe String))
-> [String]
-> ((Set String, ([(String, String)], [(String, String)])),
    Maybe String)
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse [String]
fLines
     (aliases :: Map String String
aliases, _) = (Map String String -> ProofStep -> Map String String)
-> Map String String
-> [String]
-> (Map String String, Maybe String)
forall a.
(a -> ProofStep -> a) -> a -> [String] -> (a, Maybe String)
processProof Map String String -> ProofStep -> Map String String
alias Map String String
forall k a. Map k a
Map.empty [String]
fLines
     same_rank :: String
same_rank = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "; " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, n :: String
n) -> 'v' Char -> String -> String
forall a. a -> [a] -> [a]
: String
n) ([(String, String)] -> [String]) -> [(String, String)] -> [String]
forall a b. (a -> b) -> a -> b
$
                 ((String, String) -> Bool)
-> [(String, String)] -> [(String, String)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, n :: String
n) -> String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
n Set String
p_set
                                Bool -> Bool -> Bool
&& Maybe String -> Bool
forall a. Maybe a -> Bool
isNothing (String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
n Map String String
aliases)) ([(String, String)] -> [(String, String)])
-> [(String, String)] -> [(String, String)]
forall a b. (a -> b) -> a -> b
$ [(String, String)]
cs [(String, String)] -> [(String, String)] -> [(String, String)]
forall a. [a] -> [a] -> [a]
++ [(String, String)]
axs
 case Maybe String
res of
  Just s :: String
s -> String -> IO ()
putStrLn String
s
  _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
 String -> String -> IO ()
writeFile "/tmp/graph.dot" (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ["digraph {",
  "subgraph { rank = same; " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
same_rank String -> String -> String
forall a. [a] -> [a] -> [a]
++ " }",
  (\ (_, _, d :: String
d, _) -> String
d) ((Set String, Set String, String, Map (String, [String]) String)
 -> String)
-> (((Set String, Set String, String,
      Map (String, [String]) String),
     Maybe String)
    -> (Set String, Set String, String, Map (String, [String]) String))
-> ((Set String, Set String, String,
     Map (String, [String]) String),
    Maybe String)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Set String, Set String, String, Map (String, [String]) String),
 Maybe String)
-> (Set String, Set String, String, Map (String, [String]) String)
forall a b. (a, b) -> a
fst (((Set String, Set String, String, Map (String, [String]) String),
  Maybe String)
 -> String)
-> ((Set String, Set String, String,
     Map (String, [String]) String),
    Maybe String)
-> String
forall a b. (a -> b) -> a -> b
$ ((Set String, Set String, String, Map (String, [String]) String)
 -> ProofStep
 -> (Set String, Set String, String, Map (String, [String]) String))
-> (Set String, Set String, String, Map (String, [String]) String)
-> [String]
-> ((Set String, Set String, String,
     Map (String, [String]) String),
    Maybe String)
forall a.
(a -> ProofStep -> a) -> a -> [String] -> (a, Maybe String)
processProof (Set String
-> Map String String
-> (Set String, Set String, String, Map (String, [String]) String)
-> ProofStep
-> (Set String, Set String, String, Map (String, [String]) String)
digraph Set String
p_set Map String String
aliases)
   (Set String
forall a. Set a
Set.empty, Set String
forall a. Set a
Set.empty, "", Map (String, [String]) String
forall k a. Map k a
Map.empty) [String]
fLines, "}"]

runEProverBuffered
  :: Bool -- ^ save problem
  -> Bool
  -> Bool
  -> String -- ^ options
  -> String -- ^ filename without extension
  -> String -- ^ problem
  -> IO (String, [String], Int)
runEProverBuffered :: Bool
-> Bool
-> Bool
-> String
-> String
-> String
-> IO (String, [String], Int)
runEProverBuffered saveTPTP :: Bool
saveTPTP graph :: Bool
graph fullgraph :: Bool
fullgraph options :: String
options tmpFileName :: String
tmpFileName prob :: String
prob = do
  Bool
s <- IO Bool
supportsProofObject
  let tmpFile :: String
tmpFile = String -> String
basename String
tmpFileName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".tptp"
      useProofObject :: Bool
useProofObject = Bool
s Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
fullgraph
      bin :: String
bin = if Bool
useProofObject then "eprover"
            else "eproof"
  Bool
noProg <- String -> IO Bool
missingExecutableInPath String
bin
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveTPTP (String -> String -> IO ()
writeFile String
tmpFile String
prob)
  if Bool
noProg then (String, [String], Int) -> IO (String, [String], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
bin String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found. Check your $PATH", [], -1)
    else do
   (err :: Handle
err, out :: Handle
out) <-
      do
       String
timeTmpFile <- String -> String -> IO String
getTempFile String
prob String
tmpFile
       (_, out :: Handle
out, err :: Handle
err, _) <-
        if Bool
graph Bool -> Bool -> Bool
|| Bool
fullgraph Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
s then do
              String
bufferFile <- String -> String -> IO String
getTempFile "" "eprover-proof-buffer"
              Handle
buff <- String -> IOMode -> IO Handle
openFile String
bufferFile IOMode
WriteMode
              ProcessHandle
h <- String
-> [String]
-> Maybe String
-> Maybe [(String, String)]
-> Maybe Handle
-> Maybe Handle
-> Maybe Handle
-> IO ProcessHandle
runProcess String
bin (String -> [String]
words String
options [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                    ["--proof-object" | Bool
useProofObject] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
timeTmpFile])
                    Maybe String
forall a. Maybe a
Nothing Maybe [(String, String)]
forall a. Maybe a
Nothing Maybe Handle
forall a. Maybe a
Nothing (Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
buff) (Handle -> Maybe Handle
forall a. a -> Maybe a
Just Handle
buff)
              (ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
h IO ExitCode -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
removeFile String
timeTmpFile)
               IO () -> (AsyncException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`Exception.catch` (\ ThreadKilled -> ProcessHandle -> IO ()
terminateProcess ProcessHandle
h)
              Handle -> IO ()
hClose Handle
buff
              String -> IO ()
mkGraph String
bufferFile
              String -> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveCommand (String -> IO (Handle, Handle, Handle, ProcessHandle))
-> String -> IO (Handle, Handle, Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ["egrep", "axiom|SZS",
                String
bufferFile, "&&", "rm", "-f", String
bufferFile]
        else String -> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveCommand (String -> IO (Handle, Handle, Handle, ProcessHandle))
-> String -> IO (Handle, Handle, Handle, ProcessHandle)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
             [String
bin, "--proof-object", String
options, String
timeTmpFile,
              "|", "egrep", "axiom|SZS", "&&", "rm", String
timeTmpFile]
       (Handle, Handle) -> IO (Handle, Handle)
forall (m :: * -> *) a. Monad m => a -> m a
return (Handle
out, Handle
err)
   String
perr <- Handle -> IO String
hGetContents Handle
err
   String
pout <- Handle -> IO String
hGetContents Handle
out
   let l :: [String]
l = String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
perr String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pout
       (res :: String
res, _, tUsed :: Int
tUsed) = [String] -> (String, Bool, Int)
parseOutput [String]
l
   (String, [String], Int) -> IO (String, [String], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
res, [String]
l, Int
tUsed)

runDarwin
  :: ProverBinary
  -> 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)
runDarwin :: ProverBinary -> RunProver Sentence ProofTree SoftFOLProverState
runDarwin b :: ProverBinary
b sps :: SoftFOLProverState
sps cfg :: GenericConfig ProofTree
cfg saveTPTP :: Bool
saveTPTP thName :: String
thName nGoal :: Named Sentence
nGoal = do
    let bin :: String
bin = ProverBinary -> String
darwinExe ProverBinary
b
        (options :: [String]
options, graph :: Bool
graph, fullgraph :: Bool
fullgraph) = case ProverBinary
b of
          EProver ->
           let w :: [String]
w = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg
           in ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\ e :: String
e -> String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
e ["--graph", "--full-graph"])) [String]
w,
               String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem "--graph" [String]
w, String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem "--full-graph" [String]
w)
          _ -> (GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg, Bool
False, Bool
False)
        tl :: String
tl = String -> (Int -> String) -> Maybe Int -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "10" Int -> String
forall a. Show a => a -> String
show (Maybe Int -> String) -> Maybe Int -> String
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit GenericConfig ProofTree
cfg
        extraOptions :: String
extraOptions = ProverBinary -> Bool -> String -> String
extras ProverBinary
b Bool
False String
tl
        tmpFileName :: String
tmpFileName = 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
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
$ [String]
options [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["Requested prover: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bin]
    (exitCode :: String
exitCode, out :: [String]
out, tUsed :: Int
tUsed) <- case ProverBinary
b of
      EProver -> Bool
-> Bool
-> Bool
-> String
-> String
-> String
-> IO (String, [String], Int)
runEProverBuffered Bool
saveTPTP Bool
graph Bool
fullgraph
                  String
extraOptions String
tmpFileName String
prob
      _ -> String
-> Bool -> String -> String -> String -> IO (String, [String], Int)
runDarwinProcess String
bin Bool
saveTPTP String
extraOptions String
tmpFileName String
prob
    [String]
axs <- case ProverBinary
b of
            EProver | String -> Bool
szsProved String
exitCode Bool -> Bool -> Bool
||
                      String -> Bool
szsDisproved String
exitCode ->
                         case ([(String, String)] -> ProofStep -> [(String, String)])
-> [(String, String)]
-> [String]
-> ([(String, String)], Maybe String)
forall a.
(a -> ProofStep -> a) -> a -> [String] -> (a, Maybe String)
processProof [(String, String)] -> ProofStep -> [(String, String)]
axioms [] [String]
out of
                          (l :: [(String, String)]
l, Nothing) -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> a
fst [(String, String)]
l
                          (_, Just err :: String
err) -> do
                                            String -> IO ()
putStrLn String
err
                                            [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ SoftFOLProverState -> [String]
getAxioms SoftFOLProverState
sps
            _ -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ SoftFOLProverState -> [String]
getAxioms SoftFOLProverState
sps
    let ctime :: TimeOfDay
ctime = 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
        (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 Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
nGoal) String
bin ProofTree
emptyProofTree)
                       { usedTime :: TimeOfDay
usedTime = TimeOfDay
ctime
                       , 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 = [String]
options} }

        disProvedStatus :: ProofStatus ProofTree
disProvedStatus = ProofStatus ProofTree
defaultProofStatus {goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved}
        provedStatus :: ProofStatus ProofTree
provedStatus = ProofStatus ProofTree
defaultProofStatus
          { goalName :: String
goalName = Named Sentence -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named Sentence
nGoal
          , goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
          , usedAxioms :: [String]
usedAxioms = [String]
axs
          , usedProver :: String
usedProver = String
bin
          , 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
          }
    (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 = case ProverBinary
b of
                                      EProver -> [String] -> [String]
forall a. [a] -> [a]
reverse [String]
out
                                      _ -> [String]
out,
                      timeUsed :: TimeOfDay
timeUsed = TimeOfDay
ctime })

getSZSStatusWord :: String -> Maybe String
getSZSStatusWord :: String -> Maybe String
getSZSStatusWord line :: String
line = case String -> [String]
words (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ 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 -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "%# ") String
line of
  [] -> Maybe String
forall a. Maybe a
Nothing
  w :: String
w : _ -> String -> Maybe String
forall a. a -> Maybe a
Just String
w

parseOutput :: [String] -> (String, Bool, Int)
  -- ^ (exit code, status found, used time)
parseOutput :: [String] -> (String, Bool, Int)
parseOutput = ((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)
forall c.
Read c =>
(String, Bool, c) -> String -> (String, Bool, c)
checkLine ("could not determine SZS status", Bool
False, -1)
  where checkLine :: (String, Bool, c) -> String -> (String, Bool, c)
checkLine (exCode :: String
exCode, stateFound :: Bool
stateFound, to :: c
to) line :: String
line =
          if String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Couldn't find eprover" String
line
             Bool -> Bool -> Bool
|| String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "darwin -h for further information" String
line
                -- error by running darwin.
            then (String
line, Bool
stateFound, c
to)
            else case String -> Maybe String
getSZSStatusWord String
line of
                Just szsState :: String
szsState | Bool -> Bool
not Bool
stateFound ->
                  (String
szsState, Bool
True, c
to)
                _ -> if "CPU  Time" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
line  -- get cpu time
                  then let time :: c
time = case (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isDigit (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall a. [a] -> a
last (String -> [String]
words String
line) of
                             ds :: String
ds@(_ : _) -> String -> c
forall a. Read a => String -> a
read String
ds
                             _ -> c
to
                       in (String
exCode, Bool
stateFound, c
time)
                  else (String
exCode, Bool
stateFound, c
to)