From 9bbe05a8f91264c88000bafff12062021e276bbd Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Mon, 14 Mar 2016 14:58:42 +0100
Subject: [PATCH 01/16] module extraction function

---
 Logic/Logic.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Logic/Logic.hs b/Logic/Logic.hs
index 6f12f20c8a..bb5fc27d63 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 -> [symbol] -> (sign, [Named sentence])
+                        -> Result (sign, [Named sentence])
+         extract_module _ _ = id
 
 -- | print a whole theory
 printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items

From a4ffdfbef0df89ab0bf32590c380514d98b42331 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Mon, 14 Mar 2016 15:04:33 +0100
Subject: [PATCH 02/16] return, not id

---
 Logic/Logic.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Logic/Logic.hs b/Logic/Logic.hs
index bb5fc27d63..d7f0544de1 100644
--- a/Logic/Logic.hs
+++ b/Logic/Logic.hs
@@ -619,7 +619,7 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items
          -- | extract the module 
          extract_module :: lid -> [symbol] -> (sign, [Named sentence])
                         -> Result (sign, [Named sentence])
-         extract_module _ _ = id
+         extract_module _ _ = return
 
 -- | print a whole theory
 printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items

From 5fd6270bfa78d9169d4124625898eb47fc0efb2b Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Mon, 14 Mar 2016 15:09:29 +0100
Subject: [PATCH 03/16] take IRIs as argument

---
 Logic/Logic.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Logic/Logic.hs b/Logic/Logic.hs
index d7f0544de1..9c3d5ac2a8 100644
--- a/Logic/Logic.hs
+++ b/Logic/Logic.hs
@@ -617,7 +617,7 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items
            -> Result (sign, sign, sign, EndoMap symbol, EndoMap symbol)
          equiv2cospan _ _ _ _ _ = error "equiv2cospan nyi"
          -- | extract the module 
-         extract_module :: lid -> [symbol] -> (sign, [Named sentence])
+         extract_module :: lid -> [IRI] -> (sign, [Named sentence])
                         -> Result (sign, [Named sentence])
          extract_module _ _ = return
 

From 14997b7e496dc262dc44a4c51c9b3cc87bbf7154 Mon Sep 17 00:00:00 2001
From: Till Mossakowski <till@communtu.de>
Date: Mon, 14 Mar 2016 15:10:48 +0100
Subject: [PATCH 04/16] first dummy instance of module extraction in OWL

---
 OWL2/ExtractModule.hs | 31 +++++++++++++++++++++++++++++++
 OWL2/Logic_OWL2.hs    |  2 ++
 2 files changed, 33 insertions(+)
 create mode 100644 OWL2/ExtractModule.hs

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
new file mode 100644
index 0000000000..fff07ab832
--- /dev/null
+++ b/OWL2/ExtractModule.hs
@@ -0,0 +1,31 @@
+{-# 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.AS
+import OWL2.Sign
+import OWL2.MS
+
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+
+import Common.Result
+import Common.AS_Annotation
+import qualified Common.IRI as IRI
+
+import Control.Monad
+
+extractModule :: [IRI.IRI] -> (Sign, [Named Axiom])
+                          -> Result (Sign, [Named Axiom])
+extractModule _ = return
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

From 38a49fc8944a7d280e1b0d27c1dfa3f01802ab8a Mon Sep 17 00:00:00 2001
From: Till Mossakowski <till@communtu.de>
Date: Mon, 14 Mar 2016 15:31:29 +0100
Subject: [PATCH 05/16] introduced IO, will be needed for calling owltools

---
 OWL2/ExtractModule.hs | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index fff07ab832..017498390d 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -21,11 +21,20 @@ import qualified Data.Set as Set
 import qualified Data.Map as Map
 
 import Common.Result
+import Common.ResultT
 import Common.AS_Annotation
 import qualified Common.IRI as IRI
 
 import Control.Monad
+import System.IO.Unsafe
 
 extractModule :: [IRI.IRI] -> (Sign, [Named Axiom])
                           -> Result (Sign, [Named Axiom])
-extractModule _ = return
+extractModule sig onto =
+  unsafePerformIO $ runResultT $ extractModuleAux sig onto
+
+extractModuleAux :: [IRI.IRI] -> (Sign, [Named Axiom])
+                          -> ResultT IO (Sign, [Named Axiom])
+extractModuleAux _ = liftR . return
+
+

From 66d28f86d616f3b0eabbbdc2318b46dc9057c695 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Mon, 14 Mar 2016 15:33:45 +0100
Subject: [PATCH 06/16] prepared for module extraction

---
 Static/AnalysisStructured.hs | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/Static/AnalysisStructured.hs b/Static/AnalysisStructured.hs
index 3d954d2426..14be924d15 100644
--- a/Static/AnalysisStructured.hs
+++ b/Static/AnalysisStructured.hs
@@ -680,7 +680,7 @@ 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 _ iris _) = do
   let dg0 = markHiding libEnv dg
       n = getNode nsig
   if labelHasHiding $ labDG dg0 n then
@@ -690,7 +690,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'')

From 3d9ee034f596bfcc18f642e5a17a408cab4c299e Mon Sep 17 00:00:00 2001
From: Till Mossakowski <till@communtu.de>
Date: Mon, 14 Mar 2016 15:46:45 +0100
Subject: [PATCH 07/16] machinery for calling owltools

---
 OWL2/ExtractModule.hs | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index 017498390d..e413fbca53 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -20,21 +20,30 @@ import OWL2.MS
 import qualified Data.Set as Set
 import qualified Data.Map as Map
 
+import Common.Utils
 import Common.Result
 import Common.ResultT
 import Common.AS_Annotation
 import qualified Common.IRI as IRI
 
 import Control.Monad
+import Control.Monad.Trans
 import System.IO.Unsafe
 
 extractModule :: [IRI.IRI] -> (Sign, [Named Axiom])
-                          -> Result (Sign, [Named Axiom])
-extractModule sig onto =
-  unsafePerformIO $ runResultT $ extractModuleAux sig onto
+                           -> Result (Sign, [Named Axiom])
+extractModule syms onto =
+  unsafePerformIO $ runResultT $ extractModuleAux syms onto
 
 extractModuleAux :: [IRI.IRI] -> (Sign, [Named Axiom])
-                          -> ResultT IO (Sign, [Named Axiom])
-extractModuleAux _ = liftR . return
+                              -> ResultT IO (Sign, [Named Axiom])
+extractModuleAux syms onto = do
+  let ontolgy_content = "Class: A"
+  inFile <- lift $ getTempFile ontolgy_content "owl"
+  outFile <- lift $ getTempFile "" "owl"
+  let args = [inFile, "--extract-module", "-d"] 
+             ++ map show syms ++ ["-o", outFile]
+  (code,stdout,stderr) <- lift $ executeProcess "owltools" args ""
+  lift $ return onto
 
 

From 2d0278eddd7ecc78050bcbd6d0524344711414f5 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Mon, 14 Mar 2016 21:19:11 +0100
Subject: [PATCH 08/16] the input right, but problems with creating the result

---
 OWL2/ExtractModule.hs | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index e413fbca53..0b3a81ef35 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -16,6 +16,8 @@ module OWL2.ExtractModule where
 import OWL2.AS
 import OWL2.Sign
 import OWL2.MS
+import OWL2.ManchesterPrint
+import OWL2.ParseOWLAsLibDefn
 
 import qualified Data.Set as Set
 import qualified Data.Map as Map
@@ -30,6 +32,8 @@ import Control.Monad
 import Control.Monad.Trans
 import System.IO.Unsafe
 
+import Debug.Trace
+
 extractModule :: [IRI.IRI] -> (Sign, [Named Axiom])
                            -> Result (Sign, [Named Axiom])
 extractModule syms onto =
@@ -38,12 +42,16 @@ extractModule syms onto =
 extractModuleAux :: [IRI.IRI] -> (Sign, [Named Axiom])
                               -> ResultT IO (Sign, [Named Axiom])
 extractModuleAux syms onto = do
-  let ontolgy_content = "Class: A"
-  inFile <- lift $ getTempFile ontolgy_content "owl"
+  let ontology_content = show $ printOWLBasicTheory onto 
+   -- should be a string with the ontology from onto, maybe create a G_theory and pretty print it..., show theory
+  inFile <- lift $ getTempFile ontology_content "owl"
   outFile <- lift $ getTempFile "" "owl"
   let args = [inFile, "--extract-module", "-d"] 
              ++ map show syms ++ ["-o", outFile]
   (code,stdout,stderr) <- lift $ executeProcess "owltools" args ""
+  -- in outFile is the module, it needs to be parsed, see parseOWL in ParseOWLAsLibDefn.hs, convert a LIB_DEFN to a theory...
+  libDefn <- parseOWL False outFile
+  -- do liftIO for lifting something from Result to ResultT
   lift $ return onto
 
 

From 7af6ad49991a7f73b5d4233c89648a5a523f72bd Mon Sep 17 00:00:00 2001
From: Till Mossakowski <till@communtu.de>
Date: Tue, 15 Mar 2016 08:11:06 +0100
Subject: [PATCH 09/16] avoid cyclic import

---
 Driver/ReadLibDefn.hs     |  2 +-
 Driver/WriteFn.hs         |  2 +-
 OWL2/ExtractModule.hs     | 12 ++---
 OWL2/ParseOWL.hs          | 96 +++++++++++++++++++++++++++++++++++++++
 OWL2/ParseOWLAsLibDefn.hs | 76 +++----------------------------
 5 files changed, 111 insertions(+), 77 deletions(-)
 create mode 100644 OWL2/ParseOWL.hs

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/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index 0b3a81ef35..f5e6bcc077 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -13,14 +13,14 @@ OWL 2 module extraction
 
 module OWL2.ExtractModule where
 
-import OWL2.AS
+--import OWL2.AS
 import OWL2.Sign
 import OWL2.MS
 import OWL2.ManchesterPrint
-import OWL2.ParseOWLAsLibDefn
+import OWL2.ParseOWL
 
-import qualified Data.Set as Set
-import qualified Data.Map as Map
+--import qualified Data.Set as Set
+--import qualified Data.Map as Map
 
 import Common.Utils
 import Common.Result
@@ -28,7 +28,7 @@ import Common.ResultT
 import Common.AS_Annotation
 import qualified Common.IRI as IRI
 
-import Control.Monad
+--import Control.Monad
 import Control.Monad.Trans
 import System.IO.Unsafe
 
@@ -50,7 +50,7 @@ extractModuleAux syms onto = do
              ++ map show syms ++ ["-o", outFile]
   (code,stdout,stderr) <- lift $ executeProcess "owltools" args ""
   -- in outFile is the module, it needs to be parsed, see parseOWL in ParseOWLAsLibDefn.hs, convert a LIB_DEFN to a theory...
-  libDefn <- parseOWL False outFile
+  (imap,ontos) <- parseOWL False outFile
   -- do liftIO for lifting something from Result to ResultT
   lift $ return onto
 
diff --git a/OWL2/ParseOWL.hs b/OWL2/ParseOWL.hs
new file mode 100644
index 0000000000..3283015396
--- /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 (imports Logic.Logic)
+
+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

From 60780166855ae2887fed29bcb4bb74d620ce0285 Mon Sep 17 00:00:00 2001
From: Till Mossakowski <till@communtu.de>
Date: Tue, 15 Mar 2016 08:15:43 +0100
Subject: [PATCH 10/16] removed superfluous comment

---
 OWL2/ParseOWL.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/OWL2/ParseOWL.hs b/OWL2/ParseOWL.hs
index 3283015396..063a48f87f 100644
--- a/OWL2/ParseOWL.hs
+++ b/OWL2/ParseOWL.hs
@@ -5,7 +5,7 @@ License     :  GPLv2 or higher, see LICENSE.txt
 
 Maintainer  :  Christian.Maeder@dfki.de
 Stability   :  provisional
-Portability :  non-portable (imports Logic.Logic)
+Portability :  non-portable 
 
 analyse OWL files by calling the external Java parser.
 -}

From ebd9d5c5fbf26b74c71a2eebda3e1d4911f615b0 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Tue, 15 Mar 2016 10:15:48 +0100
Subject: [PATCH 11/16] analysis of the extracted module

---
 OWL2/ExtractModule.hs | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index f5e6bcc077..16a4949db2 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -18,6 +18,7 @@ import OWL2.Sign
 import OWL2.MS
 import OWL2.ManchesterPrint
 import OWL2.ParseOWL
+import OWL2.StaticAnalysis
 
 --import qualified Data.Set as Set
 --import qualified Data.Map as Map
@@ -26,13 +27,14 @@ 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
 import Control.Monad.Trans
 import System.IO.Unsafe
 
-import Debug.Trace
+import Common.ExtSign
 
 extractModule :: [IRI.IRI] -> (Sign, [Named Axiom])
                            -> Result (Sign, [Named Axiom])
@@ -48,10 +50,14 @@ extractModuleAux syms onto = do
   outFile <- lift $ getTempFile "" "owl"
   let args = [inFile, "--extract-module", "-d"] 
              ++ map show syms ++ ["-o", outFile]
-  (code,stdout,stderr) <- lift $ executeProcess "owltools" args ""
+  (_code,_stdout,_stderr) <- lift $ executeProcess "owltools" args ""
   -- in outFile is the module, it needs to be parsed, see parseOWL in ParseOWLAsLibDefn.hs, convert a LIB_DEFN to a theory...
-  (imap,ontos) <- parseOWL False outFile
-  -- do liftIO for lifting something from Result to ResultT
-  lift $ return onto
+  (_imap,ontos) <- parseOWL False outFile
+  -- do liftR for lifting something from Result to ResultT
+  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"
 
 

From 165e0ef4d935a44abefd85962c7a878cb12c0e88 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Tue, 15 Mar 2016 13:13:08 +0100
Subject: [PATCH 12/16] changed args

---
 OWL2/ExtractModule.hs | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index 16a4949db2..89e2fa08a5 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -36,6 +36,8 @@ import System.IO.Unsafe
 
 import Common.ExtSign
 
+import Debug.Trace
+
 extractModule :: [IRI.IRI] -> (Sign, [Named Axiom])
                            -> Result (Sign, [Named Axiom])
 extractModule syms onto =
@@ -46,17 +48,17 @@ extractModuleAux :: [IRI.IRI] -> (Sign, [Named Axiom])
 extractModuleAux syms onto = do
   let ontology_content = show $ printOWLBasicTheory onto 
    -- should be a string with the ontology from onto, maybe create a G_theory and pretty print it..., show theory
-  inFile <- lift $ getTempFile ontology_content "owl"
-  outFile <- lift $ getTempFile "" "owl"
-  let args = [inFile, "--extract-module", "-d"] 
+  inFile <- lift $ getTempFile ontology_content "in"
+  outFile <- lift $ getTempFile "" "out"
+  let args = trace (show syms) $ [inFile, "--extract-module", "-m STAR"] 
              ++ map show syms ++ ["-o", outFile]
-  (_code,_stdout,_stderr) <- lift $ executeProcess "owltools" args ""
+  (_code,_stdout,_stderr) <- trace (show args) $ lift $ executeProcess "owltools" args ""
   -- in outFile is the module, it needs to be parsed, see parseOWL in ParseOWLAsLibDefn.hs, convert a LIB_DEFN to a theory...
   (_imap,ontos) <- parseOWL False outFile
   -- do liftR for lifting something from Result to ResultT
   case ontos of
    [modOnto] -> do 
-     (_ontodoc, ExtSign sig _, sens) <- liftR $ basicOWL2Analysis (modOnto, emptySign, emptyGlobalAnnos) 
+     (_ontodoc, ExtSign sig _, sens) <- trace (show modOnto) $ liftR $ basicOWL2Analysis (modOnto, emptySign, emptyGlobalAnnos) 
      lift $ return (sig, sens)
    _ -> error "the module should be just one ontology"
 

From 4d550e24fed77ad27ee89b5bb53b8f14aa513e77 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Tue, 15 Mar 2016 13:20:30 +0100
Subject: [PATCH 13/16] removed the angle brackets from IRIs

---
 OWL2/ExtractModule.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index 89e2fa08a5..6c0003af26 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -51,7 +51,7 @@ extractModuleAux syms onto = do
   inFile <- lift $ getTempFile ontology_content "in"
   outFile <- lift $ getTempFile "" "out"
   let args = trace (show syms) $ [inFile, "--extract-module", "-m STAR"] 
-             ++ map show syms ++ ["-o", outFile]
+             ++ map (\x -> show $ x{IRI.hasAngles = False}) syms ++ ["-o", outFile]
   (_code,_stdout,_stderr) <- trace (show args) $ lift $ executeProcess "owltools" args ""
   -- in outFile is the module, it needs to be parsed, see parseOWL in ParseOWLAsLibDefn.hs, convert a LIB_DEFN to a theory...
   (_imap,ontos) <- parseOWL False outFile

From 38bd7dc141c475dd6d89917538047f8b9651309d Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Tue, 15 Mar 2016 13:23:44 +0100
Subject: [PATCH 14/16] two strings for m and star

---
 OWL2/ExtractModule.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index 6c0003af26..e0e2715b0e 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -50,7 +50,7 @@ extractModuleAux syms onto = do
    -- should be a string with the ontology from onto, maybe create a G_theory and pretty print it..., show theory
   inFile <- lift $ getTempFile ontology_content "in"
   outFile <- lift $ getTempFile "" "out"
-  let args = trace (show syms) $ [inFile, "--extract-module", "-m STAR"] 
+  let args = trace (show syms) $ [inFile, "--extract-module", "-m", "STAR"] 
              ++ map (\x -> show $ x{IRI.hasAngles = False}) syms ++ ["-o", outFile]
   (_code,_stdout,_stderr) <- trace (show args) $ lift $ executeProcess "owltools" args ""
   -- in outFile is the module, it needs to be parsed, see parseOWL in ParseOWLAsLibDefn.hs, convert a LIB_DEFN to a theory...

From 2d316f4c1c4783a514d6c70f84e3fecc98658674 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Tue, 15 Mar 2016 13:55:23 +0100
Subject: [PATCH 15/16] deleted tracing messages

---
 OWL2/ExtractModule.hs | 21 ++++++++-------------
 1 file changed, 8 insertions(+), 13 deletions(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index e0e2715b0e..dc74f1c59b 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -36,8 +36,6 @@ import System.IO.Unsafe
 
 import Common.ExtSign
 
-import Debug.Trace
-
 extractModule :: [IRI.IRI] -> (Sign, [Named Axiom])
                            -> Result (Sign, [Named Axiom])
 extractModule syms onto =
@@ -46,20 +44,17 @@ extractModule syms onto =
 extractModuleAux :: [IRI.IRI] -> (Sign, [Named Axiom])
                               -> ResultT IO (Sign, [Named Axiom])
 extractModuleAux syms onto = do
-  let ontology_content = show $ printOWLBasicTheory onto 
-   -- should be a string with the ontology from onto, maybe create a G_theory and pretty print it..., show theory
+  let ontology_content = show $ printOWLBasicTheory onto
   inFile <- lift $ getTempFile ontology_content "in"
   outFile <- lift $ getTempFile "" "out"
-  let args = trace (show syms) $ [inFile, "--extract-module", "-m", "STAR"] 
-             ++ map (\x -> show $ x{IRI.hasAngles = False}) syms ++ ["-o", outFile]
-  (_code,_stdout,_stderr) <- trace (show args) $ lift $ executeProcess "owltools" args ""
-  -- in outFile is the module, it needs to be parsed, see parseOWL in ParseOWLAsLibDefn.hs, convert a LIB_DEFN to a theory...
+  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
-  -- do liftR for lifting something from Result to ResultT
   case ontos of
-   [modOnto] -> do 
-     (_ontodoc, ExtSign sig _, sens) <- trace (show modOnto) $ liftR $ basicOWL2Analysis (modOnto, emptySign, emptyGlobalAnnos) 
+   [modOnto] -> do
+     (_ontodoc, ExtSign sig _, sens) <- liftR $
+         basicOWL2Analysis (modOnto, emptySign, emptyGlobalAnnos)
      lift $ return (sig, sens)
    _ -> error "the module should be just one ontology"
-
-

From d5b702e995509f5bca70434c3649a9bd75454d79 Mon Sep 17 00:00:00 2001
From: mcodescu <mscodescu@gmail.com>
Date: Tue, 15 Mar 2016 15:42:59 +0100
Subject: [PATCH 16/16] answer to code review

---
 OWL2/ExtractModule.hs        | 5 -----
 Static/AnalysisStructured.hs | 4 +++-
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/OWL2/ExtractModule.hs b/OWL2/ExtractModule.hs
index dc74f1c59b..c92fa9d3c8 100644
--- a/OWL2/ExtractModule.hs
+++ b/OWL2/ExtractModule.hs
@@ -13,16 +13,12 @@ OWL 2 module extraction
 
 module OWL2.ExtractModule where
 
---import OWL2.AS
 import OWL2.Sign
 import OWL2.MS
 import OWL2.ManchesterPrint
 import OWL2.ParseOWL
 import OWL2.StaticAnalysis
 
---import qualified Data.Set as Set
---import qualified Data.Map as Map
-
 import Common.Utils
 import Common.Result
 import Common.ResultT
@@ -30,7 +26,6 @@ import Common.AS_Annotation
 import Common.GlobalAnnotations
 import qualified Common.IRI as IRI
 
---import Control.Monad
 import Control.Monad.Trans
 import System.IO.Unsafe
 
diff --git a/Static/AnalysisStructured.hs b/Static/AnalysisStructured.hs
index 14be924d15..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 (ExtractOrRemove _ iris _) = 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