{- |

Module : $Header$

Description : Comorphism from DL to CASL_DL

Copyright : (c) Dominik Luecke and Uni Bremen 2007

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : luecke@informatik.uni-bremen.de

Stability : experimental

Portability : non-portable (imports Logic.Logic)

The translating comorphism from DL to CASL_DL basically this is an

identity comorphism from SROIQ(D) to SROIQ(D)

-}

module Comorphisms.DL2CASL_DL

(

DL2CASL_DL(..)

)

where

import Logic.Logic

import Logic.Comorphism

import Common.AS_Annotation

import Common.Result

import Common.Id

import qualified Data.Set as Set

import qualified Data.Map as Map

-- DL

import DL.Logic_DL as LDL

import DL.AS as ADL

import qualified DL.Sign as SDL

--CASL_DL = codomain

import CASL_DL.Logic_CASL_DL

import CASL_DL.AS_CASL_DL

import CASL_DL.StatAna -- DLSign

import CASL.AS_Basic_CASL

import CASL.Sign

import CASL_DL.Sign

import CASL.Morphism

import qualified CASL_DL.PredefinedSign as PS

data DL2CASL_DL = DL2CASL_DL deriving (Show)

instance Language DL2CASL_DL

thing :: SORT

thing = PS.topSort

dataD :: SORT

dataD = PS.topSortD

instance Comorphism

DL2CASL_DL -- comorphism

DL -- lid domain

() -- sublogics domain

DLBasic -- Basic spec domain

DLBasicItem -- sentence domain

() -- symbol items domain

() -- symbol map items domain

SDL.Sign -- signature domain

SDL.DLMorphism -- morphism domain

SDL.DLSymbol -- symbol domain

SDL.RawDLSymbol -- rawsymbol domain

() -- proof tree codomain

CASL_DL -- lid codomain

() -- sublogics codomain

DL_BASIC_SPEC -- Basic spec codomain

DLFORMULA -- sentence codomain

SYMB_ITEMS -- symbol items codomain

SYMB_MAP_ITEMS -- symbol map items codomain

DLSign -- signature codomain

DLMor -- morphism codomain

Symbol -- symbol codomain

RawSymbol -- rawsymbol codomain

() -- proof tree domain

where

sourceLogic DL2CASL_DL = DL

sourceSublogic DL2CASL_DL = ()

targetLogic DL2CASL_DL = CASL_DL

mapSublogic DL2CASL_DL _ = Just ()

map_theory DL2CASL_DL = map_DL_theory

map_morphism DL2CASL_DL = error "map_morphism OWL2CASL_DL"

map_DL_theory :: (SDL.Sign, [Named DLBasicItem]) ->

Result (DLSign, [Named DLFORMULA])

map_DL_theory (sig, n_sens) =

do

osig <- mapt_sign sig

oforms <- mapM (map_named_basic_item sig) n_sens

return (osig, concat $ oforms)

isObjProp :: SDL.Sign -> Id -> Bool

isObjProp inSig pName =

let

inObjProps = Set.map (SDL.nameO) $ SDL.objectProps inSig

in

pName `Set.member` inObjProps

isDataProp :: SDL.Sign -> Id -> Bool

isDataProp inSig pName =

let

inDataProps = Set.map (SDL.nameD) $ SDL.dataProps inSig

in

pName `Set.member` inDataProps

-- Generation of a CASL_DL Signature

mapt_sign :: SDL.Sign -> Result DLSign

mapt_sign inSig =

let

inClasses = SDL.classes inSig

inDataProps = Set.map (SDL.nameD) $ SDL.dataProps inSig

inObjProps = Set.map (SDL.nameO) $ SDL.objectProps inSig

indis = Set.map (SDL.iid) $SDL.individuals inSig

oClasses = map (\x -> (x,

Set.fromList

[PredType

[thing]])) $ Set.toList $ inClasses

oObjs = map (\x -> (x,

Set.fromList

[PredType

[thing,thing]])) $ Set.toList $ inObjProps

oDtProps = map (\x -> (x,

Set.fromList

[PredType

[thing,dataD]])) $ Set.toList $ inDataProps

oIndis = map (\x -> (x,

Set.fromList

[OpType Total [] (thing)])) $ Set.toList $ indis

in

return ((emptySign emptyCASL_DLSign)

{

opMap = Map.fromList oIndis

, predMap = Map.fromList (oClasses ++ oObjs ++ oDtProps)

})

-- Preservation of the names

map_named_basic_item :: SDL.Sign -> Named DLBasicItem -> Result [Named DLFORMULA]

map_named_basic_item sign sens =

let

s = sentence sens

in

do

os <- map_basic_item sign s

return $ map (\x -> sens {sentence = x}) os

-- the top mapping function

map_basic_item :: SDL.Sign -> DLBasicItem -> Result [DLFORMULA]

map_basic_item sig sent =

case sent of

DLClass iid props _ _ ->

do

propsM <- mapM (map_class_property sig iid) props

return $ concat $ propsM

DLObjectProperty iid dc rc prel chars _ _ ->

do

opDom <- map_object_domain sig iid dc

opCod <- map_object_codomain sig iid rc

oPrel <- mapM (map_prel sig iid) prel

oChars <- mapM (map_chars sig iid) chars

return $ opDom ++ opCod ++ (concat oPrel) ++ oChars

DLDataProperty iid dc rc prel chars _ _ ->

do

dDom <- map_data_domain sig iid dc

dCod <- map_data_codomain sig iid rc

dPrel <- mapM (map_prel sig iid) prel

oChars <- case chars of

Nothing -> return $ []

Just c ->

do

y <- map_chars sig iid c

return $ [y]

return $ dDom ++ dCod ++ (concat dPrel) ++ oChars

DLIndividual iid tp fts irel _ _ ->

do

tps <- map_types sig iid tp

ofts <- mapM (map_facts sig iid) fts

orel <- mapM (map_irel sig iid) irel

return $ (tps ++ ofts ++ (concat orel))

DLMultiIndi _ _ _ _ _ rn -> fatal_error "Error during analysis, \

\ Multi-Individual was not \

\ expanded, bailing out." rn

map_irel :: SDL.Sign -> Id -> DLIndRel -> Result [DLFORMULA]

map_irel _ indi rel =

case rel of

DLSameAs ids rn -> mapM (\x -> return $ Strong_equation

(Application

(Qual_op_name indi (Op_type Total [] thing nullRange) nullRange)

[]

nullRange)

(Application

(Qual_op_name x (Op_type Total [] thing nullRange) nullRange)

[]

nullRange)

rn) ids

DLDifferentFrom ids rn -> mapM (\x -> return $ Negation

(Strong_equation

(Application

(Qual_op_name indi (Op_type Total [] thing nullRange) nullRange)

[]

nullRange)

(Application

(Qual_op_name x (Op_type Total [] thing nullRange) nullRange)

[]

nullRange)

nullRange)

rn) ids

-- translation of facts

map_facts :: SDL.Sign -> Id -> DLFacts -> Result DLFORMULA

map_facts _ indi fact =

case fact of

DLPosFact (prop, i2) rn -> return $ Predication

(Qual_pred_name prop (Pred_type [thing, thing] nullRange)

nullRange)

[Application

(Qual_op_name indi (Op_type Total [] thing nullRange) nullRange)

[]

nullRange,

Application

(Qual_op_name i2 (Op_type Total [] thing nullRange) nullRange)

[]

nullRange]

rn

DLNegFact (prop, i2) rn -> return $ Negation

(Predication

(Qual_pred_name prop (Pred_type [thing, thing] nullRange)

nullRange)

[Application

(Qual_op_name indi (Op_type Total [] thing nullRange) nullRange)

[]

nullRange,

Application

(Qual_op_name i2 (Op_type Total [] thing nullRange) nullRange)

[]

nullRange]

nullRange)

rn

map_types :: SDL.Sign -> Id -> Maybe DLType -> Result [DLFORMULA]

map_types _ iid mt =

case mt of

Nothing -> return $ []

Just t ->

case t of DLType cids rn ->

mapM (\x -> return $ Predication

(Qual_pred_name x (Pred_type [thing] nullRange) nullRange)

[Application

(Qual_op_name iid (Op_type Total [] thing nullRange) nullRange)

[]

nullRange]

rn) cids

-- mapping of characteristics

map_chars :: SDL.Sign ->

Id ->

DLChars ->

Result DLFORMULA

map_chars sig oid chs =

let

a = mkSimpleId "a"

b = mkSimpleId "b"

c = mkSimpleId "c"

in

if isObjProp sig oid

then

case chs of

DLFunctional ->

return $ Quantification Universal [Var_decl [a, b, c] thing nullRange]

(Implication

(Conjunction

[Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange,

Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var c thing nullRange]

nullRange]

nullRange)

(Strong_equation (Qual_var b thing nullRange)

(Qual_var c thing nullRange)

nullRange)

True

nullRange)

nullRange

DLInvFuntional ->

return $ Quantification Universal [Var_decl [a, b, c] thing nullRange]

(Implication

(Conjunction

[Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange,

Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var c thing nullRange, Qual_var b thing nullRange]

nullRange]

nullRange)

(Strong_equation (Qual_var a thing nullRange)

(Qual_var c thing nullRange)

nullRange)

True

nullRange)

nullRange

DLSymmetric ->

return $ Quantification Universal [Var_decl [a, b] thing nullRange]

(Implication

(Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange)

(Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var b thing nullRange, Qual_var a thing nullRange]

nullRange)

True

nullRange)

nullRange

DLTransitive ->

return $ Quantification Universal [Var_decl [a, b, c] thing nullRange]

(Implication

(Conjunction

[Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange,

Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var b thing nullRange, Qual_var c thing nullRange]

nullRange]

nullRange)

(Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var c thing nullRange]

nullRange)

True

nullRange)

nullRange

DLReflexive ->

return $ Quantification Universal [Var_decl [a] thing nullRange]

(Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var a thing nullRange]

nullRange)

nullRange

DLIrreflexive ->

return $ Quantification Universal [Var_decl [a] thing nullRange]

(Negation

(Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var a thing nullRange]

nullRange)

nullRange)

nullRange

else

fatal_error "handling of Data props nyi" nullRange

map_prel :: SDL.Sign ->

Id -> -- Id of the property

DLPropsRel ->

Result [DLFORMULA]

map_prel sig oid prel =

let

a = mkSimpleId "a"

b = mkSimpleId "b"

in

if isObjProp sig oid

then

case prel of

DLInverses ids rn ->

mapM (\x -> return $

Quantification Universal [Var_decl [a, b] thing nullRange]

(Equivalence

(Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange)

(Predication

(Qual_pred_name x (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var b thing nullRange, Qual_var a thing nullRange]

nullRange)

nullRange)

rn) ids

DLSubProperty ids rn ->

mapM (\x -> return $

Quantification Universal [Var_decl [a, b] thing nullRange]

(Implication

(Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange)

(Predication

(Qual_pred_name x (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange)

True

nullRange)

rn) ids

DLEquivalent ids rn ->

mapM (\x -> return $

Quantification Universal [Var_decl [a, b] thing nullRange]

(Equivalence

(Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange)

(Predication

(Qual_pred_name x (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange)

nullRange)

rn) ids

DLDisjoint ids rn ->

mapM (\x -> return $

Quantification Universal [Var_decl [a, b] thing nullRange]

(Negation

(Conjunction

[Predication

(Qual_pred_name oid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange,

Predication

(Qual_pred_name x (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange]

nullRange)

nullRange)

rn) ids

DLSuperProperty _ rn -> fatal_error "DLSuperProperty nyi" rn

else

error "handling of Data Props nyi"

map_object_domain :: SDL.Sign -> Id -> Maybe DLConcept -> Result [DLFORMULA]

map_object_domain sig iid mcons =

let

a = mkSimpleId "a"

b = mkSimpleId "b"

in

case mcons of

Nothing -> return []

Just cons ->

do

cs <- map_concept sig a cons

return $ [Quantification Universal [Var_decl [a] thing nullRange]

(Implication

(Quantification Existential [Var_decl [b] thing nullRange]

(Predication

(Qual_pred_name iid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange)

nullRange)

cs

True

nullRange)

nullRange]

map_data_codomain :: SDL.Sign -> Id -> Maybe DLConcept -> Result [DLFORMULA]

map_data_codomain sig iid mcons =

let

a = mkSimpleId "a"

b = mkSimpleId "b"

in

case mcons of

Nothing -> return []

Just cons ->

do

cs <- map_concept sig b cons

return $ [Quantification Universal [Var_decl [b] dataD nullRange]

(Implication

(Quantification Existential [Var_decl [a] thing nullRange]

(Predication

(Qual_pred_name iid (Pred_type [thing, dataD] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b dataD nullRange]

nullRange)

nullRange)

cs

True

nullRange)

nullRange]

map_object_codomain :: SDL.Sign -> Id -> Maybe DLConcept -> Result [DLFORMULA]

map_object_codomain sig iid mcons =

let

a = mkSimpleId "a"

b = mkSimpleId "b"

in

case mcons of

Nothing -> return []

Just cons ->

do

cs <- map_concept sig b cons

return $ [Quantification Universal [Var_decl [b] thing nullRange]

(Implication

(Quantification Existential [Var_decl [a] thing nullRange]

(Predication

(Qual_pred_name iid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b thing nullRange]

nullRange)

nullRange)

cs

True

nullRange)

nullRange]

map_data_domain :: SDL.Sign -> Id -> Maybe DLConcept -> Result [DLFORMULA]

map_data_domain sig iid mcons =

let

a = mkSimpleId "a"

b = mkSimpleId "b"

in

case mcons of

Nothing -> return []

Just cons ->

do

cs <- map_concept sig a cons

return $ [Quantification Universal [Var_decl [a] thing nullRange]

(Implication

(Quantification Existential [Var_decl [b] dataD nullRange]

(Predication

(Qual_pred_name iid (Pred_type [thing, dataD] nullRange) nullRange)

[Qual_var a thing nullRange, Qual_var b dataD nullRange]

nullRange)

nullRange)

cs

True

nullRange)

nullRange]

map_class_property :: SDL.Sign -> Id -> DLClassProperty -> Result [DLFORMULA]

map_class_property sig iid dcp =

let

a = mkSimpleId "a"

in

case dcp of

DLSubClassof con rn ->

mapM (\x ->

do

ct <- (map_concept sig a x)

return $ Quantification Universal [Var_decl [a] thing nullRange]

(Implication

(Predication

(Qual_pred_name iid (Pred_type [thing] nullRange) nullRange)

[Qual_var a thing nullRange]

nullRange)

ct

True

nullRange) rn) con

DLEquivalentTo con rn ->

mapM (\x ->

do

ct <- (map_concept sig a x)

return $ Quantification Universal [Var_decl [a] thing nullRange]

(Equivalence

(Predication

(Qual_pred_name iid (Pred_type [thing] nullRange) nullRange)

[Qual_var a thing nullRange]

nullRange)

ct

nullRange) rn) con

DLDisjointWith con rn ->

do

mapM (\x ->

do

ct <- (map_concept sig a x)

return $ Quantification Universal [Var_decl [a] thing nullRange]

(Negation

(Conjunction

[Predication

(Qual_pred_name iid (Pred_type [thing] nullRange) nullRange)

[Qual_var a thing nullRange]

nullRange,

ct]

nullRange)

nullRange)

rn) con

map_concept :: SDL.Sign -> Token -> DLConcept -> Result DLFORMULA

map_concept sign iid con =

let

a = mkSimpleId "a"

b = mkSimpleId "b"

in

case con of

DLAnd c1 c2 rn ->

do

c1t <- map_concept sign iid c1

c2t <- map_concept sign iid c2

return $ Conjunction [c1t,c2t] rn

DLOr c1 c2 rn ->

do

c1t <- map_concept sign iid c1

c2t <- map_concept sign iid c2

return $ Disjunction [c1t,c2t] rn

DLXor c1 c2 rn ->

do

c1t <- map_concept sign iid c1

c2t <- map_concept sign iid c2

return $ Conjunction

[Disjunction [c1t,c2t] nullRange,

Negation (Conjunction [c1t,c2t] nullRange)

nullRange]

rn

DLNot c1 rn ->

do

c1t <- map_concept sign iid c1

return $ Negation c1t rn

DLClassId c1 rn ->

do

return $ Predication

(Qual_pred_name c1 (Pred_type [thing] nullRange) nullRange)

[Qual_var iid thing nullRange]

rn

DLOneOf _ rn -> fatal_error "oneOf nyi" rn

DLSome rid conc rn ->

do

ct <- map_concept sign iid conc

return $ Quantification Existential [Var_decl [b] thing nullRange]

(Conjunction

[Predication

(Qual_pred_name rid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var iid thing nullRange, Qual_var b thing nullRange]

nullRange,

ct]

nullRange)

rn

DLHas rid indi rn ->

if isDataProp sign rid

then

fatal_error "handling of data props nyi" rn

else

return $ Predication

(Qual_pred_name rid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var iid thing nullRange, Qual_var (restoreToken indi) thing nullRange]

rn

DLValue rid indi rn ->

if isDataProp sign rid

then

fatal_error "handling of data props nyi" rn

else

return $ Predication

(Qual_pred_name rid (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var iid thing nullRange, Qual_var (restoreToken indi) thing nullRange]

rn

DLOnlysome rel cons rn -> map_concept sign iid $ expand (DLOnlysome rel cons rn)

DLOnly rel cons rn ->

if isDataProp sign rel

then

fatal_error "Data props are not supported in only concept" rn

else

do

ct <- map_concept sign b cons

return $ Quantification Universal [Var_decl [b] thing nullRange]

(Implication

(Predication

(Qual_pred_name rel (Pred_type [thing, thing] nullRange) nullRange)

[Qual_var iid thing nullRange,

Qual_var b thing nullRange]

nullRange)

ct

True

nullRange)

rn

DLMin rid num mcons rn ->

if isDataProp sign rid

then

fatal_error "handling of data props nyi" rn

else

do

ocons <- case mcons of

Nothing -> return $ Nothing

Just x ->

do

o <- map_concept sign a x

return $ Just o

return $

Quantification Universal [Var_decl [a] thing nullRange]

(ExtFORMULA

(

Cardinality CMin

(Qual_pred_name rid (Pred_type [thing, thing] nullRange) nullRange)

(Qual_var a thing nullRange)

(makeCASLNumber num)

ocons

rn

)) rn

DLMax rid num mcons rn ->

if isDataProp sign rid

then

fatal_error "handling of data props nyi" rn

else

do

ocons <- case mcons of

Nothing -> return $ Nothing

Just x ->

do

o <- map_concept sign a x

return $ Just o

return $

Quantification Universal [Var_decl [a] thing nullRange]

(ExtFORMULA

(

Cardinality CMax

(Qual_pred_name rid (Pred_type [thing, thing] nullRange) nullRange)

(Qual_var a thing nullRange)

(makeCASLNumber num)

ocons

rn

)) rn

DLExactly rid num mcons rn ->

if isDataProp sign rid

then

fatal_error "handling of data props nyi" rn

else

do

ocons <- case mcons of

Nothing -> return $ Nothing

Just x ->

do

o <- map_concept sign a x

return $ Just o

return $

Quantification Universal [Var_decl [a] thing nullRange]

(ExtFORMULA

(

Cardinality CExact

(Qual_pred_name rid (Pred_type [thing, thing] nullRange) nullRange)

(Qual_var a thing nullRange)

(makeCASLNumber num)

ocons

rn

)) rn

DLSelf _ -> fatal_error "nyi" nullRange

makeCASLNumber :: Int -> TERM DL_FORMULA

makeCASLNumber num = (Simple_id $ mkSimpleId $ show num) -- placeholder

restoreToken :: Id -> Token

restoreToken = head . getTokens