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

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

prover states for pellet and fact++
-}

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] -- ^ freeness constraints
    -> 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 }

{- |
  Inserts a named OWL2 axiom into the prover state.
-}
insertOWLAxiom :: ProverState -- ^ prover state containing initial logical part
               -> Named Axiom -- ^ goal to add
               -> 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 -- ^ formatted output
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)

{- |
  Pretty printing OWL goal for pellet or fact++
-}
showOWLProblem :: ProverState -- ^ prover state containing initial logical part
               -> Named Axiom -- ^ goal to print
               -> IO String -- ^ formatted output of the goal
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]))