{- |
Module      :  ./TPTP/ProveHyper.hs
Description :  Interface to the theorem prover e-krhyper in CASC-mode.
Copyright   :  (c) Otto-von-Guericke University of Magdeburg, 2020
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  mscodescu@gmail.com
Stability   :  provisional
Portability :  needs POSIX

Check out
http://www.uni-koblenz.de/~bpelzer/ekrhyper/
for details. For the ease of maintenance we are using e-krhyper in
its CASC-mode, aka tptp-input. It works for single input files and
fof-style.
-}

module TPTP.ProveHyper (hyperS, hyperProver, hyperConsChecker)
    where

import Logic.Prover

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

import TPTP.Sign
import TPTP.Morphism
import TPTP.Translate
import TPTP.Prover.ProverState
import TPTP.Sublogic

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

import System.Directory

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

import Data.Char
import Data.List
import Data.Maybe

import Data.Time.LocalTime (TimeOfDay, midnight)

-- Prover

hyperS :: String
hyperS :: String
hyperS = "ekrh"

sublogics :: Sublogic
sublogics :: Sublogic
sublogics = Sublogic
FOF

-- | The Prover implementation.
hyperProver :: Prover Sign Sentence Morphism Sublogic ProofTree
hyperProver :: Prover Sign Sentence Morphism Sublogic ProofTree
hyperProver =
  String
-> String
-> Sublogic
-> (String
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence Morphism]
    -> IO [ProofStatus ProofTree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory Sign Sentence ProofTree
    -> [FreeDefMorphism Sentence Morphism]
    -> IO (ThreadId, MVar ()))
-> Prover Sign Sentence Morphism Sublogic 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 String
hyperS String
hyperS Sublogic
sublogics String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO [ProofStatus ProofTree]
hyperGUI Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO (ThreadId, MVar ())
hyperCMDLautomaticBatch

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: String -- ^ theory name
  -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
atpFun :: String -> ATPFunctions Sign Sentence Morphism ProofTree ProverState
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 Morphism ProverState
initialProverState = InitialProverState Sign Sentence Morphism ProverState
tptpProverState
  , atpTransSenName :: TransSenName
atpTransSenName = TransSenName
transSenName
  , atpInsertSentence :: ProverState -> Named Sentence -> ProverState
atpInsertSentence = ProverState -> Named Sentence -> ProverState
insertSentenceIntoProverState
  , goalOutput :: ProverState -> Named Sentence -> [String] -> IO String
goalOutput = String -> ProverState -> Named Sentence -> [String] -> IO String
ioShowTPTPProblem String
thName
  , proverHelpText :: String
proverHelpText = "for more information visit " String -> TransSenName
forall a. [a] -> [a] -> [a]
++
                     "http://www.uni-koblenz.de/~bpelzer/ekrhyper/"
  , batchTimeEnv :: String
batchTimeEnv = "HETS_HYPER_BATCH_TIME_LIMIT"
  , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions
      { problemOutput :: String
problemOutput = ".tptp"
      , proverOutput :: String
proverOutput = ".hyper"
      , theoryConfiguration :: String
theoryConfiguration = ".hypcf" }
  , runProver :: RunProver Sentence ProofTree ProverState
runProver = RunProver Sentence ProofTree ProverState
runHyper
  , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts }

{- |
  Invokes the generic prover GUI.
-}
hyperGUI :: String -- ^ theory name
           -> Theory Sign Sentence ProofTree
           -> [FreeDefMorphism Sentence Morphism] -- ^ freeness constraints
           -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
hyperGUI :: String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO [ProofStatus ProofTree]
hyperGUI thName :: String
thName th :: Theory Sign Sentence ProofTree
th freedefs :: [FreeDefMorphism Sentence Morphism]
freedefs =
    ATPFunctions Sign Sentence Morphism ProofTree ProverState
-> Bool
-> String
-> String
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> 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 Morphism ProofTree ProverState
atpFun String
thName) Bool
True String
hyperS String
thName Theory Sign Sentence ProofTree
th
                  [FreeDefMorphism Sentence Morphism]
freedefs ProofTree
emptyProofTree

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the prover.
-}
hyperCMDLautomaticBatch ::
           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 -- ^ input theory
        -> [FreeDefMorphism Sentence Morphism] -- ^ 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 -}
hyperCMDLautomaticBatch :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO (ThreadId, MVar ())
hyperCMDLautomaticBatch 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 Morphism]
freedefs =
    ATPFunctions Sign Sentence Morphism ProofTree ProverState
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory Sign Sentence ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> 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 Morphism ProofTree ProverState
atpFun String
thName) Bool
inclProvedThs Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar String
hyperS String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory Sign Sentence ProofTree
th [FreeDefMorphism Sentence Morphism]
freedefs ProofTree
emptyProofTree

prelTxt :: String -> String
prelTxt :: TransSenName
prelTxt t :: String
t =
    "% only print essential output\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(set_verbosity(2)).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% assume all input to be in tptp-syntax\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(set_parameter(input_type, 2)).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% To prevent blowing up my memory\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(set_memory_limit(500)).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% produce SZS results\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(set_flag(szs_output_flag, true)).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% do not use special evaluable symbols\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(clear_builtins).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% initial term weight bound, 3 recommended for TPTP-problems\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(set_parameter(max_weight_initial, 3)).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% Terminate if out of memory\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(set_parameter(limit_termination_method,0)).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% Terminate if out of time\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(set_parameter(timeout_termination_method,0)).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% Start timer\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(start_wallclock_timer(" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
t String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".0)).\n"

checkOption :: String -> Bool
checkOption :: String -> Bool
checkOption a :: String
a = String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "#(" String
a Bool -> Bool -> Bool
&& String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf ")." String
a

uniteOptions :: [String] -> [String]
uniteOptions :: [String] -> [String]
uniteOptions opts :: [String]
opts =
    case [String]
opts of
      a :: String
a : b :: String
b : cs :: [String]
cs ->
          if String -> Bool
checkOption String
a
           then
               String
a String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
uniteOptions (String
b String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
cs)
           else
               (String
a String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
b) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
uniteOptions [String]
cs
      _ -> [String]
opts

runTxt :: String
runTxt :: String
runTxt =
    "% start derivation with the input received so far\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(run).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% print normal E-KRHyper proof\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "%#(print_proof).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% print result and proof using SZS terminology;\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% requires postprocessing with post_szs script for proper legibility\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(print_szs_proof).\n"

runHyper :: ProverState
           {- ^ 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 Sentence -- ^ goal to prove
           -> IO (ATPRetval, GenericConfig ProofTree)
           -- ^ (retval, configuration with proof status and complete output)
runHyper :: RunProver Sentence ProofTree ProverState
runHyper sps :: ProverState
sps cfg :: GenericConfig ProofTree
cfg saveTPTP :: Bool
saveTPTP thName :: String
thName nGoal :: Named Sentence
nGoal =
    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"
        simpleOptions :: [String]
simpleOptions = [String] -> [String]
uniteOptions ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg
        tl :: Int
tl = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg
        tScript :: TacticScript
tScript = 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 = Int
tl
          , tsExtraOpts :: [String]
tsExtraOpts = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "#")
              ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ TransSenName
prelTxt (Int -> String
forall a. Show a => a -> String
show Int
tl) String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
runTxt }
        defProofStat :: ProofStatus ProofTree
defProofStat = (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
senAttr Named Sentence
nGoal)
          String
hyperS
          ProofTree
emptyProofTree) { tacticScript :: TacticScript
tacticScript = TacticScript
tScript }
    in
        if (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all String -> Bool
checkOption [String]
simpleOptions
         then
           do
             String
prob <- String -> ProverState -> Named Sentence -> [String] -> IO String
ioShowTPTPProblem String
thName ProverState
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)
             (stdoutC :: String
stdoutC, stderrC :: String
stderrC, t_u :: TimeOfDay
t_u) <- String
-> String
-> String
-> String
-> String
-> IO (String, String, TimeOfDay)
runHyperProcess String
prob String
saveFile (Int -> String
forall a. Show a => a -> String
show Int
tl)
               ('\n' Char -> TransSenName
forall a. a -> [a] -> [a]
: [String] -> String
unlines [String]
simpleOptions) String
runTxt
             let (pStat :: ATPRetval
pStat, ret :: ProofStatus ProofTree
ret) = ProverState
-> String
-> String
-> ProofStatus ProofTree
-> (ATPRetval, ProofStatus ProofTree)
examineProof ProverState
sps String
stdoutC String
stderrC
                   ProofStatus ProofTree
defProofStat { usedTime :: TimeOfDay
usedTime = TimeOfDay
t_u }
             (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
pStat, GenericConfig ProofTree
cfg
                              { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
ret
                              , resultOutput :: [String]
resultOutput = String -> [String]
lines (String
stdoutC String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
stderrC)
                              , timeUsed :: TimeOfDay
timeUsed = ProofStatus ProofTree -> TimeOfDay
forall proof_tree. ProofStatus proof_tree -> TimeOfDay
usedTime ProofStatus ProofTree
ret })
         else (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return
                    (String -> ATPRetval
ATPError "Syntax error in options"
                    , GenericConfig ProofTree
cfg
                     { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
defProofStat
                     , resultOutput :: [String]
resultOutput = ["Parse Error"]
                     , timeUsed :: TimeOfDay
timeUsed = TimeOfDay
midnight
                     })

-- | call ekrh
runHyperProcess
  :: String -- ^ problem
  -> String -- ^ file name template
  -> String -- ^ time limit
  -> String -- ^ extra options
  -> String -- ^ run text
  -> IO (String, String, TimeOfDay) -- ^ out, err, diff time
runHyperProcess :: String
-> String
-> String
-> String
-> String
-> IO (String, String, TimeOfDay)
runHyperProcess prob :: String
prob saveFile :: String
saveFile tl :: String
tl opts :: String
opts runTxtA :: String
runTxtA = do
  String
stpTmpFile <- String -> String -> IO String
getTempFile String
prob String
saveFile
  let stpPrelFile :: String
stpPrelFile = String
stpTmpFile String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".prelude.tme"
      stpRunFile :: String
stpRunFile = String
stpTmpFile String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".run.tme"
  String -> String -> IO ()
writeFile String
stpPrelFile (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ TransSenName
prelTxt String
tl String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
opts
  String -> String -> IO ()
writeFile String
stpRunFile String
runTxtA
  HetsTime
t_start <- IO HetsTime
getHetsTime
  (_, stdoutC :: String
stdoutC, stderrC :: String
stderrC) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
hyperS
    [String
stpPrelFile, String
stpTmpFile, String
stpRunFile] ""
  HetsTime
t_end <- IO HetsTime
getHetsTime
  String -> IO ()
removeFile String
stpPrelFile
  String -> IO ()
removeFile String
stpRunFile
  String -> IO ()
removeFile String
stpTmpFile
  (String, String, TimeOfDay) -> IO (String, String, TimeOfDay)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
stdoutC, String
stderrC, HetsTime -> HetsTime -> TimeOfDay
diffHetsTime HetsTime
t_end HetsTime
t_start)

-- | Mapping type from SZS to Hets
data HyperResult = HProved | HDisproved | HTimeout | HError | HMemout

getHyperResult :: [String] -> HyperResult
getHyperResult :: [String] -> HyperResult
getHyperResult out :: [String]
out = case TransSenName -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Bool) -> TransSenName
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAlpha TransSenName -> TransSenName -> TransSenName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> TransSenName
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace)
    ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (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]
out of
  [s :: String
s] | String -> Bool
szsProved String
s -> HyperResult
HProved
    | String -> Bool
szsDisproved String
s -> HyperResult
HDisproved
    | String -> Bool
szsTimeout String
s -> HyperResult
HTimeout
    | String -> Bool
szsMemoryOut String
s -> HyperResult
HMemout
  _ -> HyperResult
HError

-- | examine SZS output
examineProof :: ProverState
             -> String
             -> String
             -> ProofStatus ProofTree
             -> (ATPRetval, ProofStatus ProofTree)
examineProof :: ProverState
-> String
-> String
-> ProofStatus ProofTree
-> (ATPRetval, ProofStatus ProofTree)
examineProof sps :: ProverState
sps stdoutC :: String
stdoutC stderrC :: String
stderrC defStatus :: ProofStatus ProofTree
defStatus =
    let outText :: String
outText = "\nOutput was:\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
stdoutC String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
stderrC
        provenStat :: ProofStatus ProofTree
provenStat = ProofStatus ProofTree
defStatus
          { usedAxioms :: [String]
usedAxioms = ProverState -> [String]
getAxioms ProverState
sps
          , proofTree :: ProofTree
proofTree = String -> ProofTree
ProofTree String
stdoutC }
     in case [String] -> HyperResult
getHyperResult ([String] -> HyperResult) -> [String] -> HyperResult
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
stdoutC of
               HProved -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
provenStat { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True })
               HTimeout -> (ATPRetval
ATPTLimitExceeded, ProofStatus ProofTree
defStatus)
               HDisproved -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
provenStat { goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved })
               HMemout -> (String -> ATPRetval
ATPError ("Out of Memory." String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
outText), ProofStatus ProofTree
defStatus)
               HError -> ( String -> ATPRetval
ATPError ("Internal Error in ekrhyper." String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
outText)
                         , ProofStatus ProofTree
defStatus)

-- Consistency Checker

hyperConsChecker :: ConsChecker Sign Sentence Sublogic Morphism ProofTree
hyperConsChecker :: ConsChecker Sign Sentence Sublogic Morphism ProofTree
hyperConsChecker = (String
-> String
-> Sublogic
-> (String
    -> TacticScript
    -> TheoryMorphism Sign Sentence Morphism ProofTree
    -> [FreeDefMorphism Sentence Morphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign Sentence Sublogic Morphism 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 String
hyperS String
hyperS Sublogic
sublogics String
-> TacticScript
-> TheoryMorphism Sign Sentence Morphism ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO (CCStatus ProofTree)
consCheck)
  { ccNeedsTimer :: Bool
ccNeedsTimer = Bool
False }

{- |
  Runs the krhyper cons-chcker. The tactic script only contains a string for the
  time limit.
-}

runTxtC :: String
runTxtC :: String
runTxtC =
    "% start derivation with the input received so far\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(run).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% print Hyper proof\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "%#(print_proof).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% print result and proof using SZS terminology;\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% requires postprocessing with post_szs script for proper legibility\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "%#(print_szs_proof).\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "% Show the model\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++
    "#(print_model).\n"

consCheck :: String
          -> TacticScript
          -> TheoryMorphism Sign Sentence Morphism ProofTree
          -> [FreeDefMorphism Sentence Morphism] -- ^ freeness constraints
          -> IO (CCStatus ProofTree)
consCheck :: String
-> TacticScript
-> TheoryMorphism Sign Sentence Morphism ProofTree
-> [FreeDefMorphism Sentence Morphism]
-> IO (CCStatus ProofTree)
consCheck thName :: String
thName (TacticScript tl :: String
tl) tm :: TheoryMorphism Sign Sentence Morphism ProofTree
tm freedefs :: [FreeDefMorphism Sentence Morphism]
freedefs =
    case TheoryMorphism Sign Sentence Morphism 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 Morphism ProofTree
tm of
      Theory sig :: Sign
sig nSens :: ThSens Sentence (ProofStatus ProofTree)
nSens -> do
          let proverStateI :: ProverState
proverStateI = InitialProverState Sign Sentence Morphism ProverState
tptpProverState Sign
sig (ThSens Sentence (ProofStatus ProofTree) -> [Named Sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens Sentence (ProofStatus ProofTree)
nSens) [FreeDefMorphism Sentence Morphism]
freedefs
              saveFile :: String
saveFile = TransSenName
basename String
thName String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".tptp"
          String
prob <- String -> ProverState -> [String] -> IO String
showTPTPProblemM String
thName ProverState
proverStateI []
          (stdoutC :: String
stdoutC, stderrC :: String
stderrC, t_u :: TimeOfDay
t_u) <-
            String
-> String
-> String
-> String
-> String
-> IO (String, String, TimeOfDay)
runHyperProcess String
prob String
saveFile String
tl "" String
runTxtC
          CCStatus ProofTree -> IO (CCStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return CCStatus :: forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
CCStatus
            { ccResult :: Maybe Bool
ccResult = case [String] -> HyperResult
getHyperResult ([String] -> HyperResult) -> [String] -> HyperResult
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
stdoutC of
                HProved -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                HDisproved -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
                _ -> Maybe Bool
forall a. Maybe a
Nothing
            , ccProofTree :: ProofTree
ccProofTree = String -> ProofTree
ProofTree (String -> ProofTree) -> String -> ProofTree
forall a b. (a -> b) -> a -> b
$ String
stdoutC String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
stderrC
            , ccUsedTime :: TimeOfDay
ccUsedTime = TimeOfDay
t_u }