{- |
Module      :  ./OWL2/ProveFact.hs
Copyright   :  (c) Domink Luecke, Uni Bremen 2009-2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable

Fact++ prover for OWL
-}

module OWL2.ProveFact (factProver, factConsChecker) where

import Logic.Prover

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

import GUI.GenericATP
import Interfaces.GenericATPState

import Proofs.BatchProcessing

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

import Data.Time (TimeOfDay, midnight)

import System.Exit
import System.Environment
import System.Directory
import System.FilePath

import Control.Concurrent
import Control.Monad (when)

import Data.Maybe

{- |
  The Prover implementation. First runs the batch prover (with graphical
  feedback), then starts the GUI prover.
-}
factProver :: Prover Sign Axiom OWLMorphism ProfSub ProofTree
factProver :: Prover Sign Axiom OWLMorphism ProfSub ProofTree
factProver = (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" "Fact" ProfSub
topS String
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO [ProofStatus ProofTree]
factGUI
  Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (ThreadId, MVar ())
factCMDLautomaticBatch)
  { proverUsable :: IO (Maybe String)
proverUsable = String -> IO (Maybe String)
checkOWLjar String
factProverJarS }

factProverJarS :: String
factProverJarS :: String
factProverJarS = "OWLFactProver.jar"

factJarS :: String
factJarS :: String
factJarS = "OWLFact.jar"

{- |
  Invokes the generic prover GUI.
-}
factGUI :: String -- ^ theory name
          -> Theory Sign Axiom ProofTree
          -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints
          -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
factGUI :: String
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO [ProofStatus ProofTree]
factGUI 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 (Prover Sign Axiom OWLMorphism ProfSub ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign Axiom OWLMorphism ProfSub ProofTree
factProver) String
thName Theory Sign Axiom ProofTree
th
                [FreeDefMorphism Axiom OWLMorphism]
freedefs ProofTree
emptyProofTree

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the Fact prover.
  Pellet specific functions are omitted by data type ATPFunctions.
-}
factCMDLautomaticBatch ::
           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 -}
factCMDLautomaticBatch :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign Axiom ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (ThreadId, MVar ())
factCMDLautomaticBatch 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 (Prover Sign Axiom OWLMorphism ProfSub ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign Axiom OWLMorphism ProfSub ProofTree
factProver) String
thName
    (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory Sign Axiom ProofTree
th [FreeDefMorphism Axiom OWLMorphism]
freedefs ProofTree
emptyProofTree

{- |
  The Cons-Checker implementation.
-}
factConsChecker :: ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
factConsChecker :: ConsChecker Sign Axiom ProfSub OWLMorphism ProofTree
factConsChecker = (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 "Fact" ProfSub
topS String
-> TacticScript
-> TheoryMorphism Sign Axiom OWLMorphism ProofTree
-> [FreeDefMorphism Axiom OWLMorphism]
-> IO (CCStatus ProofTree)
consCheck)
  { ccUsable :: IO (Maybe String)
ccUsable = String -> IO (Maybe String)
checkOWLjar String
factJarS }

{- |
  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
-> 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 Axiom OWLMorphism ProverState
initialProverState = InitialProverState Sign Axiom OWLMorphism ProverState
owlProverState
  , atpTransSenName :: TransSenName
atpTransSenName = TransSenName
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 = "Fact++"
  , batchTimeEnv :: String
batchTimeEnv = "HETS_FACT_BATCH_TIME_LIMIT"
  , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions { problemOutput :: String
problemOutput = ".owl"  -- owl-hets
                                    , proverOutput :: String
proverOutput = ".fact"
                                    , theoryConfiguration :: String
theoryConfiguration = ".pconf" }
  , runProver :: RunProver Axiom ProofTree ProverState
runProver = RunProver Axiom ProofTree ProverState
runFact
  , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts }

{- |
  Runs the Fact++ consistency checker.
-}
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 saveOWL :: Bool
saveOWL = Bool
False
        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
        problemS :: String
problemS = ProverState -> String
showOWLProblemS ProverState
proverStateI
        tmpFileName :: String
tmpFileName = TransSenName
basename String
thName String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".owl"
        pStatus :: String -> TimeOfDay -> CCStatus ProofTree
pStatus out :: String
out tUsed :: TimeOfDay
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
out String -> TransSenName
forall a. [a] -> [a] -> [a]
++ "\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
problemS
          , ccUsedTime :: TimeOfDay
ccUsedTime = TimeOfDay
tUsed }
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveOWL (String -> String -> IO ()
writeFile String
tmpFileName String
problemS)
    Maybe (Bool, ExitCode, String, TimeOfDay)
res <- String
-> String
-> Maybe String
-> Int
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
runTimedFact String
tmpFileName String
problemS Maybe String
forall a. Maybe a
Nothing
      (Int -> IO (Maybe (Bool, ExitCode, String, TimeOfDay)))
-> Int -> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
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, ExitCode, String, TimeOfDay)
res of
      Just (b :: Bool
b, ex_code :: ExitCode
ex_code, out :: String
out, t_u :: TimeOfDay
t_u) -> let pStat :: CCStatus ProofTree
pStat = String -> TimeOfDay -> CCStatus ProofTree
pStatus String
out TimeOfDay
t_u in if Bool
b then
        case ExitCode
ex_code of
          ExitFailure 10 -> CCStatus ProofTree
pStat { ccResult :: Maybe Bool
ccResult = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True }
          ExitFailure 20 -> CCStatus ProofTree
pStat { ccResult :: Maybe Bool
ccResult = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False}
          _ -> CCStatus ProofTree
pStat
        else CCStatus ProofTree
pStat
      Nothing -> String -> TimeOfDay -> CCStatus ProofTree
pStatus "Timeout" TimeOfDay
midnight

runTimedFact :: FilePath -- ^ basename of problem file
  -> String              -- ^ problem content
  -> Maybe String        -- ^ entail content
  -> Int                 -- ^ time limit in seconds
  -> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
runTimedFact :: String
-> String
-> Maybe String
-> Int
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
runTimedFact tmpFileName :: String
tmpFileName prob :: String
prob mEnt :: Maybe String
mEnt tLimit :: Int
tLimit = do
  let hasEnt :: Bool
hasEnt = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
mEnt
      jar :: String
jar = if Bool
hasEnt then String
factProverJarS else String
factJarS
      jlibName :: String
jlibName = "libFaCTPlusPlusJNI.so"
  (progTh :: Bool
progTh, toolPath :: String
toolPath) <- String -> IO (Bool, String)
check4HetsOWLjar String
jar
  Bool
hasJniLib <- String -> IO Bool
doesFileExist (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ "/lib/" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
jlibName
  (_, arch :: String
arch, _) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess "uname" ["-m"] ""
  if Bool
progTh then
        String
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
forall a. String -> IO a -> IO a
withinDirectory String
toolPath (IO (Maybe (Bool, ExitCode, String, TimeOfDay))
 -> IO (Maybe (Bool, ExitCode, String, TimeOfDay)))
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
forall a b. (a -> b) -> a -> b
$ do
          Maybe String
mJni <- ([(String, String)] -> Maybe String)
-> IO [(String, String)] -> IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup "HETS_JNI_LIBS") IO [(String, String)]
getEnvironment
          let jni :: String
jni = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe ("lib/native/" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ TransSenName
trim String
arch) Maybe String
mJni
          Bool
hasJni <- String -> IO Bool
doesFileExist (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ String
jni String -> TransSenName
</> String
jlibName
          if Bool
hasJni Bool -> Bool -> Bool
|| Bool
hasJniLib then do
            String
timeTmpFile <- String -> String -> IO String
getTempFile String
prob String
tmpFileName
            let entailsFile :: String
entailsFile = String
timeTmpFile String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".entail.owl"
                jargs :: [String]
jargs = ["-Djava.library.path=" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
jni
                        | Bool -> Bool
not Bool
hasJniLib Bool -> Bool -> Bool
|| Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
mJni ]
                   [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["-jar", String
jar, "file://" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
timeTmpFile]
                  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["file://" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
entailsFile | Bool
hasEnt ]
            case Maybe String
mEnt of
              Just entail :: String
entail -> String -> String -> IO ()
writeFile String
entailsFile String
entail
              _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            HetsTime
t_start <- IO HetsTime
getHetsTime
            Maybe (ExitCode, String, String)
mExit <- Int -> String -> [String] -> IO (Maybe (ExitCode, String, String))
timeoutCommand Int
tLimit "java" [String]
jargs
            HetsTime
t_end <- IO HetsTime
getHetsTime
            String -> IO ()
removeFile String
timeTmpFile
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hasEnt (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
entailsFile
            Maybe (Bool, ExitCode, String, TimeOfDay)
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Bool, ExitCode, String, TimeOfDay)
 -> IO (Maybe (Bool, ExitCode, String, TimeOfDay)))
-> Maybe (Bool, ExitCode, String, TimeOfDay)
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
forall a b. (a -> b) -> a -> b
$ ((ExitCode, String, String) -> (Bool, ExitCode, String, TimeOfDay))
-> Maybe (ExitCode, String, String)
-> Maybe (Bool, ExitCode, String, TimeOfDay)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (ex :: ExitCode
ex, out :: String
out, err :: String
err) ->
                  (Bool
True, ExitCode
ex, String
out String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
err, HetsTime -> HetsTime -> TimeOfDay
diffHetsTime HetsTime
t_end HetsTime
t_start)) Maybe (ExitCode, String, String)
mExit
            else Maybe (Bool, ExitCode, String, TimeOfDay)
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Bool, ExitCode, String, TimeOfDay)
 -> IO (Maybe (Bool, ExitCode, String, TimeOfDay)))
-> Maybe (Bool, ExitCode, String, TimeOfDay)
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
forall a b. (a -> b) -> a -> b
$ (Bool, ExitCode, String, TimeOfDay)
-> Maybe (Bool, ExitCode, String, TimeOfDay)
forall a. a -> Maybe a
Just (Bool
False, ExitCode
ExitSuccess, "no " String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
jlibName, TimeOfDay
midnight)
    else Maybe (Bool, ExitCode, String, TimeOfDay)
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Bool, ExitCode, String, TimeOfDay)
 -> IO (Maybe (Bool, ExitCode, String, TimeOfDay)))
-> Maybe (Bool, ExitCode, String, TimeOfDay)
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
forall a b. (a -> b) -> a -> b
$ (Bool, ExitCode, String, TimeOfDay)
-> Maybe (Bool, ExitCode, String, TimeOfDay)
forall a. a -> Maybe a
Just (Bool
False, ExitCode
ExitSuccess, String
jar String -> TransSenName
forall a. [a] -> [a] -> [a]
++ " not found.", TimeOfDay
midnight)

{- |
   Invocation of the Fact Prover.
-}
runFact :: 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)
runFact :: RunProver Axiom ProofTree ProverState
runFact sps :: ProverState
sps cfg :: GenericConfig ProofTree
cfg saveFact :: Bool
saveFact thName :: String
thName nGoal :: Named Axiom
nGoal = do
      let 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
saveFact (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 -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".entail.owl") String
entail
      Maybe (Bool, ExitCode, String, TimeOfDay)
mExit <- String
-> String
-> Maybe String
-> Int
-> IO (Maybe (Bool, ExitCode, String, TimeOfDay))
runTimedFact String
tmpFileName String
prob (String -> Maybe String
forall a. a -> Maybe a
Just String
entail) Int
tLimit
      let ((err :: ATPRetval
err, retval :: ProofStatus ProofTree
retval), output :: [String]
output, tUsed :: TimeOfDay
tUsed) = case Maybe (Bool, ExitCode, String, TimeOfDay)
mExit of
            Just (b :: Bool
b, ex :: ExitCode
ex, out :: String
out, t_u :: TimeOfDay
t_u) -> if Bool
b then let outlines :: [String]
outlines = String -> [String]
lines String
out in
                (ExitCode
-> [String] -> TimeOfDay -> (ATPRetval, ProofStatus ProofTree)
proofStat ExitCode
ex [String]
outlines TimeOfDay
t_u, [String]
outlines, TimeOfDay
t_u)
              else
                ((String -> ATPRetval
ATPError String
out, ProofStatus ProofTree
defaultProofStatus), [], TimeOfDay
t_u)
            Nothing -> ( (ATPRetval
ATPTLimitExceeded, ProofStatus ProofTree
defaultProofStatus), [], TimeOfDay
midnight)
      (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 = TimeOfDay
tUsed
            })
  where
    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 -> TransSenName
forall a. a -> [a] -> [a]
: Named Axiom -> String
forall s a. SenAttr s a -> a
senAttr Named Axiom
nGoal
    tmpFileName :: String
tmpFileName = TransSenName
basename String
thName String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
goalSuffix String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".owl"
    proofStat :: ExitCode
-> [String] -> TimeOfDay -> (ATPRetval, ProofStatus ProofTree)
proofStat exitCode :: ExitCode
exitCode out :: [String]
out tUsed :: TimeOfDay
tUsed = case ExitCode
exitCode of
      ExitFailure 10 -> (ATPRetval
ATPSuccess, (TimeOfDay -> ProofStatus ProofTree
provedStatus TimeOfDay
tUsed)
                       { 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 })
      ExitFailure 20 -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
disProvedStatus)
      ExitFailure 30 -> (ATPRetval
ATPSuccess, (TimeOfDay -> ProofStatus ProofTree
provedStatus TimeOfDay
tUsed))
      ExitFailure _ -> ( String -> ATPRetval
ATPError ([String] -> String
unlines ("Internal error." String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
out))
                       , ProofStatus ProofTree
defaultProofStatus)
      ExitSuccess -> ( String -> ATPRetval
ATPError ([String] -> String
unlines ("Internal error." String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
out))
                       , ProofStatus ProofTree
defaultProofStatus)
    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 = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg }
    defaultProofStatus :: ProofStatus ProofTree
defaultProofStatus =
      (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) (Prover Sign Axiom OWLMorphism ProfSub ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign Axiom OWLMorphism ProfSub ProofTree
factProver) ProofTree
emptyProofTree)
        { tacticScript :: TacticScript
tacticScript = TacticScript
tScript }
    disProvedStatus :: ProofStatus ProofTree
disProvedStatus = ProofStatus ProofTree
defaultProofStatus {goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved}
    provedStatus :: TimeOfDay -> ProofStatus ProofTree
provedStatus ut :: TimeOfDay
ut =
      ProofStatus ProofTree
defaultProofStatus { goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
                         , usedTime :: TimeOfDay
usedTime = TimeOfDay
ut
                         , tacticScript :: TacticScript
tacticScript = TacticScript
tScript }