module OWL2.ProverState where
import Logic.Prover
import OWL2.AS
import OWL2.Morphism
import OWL2.Sign
import OWL2.ManchesterPrint
import OWL2.XMLConversion
import Common.AS_Annotation
data ProverState = ProverState
{ ProverState -> Sign
ontologySign :: Sign,
ProverState -> [Named Axiom]
initialState :: [Named Axiom]
} deriving Int -> ProverState -> ShowS
[ProverState] -> ShowS
ProverState -> String
(Int -> ProverState -> ShowS)
-> (ProverState -> String)
-> ([ProverState] -> ShowS)
-> Show ProverState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProverState] -> ShowS
$cshowList :: [ProverState] -> ShowS
show :: ProverState -> String
$cshow :: ProverState -> String
showsPrec :: Int -> ProverState -> ShowS
$cshowsPrec :: Int -> ProverState -> ShowS
Show
owlProverState :: Sign -> [Named Axiom]
-> [FreeDefMorphism Axiom OWLMorphism]
-> ProverState
owlProverState :: Sign
-> [Named Axiom]
-> [FreeDefMorphism Axiom OWLMorphism]
-> ProverState
owlProverState sig :: Sign
sig oSens :: [Named Axiom]
oSens _ = ProverState :: Sign -> [Named Axiom] -> ProverState
ProverState
{ ontologySign :: Sign
ontologySign = Sign
sig,
initialState :: [Named Axiom]
initialState = (Named Axiom -> Bool) -> [Named Axiom] -> [Named Axiom]
forall a. (a -> Bool) -> [a] -> [a]
filter Named Axiom -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named Axiom]
oSens }
insertOWLAxiom :: ProverState
-> Named Axiom
-> ProverState
insertOWLAxiom :: ProverState -> Named Axiom -> ProverState
insertOWLAxiom pps :: ProverState
pps s :: Named Axiom
s = ProverState
pps { initialState :: [Named Axiom]
initialState = ProverState -> [Named Axiom]
initialState ProverState
pps [Named Axiom] -> [Named Axiom] -> [Named Axiom]
forall a. [a] -> [a] -> [a]
++ [Named Axiom
s] }
showOWLProblemS :: ProverState -> String
showOWLProblemS :: ProverState -> String
showOWLProblemS pst :: ProverState
pst =
let namedSens :: [Named Axiom]
namedSens = ProverState -> [Named Axiom]
initialState ProverState
pst
sign :: Sign
sign = ProverState -> Sign
ontologySign ProverState
pst
in Sign -> [Named Axiom] -> String
mkODoc Sign
sign ((Named Axiom -> Bool) -> [Named Axiom] -> [Named Axiom]
forall a. (a -> Bool) -> [a] -> [a]
filter Named Axiom -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named Axiom]
namedSens)
showOWLProblem :: ProverState
-> Named Axiom
-> IO String
showOWLProblem :: ProverState -> Named Axiom -> IO String
showOWLProblem pst :: ProverState
pst nGoal :: Named Axiom
nGoal =
let sign :: Sign
sign = ProverState -> Sign
ontologySign ProverState
pst
in String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ ProverState -> String
showOWLProblemS ProverState
pst
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n\nEntailments:\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show ((Sign, [Named Axiom]) -> Doc
printOWLBasicTheory (Sign
sign, [Named Axiom
nGoal]))