4169N/A{- |

1178N/AModule : $Header$

1178N/ACopyright : (c) Dominik Luecke, 2008

1178N/ALicense : GPLv2 or higher, see LICENSE.txt

1178N/A

1178N/AMaintainer : luecke@informatik.uni-bremen.de

1178N/AStability : provisional

1178N/APortability : non-portable

1178N/A

1178N/AThis module implements conservativity checks for OWL 2.0 based on the

1178N/Athe syntactic locality checker written in Java from the OWL-Api.

1178N/A-}

1178N/A

1178N/Amodule OWL.Conservativity

1178N/A ( localityJar

1178N/A , conserCheck

1178N/A ) where

2362N/A

2362N/Aimport Common.AS_Annotation

2362N/Aimport Common.Consistency

1178N/Aimport Common.Result

4169N/Aimport Common.ProverTools

1178N/Aimport Common.Utils

1178N/A

4033N/Aimport GUI.Utils ()

4033N/A

1178N/Aimport OWL.AS

1178N/Aimport OWL.Morphism

1178N/Aimport OWL.Print (printOWLBasicTheory)

1178N/Aimport OWL.Sign

4033N/A

1178N/Aimport System.Directory

1178N/Aimport System.Exit

4033N/Aimport System.IO

1178N/A

1178N/AlocalityJar :: String

4033N/AlocalityJar = "OWLLocality.jar"

1178N/A

1178N/A-- | Conservativity Check for Propositional Logic

4033N/AconserCheck :: String -- ^ Conser type

1178N/A -> (Sign, [Named Axiom]) -- ^ Initial sign and formulas

1178N/A -> OWLMorphism -- ^ morphism between specs

4033N/A -> [Named Axiom] -- ^ Formulas of extended spec

1178N/A -> IO (Result (Maybe (Conservativity, [Axiom])))

1178N/AconserCheck ct = uncurry $ doConservCheck localityJar ct

1178N/A

4033N/A-- | Real conservativity check in IO Monad

0N/AdoConservCheck :: String -- ^ Jar name

0N/A -> String -- ^ Conser Type

0N/A -> Sign -- ^ Signature of Onto 1

0N/A -> [Named Axiom] -- ^ Formulas of Onto 1

0N/A -> OWLMorphism -- ^ Morphism

0N/A -> [Named Axiom] -- ^ Formulas of Onto 2

0N/A -> IO (Result (Maybe (Conservativity, [Axiom])))

0N/AdoConservCheck jar ct sig1 sen1 mor sen2 =

0N/A let ontoFile = printOWLBasicTheory (otarget mor, filter isAxiom sen2)

0N/A sigFile = printOWLBasicTheory (sig1, filter isAxiom sen1)

0N/A in runLocalityChecker jar ct (show ontoFile) (show sigFile)

4033N/A

0N/A-- | Invoke the Java checker

1178N/ArunLocalityChecker :: String -- ^ Jar name

0N/A -> String -- ^ Conser Type

1178N/A -> String -- ^ Ontology

4033N/A -> String -- ^ String

1178N/A -> IO (Result (Maybe (Conservativity, [Axiom])))

0N/ArunLocalityChecker jar ct onto sig = do

1178N/A (progTh, toolPath) <- check4HetsOWLjar jar

4033N/A if progTh then withinDirectory toolPath $ do

4033N/A tempDir <- getTemporaryDirectory

4033N/A sigFile <- writeTempFile sig tempDir "ConservativityCheck.sig.owl"

0N/A let tLimit = 800

4033N/A ontoFile = sigFile ++ ".onto.owl"

1178N/A command = "java -jar " ++ jar ++ " file://" ++ ontoFile

4033N/A ++ " file://" ++ sigFile ++ " " ++ ct

4033N/A writeFile ontoFile onto

4033N/A (mExit, outh, _) <- timeoutCommand tLimit command

4033N/A removeFile ontoFile

1178N/A removeFile sigFile

4033N/A case mExit of

0N/A Just cont -> parseOutput outh cont

4033N/A Nothing ->

4033N/A return $ fail $ "Timelimit " ++ show tLimit ++ " exceeded"

4033N/A else return $ fail $ jar ++ " not found"

4033N/A

0N/AparseOutput :: Handle -- ^ handel of stdout

1178N/A -> ExitCode

0N/A -> IO (Result (Maybe (Conservativity, [Axiom])))

4033N/AparseOutput outh exit = do

1178N/A ls1 <- hGetContents outh

1178N/A let ls = lines ls1

1178N/A return $ case exit of

0N/A ExitFailure 10 -> return $ Just (Cons, [])

4033N/A ExitFailure 20 -> fail $ unlines ls

1178N/A x -> fail $ "Internal program error: " ++ show x ++ "\n" ++ unlines ls

1178N/A