{- |
Module      :  ./OWL2/ProveHermit.hs
Description :  Interface to the OWL Ontology prover via Pellett.
Copyright   :  (c) Heng Jiang, Uni Bremen 2004-2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  rick.adamy@ovgu.de
Stability   :  provisional
Portability :  needs POSIX

Interface for the Hermit Reasoner, uses GUI.GenericATP.
See <http://www.w3.org/2004/OWL/> for details on OWL, and
<http://www.hermit-reasoner.com> for Hermit
-}

module OWL2.ProveHermit
  ( runTimedHermit
  , hermitJar
  , hermitEnv
  , hermitProver
  , hermitConsChecker
  ) where

import Logic.Prover

import OWL2.Morphism
import OWL2.Sign
import OWL2.ProfilesAndSublogics
import OWL2.ProverState
import OWL2.AS

import GUI.GenericATP
import Interfaces.GenericATPState

import Proofs.BatchProcessing

import Common.AS_Annotation
import Common.ProofTree
import Common.Result as Result
import Common.ProverTools
import Common.Utils

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

import System.Directory

import Control.Monad (when)
import Control.Concurrent

import Debug.Trace


hermitS :: String
hermitS :: String
hermitS = "Hermit"

hermitJar :: String
hermitJar :: String
hermitJar = "HermiT.jar"

hermitEnv :: String
hermitEnv :: String
hermitEnv = "HERMIT_PATH"

hermitCheck :: IO (Maybe String)
hermitCheck :: IO (Maybe String)
hermitCheck = ([String] -> Maybe String) -> IO [String] -> IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
  (\ l :: [String]
l ->
    if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
l
    then String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
hermitJar String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found in $" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hermitEnv
    else Maybe String
forall a. Maybe a
Nothing)
  (IO [String] -> IO (Maybe String))
-> IO [String] -> IO (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> String -> IO [String]
check4FileAux String
hermitJar String
hermitEnv

{- |
  The Prover implementation. First runs the batch prover (with graphical
  feedback), then starts the GUI prover.
-}
hermitProver :: Prover Sign Axiom OWLMorphism ProfSub ProofTree
hermitProver :: Prover Sign Axiom OWLMorphism ProfSub ProofTree
hermitProver =
  (String
-> String
-> ProfSub
-> (String
    -> Theory Sign Axiom ProofTree
    -> [FreeDefMorphism Axiom OWLMorphism]
    -> IO [ProofStatus ProofTree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory Sign Axiom ProofTree
    -> [FreeDefMorphism Axiom OWLMorphism]
    -> IO (ThreadId, MVar ()))
-> Prover Sign Axiom OWLMorphism ProfSub 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 "java" String
hermitS ProfSub
dlS String
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO [ProofStatus ProofTree]
hermitGUI Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (ThreadId, MVar ())
hermitCMDLautomaticBatch)
  { proverUsable :: IO (Maybe String)
proverUsable = IO (Maybe String)
hermitCheck }

hermitConsChecker :: ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
hermitConsChecker :: ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
hermitConsChecker = (String
-> ProfSub
-> (String
    -> TacticScript
    -> TheoryMorphism Sign Axiom OWLMorphism ProofTree
    -> [FreeDefMorphism Axiom OWLMorphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
forall sublogics sign sentence morphism proof_tree.
String
-> sublogics
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
mkConsChecker String
hermitS ProfSub
topS String
-> TacticScript
-> TheoryMorphism Sign Axiom OWLMorphism ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (CCStatus ProofTree)
consCheck)
  { ccNeedsTimer :: Bool
ccNeedsTimer = Bool
False
  , ccUsable :: IO (Maybe String)
ccUsable = IO (Maybe String)
hermitCheck }

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: String -- ^ theory name
       -> ATPFunctions Sign Axiom OWLMorphism ProofTree ProverState
atpFun :: String -> ATPFunctions Sign Axiom OWLMorphism ProofTree ProverState
atpFun _ = 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 Axiom OWLMorphism ProverState
initialProverState = InitialProverState Sign Axiom OWLMorphism ProverState
owlProverState
  , atpTransSenName :: String -> String
atpTransSenName = String -> String
forall a. a -> a
id   -- transSenName,
  , atpInsertSentence :: ProverState -> Named Axiom -> ProverState
atpInsertSentence = ProverState -> Named Axiom -> ProverState
insertOWLAxiom
  , goalOutput :: ProverState -> Named Axiom -> [String] -> IO String
goalOutput = \ a :: ProverState
a b :: Named Axiom
b _ -> ProverState -> Named Axiom -> IO String
showOWLProblem ProverState
a Named Axiom
b
  , proverHelpText :: String
proverHelpText = "http://www.hermit-reasoner.com/using.html\n"
  , batchTimeEnv :: String
batchTimeEnv = "HETS_HermiT_BATCH_TIME_LIMIT"
  , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions { problemOutput :: String
problemOutput = ".owl"  -- owl-hets
                                    , proverOutput :: String
proverOutput = ".pellet"
                                    , theoryConfiguration :: String
theoryConfiguration = ".pconf" }
  , runProver :: RunProver Axiom ProofTree ProverState
runProver = RunProver Axiom ProofTree ProverState
runHermit
  , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts }

-- ** GUI

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

-- ** command line function

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the Hermit prover via MathServe.
  Hermit specific functions are omitted by data type ATPFunctions.
-}
hermitCMDLautomaticBatch ::
           Bool -- ^ True means include proved theorems
        -> Bool -- ^ True means save problem file
        -> MVar (Result.Result [ProofStatus ProofTree])
           -- ^ used to store the result of the batch run
        -> String -- ^ theory name
        -> TacticScript -- ^ default tactic script
        -> Theory Sign Axiom ProofTree -- ^ theory
        -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints
        -> IO (ThreadId, MVar ())
        {- ^ fst: identifier of the batch thread for killing it
        snd: MVar to wait for the end of the thread -}
hermitCMDLautomaticBatch :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (ThreadId, MVar ())
hermitCMDLautomaticBatch inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus ProofTree])
resultMVar
                         thName :: String
thName defTS :: TacticScript
defTS th :: Theory Sign Axiom ProofTree
th freedefs :: [FreeDefMorphism Axiom OWLMorphism]
freedefs =
  ATPFunctions Sign Axiom OWLMorphism ProofTree ProverState
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> 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 Axiom OWLMorphism ProofTree ProverState
atpFun String
thName) Bool
inclProvedThs Bool
saveProblem_batch
    MVar (Result [ProofStatus ProofTree])
resultMVar String
hermitS String
thName
    (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory Sign Axiom ProofTree
th [FreeDefMorphism Axiom OWLMorphism]
freedefs ProofTree
emptyProofTree

-- * Main prover functions

{- |
  Runs the Pellet service.
-}
consCheck :: String
          -> TacticScript
          -> TheoryMorphism Sign Axiom OWLMorphism ProofTree
          -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints
          -> IO (CCStatus ProofTree)
consCheck :: String
-> TacticScript
-> TheoryMorphism Sign Axiom OWLMorphism ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (CCStatus ProofTree)
consCheck thName :: String
thName (TacticScript tl :: String
tl) tm :: TheoryMorphism Sign Axiom OWLMorphism ProofTree
tm freedefs :: [FreeDefMorphism Axiom OWLMorphism]
freedefs = case TheoryMorphism Sign Axiom OWLMorphism ProofTree
-> Theory Sign Axiom ProofTree
forall sign sen mor proof_tree.
TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
tTarget TheoryMorphism Sign Axiom OWLMorphism ProofTree
tm of
  Theory sig :: Sign
sig nSens :: ThSens Axiom (ProofStatus ProofTree)
nSens -> do
    let proverStateI :: ProverState
proverStateI = InitialProverState Sign Axiom OWLMorphism ProverState
owlProverState Sign
sig (ThSens Axiom (ProofStatus ProofTree) -> [Named Axiom]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens Axiom (ProofStatus ProofTree)
nSens) [FreeDefMorphism Axiom OWLMorphism]
freedefs
        prob :: String
prob = ProverState -> String
showOWLProblemS ProverState
proverStateI
        pStatus :: [String] -> a -> CCStatus ProofTree
pStatus out :: [String]
out tUsed :: a
tUsed = CCStatus :: forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
CCStatus
          { ccResult :: Maybe Bool
ccResult = 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] -> String
unlines [String]
out String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
prob
          , 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
$ a -> Integer
forall a. Integral a => a -> Integer
toInteger a
tUsed }
        tLim :: Maybe Int
tLim = String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
tl
    Maybe (Bool, String, String)
res <- String
-> String
-> String
-> Maybe String
-> Int
-> IO (Maybe (Bool, String, String))
runTimedHermit "consistency" (String -> String
basename String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".owl") String
prob Maybe String
forall a. Maybe a
Nothing
      (Int -> IO (Maybe (Bool, String, String)))
-> Int -> IO (Maybe (Bool, String, String))
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. Bounded a => a
maxBound (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ String -> Maybe Int
forall a. Read a => String -> Maybe a
readMaybe String
tl
    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
$ case Maybe (Bool, String, String)
res of
      Nothing -> [String] -> Int -> CCStatus ProofTree
forall a. Integral a => [String] -> a -> CCStatus ProofTree
pStatus ["Timeout after " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tl String -> String -> String
forall a. [a] -> [a] -> [a]
++ " seconds"]
                 (Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (0 :: Int) Maybe Int
tLim)
      Just (progTh :: Bool
progTh, outp :: String
outp, eOut :: String
eOut) -> if Bool
progTh then
          let (_, exCode :: Maybe Bool
exCode, out :: [String]
out, tUsed :: Int
tUsed) = String -> String -> (ATPRetval, Maybe Bool, [String], Int)
analyseOutput String
outp String
eOut
          in ([String] -> Int -> CCStatus ProofTree
forall a. Integral a => [String] -> a -> CCStatus ProofTree
pStatus [String]
out Int
tUsed) { ccResult :: Maybe Bool
ccResult = Maybe Bool
exCode }
        else [String] -> Int -> CCStatus ProofTree
forall a. Integral a => [String] -> a -> CCStatus ProofTree
pStatus ["Hermit not found"] (0 :: Int)

runTimedHermit :: String -- ^ pellet subcommand
  -> FilePath            -- ^ basename of problem file
  -> String              -- ^ problem content
  -> Maybe String        -- ^ entail content
  -> Int                 -- ^ time limit in seconds
  -> IO (Maybe (Bool, String, String)) -- ^ timeout or (success, stdout, stderr)
runTimedHermit :: String
-> String
-> String
-> Maybe String
-> Int
-> IO (Maybe (Bool, String, String))
runTimedHermit opts :: String
opts tmpFileName :: String
tmpFileName prob :: String
prob entail :: Maybe String
entail secs :: Int
secs = do
  (progTh :: Bool
progTh, pPath :: String
pPath) <- String -> String -> IO (Bool, String)
check4jarFile String
hermitEnv String
hermitJar
  if Bool
progTh then String
-> IO (Maybe (Bool, String, String))
-> IO (Maybe (Bool, String, String))
forall a. String -> IO a -> IO a
withinDirectory String
pPath (IO (Maybe (Bool, String, String))
 -> IO (Maybe (Bool, String, String)))
-> IO (Maybe (Bool, String, String))
-> IO (Maybe (Bool, String, String))
forall a b. (a -> b) -> a -> b
$ do
      String
timeTmpFile <- String -> String -> IO String
getTempFile String
prob String
tmpFileName
      String
timeTmpEnt <- String -> String -> IO String
getTempFile (String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" Maybe String
entail) String
tmpFileName
      let entFile :: String
entFile = String
timeTmpFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".entail.owl"
          doEntail :: Bool
doEntail = String -> Bool -> Bool
forall a. String -> a -> a
trace (String -> String
forall a. Show a => a -> String
show String
opts) (Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
entail)
          args :: [String]
args = "-Xmx1024M" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: "-jar" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
hermitJar
           String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (if Bool
doEntail then ["--premise=file://"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
timeTmpFile, "--conclusion=file://"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
entFile, "-E"] 
              else ["-k", String
timeTmpFile]) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String]
words String
opts
      case Maybe String
entail of
        Just c :: String
c -> String -> String -> IO ()
writeFile String
entFile String
c
        Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Maybe (ExitCode, String, String)
mex <- Int -> String -> [String] -> IO (Maybe (ExitCode, String, String))
timeoutCommand Int
secs "java" [String]
args
      String -> IO ()
removeFile String
timeTmpEnt
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
doEntail (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
entFile
      Maybe (Bool, String, String) -> IO (Maybe (Bool, String, String))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Bool, String, String) -> IO (Maybe (Bool, String, String)))
-> Maybe (Bool, String, String)
-> IO (Maybe (Bool, String, String))
forall a b. (a -> b) -> a -> b
$ ((ExitCode, String, String) -> (Bool, String, String))
-> Maybe (ExitCode, String, String) -> Maybe (Bool, String, String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (_, outS :: String
outS, errS :: String
errS) -> (Bool
True, String
outS, String
errS)) Maybe (ExitCode, String, String)
mex
    else Maybe (Bool, String, String) -> IO (Maybe (Bool, String, String))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Bool, String, String) -> IO (Maybe (Bool, String, String)))
-> Maybe (Bool, String, String)
-> IO (Maybe (Bool, String, String))
forall a b. (a -> b) -> a -> b
$ (Bool, String, String) -> Maybe (Bool, String, String)
forall a. a -> Maybe a
Just (Bool
False, "", "")

runHermit :: 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
          -> Named Axiom -- ^ goal to prove
          -> IO (ATPRetval, GenericConfig ProofTree)
          -- ^ (retval, configuration with proof status and complete output)
runHermit :: RunProver Axiom ProofTree ProverState
runHermit sps :: ProverState
sps cfg :: GenericConfig ProofTree
cfg saveHermit :: Bool
saveHermit thName :: String
thName nGoal :: Named Axiom
nGoal = do
  let simpleOptions :: [String]
simpleOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg
      tLimit :: Int
tLimit = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 800 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> Maybe Int
forall proof_tree. GenericConfig proof_tree -> Maybe Int
timeLimit GenericConfig ProofTree
cfg
      goalSuffix :: String
goalSuffix = '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Named Axiom -> String
forall s a. SenAttr s a -> a
senAttr Named Axiom
nGoal
      tmpFileName :: String
tmpFileName = String -> String
basename String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
goalSuffix String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".owl"
      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 = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg
                     , tsExtraOpts :: [String]
tsExtraOpts = [String]
simpleOptions }
      defaultProofStatus :: String -> ProofStatus ProofTree
defaultProofStatus out :: String
out =
        (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus (Named Axiom -> String
forall s a. SenAttr s a -> a
senAttr Named Axiom
nGoal) String
hermitS (ProofTree -> ProofStatus ProofTree)
-> ProofTree -> ProofStatus ProofTree
forall a b. (a -> b) -> a -> b
$ String -> ProofTree
ProofTree String
out)
        { tacticScript :: TacticScript
tacticScript = TacticScript
tScript }
      prob :: String
prob = ProverState -> String
showOWLProblemS ProverState
sps
      entail :: String
entail = ProverState -> String
showOWLProblemS
             ProverState
sps { initialState :: [Named Axiom]
initialState = [ Named Axiom
nGoal {isAxiom :: Bool
isAxiom = Bool
True } ] }
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveHermit (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        String -> String -> IO ()
writeFile String
tmpFileName String
prob
        String -> String -> IO ()
writeFile (String
tmpFileName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".entail.owl") String
entail
  Maybe (Bool, String, String)
res <- String
-> String
-> String
-> Maybe String
-> Int
-> IO (Maybe (Bool, String, String))
runTimedHermit "" String
tmpFileName String
prob (String -> Maybe String
forall a. a -> Maybe a
Just String
entail) Int
tLimit
  ((err :: ATPRetval
err, retval :: ProofStatus ProofTree
retval), output :: [String]
output, tUsed :: Int
tUsed) <- ((ATPRetval, ProofStatus ProofTree), [String], Int)
-> IO ((ATPRetval, ProofStatus ProofTree), [String], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (((ATPRetval, ProofStatus ProofTree), [String], Int)
 -> IO ((ATPRetval, ProofStatus ProofTree), [String], Int))
-> ((ATPRetval, ProofStatus ProofTree), [String], Int)
-> IO ((ATPRetval, ProofStatus ProofTree), [String], Int)
forall a b. (a -> b) -> a -> b
$ case Maybe (Bool, String, String)
res of
    Nothing ->
      ((ATPRetval
ATPTLimitExceeded, String -> ProofStatus ProofTree
defaultProofStatus "Timeout"), [], Int
tLimit)
    Just (progTh :: Bool
progTh, output :: String
output, eOut :: String
eOut) ->
      if Bool
progTh then
        let (atpr :: ATPRetval
atpr, exCode :: Maybe Bool
exCode, outp :: [String]
outp, tUsed :: Int
tUsed) = String -> String -> (ATPRetval, Maybe Bool, [String], Int)
analyseOutput String
output String
eOut
            openStat :: ProofStatus ProofTree
openStat = String -> ProofStatus ProofTree
defaultProofStatus (String -> ProofStatus ProofTree)
-> String -> ProofStatus ProofTree
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
outp
            disProvedStatus :: ProofStatus ProofTree
disProvedStatus = ProofStatus ProofTree
openStat
               { goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved
               , 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 }
            provedStatus :: ProofStatus ProofTree
provedStatus = ProofStatus ProofTree
disProvedStatus
                  { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
                  , usedAxioms :: [String]
usedAxioms = (Named Axiom -> String) -> [Named Axiom] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named Axiom -> String
forall s a. SenAttr s a -> a
senAttr ([Named Axiom] -> [String]) -> [Named Axiom] -> [String]
forall a b. (a -> b) -> a -> b
$ ProverState -> [Named Axiom]
initialState ProverState
sps }
            proofStat :: ProofStatus ProofTree
proofStat = case Maybe Bool
exCode of
              Just True -> ProofStatus ProofTree
provedStatus
              Just False -> ProofStatus ProofTree
disProvedStatus
              _ -> ProofStatus ProofTree
openStat
        in ((ATPRetval
atpr, ProofStatus ProofTree
proofStat), [String]
outp, Int
tUsed)
      else
       ((String -> ATPRetval
ATPError "Could not find hermit reasoner. Is $HERMIT_PATH set?"
       , String -> ProofStatus ProofTree
defaultProofStatus ""), [], 0)
  (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]
output
    , 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
    })

analyseOutput :: String -> String -> (ATPRetval, Maybe Bool, [String], Int)
analyseOutput :: String -> String -> (ATPRetval, Maybe Bool, [String], Int)
analyseOutput err :: String
err outp :: String
outp =
  let ls :: [String]
ls = String -> [String]
lines String
outp [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String]
lines String
err
      anaHelp :: (ATPRetval, Maybe Bool, c) -> String -> (ATPRetval, Maybe Bool, c)
anaHelp (atp :: ATPRetval
atp, exCode :: Maybe Bool
exCode, to :: c
to) line :: String
line =
        case String -> [String]
words String
line of
          "Consistent:" : v :: String
v : _ -> case String
v of
              "Yes" -> (ATPRetval
ATPSuccess, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, c
to)
              "No" -> (ATPRetval
ATPSuccess, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, c
to)
              _ -> (ATPRetval
atp, Maybe Bool
exCode, c
to)
          ["true"] ->
            (ATPRetval
ATPSuccess, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True, c
to)
          ["false"] -> 
            (ATPRetval
ATPSuccess, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, c
to)
          ne :: String
ne : _ | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Non-entailments" String
ne ->
            (ATPRetval
ATPSuccess, Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False, c
to)
          "Usage:" : "java" : "Hermit" : _ -> (String -> ATPRetval
ATPError String
line, Maybe Bool
forall a. Maybe a
Nothing, c
to)
          "ERROR:" : _ -> (String -> ATPRetval
ATPError String
line, Maybe Bool
forall a. Maybe a
Nothing, c
to)
          tm :: String
tm : num :: String
num : _ | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "Time" String
tm Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
num ->
            (ATPRetval
atp, Maybe Bool
exCode, String -> c
forall a. Read a => String -> a
read String
num)
          _ -> (ATPRetval
atp, Maybe Bool
exCode, c
to)
      (atpr :: ATPRetval
atpr, st :: Maybe Bool
st, tmo :: Int
tmo) = ((ATPRetval, Maybe Bool, Int)
 -> String -> (ATPRetval, Maybe Bool, Int))
-> (ATPRetval, Maybe Bool, Int)
-> [String]
-> (ATPRetval, Maybe Bool, Int)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (ATPRetval, Maybe Bool, Int)
-> String -> (ATPRetval, Maybe Bool, Int)
forall c.
Read c =>
(ATPRetval, Maybe Bool, c) -> String -> (ATPRetval, Maybe Bool, c)
anaHelp (String -> ATPRetval
ATPError "", Maybe Bool
forall a. Maybe a
Nothing, -1) [String]
ls
  in case ATPRetval
atpr of
       ATPError s :: String
s | String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s -> (String -> ATPRetval
ATPError "unexpected hermit output", Maybe Bool
st, [String]
ls, Int
tmo)
       _ -> (ATPRetval
atpr, Maybe Bool
st, [String]
ls, Int
tmo)