OWL2CASL.hs revision e7ddd5495421698701a2bbc57a5b3390a11d12ca
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
{- |
Module : $Header$
Description : Comorphism from OWL 1.1 to CASL_Dl
Copyright : (c) Uni Bremen 2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : provisional
Portability : non-portable (via Logic.Logic)
a not yet implemented comorphism
-}
module Comorphisms.OWL2CASL (OWL2CASL (..)) where
import Logic.Logic as Logic
import Logic.Comorphism
import Common.AS_Annotation
import Common.Result
import Common.Id
import Common.ProofTree
import qualified Common.Lib.MapSet as MapSet
import Control.Monad
import Data.Char
import qualified Data.Set as Set
import qualified Data.Map as Map
-- OWL = domain
import OWL.Logic_OWL
import OWL.AS
import OWL.Sublogic
import OWL.Morphism
import qualified OWL.Sign as OS
-- CASL_DL = codomain
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism
import CASL.Sublogic
data OWL2CASL = OWL2CASL deriving Show
instance Language OWL2CASL
instance Comorphism
OWL2CASL -- comorphism
OWL -- lid domain
OWLSub -- sublogics domain
OntologyFile -- Basic spec domain
Axiom -- sentence domain
SymbItems -- symbol items domain
SymbMapItems -- symbol map items domain
OS.Sign -- signature domain
OWLMorphism -- morphism domain
Entity -- symbol domain
RawSymb -- rawsymbol domain
ProofTree -- proof tree codomain
CASL -- lid codomain
CASL_Sublogics -- sublogics codomain
CASLBasicSpec -- Basic spec codomain
CASLFORMULA -- sentence codomain
SYMB_ITEMS -- symbol items codomain
SYMB_MAP_ITEMS -- symbol map items codomain
CASLSign -- signature codomain
CASLMor -- morphism codomain
Symbol -- symbol codomain
RawSymbol -- rawsymbol codomain
ProofTree -- proof tree domain
where
sourceLogic OWL2CASL = OWL
sourceSublogic OWL2CASL = sl_top
targetLogic OWL2CASL = CASL
mapSublogic OWL2CASL _ = Just $ cFol
{ cons_features = emptyMapConsFeature }
map_theory OWL2CASL = mapTheory
map_morphism OWL2CASL = mapMorphism
isInclusionComorphism OWL2CASL = True
has_model_expansion OWL2CASL = True
-- | Mapping of OWL morphisms to CASL morphisms
mapMorphism :: OWLMorphism -> Result CASLMor
mapMorphism oMor =
do
cdm <- mapSign $ osource oMor
ccd <- mapSign $ otarget oMor
let emap = mmaps oMor
preds = Map.foldWithKey (\ (Entity ty u1) u2 -> let
i1 = uriToId u1
i2 = uriToId u2
in case ty of
Class -> Map.insert (i1, conceptPred) i2
ObjectProperty -> Map.insert (i1, objectPropPred) i2
DataProperty -> Map.insert (i1, dataPropPred) i2
_ -> id) Map.empty emap
ops = Map.foldWithKey (\ (Entity ty u1) u2 -> case ty of
NamedIndividual ->
Map.insert (uriToId u1, indiConst) (uriToId u2, Total)
_ -> id) Map.empty emap
return (embedMorphism () cdm ccd)
{ op_map = ops
, pred_map = preds }
-- | OWL topsort Thing
thing :: Id
thing = stringToId "Thing"
noThing :: Id
noThing = stringToId "Nothing"
-- | OWL bottom
mkThingPred :: Id -> PRED_SYMB
mkThingPred i =
Qual_pred_name i (toPRED_TYPE conceptPred) nullRange
-- | OWL Data topSort DATA
dataS :: SORT
dataS = stringToId $ drop 3 $ show OWLDATA
data VarOrIndi = OVar Int | OIndi URI
predefSorts :: Set.Set SORT
predefSorts = Set.singleton thing
hetsPrefix :: String
hetsPrefix = ""
conceptPred :: PredType
conceptPred = PredType [thing]
objectPropPred :: PredType
objectPropPred = PredType [thing, thing]
dataPropPred :: PredType
dataPropPred = PredType [thing, dataS]
indiConst :: OpType
indiConst = sortToOpType thing
mapSign :: OS.Sign -- ^ OWL signature
-> Result CASLSign -- ^ CASL signature
mapSign sig =
cvrt = map uriToId . Set.toList
tMp k = MapSet.fromList . map (\ u -> (u, [k]))
cPreds = thing : noThing : cvrt conc
oPreds = cvrt $ OS.indValuedRoles sig
dPreds = cvrt $ OS.dataValuedRoles sig
aPreds = foldr MapSet.union MapSet.empty
[ tMp conceptPred cPreds
, tMp objectPropPred oPreds
, tMp dataPropPred dPreds ]
in return (emptySign ())
{ sortSet = predefSorts
, predMap = aPreds
, opMap = tMp indiConst . cvrt $ OS.individuals sig
}
loadDataInformation :: OWLSub -> Sign f ()
loadDataInformation sl =
let
dts = Set.map (stringToId . printXSDName) $ datatype sl
in
(emptySign ()) { sortSet = dts }
predefinedSentences :: [Named CASLFORMULA]
predefinedSentences =
[
makeNamed "nothing in Nothing" $
Quantification Universal
[Var_decl [mkNName 1] thing nullRange]
(
Negation
(
Predication
(mkThingPred noThing)
[Qual_var (mkNName 1) thing nullRange]
nullRange
)
nullRange
)
nullRange
,
makeNamed "thing in Thing" $
Quantification Universal
[Var_decl [mkNName 1] thing nullRange]
(
Predication
(mkThingPred thing)
[Qual_var (mkNName 1) thing nullRange]
nullRange
)
nullRange
]
mapTheory :: (OS.Sign, [Named Axiom])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory (owlSig, owlSens) =
let
sublogic =
sl_max (sl_sig owlSig) $
foldl sl_max sl_bottom $ map (sl_ax . sentence) owlSens
in
do
cSig <- mapSign owlSig
let pSig = loadDataInformation sublogic
(cSensI, nSig) <- foldM (\ (x, y) z ->
do
(sen, sig) <- mapSentence y z
return (sen : x, uniteCASLSign sig y)
) ([], cSig) owlSens
let cSens = concatMap (\ x ->
case x of
Nothing -> []
Just a -> [a]
) cSensI
return (uniteCASLSign nSig pSig, predefinedSentences ++ cSens)
-- | mapping of OWL to CASL_DL formulae
mapSentence :: CASLSign -- ^ CASL Signature
-> Named Axiom -- ^ OWL Sentence
-> Result (Maybe (Named CASLFORMULA), CASLSign) -- ^ CASL Sentence
mapSentence cSig inSen = do
(outAx, outSig) <- mapAxiom cSig $ sentence inSen
return (fmap (flip mapNamed inSen . const) outAx, outSig)
-- | Mapping of Axioms
mapAxiom :: CASLSign -- ^ CASL Signature
-> Axiom -- ^ OWL Axiom
-> Result (Maybe CASLFORMULA, CASLSign) -- ^ CASL Formula
mapAxiom cSig ax =
let
a = 1
b = 2
c = 3
in
case ax of
PlainAxiom _ pAx ->
case pAx of
SubClassOf sub super ->
do
domT <- mapDescription cSig sub a
codT <- mapDescription cSig super a
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange]
(Implication
domT
codT
True
nullRange) nullRange, cSig)
EquivOrDisjointClasses eD dS ->
do
decrsS <- mapDescriptionListP cSig a $ comPairs dS dS
let decrsP =
case eD of
Equivalent ->
map (\ (x, y) -> Equivalence x y nullRange)
decrsS
Disjoint ->
map (\ (x, y) -> Negation
(Conjunction [x, y] nullRange) nullRange)
decrsS
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange]
(
Conjunction decrsP nullRange
) nullRange, cSig)
DisjointUnion cls sD ->
do
decrs <- mapDescriptionList cSig a sD
decrsS <- mapDescriptionListP cSig a $ comPairs sD sD
let decrsP = map (\ (x, y) -> Conjunction [x, y] nullRange)
decrsS
mcls <- mapClassURI cSig cls (mkNName a)
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange]
(
Equivalence
mcls -- The class
( -- The rest
Conjunction
[
Disjunction decrs nullRange
, Negation
(
Conjunction decrsP nullRange
)
nullRange
]
nullRange
)
nullRange
) nullRange, cSig)
SubObjectPropertyOf ch op ->
do
os <- mapSubObjProp cSig ch op c
return (Just os, cSig)
EquivOrDisjointObjectProperties disOrEq oExLst ->
do
pairs <- mapComObjectPropsList cSig oExLst a b
return (Just $ Quantification Universal
[ Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] thing nullRange]
(
Conjunction
(
case disOrEq of
Equivalent ->
map (\ (x, y) ->
Equivalence x y nullRange) pairs
Disjoint ->
map (\ (x, y) ->
(Negation
(Conjunction [x, y] nullRange)
nullRange
)
) pairs
)
nullRange
)
nullRange, cSig)
ObjectPropertyDomainOrRange domOrRn objP descr ->
do
tobjP <- mapObjProp cSig objP a b
tdsc <- mapDescription cSig descr $
case domOrRn of
ObjDomain -> a
ObjRange -> b
let vars = case domOrRn of
ObjDomain -> (mkNName a, mkNName b)
ObjRange -> (mkNName b, mkNName a)
return (Just $ Quantification Universal
[Var_decl [fst vars] thing nullRange]
(
Quantification Existential
[Var_decl [snd vars] thing nullRange]
(
Implication
tobjP
tdsc
True
nullRange
)
nullRange
)
nullRange, cSig)
InverseObjectProperties o1 o2 ->
do
so1 <- mapObjProp cSig o1 a b
so2 <- mapObjProp cSig o2 b a
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] thing nullRange]
(
Equivalence
so1
so2
nullRange
)
nullRange, cSig)
ObjectPropertyCharacter cha o ->
case cha of
Functional ->
do
so1 <- mapObjProp cSig o a b
so2 <- mapObjProp cSig o a c
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] thing nullRange
, Var_decl [mkNName c] thing nullRange
]
(
Implication
(
Conjunction [so1, so2] nullRange
)
(
Strong_equation
(
Qual_var (mkNName b) thing nullRange
)
(
Qual_var (mkNName c) thing nullRange
)
nullRange
)
True
nullRange
)
nullRange, cSig)
InverseFunctional ->
do
so1 <- mapObjProp cSig o a c
so2 <- mapObjProp cSig o b c
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] thing nullRange
, Var_decl [mkNName c] thing nullRange
]
(
Implication
(
Conjunction [so1, so2] nullRange
)
(
Strong_equation
(
Qual_var (mkNName a) thing nullRange
)
(
Qual_var (mkNName b) thing nullRange
)
nullRange
)
True
nullRange
)
nullRange, cSig)
Reflexive ->
do
so <- mapObjProp cSig o a a
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange]
(
Implication
(
Membership
(Qual_var (mkNName a) thing nullRange)
thing
nullRange
)
so
True
nullRange
)
nullRange, cSig)
Irreflexive ->
do
so <- mapObjProp cSig o a a
return
(Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange]
(
Implication
(
Membership
(Qual_var (mkNName a) thing nullRange)
thing
nullRange
)
(
Negation
so
nullRange
)
True
nullRange
)
nullRange, cSig)
Symmetric ->
do
so1 <- mapObjProp cSig o a b
so2 <- mapObjProp cSig o b a
return
(Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] thing nullRange]
(
Implication
so1
so2
True
nullRange
)
nullRange, cSig)
Asymmetric ->
do
so1 <- mapObjProp cSig o a b
so2 <- mapObjProp cSig o b a
return
(Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] thing nullRange]
(
Implication
so1
(Negation so2 nullRange)
True
nullRange
)
nullRange, cSig)
Antisymmetric ->
do
so1 <- mapObjProp cSig o a b
so2 <- mapObjProp cSig o b a
return
(Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] thing nullRange]
(
Implication
(Conjunction [so1, so2] nullRange)
(
Strong_equation
(
Qual_var (mkNName a) thing nullRange
)
(
Qual_var (mkNName b) thing nullRange
)
nullRange
)
True
nullRange
)
nullRange, cSig)
Transitive ->
do
so1 <- mapObjProp cSig o a b
so2 <- mapObjProp cSig o b c
so3 <- mapObjProp cSig o a c
return
(Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] thing nullRange
, Var_decl [mkNName c] thing nullRange]
(
Implication
(
Conjunction [so1, so2] nullRange
)
so3
True
nullRange
)
nullRange, cSig)
SubDataPropertyOf dP1 dP2 ->
do
l <- mapDataProp cSig dP1 a b
r <- mapDataProp cSig dP2 a b
return (Just $ Quantification Universal
[ Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] dataS nullRange]
(
Implication
l
r
True
nullRange
)
nullRange, cSig)
EquivOrDisjointDataProperties disOrEq dlst ->
do
pairs <- mapComDataPropsList cSig dlst a b
return (Just $ Quantification Universal
[ Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] dataS nullRange]
(
Conjunction
(
case disOrEq of
Equivalent ->
map (\ (x, y) ->
Equivalence x y nullRange) pairs
Disjoint ->
map (\ (x, y) ->
(Negation
(Conjunction [x, y] nullRange)
nullRange
)
) pairs
)
nullRange
)
nullRange, cSig)
DataPropertyDomainOrRange domRn dpex ->
do
oEx <- mapDataProp cSig dpex a b
case domRn of
DataDomain mdom ->
do
odes <- mapDescription cSig mdom a
let vars = (mkNName a, mkNName b)
return (Just $ Quantification Universal
[Var_decl [fst vars] thing nullRange]
(Quantification Existential
[Var_decl [snd vars] dataS nullRange]
(Implication oEx odes True nullRange)
nullRange) nullRange, cSig)
DataRange rn ->
do
odes <- mapDataRange cSig rn b
let vars = (mkNName a, mkNName b)
return (Just $ Quantification Universal
[Var_decl [fst vars] thing nullRange]
(Quantification Existential
[Var_decl [snd vars] dataS nullRange]
(Implication oEx odes True nullRange)
nullRange) nullRange, cSig)
FunctionalDataProperty o ->
do
so1 <- mapDataProp cSig o a b
so2 <- mapDataProp cSig o a c
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange
, Var_decl [mkNName b] dataS nullRange
, Var_decl [mkNName c] dataS nullRange
]
(
Implication
(
Conjunction [so1, so2] nullRange
)
(
Strong_equation
(
Qual_var (mkNName b) dataS nullRange
)
(
Qual_var (mkNName c) dataS nullRange
)
nullRange
)
True
nullRange
)
nullRange, cSig
)
SameOrDifferentIndividual sameOrDiff indis ->
do
inD <- mapM (mapIndivURI cSig) indis
let inDL = comPairs inD inD
return (Just $ Conjunction
(map (\ (x, y) -> case sameOrDiff of
Same -> Strong_equation x y nullRange
Different -> Negation
(Strong_equation x y nullRange) nullRange
) inDL)
nullRange, cSig)
ClassAssertion indi cls ->
do
inD <- mapIndivURI cSig indi
ocls <- mapDescription cSig cls a
return (Just $ Quantification Universal
[Var_decl [mkNName a] thing nullRange]
(
Implication
(Strong_equation
(Qual_var (mkNName a) thing nullRange)
inD
nullRange
)
ocls
True
nullRange
)
nullRange, cSig)
ObjectPropertyAssertion ass ->
case ass of
Assertion objProp posNeg sourceInd targetInd ->
do
inS <- mapIndivURI cSig sourceInd
inT <- mapIndivURI cSig targetInd
oPropH <- mapObjProp cSig objProp a b
let oProp = case posNeg of
Positive -> oPropH
Negative -> Negation
oPropH
nullRange
return (Just $ Quantification Universal
[Var_decl [mkNName a]
thing nullRange
, Var_decl [mkNName b]
thing nullRange]
(
Implication
(
Conjunction
[
Strong_equation
(Qual_var (mkNName a) thing
nullRange)
inS
nullRange
, Strong_equation
(Qual_var (mkNName b) thing
nullRange)
inT
nullRange
]
nullRange
)
oProp
True
nullRange
)
nullRange, cSig)
DataPropertyAssertion ass ->
case ass of
Assertion dPropExp posNeg sourceInd targetInd ->
do
inS <- mapIndivURI cSig sourceInd
inT <- mapConstant cSig targetInd
dPropH <- mapDataProp cSig dPropExp a b
let dProp = case posNeg of
Positive -> dPropH
Negative -> Negation
dPropH
nullRange
return (Just $ Quantification Universal
[Var_decl [mkNName a]
thing nullRange
, Var_decl [mkNName b]
dataS nullRange]
(
Implication
(
Conjunction
[
Strong_equation
(Qual_var (mkNName a) thing nullRange)
inS
nullRange
, Strong_equation
(Qual_var (mkNName b) dataS nullRange)
inT
nullRange
]
nullRange
)
dProp
True
nullRange
)
nullRange, cSig)
Declaration _ ->
return (Nothing, cSig)
EntityAnno _ ->
return (Nothing, cSig)
{- | Mapping along ObjectPropsList for creation of pairs for commutative
operations. -}
mapComObjectPropsList :: CASLSign -- ^ CASLSignature
-> [ObjectPropertyExpression]
-> Int -- ^ First variable
-> Int -- ^ Last variable
-> Result [(CASLFORMULA, CASLFORMULA)]
mapComObjectPropsList cSig props num1 num2 =
mapM (\ (x, z) -> do
l <- mapObjProp cSig x num1 num2
r <- mapObjProp cSig z num1 num2
return (l, r)
) $ comPairs props props
-- | mapping of data constants
mapConstant :: CASLSign
-> Constant
-> Result (TERM ())
mapConstant _ c =
do
let cl = case c of
Constant l _ -> l
return $ Application
(
Qual_op_name
(stringToId cl)
(Op_type Total [] dataS nullRange)
nullRange
)
[]
nullRange
-- | Mapping of subobj properties
mapSubObjProp :: CASLSign
-> SubObjectPropertyExpression
-> ObjectPropertyExpression
-> Int
-> Result CASLFORMULA
mapSubObjProp cSig prop oP num1 =
let
num2 = num1 + 1
in
case prop of
OPExpression oPL ->
do
l <- mapObjProp cSig oPL num1 num2
r <- mapObjProp cSig oP num1 num2
return $ Quantification Universal
[ Var_decl [mkNName num1] thing nullRange
, Var_decl [mkNName num2] thing nullRange]
(
Implication
r
l
True
nullRange
)
nullRange
SubObjectPropertyChain props ->
do
let zprops = zip (tail props) [(num2 + 1) ..]
(_, vars) = unzip zprops
oProps <- mapM (\ (z, x, y) -> mapObjProp cSig z x y) $
zip3 props ((num1 : vars) ++ [num2]) $
tail ((num1 : vars) ++ [num2])
ooP <- mapObjProp cSig oP num1 num2
return $ Quantification Universal
[ Var_decl [mkNName num1] thing nullRange
, Var_decl [mkNName num2] thing nullRange]
(
Quantification Universal
(
map (\ x -> Var_decl [mkNName x] thing nullRange) vars
)
(
Implication
(Conjunction oProps nullRange)
ooP
True
nullRange
)
nullRange
)
nullRange
{- | Mapping along DataPropsList for creation of pairs for commutative
operations. -}
mapComDataPropsList :: CASLSign
-> [DataPropertyExpression]
-> Int -- ^ First variable
-> Int -- ^ Last variable
-> Result [(CASLFORMULA, CASLFORMULA)]
mapComDataPropsList cSig props num1 num2 =
mapM (\ (x, z) -> do
l <- mapDataProp cSig x num1 num2
r <- mapDataProp cSig z num1 num2
return (l, r)
) $ comPairs props props
-- | Mapping of data properties
mapDataProp :: CASLSign
-> DataPropertyExpression
-> Int
-> Int
-> Result CASLFORMULA
mapDataProp _ dP nO nD =
do
let
l = mkNName nO
r = mkNName nD
ur <- uriToIdM dP
return $ Predication
(Qual_pred_name ur (toPRED_TYPE dataPropPred) nullRange)
[Qual_var l thing nullRange, Qual_var r dataS nullRange]
nullRange
-- | Mapping of obj props
mapObjProp :: CASLSign
-> ObjectPropertyExpression
-> Int
-> Int
-> Result CASLFORMULA
mapObjProp cSig ob num1 num2 =
case ob of
OpURI u ->
do
let l = mkNName num1
r = mkNName num2
ur <- uriToIdM u
return $ Predication
(Qual_pred_name ur (toPRED_TYPE objectPropPred) nullRange)
[Qual_var l thing nullRange, Qual_var r thing nullRange]
nullRange
InverseOp u ->
mapObjProp cSig u num2 num1
-- | Mapping of obj props with Individuals
mapObjPropI :: CASLSign
-> ObjectPropertyExpression
-> VarOrIndi
-> VarOrIndi
-> Result CASLFORMULA
mapObjPropI cSig ob lP rP =
case ob of
OpURI u ->
do
lT <- case lP of
OVar num1 -> return $ Qual_var (mkNName num1)
thing nullRange
OIndi indivID -> mapIndivURI cSig indivID
rT <- case rP of
OVar num1 -> return $ Qual_var (mkNName num1)
thing nullRange
OIndi indivID -> mapIndivURI cSig indivID
ur <- uriToIdM u
return $ Predication
(Qual_pred_name ur
(toPRED_TYPE objectPropPred) nullRange)
[lT,
rT
]
nullRange
InverseOp u -> mapObjPropI cSig u rP lP
-- | Mapping of Class URIs
mapClassURI :: CASLSign
-> OwlClassURI
-> Token
-> Result CASLFORMULA
mapClassURI _ uril uid =
do
ur <- uriToIdM uril
return $ Predication
(Qual_pred_name ur (toPRED_TYPE conceptPred) nullRange)
[Qual_var uid thing nullRange]
nullRange
-- | Mapping of Individual URIs
mapIndivURI :: CASLSign
-> IndividualURI
-> Result (TERM ())
mapIndivURI _ uriI =
do
ur <- uriToIdM uriI
return $ Application
(
Qual_op_name
ur
(Op_type Total [] thing nullRange)
nullRange
)
[]
nullRange
uriToIdM :: URI -> Result Id
uriToIdM = return . uriToId
-- | Extracts Id from URI
uriToId :: URI -> Id
uriToId urI =
let
ur = case urI of
QN _ "Thing" _ _ -> mkQName "Thing"
QN _ "Nothing" _ _ -> mkQName "Nothing"
_ -> urI
repl a = if isAlphaNum a
then
a
else
'_'
nP = map repl $ namePrefix ur
lP = map repl $ localPart ur
nU = map repl $ namespaceUri ur
in stringToId $ nU ++ "" ++ nP ++ "" ++ lP
-- | Mapping of a list of descriptions
mapDescriptionList :: CASLSign
-> Int
-> [Description]
-> Result [CASLFORMULA]
mapDescriptionList cSig n lst =
mapM (uncurry $ mapDescription cSig)
$ zip lst $ replicate (length lst) n
-- | Mapping of a list of pairs of descriptions
mapDescriptionListP :: CASLSign
-> Int
-> [(Description, Description)]
-> Result [(CASLFORMULA, CASLFORMULA)]
mapDescriptionListP cSig n lst =
do
let (l, r) = unzip lst
llst <- mapDescriptionList cSig n l
rlst <- mapDescriptionList cSig n r
let olst = zip llst rlst
return olst
-- | Build a name
mkNName :: Int -> Token
mkNName i = mkSimpleId $ hetsPrefix ++ mkNName_H i
where
mkNName_H k =
case k of
0 -> ""
j -> mkNName_H (j `div` 26) ++ [chr (j `mod` 26 + 96)]
-- | Get all distinct pairs for commutative operations
comPairs :: [t] -> [t1] -> [(t, t1)]
comPairs [] [] = []
comPairs _ [] = []
comPairs [] _ = []
comPairs (a : as) (_ : bs) = zip (replicate (length bs) a) bs ++ comPairs as bs
-- | mapping of Data Range
mapDataRange :: CASLSign
-> DataRange -- ^ OWL DataRange
-> Int -- ^ Current Variablename
-> Result CASLFORMULA -- ^ CASL_DL Formula
mapDataRange cSig rn inId =
do
let uid = mkNName inId
case rn of
DRDatatype uril ->
do
ur <- uriToIdM uril
return $ Membership
(Qual_var uid thing nullRange)
ur
nullRange
DataComplementOf dr ->
do
dc <- mapDataRange cSig dr inId
return $ Negation dc nullRange
DataOneOf _ -> error "nyi"
DatatypeRestriction _ _ -> error "nyi"
-- | mapping of OWL Descriptions
mapDescription :: CASLSign
-> Description -- ^ OWL Description
-> Int -- ^ Current Variablename
-> Result CASLFORMULA -- ^ CASL_DL Formula
mapDescription cSig des var =
case des of
OWLClassDescription cl -> mapClassURI cSig cl (mkNName var)
ObjectJunction jt desL ->
do
desO <- mapM (flip (mapDescription cSig) var) desL
return $ case jt of
UnionOf -> Disjunction desO nullRange
IntersectionOf -> Conjunction desO nullRange
ObjectComplementOf descr ->
do
desO <- mapDescription cSig descr var
return $ Negation desO nullRange
ObjectOneOf indS ->
do
indO <- mapM (mapIndivURI cSig) indS
let varO = Qual_var (mkNName var) thing nullRange
let forms = map (mkStEq varO) indO
return $ Disjunction forms nullRange
ObjectValuesFrom qt oprop descr ->
do
opropO <- mapObjProp cSig oprop var (var + 1)
descO <- mapDescription cSig descr (var + 1)
case qt of
SomeValuesFrom ->
return $ Quantification Existential [Var_decl [mkNName
(var + 1)]
thing nullRange]
(
Conjunction
[opropO, descO]
nullRange
)
nullRange
AllValuesFrom ->
return $ Quantification Universal [Var_decl [mkNName
(var + 1)]
thing nullRange]
(
Implication
opropO descO
True
nullRange
)
nullRange
ObjectExistsSelf oprop -> mapObjProp cSig oprop var var
ObjectHasValue oprop indiv ->
mapObjPropI cSig oprop (OVar var) (OIndi indiv)
ObjectCardinality c ->
case c of
Cardinality ct n oprop d
->
do
let vlst = [(var + 1) .. (n + var)]
vlstM = [(var + 1) .. (n + var + 1)]
dOut <- (\ x -> case x of
Nothing -> return []
Just y ->
mapM (mapDescription cSig y) vlst
) d
let dlst = map (\ (x, y) ->
Negation
(
Strong_equation
(Qual_var (mkNName x) thing nullRange)
(Qual_var (mkNName y) thing nullRange)
nullRange
)
nullRange
) $ comPairs vlst vlst
dlstM = map (\ (x, y) ->
Strong_equation
(Qual_var (mkNName x) thing nullRange)
(Qual_var (mkNName y) thing nullRange)
nullRange
) $ comPairs vlstM vlstM
qVars = map (\ x ->
Var_decl [mkNName x]
thing nullRange
) vlst
qVarsM = map (\ x ->
Var_decl [mkNName x]
thing nullRange
) vlstM
oProps <- mapM (mapObjProp cSig oprop var) vlst
oPropsM <- mapM (mapObjProp cSig oprop var) vlstM
let minLst = Quantification Existential
qVars
(
Conjunction
(dlst ++ dOut ++ oProps)
nullRange
)
nullRange
let maxLst = Quantification Universal
qVarsM
(
Implication
(Conjunction (oPropsM ++ dOut) nullRange)
(Disjunction dlstM nullRange)
True
nullRange
)
nullRange
case ct of
MinCardinality -> return minLst
MaxCardinality -> return maxLst
ExactCardinality -> return $
Conjunction
[minLst, maxLst]
nullRange
DataValuesFrom _ _ _ _ -> fail "data handling nyi"
DataHasValue _ _ -> fail "data handling nyi"
DataCardinality _ -> fail "data handling nyi"