{- |
Module      :  ./OWL2/ParseOWLAsLibDefn.hs
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.ParseOWLAsLibDefn (parseOWLAsLibDefn) where

import OWL2.AS

import Data.Maybe
import qualified Data.Map as Map

import Common.Id
import Common.IRI
import Common.LibName
import Common.ResultT
import Common.AS_Annotation
import Common.Utils

import Logic.Grothendieck

import OWL2.Logic_OWL2
import OWL2.ParseOWL

import Syntax.AS_Library
import Syntax.AS_Structured

-- | call for owl parser (env. variable $HETS_OWL_TOOLS muss be defined)
parseOWLAsLibDefn :: Bool                  -- ^ Sets Option.quick
         -> FilePath              -- ^ local filepath or uri
         -> ResultT IO [LIB_DEFN] -- ^ map: uri -> OntologyFile
parseOWLAsLibDefn :: Bool -> FilePath -> ResultT IO [LIB_DEFN]
parseOWLAsLibDefn quick :: Bool
quick fn :: FilePath
fn = do
   (imap :: Map FilePath FilePath
imap, ontodocs :: [OntologyDocument]
ontodocs) <- Bool
-> FilePath
-> ResultT IO (Map FilePath FilePath, [OntologyDocument])
parseOWL Bool
quick FilePath
fn
   [LIB_DEFN] -> ResultT IO [LIB_DEFN]
forall (m :: * -> *) a. Monad m => a -> m a
return ([LIB_DEFN] -> ResultT IO [LIB_DEFN])
-> [LIB_DEFN] -> ResultT IO [LIB_DEFN]
forall a b. (a -> b) -> a -> b
$ (OntologyDocument -> LIB_DEFN) -> [OntologyDocument] -> [LIB_DEFN]
forall a b. (a -> b) -> [a] -> [b]
map (Map FilePath FilePath -> OntologyDocument -> LIB_DEFN
convertToLibDefN Map FilePath FilePath
imap) [OntologyDocument]
ontodocs

createSpec :: OntologyDocument -> [SPEC_NAME] -> Annoted SPEC
createSpec :: OntologyDocument -> [SPEC_NAME] -> Annoted SPEC
createSpec o :: OntologyDocument
o imps :: [SPEC_NAME]
imps = [SPEC_NAME] -> Annoted SPEC -> Annoted SPEC
addImports [SPEC_NAME]
imps (Annoted SPEC -> Annoted SPEC)
-> (G_basic_spec -> Annoted SPEC) -> G_basic_spec -> Annoted SPEC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_basic_spec -> Annoted SPEC
makeSpec (G_basic_spec -> Annoted SPEC) -> G_basic_spec -> Annoted SPEC
forall a b. (a -> b) -> a -> b
$ OWL2 -> OntologyDocument -> G_basic_spec
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> basic_spec -> G_basic_spec
G_basic_spec OWL2
OWL2 OntologyDocument
o

convertone :: OntologyDocument -> SPEC_NAME -> [SPEC_NAME] -> Annoted LIB_ITEM
convertone :: OntologyDocument -> SPEC_NAME -> [SPEC_NAME] -> Annoted LIB_ITEM
convertone o :: OntologyDocument
o oname :: SPEC_NAME
oname i :: [SPEC_NAME]
i = SPEC_NAME -> Annoted SPEC -> Annoted LIB_ITEM
makeSpecItem SPEC_NAME
oname (Annoted SPEC -> Annoted LIB_ITEM)
-> Annoted SPEC -> Annoted LIB_ITEM
forall a b. (a -> b) -> a -> b
$ OntologyDocument -> [SPEC_NAME] -> Annoted SPEC
createSpec OntologyDocument
o [SPEC_NAME]
i

convertToLibDefN :: Map.Map String String -> OntologyDocument -> LIB_DEFN
convertToLibDefN :: Map FilePath FilePath -> OntologyDocument -> LIB_DEFN
convertToLibDefN imap :: Map FilePath FilePath
imap o :: OntologyDocument
o = LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn LibName
ln
    (OWL2 -> Annoted LIB_ITEM
forall lid. Language lid => lid -> Annoted LIB_ITEM
makeLogicItem OWL2
OWL2 Annoted LIB_ITEM -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. a -> [a] -> [a]
: [Annoted LIB_ITEM]
imp_libs [Annoted LIB_ITEM] -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. [a] -> [a] -> [a]
++ [OntologyDocument -> SPEC_NAME -> [SPEC_NAME] -> Annoted LIB_ITEM
convertone OntologyDocument
o SPEC_NAME
oname [SPEC_NAME]
imps2]) Range
nullRange []
  where ont :: Ontology
ont = OntologyDocument -> Ontology
ontology OntologyDocument
o
        il :: [(FilePath, FilePath)]
il = Map FilePath FilePath -> [(FilePath, FilePath)]
forall k a. Map k a -> [(k, a)]
Map.toList Map FilePath FilePath
imap
        is :: [FilePath]
is = ((FilePath, FilePath) -> FilePath)
-> [(FilePath, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath, FilePath) -> FilePath
forall a b. (a, b) -> b
snd [(FilePath, FilePath)]
il
        ln :: LibName
ln = case FilePath -> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup FilePath
libstr ([(FilePath, FilePath)] -> Maybe FilePath)
-> [(FilePath, FilePath)] -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ ((FilePath, FilePath) -> (FilePath, FilePath))
-> [(FilePath, FilePath)] -> [(FilePath, FilePath)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: FilePath
a, b :: FilePath
b) -> (FilePath
b, FilePath
a)) [(FilePath, FilePath)]
il of
            Just s :: FilePath
s -> FilePath -> LibName -> LibName
setFilePath (FilePath -> LibName -> LibName) -> FilePath -> LibName -> LibName
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath
tryToStripPrefix "file:" FilePath
s
            Nothing -> FilePath -> LibName -> LibName
setFilePath FilePath
libstr
          (LibName -> LibName) -> LibName -> LibName
forall a b. (a -> b) -> a -> b
$ SPEC_NAME -> LibName
iriLibName SPEC_NAME
oname
        imps :: [SPEC_NAME]
imps = Ontology -> [SPEC_NAME]
importsDocuments Ontology
ont
        imps2 :: [SPEC_NAME]
imps2 = (SPEC_NAME -> Bool) -> [SPEC_NAME] -> [SPEC_NAME]
forall a. (a -> Bool) -> [a] -> [a]
filter ((FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
is) (FilePath -> Bool) -> (SPEC_NAME -> FilePath) -> SPEC_NAME -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPEC_NAME -> FilePath
forall a. Show a => a -> FilePath
show (SPEC_NAME -> FilePath)
-> (SPEC_NAME -> SPEC_NAME) -> SPEC_NAME -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SPEC_NAME -> SPEC_NAME
setAngles Bool
False) [SPEC_NAME]
imps
        oname :: SPEC_NAME
oname = SPEC_NAME -> Maybe SPEC_NAME -> SPEC_NAME
forall a. a -> Maybe a -> a
fromMaybe SPEC_NAME
nullIRI (Maybe SPEC_NAME -> SPEC_NAME) -> Maybe SPEC_NAME -> SPEC_NAME
forall a b. (a -> b) -> a -> b
$ Ontology -> Maybe SPEC_NAME
mOntologyIRI Ontology
ont
        libstr :: FilePath
libstr = SPEC_NAME -> FilePath
forall a. Show a => a -> FilePath
show (SPEC_NAME -> FilePath) -> SPEC_NAME -> FilePath
forall a b. (a -> b) -> a -> b
$ Bool -> SPEC_NAME -> SPEC_NAME
setAngles Bool
False SPEC_NAME
oname
        imp_libs :: [Annoted LIB_ITEM]
imp_libs = (SPEC_NAME -> Annoted LIB_ITEM)
-> [SPEC_NAME] -> [Annoted LIB_ITEM]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> SPEC_NAME -> Annoted LIB_ITEM
addDownload Bool
False) [SPEC_NAME]
imps2