{- |
Module      :  ./OWL2/Conservativity.hs
Copyright   :  (c) Dominik Luecke, 2008
License     :  GPLv2 or higher, see LICENSE.txt

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

This module implements conservativity checks for OWL 2.0 based on the
the syntactic locality checker written in Java from the OWL-Api.
-}

module OWL2.Conservativity
  ( localityJar
  , conserCheck
  ) where

import Common.AS_Annotation
import Common.Consistency
import Common.Result
import Common.ProverTools
import Common.Utils
import qualified Control.Monad.Fail as Fail

import GUI.Utils ()

import OWL2.AS
import OWL2.Morphism
import OWL2.Sign
import OWL2.XMLConversion

import System.Directory
import System.Exit

localityJar :: String
localityJar :: String
localityJar = "OWLLocality.jar"

-- | Conservativity Check for Propositional Logic
conserCheck :: String                        -- ^ Conser type
           -> (Sign, [Named Axiom])       -- ^ Initial sign and formulas
           -> OWLMorphism                    -- ^ morphism between specs
           -> [Named Axiom]               -- ^ Formulas of extended spec
           -> IO (Result (Conservativity, [Axiom]))
conserCheck :: String
-> (Sign, [Named Axiom])
-> OWLMorphism
-> [Named Axiom]
-> IO (Result (Conservativity, [Axiom]))
conserCheck ct :: String
ct = (Sign
 -> [Named Axiom]
 -> OWLMorphism
 -> [Named Axiom]
 -> IO (Result (Conservativity, [Axiom])))
-> (Sign, [Named Axiom])
-> OWLMorphism
-> [Named Axiom]
-> IO (Result (Conservativity, [Axiom]))
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Sign
  -> [Named Axiom]
  -> OWLMorphism
  -> [Named Axiom]
  -> IO (Result (Conservativity, [Axiom])))
 -> (Sign, [Named Axiom])
 -> OWLMorphism
 -> [Named Axiom]
 -> IO (Result (Conservativity, [Axiom])))
-> (Sign
    -> [Named Axiom]
    -> OWLMorphism
    -> [Named Axiom]
    -> IO (Result (Conservativity, [Axiom])))
-> (Sign, [Named Axiom])
-> OWLMorphism
-> [Named Axiom]
-> IO (Result (Conservativity, [Axiom]))
forall a b. (a -> b) -> a -> b
$ String
-> String
-> Sign
-> [Named Axiom]
-> OWLMorphism
-> [Named Axiom]
-> IO (Result (Conservativity, [Axiom]))
doConservCheck String
localityJar String
ct

-- | Real conservativity check in IO Monad
doConservCheck :: String            -- ^ Jar name
               -> String            -- ^ Conser Type
               -> Sign              -- ^ Signature of Onto 1
               -> [Named Axiom]  -- ^ Formulas of Onto 1
               -> OWLMorphism       -- ^ Morphism
               -> [Named Axiom]  -- ^ Formulas of Onto 2
               -> IO (Result (Conservativity, [Axiom]))
doConservCheck :: String
-> String
-> Sign
-> [Named Axiom]
-> OWLMorphism
-> [Named Axiom]
-> IO (Result (Conservativity, [Axiom]))
doConservCheck jar :: String
jar ct :: String
ct sig1 :: Sign
sig1 sen1 :: [Named Axiom]
sen1 mor :: OWLMorphism
mor sen2 :: [Named Axiom]
sen2 =
  let ontoFile :: String
ontoFile = Sign -> [Named Axiom] -> String
mkODoc (OWLMorphism -> Sign
otarget OWLMorphism
mor) [Named Axiom]
sen2
      sigFile :: String
sigFile = Sign -> [Named Axiom] -> String
mkODoc Sign
sig1 ((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]
sen1)
  in String
-> String
-> String
-> String
-> IO (Result (Conservativity, [Axiom]))
runLocalityChecker String
jar String
ct String
ontoFile String
sigFile

-- | Invoke the Java checker
runLocalityChecker :: String            -- ^ Jar name
                   -> String            -- ^ Conser Type
                   -> String            -- ^ Ontology
                   -> String            -- ^ String
                   -> IO (Result (Conservativity, [Axiom]))
runLocalityChecker :: String
-> String
-> String
-> String
-> IO (Result (Conservativity, [Axiom]))
runLocalityChecker jar :: String
jar ct :: String
ct onto :: String
onto sig :: String
sig = do
  (progTh :: Bool
progTh, toolPath :: String
toolPath) <- String -> IO (Bool, String)
check4HetsOWLjar String
jar
  if Bool
progTh then String
-> IO (Result (Conservativity, [Axiom]))
-> IO (Result (Conservativity, [Axiom]))
forall a. String -> IO a -> IO a
withinDirectory String
toolPath (IO (Result (Conservativity, [Axiom]))
 -> IO (Result (Conservativity, [Axiom])))
-> IO (Result (Conservativity, [Axiom]))
-> IO (Result (Conservativity, [Axiom]))
forall a b. (a -> b) -> a -> b
$ do
      String
sigFile <- String -> String -> IO String
getTempFile String
sig "ConservativityCheck.sig.owl"
      let tLimit :: Int
tLimit = 800
          ontoFile :: String
ontoFile = String
sigFile String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".onto.owl"
          jargs :: [String]
jargs = ["-jar", String
jar, "file://" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ontoFile, "file://" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sigFile, String
ct]
      String -> String -> IO ()
writeFile String
ontoFile String
onto
      Maybe (ExitCode, String, String)
mExit <- Int -> String -> [String] -> IO (Maybe (ExitCode, String, String))
timeoutCommand Int
tLimit "java" [String]
jargs
      String -> IO ()
removeFile String
ontoFile
      String -> IO ()
removeFile String
sigFile
      Result (Conservativity, [Axiom])
-> IO (Result (Conservativity, [Axiom]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [Axiom])
 -> IO (Result (Conservativity, [Axiom])))
-> Result (Conservativity, [Axiom])
-> IO (Result (Conservativity, [Axiom]))
forall a b. (a -> b) -> a -> b
$ case Maybe (ExitCode, String, String)
mExit of
        Just (cont :: ExitCode
cont, out :: String
out, _) -> String -> ExitCode -> Result (Conservativity, [Axiom])
parseOutput String
out ExitCode
cont
        Nothing -> String -> Result (Conservativity, [Axiom])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Conservativity, [Axiom]))
-> String -> Result (Conservativity, [Axiom])
forall a b. (a -> b) -> a -> b
$ "Timelimit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
tLimit String -> String -> String
forall a. [a] -> [a] -> [a]
++ " exceeded"
    else Result (Conservativity, [Axiom])
-> IO (Result (Conservativity, [Axiom]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [Axiom])
 -> IO (Result (Conservativity, [Axiom])))
-> Result (Conservativity, [Axiom])
-> IO (Result (Conservativity, [Axiom]))
forall a b. (a -> b) -> a -> b
$ String -> Result (Conservativity, [Axiom])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Conservativity, [Axiom]))
-> String -> Result (Conservativity, [Axiom])
forall a b. (a -> b) -> a -> b
$ String
jar String -> String -> String
forall a. [a] -> [a] -> [a]
++ " not found"

parseOutput :: String
            -> ExitCode
            -> Result (Conservativity, [Axiom])
parseOutput :: String -> ExitCode -> Result (Conservativity, [Axiom])
parseOutput ls1 :: String
ls1 exit :: ExitCode
exit = do
  let ls :: [String]
ls = String -> [String]
lines String
ls1
  case ExitCode
exit of
    ExitFailure 10 -> (Conservativity, [Axiom]) -> Result (Conservativity, [Axiom])
forall (m :: * -> *) a. Monad m => a -> m a
return (Conservativity
Cons, [])
    ExitFailure 20 -> String -> Result (Conservativity, [Axiom])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Conservativity, [Axiom]))
-> String -> Result (Conservativity, [Axiom])
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
ls
    x :: ExitCode
x -> String -> Result (Conservativity, [Axiom])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Conservativity, [Axiom]))
-> String -> Result (Conservativity, [Axiom])
forall a b. (a -> b) -> a -> b
$ "Internal program error: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ExitCode -> String
forall a. Show a => a -> String
show ExitCode
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
ls