{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances #-}
{- |
Module      :  ./OWL2/DMU2OWL2.hs
Description :  translating DMU xml to OWL
Copyright   :  (c) Christian Maeder, DFKI and Uni Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

translating DMU xml to OWL using OntoDMU.jar by Marco Franke from BIBA
-}

module OWL2.DMU2OWL2 where

import Logic.Logic
import Logic.Comorphism

import Common.AS_Annotation
import Common.DefaultMorphism
import Common.ExtSign
import Common.GlobalAnnotations
import Common.ProofTree
import Common.Result
import Common.Utils
import Common.Lib.State

import qualified Data.Map as Map

import DMU.Logic_DMU

import OWL2.AS
import OWL2.Logic_OWL2
import OWL2.Morphism
import OWL2.Sign
import OWL2.StaticAnalysis
import OWL2.ProfilesAndSublogics
import OWL2.ParseMS
import OWL2.Symbols
import OWL2.Function
import OWL2.Extract

import Text.ParserCombinators.Parsec (eof, runParser)

import Control.Monad
import qualified Control.Monad.Fail as Fail

import System.Directory
import System.IO.Unsafe (unsafePerformIO)

-- | The identity of the comorphism
data DMU2OWL2 = DMU2OWL2 deriving Int -> DMU2OWL2 -> ShowS
[DMU2OWL2] -> ShowS
DMU2OWL2 -> String
(Int -> DMU2OWL2 -> ShowS)
-> (DMU2OWL2 -> String) -> ([DMU2OWL2] -> ShowS) -> Show DMU2OWL2
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DMU2OWL2] -> ShowS
$cshowList :: [DMU2OWL2] -> ShowS
show :: DMU2OWL2 -> String
$cshow :: DMU2OWL2 -> String
showsPrec :: Int -> DMU2OWL2 -> ShowS
$cshowsPrec :: Int -> DMU2OWL2 -> ShowS
Show

instance Language DMU2OWL2 -- default definition is okay

instance Comorphism DMU2OWL2
   DMU () Text () () () Text (DefaultMorphism Text) () () ()
   OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems
       Sign OWLMorphism Entity RawSymb ProofTree where
    sourceLogic :: DMU2OWL2 -> DMU
sourceLogic DMU2OWL2 = DMU
DMU
    sourceSublogic :: DMU2OWL2 -> ()
sourceSublogic DMU2OWL2 = ()
forall l. SemiLatticeWithTop l => l
top
    targetLogic :: DMU2OWL2 -> OWL2
targetLogic DMU2OWL2 = OWL2
OWL2
    mapSublogic :: DMU2OWL2 -> () -> Maybe ProfSub
mapSublogic DMU2OWL2 _ = ProfSub -> Maybe ProfSub
forall a. a -> Maybe a
Just ProfSub
forall l. SemiLatticeWithTop l => l
top
    map_theory :: DMU2OWL2 -> (Text, [Named ()]) -> Result (Sign, [Named Axiom])
map_theory DMU2OWL2 = (Text, [Named ()]) -> Result (Sign, [Named Axiom])
mapTheory
    map_morphism :: DMU2OWL2 -> DefaultMorphism Text -> Result OWLMorphism
map_morphism DMU2OWL2 _ = OWLMorphism -> Result OWLMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (OWLMorphism -> Result OWLMorphism)
-> OWLMorphism -> Result OWLMorphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> OWLMorphism
inclOWLMorphism Sign
emptySign Sign
emptySign
    has_model_expansion :: DMU2OWL2 -> Bool
has_model_expansion DMU2OWL2 = Bool
True
    is_weakly_amalgamable :: DMU2OWL2 -> Bool
is_weakly_amalgamable DMU2OWL2 = Bool
True
    isInclusionComorphism :: DMU2OWL2 -> Bool
isInclusionComorphism DMU2OWL2 = Bool
True

mapTheory :: (Text, [Named ()]) -> Result (Sign, [Named Axiom])
mapTheory :: (Text, [Named ()]) -> Result (Sign, [Named Axiom])
mapTheory = String -> Result (Sign, [Named Axiom])
forall (m :: * -> *).
MonadFail m =>
String -> m (Sign, [Named Axiom])
readOWL (String -> Result (Sign, [Named Axiom]))
-> ((Text, [Named ()]) -> String)
-> (Text, [Named ()])
-> Result (Sign, [Named Axiom])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO String -> String
forall a. IO a -> a
unsafePerformIO (IO String -> String)
-> ((Text, [Named ()]) -> IO String)
-> (Text, [Named ()])
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO String
runOntoDMU (String -> IO String)
-> ((Text, [Named ()]) -> String)
-> (Text, [Named ()])
-> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
fromText (Text -> String)
-> ((Text, [Named ()]) -> Text) -> (Text, [Named ()]) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, [Named ()]) -> Text
forall a b. (a, b) -> a
fst

runOntoDMU :: String -> IO String
runOntoDMU :: String -> IO String
runOntoDMU str :: String
str = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
str then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "" else do
  String
ontoDMUpath <- String -> String -> IO String
getEnvDef "HETS_ONTODMU" "DMU/OntoDMU.jar"
  String
tmpFile <- String -> String -> IO String
getTempFile String
str "ontoDMU.xml"
  (_, out :: String
out, _) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess "java"
    ["-jar", String
ontoDMUpath, "-f", String
tmpFile] ""
  String -> IO ()
removeFile String
tmpFile
  String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
out

readOWL :: Fail.MonadFail m => String -> m (Sign, [Named Axiom])
readOWL :: String -> m (Sign, [Named Axiom])
readOWL str :: String
str = case GenParser Char () OntologyDocument
-> () -> String -> String -> Either ParseError OntologyDocument
forall tok st a.
GenParser tok st a -> st -> String -> [tok] -> Either ParseError a
runParser ((OntologyDocument -> () -> OntologyDocument)
-> GenParser Char () OntologyDocument
-> ParsecT String () Identity ()
-> GenParser Char () OntologyDocument
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 OntologyDocument -> () -> OntologyDocument
forall a b. a -> b -> a
const (PrefixMap -> GenParser Char () OntologyDocument
forall st. PrefixMap -> CharParser st OntologyDocument
parseOntologyDocument PrefixMap
forall k a. Map k a
Map.empty) ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) () "" String
str of
  Left er :: ParseError
er -> String -> m (Sign, [Named Axiom])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (Sign, [Named Axiom]))
-> String -> m (Sign, [Named Axiom])
forall a b. (a -> b) -> a -> b
$ ParseError -> String
forall a. Show a => a -> String
show ParseError
er
  Right ontoFile :: OntologyDocument
ontoFile -> let
    newont :: OntologyDocument
newont = Action -> AMap -> OntologyDocument -> OntologyDocument
forall a. Function a => Action -> AMap -> a -> a
function Action
Expand (StringMap -> AMap
StringMap (StringMap -> AMap) -> StringMap -> AMap
forall a b. (a -> b) -> a -> b
$ PrefixMap -> StringMap
changePrefixMapTypeToString (PrefixMap -> StringMap) -> PrefixMap -> StringMap
forall a b. (a -> b) -> a -> b
$ OntologyDocument -> PrefixMap
prefixDeclaration OntologyDocument
ontoFile) OntologyDocument
ontoFile
    newstate :: Sign
newstate = State Sign () -> Sign -> Sign
forall s a. State s a -> s -> s
execState (OntologyDocument -> State Sign ()
extractSign OntologyDocument
newont) Sign
emptySign
    in case (OntologyDocument, Sign, GlobalAnnos)
-> Result (OntologyDocument, ExtSign Sign Entity, [Named Axiom])
basicOWL2Analysis
    (OntologyDocument
ontoFile, Sign
newstate, GlobalAnnos
emptyGlobalAnnos) of
    Result ds :: [Diagnosis]
ds ms :: Maybe (OntologyDocument, ExtSign Sign Entity, [Named Axiom])
ms -> case Maybe (OntologyDocument, ExtSign Sign Entity, [Named Axiom])
ms of
      Nothing -> String -> m (Sign, [Named Axiom])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (Sign, [Named Axiom]))
-> String -> m (Sign, [Named Axiom])
forall a b. (a -> b) -> a -> b
$ Int -> [Diagnosis] -> String
showRelDiags 1 [Diagnosis]
ds
      Just (_, ExtSign sig :: Sign
sig _, sens :: [Named Axiom]
sens) -> (Sign, [Named Axiom]) -> m (Sign, [Named Axiom])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sig, [Named Axiom]
sens)