1060N/A{- |

1060N/AModule : $Header$

1060N/ADescription : Comorphism from OWL 1.1 to DL

1060N/ACopyright : (c) Uni Bremen 2007

1060N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt

1060N/A

1060N/AMaintainer : luecke@informatik.uni-bremen.de

1060N/AStability : provisional

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

1060N/A

1060N/Aa not yet implemented comorphism

1060N/A-}

1060N/A

1060N/Amodule Comorphisms.OWL2DL where

1060N/A

1060N/Aimport Logic.Logic

1060N/Aimport Logic.Comorphism

1060N/A

1060N/A--OWL = domain

1060N/Aimport OWL.Logic_OWL

1060N/Aimport OWL.AS

1060N/Aimport OWL.Sign as OWL

1060N/A

1060N/A--DL = codomain

1060N/Aimport DL.Logic_DL

4495N/Aimport DL.AS

5636N/Aimport DL.Sign as DL

1060N/A

1060N/Aimport Common.AS_Annotation

1060N/Aimport Common.DocUtils

3831N/Aimport Common.Id

3831N/Aimport Common.ProofTree

3831N/Aimport Common.Result

3831N/A

3831N/Aimport qualified Data.Set as Set

3831N/A

3831N/Adata OWL2DL = OWL2DL deriving Show

3831N/A

3831N/Ainstance Language OWL2DL

3842N/A

3831N/Ainstance Comorphism

3842N/A OWL2DL -- comorphism

3831N/A OWL -- lid domain

3831N/A () -- sublogics domain

3831N/A OntologyFile -- Basic spec domain

3831N/A Sentence -- sentence domain

3831N/A () -- symbol items domain

3831N/A () -- symbol map items domain

3842N/A OWL.Sign -- signature domain

3842N/A OWL_Morphism -- morphism domain

3831N/A () -- symbol domain

3842N/A () -- rawsymbol domain

3831N/A ProofTree -- proof tree codomain

5636N/A DL -- lid codomain

2976N/A () -- Sublogics

3831N/A DLBasic -- basic_spec

1060N/A DLBasicItem -- sentence

() -- symb_items

() -- symb_map_items

DL.Sign -- sign

DLMorphism -- morphism

DLSymbol -- symbol

RawDLSymbol -- raw_symbol

() -- proof_tree

where

sourceLogic OWL2DL = OWL

sourceSublogic OWL2DL = ()

targetLogic OWL2DL = DL

mapSublogic OWL2DL _ = Just ()

map_theory OWL2DL = mapTheory

map_morphism = mapDefaultMorphism

qNameToId :: QName -> Id

qNameToId = stringToId . localPart

mapTheory :: (OWL.Sign, [Named Sentence])

-> Result (DL.Sign, [Named DLBasicItem])

mapTheory (osign, sens) = do

let

cs = Set.map qNameToId $ concepts osign

ps = Set.map qNameToId $ datatypes osign

ds = Set.map (QualDataProp . qNameToId) $ dataValuedRoles osign

os = Set.map (QualObjProp . qNameToId) $ indValuedRoles osign

is = Set.map (flip QualIndiv [] . qNameToId) $ OWL.individuals osign

ns <- mapM (mapNamedM mapSenM) sens

return (emptyDLSig

{ classes = Set.union cs $ classes emptyDLSig

, pData = Set.union ps $ pData emptyDLSig

, dataProps = ds

, objectProps = Set.union os $ objectProps emptyDLSig

, DL.individuals = is}, ns)

getAxiom :: Sentence -> Axiom

getAxiom s = case s of

OWLAxiom a -> a

OWLFact a -> a

toDLJunction :: JunctionType -> DLConcept -> DLConcept -> Range -> DLConcept

toDLJunction ty = case ty of

UnionOf -> DLOr

IntersectionOf -> DLAnd

toConcept :: Description -> Result DLConcept

toConcept des = let err = fail $ "OWL2DL.toConcept " ++ showDoc des "" in

case des of

OWLClass curi -> return $ DLClassId (qNameToId curi) nullRange

ObjectJunction ty ds | not $ null ds -> do

cs <- mapM toConcept ds

return $ foldr1 (\ c1 c2 -> toDLJunction ty c1 c2 nullRange) cs

ObjectComplementOf d -> do

c <- toConcept d

return $ DLNot c nullRange

ObjectOneOf is -> return $ DLOneOf (map qNameToId is) nullRange

_ -> err

{-

ObjectAllValuesFrom ope d

ObjectSomeValuesFrom ope d

ObjectExistsSelf ope

ObjectHasValue ope i

ObjectMinCardinality c ope md

ObjectMaxCardinality c ope md

ObjectExactCardinality c ope md

DataAllValuesFrom dpe dpes dr

DataSomeValuesFrom dpe dpes dr

DataHasValue dpe con

DataMinCardinality c dpe mdr

DataMaxCardinality c dpe mdr

DataExactCardinality c dpe mdr

-}

mapSenM :: Sentence -> Result DLBasicItem

mapSenM sen = let err = fail $ "OWL2DL.mapSenM " ++ showDoc sen "" in

case getAxiom sen of

PlainAxiom _ paxiom -> case paxiom of

SubClassOf sub super -> case sub of

OWLClass curi -> do

c <- toConcept super

return $ DLClass (qNameToId curi)

[DLSubClassof [c] nullRange] Nothing nullRange

_ -> err

EquivOrDisjointClasses ty (cl : cs) -> case cl of

OWLClass curi -> do

es <- mapM toConcept cs

return $ DLClass (qNameToId curi)

[(case ty of

Equivalent -> DLEquivalentTo

Disjoint -> DLDisjointWith) es nullRange] Nothing nullRange

_ -> err

_ -> err

_ -> err

{-

DisjointUnion _as OwlClassURI ds ->

SubObjectPropertyOf _as subOpe ope ->

EquivalentObjectProperties _as opes ->

DisjointObjectProperties _as opes ->

ObjectPropertyDomain _as ope d ->

ObjectPropertyRange _as ope d ->

InverseObjectProperties _as ope ope ->

FunctionalObjectProperty _as ope ->

InverseFunctionalObjectProperty _as ope ->

ReflexiveObjectProperty _as ope ->

IrreflexiveObjectProperty _as ope ->

SymmetricObjectProperty _as ope ->

AntisymmetricObjectProperty _as ope ->

TransitiveObjectProperty _as ope ->

-- DataPropertyAxiom

SubDataPropertyOf _as dpe dpe ->

EquivalentDataProperties _as dpes ->

DisjointDataProperties _as dpes ->

DataPropertyDomain _as dpe d ->

DataPropertyRange _as dpe dr ->

FunctionalDataProperty _as dpe ->

-- Fact

SameIndividual _as is ->

DifferentIndividuals _as is ->

ClassAssertion _as i d ->

ObjectPropertyAssertion _as ope si ti ->

NegativeObjectPropertyAssertion _as ope si ti ->

DataPropertyAssertion _as dpe si tv ->

NegativeDataPropertyAssertion _as dpe si tv ->

Declaration _as e ->

EntityAnno ea ->

-}