d29201dd5328b88140ce050100693c501852657dChristian Maeder{- |

8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : Interface to the OWL Ontology prover via Pellet.

8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlCopyright : (c) Heng Jiang, Uni Bremen 2004-2008

8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : jiang@informatik.uni-bremen.de

8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlStability : provisional

8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlPortability : needs POSIX

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl

8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlInterface for the Pellet service, uses GUI.GenericATP.

8cc6f43935309fe1206828425baf6fc35a88d575Martin KühlSee <http://www.w3.org/2004/OWL/> for details on OWL, and

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl<http://pellet.owldl.com/> for Pellet.

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl-}

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühlmodule OWL.ProvePellet (pelletProver,pelletGUI,pelletCMDLautomatic,

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl pelletCMDLautomaticBatch,

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl pelletConsChecker) where

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühl

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühlimport Logic.Prover

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühlimport OWL.AS

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport OWL.Morphism

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport OWL.Sign

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport OWL.Print

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport OWL.Sublogic

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühlimport GUI.GenericATP

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport Interfaces.GenericATPState

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühlimport GUI.Utils (createTextSaveDisplay, infoDialog)

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühlimport Proofs.BatchProcessing

521e1648b2c66064c41e9ac47bcd510356ed2355Adrián Riesco

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühlimport Common.AS_Annotation

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühlimport Common.ProofTree

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport Common.Result as Result

8cc6f43935309fe1206828425baf6fc35a88d575Martin Kühlimport Common.Utils

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

521e1648b2c66064c41e9ac47bcd510356ed2355Adrián Riescoimport Data.List (isPrefixOf)

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport Data.Maybe

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühlimport Data.Time (timeToTimeOfDay)

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport Data.Time.Clock (UTCTime(..), secondsToDiffTime, getCurrentTime)

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport qualified Control.Concurrent as Concurrent

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport System.Exit

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport System.IO

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport System.Process

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport System.Directory

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport Control.Monad (when)

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühlimport Control.Concurrent

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühl

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühldata PelletProverState = PelletProverState

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl { ontologySign :: Sign

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl , initialState :: [Named Axiom] }

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühl deriving (Show)

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühldata PelletProblem = PelletProblem

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl { identifier :: PelletID

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl -- , description :: Description

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühl , problemProverState :: PelletProverState

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl -- , settings :: [PelletSetting]

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl } deriving (Show)

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühltype PelletID = String

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühl

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl{-

f78126c371b40713bdf7268be1e871198bb6aecfAdrián Riescodata PelletSetting = PelletSetting

f78126c371b40713bdf7268be1e871198bb6aecfAdrián Riesco { settingName :: String

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühl , settingValue :: [String]

f78126c371b40713bdf7268be1e871198bb6aecfAdrián Riesco } deriving (Show)

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl-}

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühl-- * Prover implementation

d2020d73b5be74ca654c2facd411387941c6b206Martin KühlpelletProverState :: Sign

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl -> [Named Axiom]

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints

26b4844ded8825ca5925fb5e9231e663095be699Martin Kühl -> PelletProverState

d2020d73b5be74ca654c2facd411387941c6b206Martin KühlpelletProverState sig oSens _ = PelletProverState

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl { ontologySign = sig

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl ,initialState = filter isAxiom oSens }

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl{- |

010997ddd12186698c1ebdbcddb63a670552b3c2Adrián Riesco The Prover implementation. First runs the batch prover (with graphical feedback), then starts the GUI prover.

010997ddd12186698c1ebdbcddb63a670552b3c2Adrián Riesco-}

010997ddd12186698c1ebdbcddb63a670552b3c2Adrián RiescopelletProver :: Prover Sign Axiom OWLMorphism OWLSub ProofTree

010997ddd12186698c1ebdbcddb63a670552b3c2Adrián RiescopelletProver = (mkProverTemplate "Pellet" sl_top pelletGUI)

1d48923f0ec0898cfc40df24690af805fa4369edAdrián Riesco { proveCMDLautomatic = Just pelletCMDLautomatic

1d48923f0ec0898cfc40df24690af805fa4369edAdrián Riesco , proveCMDLautomaticBatch = Just pelletCMDLautomaticBatch }

1d48923f0ec0898cfc40df24690af805fa4369edAdrián Riesco

1d48923f0ec0898cfc40df24690af805fa4369edAdrián RiescopelletConsChecker :: ConsChecker Sign Axiom OWLSub

d2020d73b5be74ca654c2facd411387941c6b206Martin Kühl OWLMorphism ProofTree

ccead401e8728af7734715b70ec4f5c34096b683Martin KühlpelletConsChecker = (mkProverTemplate "Pellet Consistency Checker" sl_top

ccead401e8728af7734715b70ec4f5c34096b683Martin Kühl (\ s -> consCheck True s $ TacticScript "800"))

ccead401e8728af7734715b70ec4f5c34096b683Martin Kühl { proveCMDLautomatic = Just

ccead401e8728af7734715b70ec4f5c34096b683Martin Kühl $ \ s ts t -> fmap return . consCheck False s ts t }

ccead401e8728af7734715b70ec4f5c34096b683Martin Kühl

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- |

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Record for prover specific functions. This is used by both GUI and command

ccead401e8728af7734715b70ec4f5c34096b683Martin Kühl line interface.

-}

atpFun :: String -- ^ theory name

-> ATPFunctions Sign Axiom OWLMorphism ProofTree PelletProverState

atpFun thName = ATPFunctions

{ initialProverState = pelletProverState,

atpTransSenName = id, -- transSenName,

atpInsertSentence = insertOWLAxiom,

goalOutput = showOWLProblem thName,

proverHelpText = "http://clarkparsia.com/pellet/\n",

batchTimeEnv = "HETS_Pellet_BATCH_TIME_LIMIT",

fileExtensions = FileExtensions{problemOutput = ".owl", -- owl-hets

proverOutput = ".pellet",

theoryConfiguration = ".pconf"},

runProver = runPellet,

createProverOptions = extraOpts}

{- |

Inserts a named OWL axiom into pellet prover state.

-}

insertOWLAxiom :: PelletProverState -- ^ prover state containing

-- initial logical part

-> Named Axiom -- ^ goal to add

-> PelletProverState

insertOWLAxiom pps s =

pps{initialState = (initialState pps) ++ [s]}

-- ** GUI

{- |

Invokes the generic prover GUI.

-}

pelletGUI :: String -- ^ theory name

-> Theory Sign Axiom ProofTree

-> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints

-> IO([ProofStatus ProofTree]) -- ^ proof status for each goal

pelletGUI thName th freedefs =

genericATPgui (atpFun thName) True (proverName pelletProver) thName th

freedefs emptyProofTree

-- ** command line functions

{- |

Implementation of 'Logic.Prover.proveCMDLautomatic' which provides an

automatic command line interface for a single goal.

Pellet specific functions are omitted by data type ATPFunctions.

-}

pelletCMDLautomatic ::

String -- ^ theory name

-> TacticScript -- ^ default tactic script

-> Theory Sign Axiom ProofTree

-- ^ theory consisting of a signature and a list of Named sentence

-> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints

-> IO (Result.Result ([ProofStatus ProofTree]))

-- ^ Proof status for goals and lemmas

pelletCMDLautomatic thName defTS th freedefs =

genericCMDLautomatic (atpFun thName) (proverName pelletProver) thName

(parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

{- |

Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an

automatic command line interface to the Pellet prover via MathServe.

Pellet specific functions are omitted by data type ATPFunctions.

-}

pelletCMDLautomaticBatch ::

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 Axiom ProofTree -- ^ theory

-> [FreeDefMorphism Axiom OWLMorphism] -- ^ 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

pelletCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar

thName defTS th freedefs =

genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch

resultMVar (proverName pelletProver) thName

(parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

-- * Main prover functions

{- |

Runs the Pellet service.

-}

spamOutput :: ProofStatus ProofTree -> IO ()

spamOutput ps =

let

dName = goalName ps

dStat = goalStatus ps

dTree = proofTree ps

in

case dStat of

Open (Reason l) ->

createTextSaveDisplay "Pellet prover" ("./"++ dName ++".pellet.log")

$ unlines

(show dTree :l)

Disproved -> createTextSaveDisplay "Pellet prover" (dName ++".pellet.owl")

(

show dTree

)

Proved (Just True) -> -- consistent

do --createInfoWindow "Pellet consistency check"

-- "This ontology is consistent."

createTextSaveDisplay "Pellet prover" ("./"++ dName ++".pellet.log")

(

-- "I found a model for the theory " ++

-- dName ++". :) \n" ++

show dTree

)

Proved (Just False) -> -- not consistent

do --createInfoWindow "Pellet consistency check"

-- "This ontology is not consistent."

createTextSaveDisplay "Pellet prover" ("./"++ dName ++".pellet.log")

(

-- "I found a model for the theory " ++

-- dName ++". :) \n" ++

show dTree

)

Proved Nothing -> return () -- todo: another errors

getEnvSec :: String -> IO String

getEnvSec s = getEnvDef s ""

consCheck :: Bool -> String

-> TacticScript

-> TheoryMorphism Sign Axiom OWLMorphism ProofTree

-> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints

-> IO([ProofStatus ProofTree])

consCheck doSpamOutput thName tac@(TacticScript tl) tm freedefs =

case tTarget tm of

Theory sig nSens ->

let

saveOWL = False

timeLimitI = fromMaybe 800 $ readMaybe tl

proverStateI = pelletProverState sig

(toNamedList nSens) freedefs

-- problem = showOWLProblemA thName proverStateI []

problemS = showOWLProblemS thName proverStateI []

simpleOptions = "consistency "

extraOptions = ""

saveFileName = reverse $ fst $ span (/='/') $ reverse thName

tmpFileName = saveFileName

pStatus out tUsed = ProofStatus

{ goalName = thName

, goalStatus = Disproved

, usedAxioms = getAxioms

, usedProver = proverName pelletProver

, proofTree = ProofTree $ unlines out ++ "\n\n" ++ problemS

, usedTime = timeToTimeOfDay

$ secondsToDiffTime $ toInteger tUsed

, tacticScript = tac }

proofStatM :: ExitCode -> String -> [String]

-> Int -> ProofStatus ProofTree

proofStatM exitCode _ out tUsed =

case exitCode of

ExitSuccess -> -- consistent

(pStatus out tUsed)

{ goalStatus = Proved (Just True) }

ExitFailure 1 -> -- not consistent

(pStatus out tUsed)

{ goalStatus = Proved (Just False) }

ExitFailure 2 -> -- error by runing pellet

(pStatus out tUsed)

{ proofTree = ProofTree "Cannot run pellet." }

ExitFailure 3 -> -- timeout

(pStatus out tUsed)

{ goalStatus = openGoalStatus

, proofTree = ProofTree $ unlines out ++ "\n\n" ++ "timeout"

++ unlines out

, usedTime = timeToTimeOfDay $ secondsToDiffTime 0 }

ExitFailure 4 -> -- error by runing pellet

(pStatus out tUsed)

{ proofTree = ProofTree $ "Pellet returned an error.\n"

++ unlines out }

ExitFailure _ -> -- another errors

pStatus out tUsed

getAxioms =

map senAttr $ initialState proverStateI

timeWatch :: Int

-> IO (ProofStatus ProofTree)

-> IO (ProofStatus ProofTree)

timeWatch time process =

do

mvar <- newEmptyMVar

tid1 <- forkIO $ do z <- process

putMVar mvar (Just z)

tid2 <- forkIO $ do threadDelay (time * 1000000)

putMVar mvar Nothing

res <- takeMVar mvar

case res of

Just z -> do

killThread tid2 `catch` print

return z

Nothing -> do

killThread tid1 `catch` print

return (ProofStatus{

goalName = thName

, goalStatus = openGoalStatus

, usedAxioms = getAxioms

, usedProver = proverName pelletProver

, proofTree = ProofTree ("\n\n" ++ "timeout")

, usedTime = timeToTimeOfDay $ secondsToDiffTime 0

, tacticScript = tac

})

in

do

(progTh, progEx) <- check4Pellet

case (progTh, progEx) of

(True,True) -> do

when saveOWL

(writeFile (saveFileName ++".owl") problemS)

t <- getCurrentTime

tempDir <- getTemporaryDirectory

let timeTmpFile = tempDir ++ "/" ++ tmpFileName

++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".owl"

tmpURI = "file://" ++ timeTmpFile

writeFile timeTmpFile $ problemS

let command = "sh pellet.sh "

++ simpleOptions ++ extraOptions

++ tmpURI

pPath <- getEnvSec "PELLET_PATH"

setCurrentDirectory(pPath)

outState <- timeWatch timeLimitI $

(do

(_, outh, errh, proch) <- runInteractiveCommand command

waitForProcess proch

outp <- hGetContents outh

eOut <- hGetContents errh

let (exCode, output, tUsed) = analyseOutput outp eOut

let outState = proofStatM exCode simpleOptions

output tUsed

return outState

)

when doSpamOutput $ spamOutput outState

removeFile timeTmpFile

return [outState]

(b, _) -> do

let mess = "Pellet not " ++

if b then "executable" else "found"

infoDialog "Pellet prover" mess

return [(openProofStatus thName (proverName pelletProver)

$ ProofTree mess)

{ usedAxioms = getAxioms

, tacticScript = tac

}]

check4Pellet :: IO (Bool, Bool)

check4Pellet =

do

pPath <- getEnvSec "PELLET_PATH"

progTh <- doesFileExist $ pPath ++ "/pellet.sh"

progEx <- if (progTh)

then

do

progPerms <- getPermissions $ pPath ++ "/pellet.sh"

return $ executable $ progPerms

else

return False

return $ (progTh, progEx)

-- TODO: Pellet Prove for single goals.

runPellet :: PelletProverState

-- ^ 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)

runPellet sps cfg savePellet thName nGoal =

do

(progTh, progEx) <- check4Pellet

case (progTh,progEx) of

(True,True) -> do

let prob = showOWLProblemS thName sps []

let entail = showOWLProblemS thName

(sps{initialState = [nGoal{isAxiom=True}]}) []

when savePellet

(writeFile (saveFileName ++".owl") prob)

when savePellet

(writeFile (saveFileName ++".entail.owl") entail)

t <- getCurrentTime

tempDir <- getTemporaryDirectory

let timeTmpFile = tempDir ++ "/" ++ tmpFileName ++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".owl"

entailsFile = tempDir ++ "/" ++ tmpFileName ++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".entails.owl"

writeFile timeTmpFile prob

writeFile entailsFile entail

let command = "sh pellet.sh " ++ extraOptions ++ " " ++ entailsFile

++ " " ++ timeTmpFile

pPath <- getEnvSec "PELLET_PATH"

setCurrentDirectory(pPath)

((err, retval),output, tUsed) <- case tLimit of

Nothing ->

do

(_, outh, errh, proch) <- runInteractiveCommand command

waitForProcess proch

output <- hGetContents outh

eOut <- hGetContents errh

let (exCode, outp, tUsed) = analyseOutput output eOut

return $ (proofStat exCode simpleOptions outp tUsed,

outp, tUsed)

Just tm ->

timeWatchP tm

(do

(_, outh, errh, proch) <- runInteractiveCommand command

waitForProcess proch

output <- hGetContents outh

eOut <- hGetContents errh

let (exCode, outp, tUsed) = analyseOutput output eOut

return $ (proofStat exCode simpleOptions outp tUsed,

outp, tUsed)

)

removeFile timeTmpFile

removeFile entailsFile

return (err,

cfg{proofStatus = retval,

resultOutput = output,

timeUsed = timeToTimeOfDay $

secondsToDiffTime $ toInteger tUsed})

(True,False) -> return

(ATPError "Pellet prover found, but file is not executable.",

emptyConfig (proverName pelletProver)

(senAttr nGoal) emptyProofTree)

(False,_) -> return

(ATPError "Could not find pellet prover. Is $PELLET_PATH set?",

emptyConfig (proverName pelletProver)

(senAttr nGoal) emptyProofTree)

where

simpleOptions = extraOpts cfg

tLimit = timeLimit cfg

extraOptions = "entail -e "

goalSuffix = '_' : senAttr nGoal

saveFileName = thName ++ goalSuffix

tmpFileName = reverse (takeWhile (/= '/') $ reverse thName) ++ goalSuffix

timeWatchP :: Int -> IO ((ATPRetval, ProofStatus ProofTree), [String], Int)

-> IO ((ATPRetval, ProofStatus ProofTree), [String] , Int)

timeWatchP time process =

do

mvar <- newEmptyMVar

tid1 <- forkIO $ do z <- process

putMVar mvar (Just z)

tid2 <- forkIO $ do threadDelay (time * 1000000)

putMVar mvar Nothing

res <- takeMVar mvar

case res of

Just z -> do

killThread tid2 `catch` (\e -> putStrLn (show e))

return z

Nothing -> do

killThread tid1 `catch` (\e -> putStrLn (show e))

return ((ATPTLimitExceeded

, defaultProofStatus simpleOptions)

, [],time)

proofStat exitCode options out tUsed =

case exitCode of

ExitSuccess -> (ATPSuccess, (provedStatus options tUsed)

{

usedAxioms = map senAttr $

initialState sps

}

)

ExitFailure 2 -> (ATPError (unlines ("Internal error.":out)),

defaultProofStatus options)

ExitFailure 112 ->

(ATPTLimitExceeded, defaultProofStatus options)

ExitFailure 105 ->

(ATPBatchStopped, defaultProofStatus options)

ExitFailure _ ->

(ATPSuccess, disProvedStatus options)

tScript opts = TacticScript $ show $ ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg

, tsExtraOpts = opts }

defaultProofStatus opts =

(openProofStatus

(senAttr nGoal) (proverName pelletProver) $

emptyProofTree)

{ tacticScript = tScript opts }

disProvedStatus opts = (defaultProofStatus opts)

{goalStatus = Disproved}

provedStatus opts ut =

ProofStatus {

goalName = senAttr nGoal

,goalStatus = Proved (Just True)

,usedAxioms = getAxioms -- []

,usedProver = proverName pelletProver

,proofTree = emptyProofTree

,usedTime = timeToTimeOfDay $

secondsToDiffTime $ toInteger ut

,tacticScript = tScript opts }

getAxioms = []

analyseOutput :: String -> String -> (ExitCode, [String], Int)

analyseOutput err outp =

let

errL = lines err

outL = lines outp

anaHelp x [] = x

anaHelp (exCode, output, to) (line:ls) =

let (okey, ovalue) = span (/=':') line

in

if "Usage: java Pellet" `isPrefixOf` line

-- error by running pellet.

then (ExitFailure 2, (output ++ [line]), to)

else if okey == "Consistent" -- consistent state

then if (tail $ tail ovalue) == "Yes" then

anaHelp (ExitSuccess, (output ++ [line]), to) ls

else anaHelp (ExitFailure 1, (output ++ [line]), to) ls

else if "Time" `isPrefixOf` okey -- get cup time

then anaHelp (exCode, (output ++ [line]),

((read $ fst $ span (/=' ') $ tail ovalue)::Int)) ls

else if "All axioms are entailed" `isPrefixOf` line

then

anaHelp (ExitSuccess, (output ++ [line]), to) ls

else if "Non-entailments:" `isPrefixOf` line

then

anaHelp (ExitFailure 5, (output ++ [line]), to) ls

else if "ERROR:" `isPrefixOf` line

then

anaHelp (ExitFailure 4, (output ++ [line]), to) ls

else

anaHelp (exCode, (output ++ [line]), to) ls

in

anaHelp (ExitFailure 1, [], -1) (outL ++ errL)

showOWLProblemS :: String -- ^ theory name

-> PelletProverState -- ^ prover state containing

-- initial logical part

-> [String] -- ^ extra options

-> String -- ^ formatted output of the goal

showOWLProblemS thName pst _ =

let namedSens = initialState $ problemProverState

$ genPelletProblemS thName pst Nothing

sign = ontologySign $ problemProverState

$ genPelletProblemS thName pst Nothing

in show $ printOWLBasicTheory (sign, filter (\ax -> isAxiom(ax)) namedSens)

{- |

Pretty printing SoftFOL goal in DFG format.

-}

showOWLProblem :: String -- ^ theory name

-> PelletProverState -- ^ prover state containing

-- initial logical part

-> Named Axiom -- ^ goal to print

-> [String] -- ^ extra options

-> IO String -- ^ formatted output of the goal

showOWLProblem thName pst nGoal _ =

let namedSens = initialState $ problemProverState

$ genPelletProblemS thName pst Nothing

sign = ontologySign $ problemProverState

$ genPelletProblemS thName pst Nothing

in return $

((show $ printOWLBasicTheory (sign, filter (\ax -> isAxiom(ax)) namedSens))

++ "\n\nEntailments:\n\n" ++

(show $ printOWLBasicTheory (sign, [nGoal]))

)

{- |

Generate a SoftFOL problem with time stamp while maybe adding a goal.

-}

genPelletProblemS :: String -> PelletProverState

-> Maybe (Named Axiom)

-> PelletProblem

genPelletProblemS thName pps m_nGoal =

PelletProblem

{identifier = thName

, problemProverState = pps

{ initialState = initialState pps ++

(maybe [] (\g -> g:[]) m_nGoal)}

}