diff --git a/Driver/ReadLibDefn.hs b/Driver/ReadLibDefn.hs index 31aa08beec..86ce08f7e0 100644 --- a/Driver/ReadLibDefn.hs +++ b/Driver/ReadLibDefn.hs @@ -111,7 +111,7 @@ readLibDefn lgraph opts mr file fileForPos input = Qvt -> liftIO $ fmap (: []) $ parseQvt file TPTPIn -> liftIO $ fmap (: []) $ parseTPTP input file #ifndef NOOWLLOGIC - OWLIn _ -> parseOWL (isStructured opts) file + OWLIn _ -> parseOWLAsLibDefn (isStructured opts) file #endif _ -> case runParser (library lgraph { dolOnly = ty == DOLIn }) (emptyAnnos ()) fileForPos input of diff --git a/Driver/WriteFn.hs b/Driver/WriteFn.hs index 2862290b59..98d56cda43 100644 --- a/Driver/WriteFn.hs +++ b/Driver/WriteFn.hs @@ -95,7 +95,7 @@ import VSE.ToSExpr #ifndef NOOWLLOGIC import OWL2.CreateOWL import OWL2.Logic_OWL2 -import OWL2.ParseOWLAsLibDefn (convertOWL) +import OWL2.ParseOWL (convertOWL) import qualified OWL2.ManchesterPrint as OWL2 (prepareBasicTheory) import qualified OWL2.ManchesterParser as OWL2 (basicSpec) #endif diff --git a/Logic/Logic.hs b/Logic/Logic.hs index 6f12f20c8a..9c3d5ac2a8 100644 --- a/Logic/Logic.hs +++ b/Logic/Logic.hs @@ -616,7 +616,10 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items equiv2cospan :: lid -> sign -> sign -> [symb_items] -> [symb_items] -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol) equiv2cospan _ _ _ _ _ = error "equiv2cospan nyi" - + -- | extract the module + extract_module :: lid -> [IRI] -> (sign, [Named sentence]) + -> Result (sign, [Named sentence]) + extract_module _ _ = return -- | print a whole theory printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs new file mode 100644 index 0000000000..c92fa9d3c8 --- /dev/null +++ b/OWL2/ExtractModule.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{- | +Module : $Header$ +Copyright : Till Mossakowski, Uni Magdeburg 2016 +License : GPLv2 or higher, see LICENSE.txt + +Maintainer : till@iws.cs.ovgu.de +Stability : provisional +Portability : portable + +OWL 2 module extraction +-} + +module OWL2.ExtractModule where + +import OWL2.Sign +import OWL2.MS +import OWL2.ManchesterPrint +import OWL2.ParseOWL +import OWL2.StaticAnalysis + +import Common.Utils +import Common.Result +import Common.ResultT +import Common.AS_Annotation +import Common.GlobalAnnotations +import qualified Common.IRI as IRI + +import Control.Monad.Trans +import System.IO.Unsafe + +import Common.ExtSign + +extractModule :: [IRI.IRI] -> (Sign, [Named Axiom]) + -> Result (Sign, [Named Axiom]) +extractModule syms onto = + unsafePerformIO $ runResultT $ extractModuleAux syms onto + +extractModuleAux :: [IRI.IRI] -> (Sign, [Named Axiom]) + -> ResultT IO (Sign, [Named Axiom]) +extractModuleAux syms onto = do + let ontology_content = show $ printOWLBasicTheory onto + inFile <- lift $ getTempFile ontology_content "in" + outFile <- lift $ getTempFile "" "out" + let args = [inFile, "--extract-module", "-m", "STAR"] + ++ map (\x -> show $ x{IRI.hasAngles = False}) syms + ++ ["-o", outFile] + (_code,_stdout,_stderr) <- lift $ executeProcess "owltools" args "" + (_imap,ontos) <- parseOWL False outFile + case ontos of + [modOnto] -> do + (_ontodoc, ExtSign sig _, sens) <- liftR $ + basicOWL2Analysis (modOnto, emptySign, emptyGlobalAnnos) + lift $ return (sig, sens) + _ -> error "the module should be just one ontology" diff --git a/OWL2/Logic_OWL2.hs b/OWL2/Logic_OWL2.hs index afadcb474e..1f26cefc62 100644 --- a/OWL2/Logic_OWL2.hs +++ b/OWL2/Logic_OWL2.hs @@ -52,6 +52,7 @@ import OWL2.StaticAnalysis import OWL2.Symbols import OWL2.Taxonomy import OWL2.Theorem +import OWL2.ExtractModule data OWL2 = OWL2 @@ -130,6 +131,7 @@ instance StaticAnalysis OWL2 OntologyDocument Axiom signature_colimit OWL2 = return . signColimit corresp2th OWL2 = corr2theo equiv2cospan OWL2 = addEquiv + extract_module OWL2 = extractModule #ifdef UNI_PACKAGE theory_to_taxonomy OWL2 = onto2Tax #endif diff --git a/OWL2/ParseOWL.hs b/OWL2/ParseOWL.hs new file mode 100644 index 0000000000..063a48f87f --- /dev/null +++ b/OWL2/ParseOWL.hs @@ -0,0 +1,96 @@ +{- | +Module : $Header$ +Copyright : Heng Jiang, Uni Bremen 2004-2007 +License : GPLv2 or higher, see LICENSE.txt + +Maintainer : Christian.Maeder@dfki.de +Stability : provisional +Portability : non-portable + +analyse OWL files by calling the external Java parser. +-} + +module OWL2.ParseOWL (parseOWL, convertOWL) where + +import OWL2.MS +import OWL2.Rename + +import qualified Data.ByteString.Lazy as L +import Data.List +import Data.Maybe +import qualified Data.Map as Map + +import Common.XmlParser +import Common.ProverTools +import Common.Result +import Common.ResultT +import Common.Utils + +import Control.Monad +import Control.Monad.Trans + +import OWL2.XML + +import System.Directory +import System.Exit +import System.FilePath + +import Text.XML.Light hiding (QName) + +-- | call for owl parser (env. variable $HETS_OWL_TOOLS muss be defined) +parseOWL :: Bool -- ^ Sets Option.quick + -> FilePath -- ^ local filepath or uri + -> ResultT IO (Map.Map String String, [OntologyDocument]) -- ^ map: uri -> OntologyFile +parseOWL quick fn = do + tmpFile <- lift $ getTempFile "" "owlTemp.xml" + (exitCode, _, errStr) <- parseOWLAux quick fn ["-o", "xml", tmpFile] + case (exitCode, errStr) of + (ExitSuccess, "") -> do + cont <- lift $ L.readFile tmpFile + lift $ removeFile tmpFile + parseProc cont + _ -> fail $ "process stop! " ++ shows exitCode "\n" ++ errStr + +parseOWLAux :: Bool -- ^ Sets Option.quick + -> FilePath -- ^ local filepath or uri + -> [String] -- ^ arguments for java parser + -> ResultT IO (ExitCode, String, String) +parseOWLAux quick fn args = do + let jar = "OWL2Parser.jar" + (hasJar, toolPath) <- lift $ check4HetsOWLjar jar + if hasJar + then lift $ executeProcess "java" (["-jar", toolPath jar] + ++ args ++ [fn] ++ ["-qk" | quick]) "" + else fail $ jar + ++ " not found, check your environment variable: " ++ hetsOWLenv + +-- | converts owl file to desired syntax using owl-api +convertOWL :: FilePath -> String -> IO String +convertOWL fn tp = do + Result ds mRes <- runResultT + $ parseOWLAux False fn ["-o-sys", tp] + case mRes of + Just (exitCode, content, errStr) -> case (exitCode, errStr) of + (ExitSuccess, "") -> return content + _ -> error $ "process stop! " ++ shows exitCode "\n" ++ errStr + _ -> error $ showRelDiags 2 ds + +parseProc :: L.ByteString + -> ResultT IO (Map.Map String String, [OntologyDocument]) +parseProc str = do + res <- lift $ parseXml str + case res of + Left err -> fail err + Right el -> let + es = elChildren el + mis = concatMap (filterElementsName $ isSmth "Missing") es + imap = Map.fromList . mapMaybe (\ e -> do + imp <- findAttr (unqual "name") e + ont <- findAttr (unqual "ontiri") e + return (imp, ont)) $ concatMap (filterElementsName $ isSmth "Loaded") es + in do + unless (null mis) . liftR . justWarn () $ "Missing imports: " + ++ intercalate ", " (map strContent mis) + return (imap, unifyDocs . map (xmlBasicSpec imap) + $ concatMap (filterElementsName $ isSmth "Ontology") es) + diff --git a/OWL2/ParseOWLAsLibDefn.hs b/OWL2/ParseOWLAsLibDefn.hs index f49b8cc121..80e85eaaf6 100644 --- a/OWL2/ParseOWLAsLibDefn.hs +++ b/OWL2/ParseOWLAsLibDefn.hs @@ -10,99 +10,37 @@ Portability : non-portable (imports Logic.Logic) analyse OWL files by calling the external Java parser. -} -module OWL2.ParseOWLAsLibDefn (parseOWL, convertOWL) where +module OWL2.ParseOWLAsLibDefn (parseOWLAsLibDefn) where import OWL2.AS import OWL2.MS -import OWL2.Rename -import qualified Data.ByteString.Lazy as L import Data.List import Data.Maybe import qualified Data.Map as Map -import Common.XmlParser import Common.Id import Common.IRI import Common.LibName -import Common.ProverTools -import Common.Result import Common.ResultT import Common.AS_Annotation -import Common.Utils - -import Control.Monad -import Control.Monad.Trans import Logic.Grothendieck + import OWL2.Logic_OWL2 -import OWL2.XML +import OWL2.ParseOWL import Syntax.AS_Library import Syntax.AS_Structured -import System.Directory -import System.Exit -import System.FilePath - -import Text.XML.Light hiding (QName) -- | call for owl parser (env. variable $HETS_OWL_TOOLS muss be defined) -parseOWL :: Bool -- ^ Sets Option.quick +parseOWLAsLibDefn :: Bool -- ^ Sets Option.quick -> FilePath -- ^ local filepath or uri -> ResultT IO [LIB_DEFN] -- ^ map: uri -> OntologyFile -parseOWL quick fn = do - tmpFile <- lift $ getTempFile "" "owlTemp.xml" - (exitCode, _, errStr) <- parseOWLAux quick fn ["-o", "xml", tmpFile] - case (exitCode, errStr) of - (ExitSuccess, "") -> do - cont <- lift $ L.readFile tmpFile - lift $ removeFile tmpFile - parseProc cont - _ -> fail $ "process stop! " ++ shows exitCode "\n" ++ errStr - -parseOWLAux :: Bool -- ^ Sets Option.quick - -> FilePath -- ^ local filepath or uri - -> [String] -- ^ arguments for java parser - -> ResultT IO (ExitCode, String, String) -parseOWLAux quick fn args = do - let jar = "OWL2Parser.jar" - (hasJar, toolPath) <- lift $ check4HetsOWLjar jar - if hasJar - then lift $ executeProcess "java" (["-jar", toolPath jar] - ++ args ++ [fn] ++ ["-qk" | quick]) "" - else fail $ jar - ++ " not found, check your environment variable: " ++ hetsOWLenv - --- | converts owl file to desired syntax using owl-api -convertOWL :: FilePath -> String -> IO String -convertOWL fn tp = do - Result ds mRes <- runResultT - $ parseOWLAux False fn ["-o-sys", tp] - case mRes of - Just (exitCode, content, errStr) -> case (exitCode, errStr) of - (ExitSuccess, "") -> return content - _ -> error $ "process stop! " ++ shows exitCode "\n" ++ errStr - _ -> error $ showRelDiags 2 ds - -parseProc :: L.ByteString -> ResultT IO [LIB_DEFN] -parseProc str = do - res <- lift $ parseXml str - case res of - Left err -> fail err - Right el -> let - es = elChildren el - mis = concatMap (filterElementsName $ isSmth "Missing") es - imap = Map.fromList . mapMaybe (\ e -> do - imp <- findAttr (unqual "name") e - ont <- findAttr (unqual "ontiri") e - return (imp, ont)) $ concatMap (filterElementsName $ isSmth "Loaded") es - in do - unless (null mis) . liftR . justWarn () $ "Missing imports: " - ++ intercalate ", " (map strContent mis) - return . map (convertToLibDefN imap) - . unifyDocs . map (xmlBasicSpec imap) - $ concatMap (filterElementsName $ isSmth "Ontology") es +parseOWLAsLibDefn quick fn = do + (imap, ontodocs) <- parseOWL quick fn + return $ map (convertToLibDefN imap) ontodocs qNameToIRI :: QName -> SPEC_NAME qNameToIRI qn = let s = showQN qn in diff --git a/Static/AnalysisStructured.hs b/Static/AnalysisStructured.hs index 3d954d2426..c337a43339 100644 --- a/Static/AnalysisStructured.hs +++ b/Static/AnalysisStructured.hs @@ -680,7 +680,9 @@ gsigUnionMaybe lg both mn gsig = case mn of anaExtraction :: LogicGraph -> LibEnv -> DGraph -> NodeSig -> NodeName -> Range -> EXTRACTION -> Result (NodeSig, DGraph) -anaExtraction lg libEnv dg nsig name rg _extr = do +anaExtraction lg libEnv dg nsig name rg (ExtractOrRemove b iris _) = if not b then + fail "analysis of remove not implemented yet" + else do let dg0 = markHiding libEnv dg n = getNode nsig if labelHasHiding $ labDG dg0 n then @@ -690,7 +692,14 @@ anaExtraction lg libEnv dg nsig name rg _extr = do gth = case (globalTheory . labDG dgThm) n of Nothing -> error "not able to compute theory" Just th -> th - (nsig', dg') = insGTheory dg (setSrcRange rg name) DGExtract gth + mTh <- case gth of + G_theory lid syntax (ExtSign sig _) _ gsens _ -> do + let nsens = toNamedList gsens + (msig, msens) <- extract_module lid iris (sig, nsens) + return $ G_theory lid syntax + (ExtSign msig $ foldl Set.union Set.empty $ sym_of lid msig) startSigId + (toThSens msens) startThId + let (nsig', dg') = insGTheory dg (setSrcRange rg name) DGExtract mTh incl <- ginclusion lg (getSig nsig') (getSig nsig) let dg'' = insLink dg' incl globalThm SeeSource (getNode nsig') n return (nsig', dg'')