ProverState.hs

{- |
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
    { ontologySign :: Sign,
      initialState :: [Named Axiom]
    } deriving Show

owlProverState :: Sign -> [Named Axiom]
    -> [FreeDefMorphism Axiom OWLMorphism] -- ^ freeness constraints
    -> ProverState
owlProverState sig oSens _ = ProverState
    { ontologySign = sig,
    initialState = filter isAxiom 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 pps s = pps { initialState = initialState pps ++ [s] }

showOWLProblemS :: ProverState -> String -- ^ formatted output
showOWLProblemS pst =
    let namedSens = initialState pst
        sign = ontologySign pst
    in mkODoc sign (filter isAxiom 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 pst nGoal =
  let sign = ontologySign pst
  in return $ showOWLProblemS pst
       ++ "\n\nEntailments:\n\n" ++ show (printOWLBasicTheory (sign, [nGoal]))