4033N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

0N/A{- |

0N/AModule : $Header$

0N/ADescription : Comorphism from CASL to OWL2

0N/ACopyright : (c) C. Maeder, DFKI GmbH 2012

0N/ALicense : GPLv2 or higher, see LICENSE.txt

0N/A

0N/AMaintainer : Christian.Maeder@dfki.de

0N/AStability : provisional

0N/APortability : non-portable (via Logic.Logic)

0N/A-}

0N/A

0N/Amodule OWL2.CASL2OWL where

0N/A

0N/Aimport Logic.Logic as Logic

0N/Aimport Logic.Comorphism

0N/A

2362N/Aimport Common.AS_Annotation

2362N/Aimport Common.DocUtils

2362N/Aimport Common.Result

1178N/Aimport Common.Id

4169N/Aimport Common.ProofTree

0N/Aimport Common.ProofUtils

0N/Aimport qualified Common.Lib.MapSet as MapSet

4033N/A

4033N/Aimport Data.Char

0N/Aimport qualified Data.Set as Set

1178N/Aimport qualified Data.Map as Map

1178N/Aimport Data.List

1178N/A

4033N/A-- OWL = codomain

1178N/Aimport OWL2.Logic_OWL2

1178N/Aimport OWL2.MS

4033N/Aimport OWL2.AS

1178N/Aimport OWL2.ProfilesAndSublogics

1178N/Aimport OWL2.ManchesterPrint ()

4033N/Aimport OWL2.Morphism

1178N/Aimport OWL2.Symbols

1178N/Aimport OWL2.Sign as OS

4033N/A

1178N/A-- CASL = domain

1178N/Aimport CASL.Logic_CASL

4033N/Aimport CASL.AS_Basic_CASL

1178N/Aimport CASL.Disambiguate

1178N/Aimport CASL.Sign as CS

4033N/Aimport qualified CASL.MapSentence as MapSen

1178N/Aimport CASL.Morphism

1178N/Aimport CASL.SimplifySen

4033N/Aimport CASL.Sublogic

1178N/Aimport CASL.ToDoc

1178N/Aimport CASL.Overload

1178N/A

4033N/Adata CASL2OWL = CASL2OWL deriving Show

0N/A

0N/Ainstance Language CASL2OWL

0N/A

0N/Ainstance Comorphism

0N/A CASL2OWL -- comorphism

0N/A CASL -- lid domain

0N/A CASL_Sublogics -- sublogics domain

0N/A CASLBasicSpec -- Basic spec domain

0N/A CASLFORMULA -- sentence domain

4033N/A SYMB_ITEMS -- symbol items domain

0N/A SYMB_MAP_ITEMS -- symbol map items domain

1178N/A CASLSign -- signature domain

0N/A CASLMor -- morphism domain

0N/A Symbol -- symbol domain

4033N/A RawSymbol -- rawsymbol domain

0N/A ProofTree -- proof tree domain

0N/A OWL2 -- lid codomain

4033N/A ProfSub -- sublogics codomain

1178N/A OntologyDocument -- Basic spec codomain

1178N/A Axiom -- sentence codomain

0N/A SymbItems -- symbol items codomain

4033N/A SymbMapItems -- symbol map items codomain

0N/A OS.Sign -- signature codomain

0N/A OWLMorphism -- morphism codomain

4033N/A Entity -- symbol codomain

0N/A RawSymb -- rawsymbol codomain

0N/A ProofTree -- proof tree codomain

4033N/A where

0N/A sourceLogic CASL2OWL = CASL

4033N/A sourceSublogic CASL2OWL = caslTop

0N/A { sub_features = LocFilSub }

1178N/A targetLogic CASL2OWL = OWL2

0N/A mapSublogic CASL2OWL _ = Just topS

0N/A map_theory CASL2OWL = mapTheory

4033N/A map_morphism CASL2OWL = mapMorphism

0N/A map_symbol CASL2OWL _ = mapSymbol

0N/A has_model_expansion CASL2OWL = True

4033N/A

0N/A-- | Mapping of CASL morphisms

0N/AmapMorphism :: Morphism f e m -> Result OWLMorphism

4033N/AmapMorphism _ = fail "CASL2OWL.mapMorphism"

0N/A

0N/AmapSymbol :: Symbol -> Set.Set Entity

4033N/AmapSymbol _ = Set.empty

0N/A

0N/A{- names must be disambiguated as is done in CASL.Qualify or SuleCFOL2SoftFOL.

4033N/A Ops or preds in the overload relation denote the same objectProperty!

0N/A-}

0N/AidToIRI :: Id -> QName

4033N/AidToIRI = idToAnonIRI False

0N/A

0N/AidToAnonIRI :: Bool -> Id -> QName

4033N/AidToAnonIRI b i = nullQName

0N/A { localPart = (if b then ('_' :) else id) . transString $ show i

0N/A , iriPos = rangeOfId i }

4033N/A

0N/AmapSign :: CS.Sign f e -> Result (OS.Sign, [Named Axiom])

0N/AmapSign csig = let

4033N/A esorts = emptySortSet csig

0N/A (eqs, subss) = eqAndSubsorts False $ sortRel csig

0N/A ss = sortSet csig

4033N/A nsorts = Set.difference ss esorts

0N/A mkMisc ed l = PlainAxiom (Misc []) $ ListFrameBit (Just $ EDRelation ed)

0N/A $ ExpressionBit $ map toACE l

4033N/A disjSorts s = if Set.size s <= 1 then [] else

0N/A let (m, r) = Set.deleteFindMin s

0N/A in concatMap (\ t -> case t of

4033N/A _ | haveCommonSubsorts csig t m

1178N/A || haveCommonSupersorts True csig t m -> []

1178N/A | otherwise -> [makeNamed ("disjoint " ++ show m ++ " and " ++ show t)

0N/A $ mkMisc Disjoint [m, t]]

4033N/A ) (Set.toList r) ++ disjSorts r

0N/A eqSorts = map (\ es -> makeNamed ("equal sorts " ++ show es)

0N/A $ mkMisc Equivalent es) eqs

4033N/A subSens = map (\ (s, ts) -> makeNamed

0N/A ("subsort " ++ show s ++ " of " ++ show ts) $ toSC s ts) subss

4033N/A nonEmptySens = map (\ s -> mkIndi True s [s]) $ Set.toList nsorts

0N/A sortSens = eqSorts ++ disjSorts ss ++ subSens ++ nonEmptySens

4033N/A mkIndi b i ts = makeNamed

4033N/A ("individual " ++ show i ++ " of class " ++ showDoc ts "")

0N/A $ PlainAxiom (SimpleEntity $ Entity NamedIndividual

0N/A $ idToAnonIRI b i)

0N/A $ ListFrameBit (Just Types) $ ExpressionBit

0N/A $ map toACE ts

1178N/A om = opMap csig

0N/A keepMaxs = keepMinimals1 False csig id

1178N/A mk s i m = makeNamed (s ++ show i ++ m) . PlainAxiom

0N/A (ObjectEntity $ ObjectProp $ idToIRI i)

0N/A toC = Expression . idToIRI

0N/A toSC i = PlainAxiom (ClassEntity $ toC i) . ListFrameBit (Just SubClass)

0N/A . ExpressionBit . map toACE

0N/A toACE i = ([], toC i)

4033N/A toEBit i = ExpressionBit [toACE i]

4033N/A mkDR dr = ListFrameBit (Just $ DRRelation dr) . toEBit

0N/A toIris = Set.map idToIRI

0N/A (cs, ncs) = MapSet.partition (null . opArgs) om

0N/A (sos, os) = MapSet.partition isSingleArgOp ncs

0N/A (sps, rps) = MapSet.partition (isSingle . predArgs) pm

1178N/A (bps, ps) = MapSet.partition isBinPredType rps

0N/A pm = predMap csig

0N/A osig = OS.emptySign

0N/A { concepts = toIris $ Set.unions [ ss, MapSet.keysSet sps ]

0N/A , objectProperties = toIris $ Set.union (MapSet.keysSet sos)

0N/A $ MapSet.keysSet bps

4033N/A , individuals = toIris $ MapSet.keysSet cs

4033N/A }

0N/A mkHint b i s = hint () ("not translated" ++ (if b then " op " else " pred ")

0N/A ++ shows i (if b then " :" else " : ") ++ showDoc s "") $ posOfId i

0N/A in do

0N/A s1 <- Map.foldWithKey (\ i s ml -> do

1178N/A l <- ml

0N/A return $ mkIndi False i

4033N/A (keepMinimals csig id $ map opRes $ Set.toList s) : l)

4033N/A (return sortSens) (MapSet.toMap cs)

4033N/A s2 <- Map.foldWithKey (\ i s ml -> do

0N/A l <- ml

4033N/A let sl = Set.toList s

0N/A mki = mk "plain function " i

4033N/A case (keepMaxs $ concatMap opArgs sl, keepMaxs $ map opRes sl) of

0N/A ([a], [r]) -> return

4033N/A $ [ mki " character" $ ListFrameBit Nothing

4033N/A $ ObjectCharacteristics [([], Functional)]

4033N/A , mki " domain" $ mkDR ADomain a, mki " range" $ mkDR ARange r]

0N/A ++ l

4033N/A (as, rs) -> fail $ "CASL2OWL.mapSign2: " ++ show i ++ " args: "

0N/A ++ show as ++ " resulttypes: " ++ show rs)

4033N/A (return s1) (MapSet.toMap sos)

4033N/A s3 <- Map.foldWithKey (\ i s ml -> do

4033N/A l <- ml

0N/A let mkp = mk "binary predicate " i

1178N/A case map keepMaxs . transpose . map predArgs $ Set.toList s of

0N/A [[a], [r]] -> return

0N/A $ [mkp " domain" $ mkDR ADomain a, mkp " range" $ mkDR ARange r]

0N/A ++ l

0N/A ts -> fail $ "CASL2OWL.mapSign3: " ++ show i ++ " types: " ++ show ts)

0N/A (return s2) (MapSet.toMap bps)

4033N/A s4 <- Map.foldWithKey (\ i s ml ->

4033N/A case keepMaxs $ concatMap predArgs $ Set.toList s of

0N/A [r] -> do

0N/A l <- ml

0N/A return $ makeNamed ("plain predicate " ++ show i) (toSC r [i]) : l

0N/A ts -> fail $ "CASL2OWL.mapSign4: " ++ show i ++ " types: " ++ show ts)

1178N/A (return s3) (MapSet.toMap sps)

0N/A MapSet.foldWithKey (\ i s m -> m >> mkHint True i s) (return ()) os

0N/A MapSet.foldWithKey (\ i s m -> m >> mkHint False i s) (return ()) ps

0N/A return (osig, s4)

0N/A

0N/A{- binary predicates and single argument functions should become

4033N/A objectProperties.

4033N/A Serge also turned constructors into concepts.

1178N/A How to treat multi-argument predicates and functions?

1178N/A Maybe create tuple concepts?

4033N/A-}

1178N/A

0N/AmapTheory :: (FormExtension f, TermExtension f)

=> (CS.Sign f e, [Named (FORMULA f)]) -> Result (OS.Sign, [Named Axiom])

mapTheory (sig, sens) = do

let mor = disambigSig sig

tar = mtarget mor

ns = map (mapNamed $ MapSen.mapMorphForm (const id) mor) sens

mapM_ (flip (hint ()) nullRange

. ("not translated\n" ++) . show . printTheoryFormula

. mapNamed (simplifySen (const return) (const id) tar)) ns

mapSign tar

-- | translate to a valid OWL string

transString :: String -> String

transString str = let

x = 'X'

replaceChar1 d | d == x = [x, x] -- code out existing x!

| isAlphaNum d = [d]

| otherwise = x : replaceChar d

in case str of

"" -> [x]

c : s -> let l = replaceChar1 c in

(if isDigit c then [x, c]

else l) ++ concatMap replaceChar1 s

-- | injective replacement of special characters

replaceChar :: Char -> String

-- <http://www.htmlhelp.com/reference/charset/>

replaceChar c = if isAlphaNum c then [c] else lookupCharMap c