66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederModule : $Header$

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederDescription : Comorphism from OWL 2 to CASL_Dl

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederCopyright : (c) Francisc-Nicolae Bungiu, Felix Gabriel Mance

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : f.bungiu@jacobs-university.de

66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : provisional

fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederPortability : non-portable (via Logic.Logic)

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder-}

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule OWL2.OWL22CASL (OWL22CASL (..)) where

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Logic.Logic as Logic

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Logic.Comorphism

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Common.AS_Annotation

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Result

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.Id

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Control.Monad

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Data.Char

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maederimport qualified Data.Set as Set

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Data.Map as Map

712f5e5ca1c3a5cfdd28518154ecf2dd0994cdb5Christian Maederimport qualified Common.Lib.MapSet as MapSet

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maederimport qualified Common.Lib.Rel as Rel

f71a8dcf94fd9eb3c9800e16dcdc5e5ff74e5c22Christian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-- the DL with the initial signature for OWL

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederimport CASL_DL.PredefinedCASLAxioms

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- OWL = domain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport OWL2.Logic_OWL2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport OWL2.Keywords

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport OWL2.MS

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport OWL2.AS

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport OWL2.Parse

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport OWL2.Print

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport OWL2.ProfilesAndSublogics

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport OWL2.ManchesterPrint ()

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederimport OWL2.Morphism

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maederimport OWL2.Symbols

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport qualified OWL2.Sign as OS

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- CASL_DL = codomain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.Logic_CASL

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.AS_Basic_CASL

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.Sign

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.Morphism

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.Sublogic

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- import OWL2.ManchesterParser

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederimport Common.ProofTree

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Common.DocUtils

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Data.Maybe

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Text.ParserCombinators.Parsec

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maederdata OWL22CASL = OWL22CASL deriving Show

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederinstance Language OWL22CASL

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederinstance Comorphism

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder OWL22CASL -- comorphism

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder OWL2 -- lid domain

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder ProfSub -- sublogics domain

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder OntologyDocument -- Basic spec domain

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder Axiom -- sentence domain

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder SymbItems -- symbol items domain

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder SymbMapItems -- symbol map items domain

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder OS.Sign -- signature domain

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder OWLMorphism -- morphism domain

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder Entity -- symbol domain

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder RawSymb -- rawsymbol domain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ProofTree -- proof tree codomain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder CASL -- lid codomain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder CASL_Sublogics -- sublogics codomain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder CASLBasicSpec -- Basic spec codomain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder CASLFORMULA -- sentence codomain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder SYMB_ITEMS -- symbol items codomain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder SYMB_MAP_ITEMS -- symbol map items codomain

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder CASLSign -- signature codomain

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder CASLMor -- morphism codomain

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder Symbol -- symbol codomain

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder RawSymbol -- rawsymbol codomain

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder ProofTree -- proof tree domain

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder where

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder sourceLogic OWL22CASL = OWL2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder sourceSublogic OWL22CASL = topS

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder targetLogic OWL22CASL = CASL

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder mapSublogic OWL22CASL _ = Just $ cFol

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder { cons_features = emptyMapConsFeature }

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder map_theory OWL22CASL = mapTheory

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder map_morphism OWL22CASL = mapMorphism

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder map_symbol OWL22CASL _ = mapSymbol

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder isInclusionComorphism OWL22CASL = True

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder has_model_expansion OWL22CASL = True

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder-- s = emptySign ()

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederuniteL :: [CASLSign] -> CASLSign

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederuniteL = foldl1 uniteCASLSign

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederfailMsg :: Pretty a => a -> Result b

f0742398d4587242b1a115de113cd17f63dcb6d0Christian MaederfailMsg a = fail $ "cannot translate " ++ showDoc a "\n"

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederobjectPropPred :: PredType

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederobjectPropPred = PredType [thing, thing]

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederdataPropPred :: PredType

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaederdataPropPred = PredType [thing, dataS]

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederindiConst :: OpType

c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian MaederindiConst = OpType Total [] thing

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederuriToIdM :: IRI -> Result Id

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederuriToIdM = return . uriToId

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder-- | Extracts Id from URI

fb69cd512eab767747f109e40322df7cae2f7bdfChristian MaederuriToId :: IRI -> Id

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederuriToId urI =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let l = localPart urI

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ur = if isThing urI then mkQName l else urI

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder repl a = if isAlphaNum a then [a] else "_u"

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder nP = concatMap repl $ namePrefix ur

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder lP = concatMap repl l

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder in stringToId $ (if isDatatypeKey urI then "" else nP) ++ lP

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertokDecl :: Token -> VAR_DECL

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertokDecl = flip mkVarDecl thing

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertokDataDecl :: Token -> VAR_DECL

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertokDataDecl = flip mkVarDecl dataS

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

772abb916b994ad9461ddb11c88829251c5ac87aChristian MaedernameDecl :: Int -> SORT -> VAR_DECL

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedernameDecl = mkVarDecl . mkNName

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederthingDecl :: Int -> VAR_DECL

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederthingDecl = flip nameDecl thing

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederdataDecl :: Int -> VAR_DECL

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederdataDecl = flip nameDecl dataS

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederqualThing :: Int -> TERM f

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaederqualThing = toQualVar . thingDecl

08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederqualData :: Int -> TERM f

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederqualData = toQualVar . dataDecl

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederimplConj :: [FORMULA f] -> FORMULA f -> FORMULA f

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederimplConj = mkImpl . conjunct

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermkNC :: [FORMULA f] -> FORMULA f

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermkNC = mkNeg . conjunct

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedermkEqVar :: VAR_DECL -> TERM f -> FORMULA f

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedermkEqVar = mkStEq . toQualVar

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedermkFEI :: [VAR_DECL] -> [VAR_DECL] -> FORMULA f -> FORMULA f -> FORMULA f

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermkFEI l1 l2 f = mkForall l1 . mkExist l2 . mkImpl f

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermkFIE :: [Int] -> [FORMULA f] -> Int -> Int -> FORMULA f

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermkFIE l1 l2 x y = mkVDecl l1 $ implConj l2 $ mkEqVar (thingDecl x) $ qualThing y

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermkRI :: [Int] -> Int -> FORMULA f -> FORMULA f

05e2a3161e4589a717c6fe5c7306820273a473c5Christian MaedermkRI l x so = mkVDecl l $ mkImpl (mkMember (qualThing x) thing) so

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

mkThingVar :: VAR -> TERM f

mkThingVar v = Qual_var v thing nullRange

mkEqDecl :: Int -> TERM f -> FORMULA f

mkEqDecl i = mkEqVar (thingDecl i)

mkVDecl :: [Int] -> FORMULA f -> FORMULA f

mkVDecl = mkForall . map thingDecl

mkVDataDecl :: [Int] -> FORMULA f -> FORMULA f

mkVDataDecl = mkForall . map dataDecl

mk1VDecl :: FORMULA f -> FORMULA f

mk1VDecl = mkVDecl [1]

mkPred :: PredType -> [TERM f] -> PRED_NAME -> FORMULA f

mkPred c tl u = mkPredication (mkQualPred u $ toPRED_TYPE c) tl

mkMember :: TERM f -> SORT -> FORMULA f

mkMember t s = Membership t s nullRange

-- | Get all distinct pairs for commutative operations

comPairs :: [t] -> [t1] -> [(t, t1)]

comPairs [] [] = []

comPairs _ [] = []

comPairs [] _ = []

comPairs (a : as) (_ : bs) = mkPairs a bs ++ comPairs as bs

mkPairs :: t -> [s] -> [(t, s)]

mkPairs a = map (\ b -> (a, b))

data VarOrIndi = OVar Int | OIndi IRI

deriving (Show, Eq, Ord)

-- | 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 }

mapSymbol :: Entity -> Set.Set Symbol

mapSymbol (Entity ty iri) = let

syN = Set.singleton . Symbol (uriToId iri)

in case ty of

Class -> syN $ PredAsItemType conceptPred

ObjectProperty -> syN $ PredAsItemType objectPropPred

DataProperty -> syN $ PredAsItemType dataPropPred

NamedIndividual -> syN $ OpAsItemType indiConst

AnnotationProperty -> Set.empty

Datatype -> Set.empty

mapSign :: OS.Sign -> Result CASLSign

mapSign sig =

let conc = OS.concepts sig

cvrt = map uriToId . Set.toList

tMp k = MapSet.fromList . map (\ u -> (u, [k]))

cPreds = thing : nothing : cvrt conc

oPreds = cvrt $ OS.objectProperties sig

dPreds = cvrt $ OS.dataProperties sig

aPreds = foldr MapSet.union MapSet.empty

[ tMp conceptPred cPreds

, tMp objectPropPred oPreds

, tMp dataPropPred dPreds ]

in return $ uniteCASLSign predefSign (emptySign ())

{ predMap = aPreds

, opMap = tMp indiConst . cvrt $ OS.individuals sig

}

loadDataInformation :: ProfSub -> Sign f ()

loadDataInformation _ = let dts = Set.fromList $ map stringToId datatypeKeys

in (emptySign ()) { sortRel = Rel.fromKeysSet dts }

mapTheory :: (OS.Sign, [Named Axiom]) -> Result (CASLSign, [Named CASLFORMULA])

mapTheory (owlSig, owlSens) = let sl = topS in do

cSig <- mapSign owlSig

let pSig = loadDataInformation sl

dTypes = (emptySign ()) {sortRel = Rel.transClosure $ Rel.fromList

$ map (\ d -> (uriToId d, dataS))

$ predefIRIs ++ Set.toList (OS.datatypes owlSig)}

(cSens, nSig) <- foldM (\ (x, y) z -> do

(sen, sig) <- mapSentence y z

return (sen ++ x, uniteCASLSign sig y)) ([], cSig) owlSens

return (foldl1 uniteCASLSign [nSig, pSig, dTypes],

predefinedAxioms ++ cSens)

-- | mapping of OWL to CASL_DL formulae

mapSentence :: CASLSign -> Named Axiom -> Result ([Named CASLFORMULA], CASLSign)

mapSentence cSig inSen = do

(outAx, outSig) <- mapAxioms cSig $ sentence inSen

return (map (flip mapNamed inSen . const) outAx, outSig)

mapVar :: CASLSign -> VarOrIndi -> Result (TERM ())

mapVar cSig v = case v of

OVar n -> return $ qualThing n

OIndi i -> mapIndivURI cSig i

-- | Mapping of Class URIs

mapClassURI :: CASLSign -> Class -> Token -> Result CASLFORMULA

mapClassURI _ c t = fmap (mkPred conceptPred [mkThingVar t]) $ uriToIdM c

-- | Mapping of Individual URIs

mapIndivURI :: CASLSign -> Individual -> Result (TERM ())

mapIndivURI _ uriI = do

ur <- uriToIdM uriI

return $ mkAppl (mkQualOp ur (Op_type Total [] thing nullRange)) []

mapNNInt :: NNInt -> TERM ()

mapNNInt int = let NNInt uInt = int in foldr1 joinDigits $ map mkDigit uInt

mapIntLit :: IntLit -> TERM ()

mapIntLit int =

let cInt = mapNNInt $ absInt int

in if isNegInt int then negateInt $ upcast cInt integer

else upcast cInt integer

mapDecLit :: DecLit -> TERM ()

mapDecLit dec =

let ip = truncDec dec

np = absInt ip

fp = fracDec dec

n = mkDecimal (mapNNInt np) (mapNNInt fp)

in if isNegInt ip then negateFloat n else n

mapFloatLit :: FloatLit -> TERM ()

mapFloatLit f =

let fb = floatBase f

ex = floatExp f

in mkFloat (mapDecLit fb) (mapIntLit ex)

mapNrLit :: Literal -> TERM ()

mapNrLit l = case l of

NumberLit f

| isFloatInt f -> mapIntLit $ truncDec $ floatBase f

| isFloatDec f -> mapDecLit $ floatBase f

| otherwise -> mapFloatLit f

_ -> error "not number literal"

mapLiteral :: Literal -> Result (TERM ())

mapLiteral lit = return $ case lit of

Literal l ty -> Sorted_term (case ty of

Untyped _ -> foldr consChar emptyStringTerm l

Typed dt -> case getDatatypeCat dt of

OWL2Number -> let p = parse literal "" l in case p of

Right nr -> mapNrLit nr

_ -> error "cannot parse number literal"

OWL2Bool -> case l of

"true" -> trueT

_ -> falseT

_ -> foldr consChar emptyStringTerm l) dataS nullRange

_ -> mapNrLit lit

-- | Mapping of data properties

mapDataProp :: CASLSign -> DataPropertyExpression -> Int -> Int

-> Result CASLFORMULA

mapDataProp _ dp a b = fmap (mkPred dataPropPred [qualThing a, qualData b])

$ uriToIdM dp

-- | Mapping of obj props

mapObjProp :: CASLSign -> ObjectPropertyExpression -> Int -> Int

-> Result CASLFORMULA

mapObjProp cSig ob a b = case ob of

ObjectProp u -> fmap (mkPred objectPropPred $ map qualThing [a, b])

$ uriToIdM u

ObjectInverseOf u -> mapObjProp cSig u b a

-- | Mapping of obj props with Individuals

mapObjPropI :: CASLSign -> ObjectPropertyExpression -> VarOrIndi -> VarOrIndi

-> Result CASLFORMULA

mapObjPropI cSig ob lP rP = case ob of

ObjectProp u -> do

l <- mapVar cSig lP

r <- mapVar cSig rP

fmap (mkPred objectPropPred [l, r]) $ uriToIdM u

ObjectInverseOf u -> mapObjPropI cSig u rP lP

-- | mapping of individual list

mapComIndivList :: CASLSign -> SameOrDifferent -> Maybe Individual

-> [Individual] -> Result [CASLFORMULA]

mapComIndivList cSig sod mol inds = do

fs <- mapM (mapIndivURI cSig) inds

tps <- case mol of

Nothing -> return $ comPairs fs fs

Just ol -> do

f <- mapIndivURI cSig ol

return $ mkPairs f fs

return $ map (\ (x, y) -> case sod of

Same -> mkStEq x y

Different -> mkNeg $ mkStEq x y) tps

{- | Mapping along DataPropsList for creation of pairs for commutative

operations. -}

mapComDataPropsList :: CASLSign -> Maybe DataPropertyExpression

-> [DataPropertyExpression] -> Int -> Int

-> Result [(CASLFORMULA, CASLFORMULA)]

mapComDataPropsList cSig md props a b = do

fs <- mapM (\ x -> mapDataProp cSig x a b) props

case md of

Nothing -> return $ comPairs fs fs

Just dp -> fmap (`mkPairs` fs) $ mapDataProp cSig dp a b

{- | Mapping along ObjectPropsList for creation of pairs for commutative

operations. -}

mapComObjectPropsList :: CASLSign -> Maybe ObjectPropertyExpression

-> [ObjectPropertyExpression] -> Int -> Int

-> Result [(CASLFORMULA, CASLFORMULA)]

mapComObjectPropsList cSig mol props a b = do

fs <- mapM (\ x -> mapObjProp cSig x a b) props

case mol of

Nothing -> return $ comPairs fs fs

Just ol -> fmap (`mkPairs` fs) $ mapObjProp cSig ol a b

-- | mapping of Data Range

mapDataRange :: CASLSign -> DataRange -> Int -> Result (CASLFORMULA, CASLSign)

mapDataRange cSig dr i = case dr of

DataType d fl -> do

let dt = mkMember (qualData i) $ uriToId d

(sens, s) <- mapAndUnzipM (mapFacet cSig i) fl

return (conjunct $ dt : sens, uniteL $ cSig : s)

DataComplementOf drc -> do

(sens, s) <- mapDataRange cSig drc i

return (mkNeg sens, uniteCASLSign cSig s)

DataJunction jt drl -> do

(jl, sl) <- mapAndUnzipM ((\ s v r -> mapDataRange s r v) cSig i) drl

let usig = uniteL sl

return $ case jt of

IntersectionOf -> (conjunct jl, usig)

UnionOf -> (disjunct jl, usig)

DataOneOf cs -> do

ls <- mapM mapLiteral cs

return (disjunct $ map (mkStEq $ qualData i) ls, cSig)

mkFacetPred :: TERM f -> ConstrainingFacet -> Int -> (FORMULA f, Id)

mkFacetPred lit f var =

let cf = mkInfix $ fromCF f

in (mkPred dataPred [qualData var, lit] cf, cf)

mapFacet :: CASLSign -> Int -> (ConstrainingFacet, RestrictionValue)

-> Result (CASLFORMULA, CASLSign)

mapFacet sig var (f, r) = do

con <- mapLiteral r

let (fp, cf) = mkFacetPred con f var

return (fp, uniteCASLSign sig $ (emptySign ())

{predMap = MapSet.fromList [(cf, [dataPred])]})

cardProps :: Bool -> CASLSign

-> Either ObjectPropertyExpression DataPropertyExpression -> Int

-> [Int] -> Result [CASLFORMULA]

cardProps b cSig prop var vLst =

if b then let Left ope = prop in mapM (mapObjProp cSig ope var) vLst

else let Right dpe = prop in mapM (mapDataProp cSig dpe var) vLst

mapCard :: Bool -> CASLSign -> CardinalityType -> Int

-> Either ObjectPropertyExpression DataPropertyExpression

-> Maybe (Either ClassExpression DataRange) -> Int

-> Result (FORMULA (), CASLSign)

mapCard b cSig ct n prop d var = do

let vlst = map (var +) [1 .. n]

vlstM = vlst ++ [n + var + 1]

(dOut, s) <- case d of

Nothing -> return ([], [emptySign ()])

Just y ->

if b then let Left ce = y in mapAndUnzipM

(mapDescription cSig ce) vlst

else let Right dr = y in mapAndUnzipM (mapDataRange cSig dr) vlst

let dlst = map (\ (x, y) -> mkNeg $ mkStEq (qualThing x) $ qualThing y)

$ comPairs vlst vlst

dlstM = map (\ (x, y) -> mkStEq (qualThing x) $ qualThing y)

$ comPairs vlstM vlstM

qVars = map thingDecl vlst

qVarsM = map thingDecl vlstM

oProps <- cardProps b cSig prop var vlst

oPropsM <- cardProps b cSig prop var vlstM

let minLst = mkExist qVars $ conjunct $ dlst ++ dOut ++ oProps

maxLst = mkForall qVarsM $ mkImpl (conjunct $ oPropsM ++ dOut)

$ disjunct dlstM

ts = uniteL $ cSig : s

return $ case ct of

MinCardinality -> (minLst, ts)

MaxCardinality -> (maxLst, ts)

ExactCardinality -> (conjunct [minLst, maxLst], ts)

-- | mapping of OWL2 Descriptions

mapDescription :: CASLSign -> ClassExpression -> Int ->

Result (CASLFORMULA, CASLSign)

mapDescription cSig desc var = case desc of

Expression u -> do

c <- mapClassURI cSig u $ mkNName var

return (c, cSig)

ObjectJunction ty ds -> do

(els, s) <- mapAndUnzipM (flip (mapDescription cSig) var) ds

return ((case ty of

UnionOf -> disjunct

IntersectionOf -> conjunct)

els, uniteL $ cSig : s)

ObjectComplementOf d -> do

(els, s) <- mapDescription cSig d var

return (mkNeg els, uniteCASLSign cSig s)

ObjectOneOf is -> do

il <- mapM (mapIndivURI cSig) is

return (disjunct $ map (mkStEq $ qualThing var) il, cSig)

ObjectValuesFrom ty o d -> let n = var + 1 in do

oprop0 <- mapObjProp cSig o var n

(desc0, s) <- mapDescription cSig d n

return $ case ty of

SomeValuesFrom -> (mkExist [thingDecl n] $ conjunct [oprop0, desc0],

uniteCASLSign cSig s)

AllValuesFrom -> (mkVDecl [n] $ mkImpl oprop0 desc0,

uniteCASLSign cSig s)

ObjectHasSelf o -> do

op <- mapObjProp cSig o var var

return (op, cSig)

ObjectHasValue o i -> do

op <- mapObjPropI cSig o (OVar var) (OIndi i)

return (op, cSig)

ObjectCardinality (Cardinality ct n oprop d) -> mapCard True cSig ct n

(Left oprop) (fmap Left d) var

DataValuesFrom ty dpe dr -> let n = var + 1 in do

oprop0 <- mapDataProp cSig dpe var n

(desc0, s) <- mapDataRange cSig dr n

let ts = uniteCASLSign cSig s

return $ case ty of

SomeValuesFrom -> (mkExist [dataDecl n] $ conjunct [oprop0, desc0],

ts)

AllValuesFrom -> (mkVDataDecl [n] $ mkImpl oprop0 desc0, ts)

DataHasValue dpe c -> do

con <- mapLiteral c

return (mkPred dataPropPred [qualThing var, con] $ uriToId dpe, cSig)

DataCardinality (Cardinality ct n dpe dr) -> mapCard False cSig ct n

(Right dpe) (fmap Right dr) var

-- | Mapping of a list of descriptions

mapDescriptionList :: CASLSign -> Int -> [ClassExpression]

-> Result ([CASLFORMULA], CASLSign)

mapDescriptionList cSig n lst = do

(els, s) <- mapAndUnzipM (uncurry $ mapDescription cSig)

$ zip lst $ replicate (length lst) n

return (els, uniteL $ cSig : s)

-- | Mapping of a list of pairs of descriptions

mapDescriptionListP :: CASLSign -> Int -> [(ClassExpression, ClassExpression)]

-> Result ([(CASLFORMULA, CASLFORMULA)], CASLSign)

mapDescriptionListP cSig n lst = do

let (l, r) = unzip lst

([lls, rls], s) <- mapAndUnzipM (mapDescriptionList cSig n) [l, r]

return (zip lls rls, uniteL $ cSig : s)

mapFact :: CASLSign -> Extended -> Fact -> Result CASLFORMULA

mapFact cSig ex f = case f of

ObjectPropertyFact posneg obe ind -> case ex of

SimpleEntity (Entity NamedIndividual siri) -> do

inS <- mapIndivURI cSig siri

inT <- mapIndivURI cSig ind

oPropH <- mapObjProp cSig obe 1 2

let oProp = case posneg of

Positive -> oPropH

Negative -> Negation oPropH nullRange

return $ mkVDecl [1, 2] $ implConj

[mkEqDecl 1 inS, mkEqDecl 2 inT] oProp

_ -> fail $ "ObjectPropertyFactsFacts Entity fail: " ++ show f

DataPropertyFact posneg dpe lit -> case ex of

SimpleEntity (Entity NamedIndividual iri) -> do

inS <- mapIndivURI cSig iri

inT <- mapLiteral lit

oPropH <- mapDataProp cSig dpe 1 2

let oProp = case posneg of

Positive -> oPropH

Negative -> Negation oPropH nullRange

return $ mkForall [thingDecl 1, dataDecl 2] $ implConj

[mkEqDecl 1 inS, mkEqVar (dataDecl 2) $ upcast inT dataS] oProp

_ -> fail $ "DataPropertyFact Entity fail " ++ show f

mapCharact :: CASLSign -> ObjectPropertyExpression -> Character

-> Result CASLFORMULA

mapCharact cSig ope c = case c of

Functional -> do

so1 <- mapObjProp cSig ope 1 2

so2 <- mapObjProp cSig ope 1 3

return $ mkFIE [1, 2, 3] [so1, so2] 2 3

InverseFunctional -> do

so1 <- mapObjProp cSig ope 1 3

so2 <- mapObjProp cSig ope 2 3

return $ mkFIE [1, 2, 3] [so1, so2] 1 2

Reflexive -> do

so <- mapObjProp cSig ope 1 1

return $ mkRI [1] 1 so

Irreflexive -> do

so <- mapObjProp cSig ope 1 1

return $ mkRI [1] 1 $ mkNeg so

Symmetric -> do

so1 <- mapObjProp cSig ope 1 2

so2 <- mapObjProp cSig ope 2 1

return $ mkVDecl [1, 2] $ mkImpl so1 so2

Asymmetric -> do

so1 <- mapObjProp cSig ope 1 2

so2 <- mapObjProp cSig ope 2 1

return $ mkVDecl [1, 2] $ mkImpl so1 $ mkNeg so2

Antisymmetric -> do

so1 <- mapObjProp cSig ope 1 2

so2 <- mapObjProp cSig ope 2 1

return $ mkFIE [1, 2] [so1, so2] 1 2

Transitive -> do

so1 <- mapObjProp cSig ope 1 2

so2 <- mapObjProp cSig ope 2 3

so3 <- mapObjProp cSig ope 1 3

return $ mkVDecl [1, 2, 3] $ implConj [so1, so2] so3

-- | Mapping of ObjectSubPropertyChain

mapSubObjPropChain :: CASLSign -> [ObjectPropertyExpression]

-> ObjectPropertyExpression -> Int -> Result CASLFORMULA

mapSubObjPropChain cSig props oP n = let m = n + 1 in do

let (_, vars) = unzip $ zip (tail props) [m + 1 ..]

vl = n : vars ++ [m]

oProps <- mapM (\ (z, x, y) -> mapObjProp cSig z x y) $

zip3 props vl $ tail vl

ooP <- mapObjProp cSig oP n m

return $ mkVDecl [1, 2] $ mkVDecl vars $ implConj oProps ooP

-- | Mapping of subobj properties

mapSubObjProp :: CASLSign -> ObjectPropertyExpression

-> ObjectPropertyExpression -> Int -> Result CASLFORMULA

mapSubObjProp cSig e1 e2 a = do

let b = a + 1

l <- mapObjProp cSig e1 a b

r <- mapObjProp cSig e2 a b

return $ mkForallRange (map thingDecl [a, b]) (mkImpl l r) nullRange

mkEDPairs :: CASLSign -> [Int] -> Maybe Relation -> [(FORMULA f, FORMULA f)]

-> Result ([FORMULA f], CASLSign)

mkEDPairs s il mr pairs = do

let ls = map (\ (x, y) -> mkVDecl il

$ case fromMaybe (error "expected EDRelation") mr of

EDRelation Equivalent -> mkEqv x y

EDRelation Disjoint -> mkNC [x, y]

_ -> error "expected EDRelation") pairs

return (ls, s)

-- | Mapping of ListFrameBit

mapListFrameBit :: CASLSign -> Extended -> Maybe Relation -> ListFrameBit

-> Result ([CASLFORMULA], CASLSign)

mapListFrameBit cSig ex rel lfb = case lfb of

AnnotationBit _ -> return ([], cSig)

ExpressionBit cls -> case ex of

Misc _ -> let cel = map snd cls in do

(els, s) <- mapDescriptionListP cSig 1 $ comPairs cel cel

mkEDPairs (uniteCASLSign cSig s) [1] rel els

SimpleEntity (Entity ty iri) -> do

(els, s) <- mapAndUnzipM (\ (_, c) -> mapDescription cSig c 1) cls

case ty of

NamedIndividual | rel == Just Types -> do

inD <- mapIndivURI cSig iri

return (map (mk1VDecl . mkImpl (mkEqDecl 1 inD)) els,

uniteL $ cSig : s)

DataProperty | rel == (Just $ DRRelation ADomain) -> do

oEx <- mapDataProp cSig iri 1 2

let vars = (mkNName 1, mkNName 2)

return (map (mkFEI [tokDecl $ fst vars]

[mkVarDecl (snd vars) dataS] oEx) els, uniteL $ cSig : s)

_ -> failMsg lfb

ObjectEntity oe -> case rel of

Nothing -> failMsg lfb

Just re -> case re of

DRRelation r -> do

tobjP <- mapObjProp cSig oe 1 2

(tdsc, s) <- mapAndUnzipM (\ (_, c) -> mapDescription cSig c

$ case r of

ADomain -> 1

ARange -> 2) cls

let vars = case r of

ADomain -> (mkNName 1, mkNName 2)

ARange -> (mkNName 2, mkNName 1)

return (map (mkFEI [tokDecl $ fst vars]

[tokDecl $ snd vars] tobjP) tdsc, uniteL $ cSig : s)

_ -> failMsg lfb

ClassEntity ce -> let cel = map snd cls in case rel of

Nothing -> return ([], cSig)

Just r -> case r of

EDRelation _ -> do

(decrsS, s) <- mapDescriptionListP cSig 1 $ mkPairs ce cel

mkEDPairs (uniteCASLSign cSig s) [1] rel decrsS

SubClass -> do

(domT, s1) <- mapDescription cSig ce 1

(codT, s2) <- mapDescriptionList cSig 1 cel

return (map (mk1VDecl . mkImpl domT) codT,

uniteL [cSig, s1, s2])

_ -> failMsg lfb

ObjectBit ol -> let opl = map snd ol in case rel of

Nothing -> failMsg lfb

Just r -> case ex of

Misc _ -> do

pairs <- mapComObjectPropsList cSig Nothing opl 1 2

mkEDPairs cSig [1, 2] rel pairs

ObjectEntity op -> case r of

EDRelation _ -> do

pairs <- mapComObjectPropsList cSig (Just op) opl 1 2

mkEDPairs cSig [1, 2] rel pairs

SubPropertyOf -> do

os <- mapM (\ (o1, o2) -> mapSubObjProp cSig o1 o2 3)

$ mkPairs op opl

return (os, cSig)

InverseOf -> do

os1 <- mapM (\ o1 -> mapObjProp cSig o1 1 2) opl

o2 <- mapObjProp cSig op 2 1

return (map (mkVDecl [1, 2] . mkEqv o2) os1, cSig)

_ -> failMsg lfb

_ -> failMsg lfb

DataBit anl -> let dl = map snd anl in case rel of

Nothing -> return ([], cSig)

Just r -> case ex of

Misc _ -> do

pairs <- mapComDataPropsList cSig Nothing dl 1 2

mkEDPairs cSig [1, 2] rel pairs

SimpleEntity (Entity DataProperty iri) -> case r of

SubPropertyOf -> do

os1 <- mapM (\ o1 -> mapDataProp cSig o1 1 2) dl

o2 <- mapDataProp cSig iri 2 1

return (map (mkForall [thingDecl 1, dataDecl 2]

. mkImpl o2) os1, cSig)

EDRelation _ -> do

pairs <- mapComDataPropsList cSig (Just iri) dl 1 2

mkEDPairs cSig [1, 2] rel pairs

_ -> return ([], cSig)

_ -> failMsg lfb

IndividualSameOrDifferent al -> case rel of

Nothing -> failMsg lfb

Just (SDRelation re) -> do

let SimpleEntity (Entity NamedIndividual iri) = ex

fs <- mapComIndivList cSig re (Just iri) $ map snd al

return (fs, cSig)

_ -> failMsg lfb

DataPropRange dpr -> case ex of

SimpleEntity (Entity DataProperty iri) -> do

oEx <- mapDataProp cSig iri 1 2

(odes, s) <- mapAndUnzipM (\ (_, c) -> mapDataRange cSig c 2) dpr

let vars = (mkNName 1, mkNName 2)

return (map (mkFEI [tokDecl $ fst vars]

[tokDataDecl $ snd vars] oEx) odes, uniteL $ cSig : s)

_ -> failMsg lfb

IndividualFacts indf -> do

fl <- mapM (mapFact cSig ex . snd) indf

return (fl, cSig)

ObjectCharacteristics ace -> case ex of

ObjectEntity ope -> do

cl <- mapM (mapCharact cSig ope . snd) ace

return (cl, cSig)

_ -> failMsg ace

-- | Mapping of AnnFrameBit

mapAnnFrameBit :: CASLSign -> Extended -> AnnFrameBit

-> Result ([CASLFORMULA], CASLSign)

mapAnnFrameBit cSig ex afb =

let err = fail $ "could not translate " ++ show afb in case afb of

AnnotationFrameBit _ -> return ([], cSig)

DataFunctional -> case ex of

SimpleEntity (Entity _ iri) -> do

so1 <- mapDataProp cSig iri 1 2

so2 <- mapDataProp cSig iri 1 3

return ([mkForall (thingDecl 1 : map dataDecl [2, 3]) $ implConj

[so1, so2] $ mkEqVar (dataDecl 2) $ qualData 3], cSig)

_ -> err

DatatypeBit dr -> case ex of

SimpleEntity (Entity Datatype iri) -> do

(odes, s) <- mapDataRange cSig dr 2

return ([mkVDataDecl [2] $ mkEqv odes $ mkMember

(qualData 2) $ uriToId iri], uniteCASLSign cSig s)

_ -> err

ClassDisjointUnion clsl -> case ex of

SimpleEntity (Entity Class iri) -> do

(decrs, s1) <- mapDescriptionList cSig 1 clsl

(decrsS, s2) <- mapDescriptionListP cSig 1 $ comPairs clsl clsl

let decrsP = map (\ (x, y) -> conjunct [x, y]) decrsS

mcls <- mapClassURI cSig iri $ mkNName 1

return ([mk1VDecl $ mkEqv mcls $ conjunct

[disjunct decrs, mkNC decrsP]], uniteL [cSig, s1, s2])

_ -> err

ClassHasKey opl dpl -> do

let ClassEntity ce = ex

lo = length opl

ld = length dpl

uptoOP = [2 .. lo + 1]

uptoDP = [lo + 2 .. lo + ld + 1]

tl = lo + ld + 2

ol <- mapM (\ (n, o) -> mapObjProp cSig o 1 n) $ zip uptoOP opl

nol <- mapM (\ (n, o) -> mapObjProp cSig o tl n) $ zip uptoOP opl

dl <- mapM (\ (n, d) -> mapDataProp cSig d 1 n) $ zip uptoDP dpl

ndl <- mapM (\ (n, d) -> mapDataProp cSig d tl n) $ zip uptoDP dpl

(keys, s) <-

mapKey cSig ce (ol ++ dl) (nol ++ ndl) tl (uptoOP ++ uptoDP) lo

return ([keys], uniteCASLSign cSig s)

ObjectSubPropertyChain oplst -> do

os <- mapM (\ cd -> mapSubObjPropChain cSig oplst cd 3) oplst

return (os, cSig)

keyDecl :: Int -> [Int] -> [VAR_DECL]

keyDecl h il = map thingDecl (take h il) ++ map dataDecl (drop h il)

mapKey :: CASLSign -> ClassExpression -> [FORMULA ()] -> [FORMULA ()]

-> Int -> [Int] -> Int -> Result (FORMULA (), CASLSign)

mapKey cSig ce pl npl p i h = do

(nce, s) <- mapDescription cSig ce 1

(c3, _) <- mapDescription cSig ce p

let un = mkForall [thingDecl p] $ implConj (c3 : npl)

$ mkStEq (qualThing p) $ qualThing 1

return (mkForall [thingDecl 1] $ mkImpl nce

$ mkExist (keyDecl h i) $ conjunct $ pl ++ [un], s)

mapAxioms :: CASLSign -> Axiom -> Result ([CASLFORMULA], CASLSign)

mapAxioms cSig (PlainAxiom ex fb) = case fb of

ListFrameBit rel lfb -> mapListFrameBit cSig ex rel lfb

AnnFrameBit _ afb -> mapAnnFrameBit cSig ex afb