Merge pull request #1601 from spechub/1587_extracting_modules

1587 extracting modules

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

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

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

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  :  [email protected]
+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"

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

OWL2/ParseOWL.hs

@@ -0,0 +1,96 @@
+{- |
+Module      :  $Header$
+Copyright   :  Heng Jiang, Uni Bremen 2004-2007
+License     :  GPLv2 or higher, see LICENSE.txt
+
+Maintainer  :  [email protected]
+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)
+

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

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'')