{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./OWL2/Morphism.hs
Description : OWL Morphisms
Copyright : (c) Dominik Luecke, 2008, Felix Gabriel Mance, 2011
License : GPLv2 or higher, see LICENSE.txt
Maintainer : f.mance@jacobs-university.de
Stability : provisional
Portability : portable
Morphisms for OWL
-}
module OWL2.Morphism where
import Common.IRI
import OWL2.AS
import OWL2.MS
import OWL2.Sign
import OWL2.ManchesterPrint ()
import OWL2.Symbols
import OWL2.Function
import Common.DocUtils
import Common.Doc
import Common.Result
import Common.Utils (composeMap)
import Common.Lib.State (execState)
import Common.Lib.MapSet (setToMap)
import Common.Id(nullRange)
import Control.Monad
import Data.Data
import Data.List (stripPrefix)
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set
data OWLMorphism = OWLMorphism
{ osource :: Sign
, otarget :: Sign
, mmaps :: MorphMap
, pmap :: StringMap
} deriving (Show, Eq, Ord, Typeable, Data)
inclOWLMorphism :: Sign -> Sign -> OWLMorphism
inclOWLMorphism s t = OWLMorphism
{ osource = s
, otarget = t
, pmap = Map.empty
, mmaps = Map.empty }
isOWLInclusion :: OWLMorphism -> Bool
isOWLInclusion m = Map.null (pmap m)
&& Map.null (mmaps m) && isSubSign (osource m) (otarget m)
symMap :: MorphMap -> Map.Map Entity Entity
symMap = Map.mapWithKey (\ (Entity lb ty _) -> Entity lb ty)
inducedElems :: MorphMap -> [Entity]
inducedElems = Map.elems . symMap
inducedSign :: MorphMap -> StringMap -> Sign -> Sign
inducedSign m t s =
let new = execState (do
mapM_ (modEntity Set.delete) $ Map.keys m
mapM_ (modEntity Set.insert) $ inducedElems m) s
in function Rename (StringMap t) new
inducedPref :: String -> String -> Sign -> (MorphMap, StringMap)
-> Result (MorphMap, StringMap)
inducedPref v u sig (m, t) =
let pm = prefixMap sig
in if Set.member v $ Map.keysSet pm
then if u == v then return (m, t) else return (m, Map.insert v u t)
else
plain_error (Map.empty, Map.empty) ("unknown symbol: " ++ showDoc v "\nin signature:\n" ++ showDoc sig "") nullRange
inducedFromMor :: Map.Map RawSymb RawSymb -> Sign -> Result OWLMorphism
inducedFromMor rm sig = do
let syms = symOf sig
(mm, tm) <- foldM (\ (m, t) p -> case p of
(ASymbol s@(Entity _ _ v), ASymbol (Entity _ _ u)) ->
if Set.member s syms
then return $ if u == v then (m, t) else (Map.insert s u m, t)
else fail $ "unknown symbol: " ++ showDoc s "\n" ++ shows sig ""
(AnUri v, AnUri u) -> case filter (`Set.member` syms)
$ map (`mkEntity` v) entityTypes of
[] -> let v2 = showIRICompact v
u2 = showIRICompact u
in inducedPref v2 u2 sig (m, t)
l -> return $ if u == v then (m, t) else
(foldr (`Map.insert` u) m l, t)
(APrefix v, APrefix u) -> inducedPref v u sig (m, t)
_ -> error "OWL2.Morphism.inducedFromMor") (Map.empty, Map.empty)
$ Map.toList rm
return OWLMorphism
{ osource = sig
, otarget = inducedSign mm tm sig
, pmap = tm
, mmaps = mm }
symMapOf :: OWLMorphism -> Map.Map Entity Entity
symMapOf mor = Map.union (symMap $ mmaps mor) $ setToMap $ symOf $ osource mor
instance Pretty OWLMorphism where
pretty m = let
s = osource m
srcD = specBraces $ space <> pretty s
t = otarget m
in fsep $ if isOWLInclusion m then
if isSubSign t s then
[text "identity morphism over", srcD]
else
[ text "inclusion morphism of"
, srcD
, text "extended with"
, pretty $ Set.difference (symOf t) $ symOf s ]
else
[ pretty $ mmaps m
, pretty $ pmap m
, colon <+> srcD, mapsto <+> specBraces (space <> pretty t) ]
legalMor :: OWLMorphism -> Result ()
legalMor m = let mm = mmaps m in unless
(Set.isSubsetOf (Map.keysSet mm) (symOf $ osource m)
&& Set.isSubsetOf (Set.fromList $ inducedElems mm) (symOf $ otarget m))
$ fail "illegal OWL2 morphism"
composeMor :: OWLMorphism -> OWLMorphism -> Result OWLMorphism
composeMor m1 m2 =
let nm = Set.fold (\ s@(Entity _ ty u) -> let
t = getIri ty u $ mmaps m1
r = getIri ty t $ mmaps m2
in if r == u then id else Map.insert s r) Map.empty
. symOf $ osource m1
in return m1
{ otarget = otarget m2
, pmap = composeMap (prefixMap $ osource m1) (pmap m1) $ pmap m2
, mmaps = nm }
cogeneratedSign :: Set.Set Entity -> Sign -> Result OWLMorphism
cogeneratedSign s sign =
let sig2 = execState (mapM_ (modEntity Set.delete) $ Set.toList s) sign
in if isSubSign sig2 sign then return $ inclOWLMorphism sig2 sign else
fail "non OWL2 subsignatures for (co)generatedSign"
generatedSign :: Set.Set Entity -> Sign -> Result OWLMorphism
generatedSign s sign = cogeneratedSign (Set.difference (symOf sign) s) sign
matchesSym :: Entity -> RawSymb -> Bool
matchesSym e@(Entity _ _ u) r = case r of
ASymbol s -> s == e
AnUri s -> s == u -- || expandedIRI s == expandedIRI u
|| case
stripPrefix (reverse $ show $ iriPath s) (reverse $ show $ iriPath u) of
Just (c : _) | null (prefixName s) -> elem c "/#"
_ -> False
APrefix p -> p == prefixName u
statSymbItems :: Sign -> [SymbItems] -> [RawSymb]
statSymbItems sig = map (function Expand . StringMap $ prefixMap sig)
. concatMap
(\ (SymbItems m us) -> case m of
AnyEntity -> map AnUri us
EntityType ty -> map (ASymbol . mkEntity ty) us
PrefixO -> map (APrefix . showIRI) us)
statSymbMapItems :: Sign -> Maybe Sign -> [SymbMapItems]
-> Result (Map.Map RawSymb RawSymb)
statSymbMapItems sig mtsig =
fmap (Map.fromList . map (\ (r1, r2) ->
let f = function Expand . StringMap . prefixMap
f1 = f sig
f2 = f $ fromMaybe sig mtsig
in (f1 r1, f2 r2)) . Map.toList)
. foldM (\ m (s, t) -> case Map.lookup s m of
Nothing -> return $ Map.insert s t m
Just u -> case (u, t) of
(AnUri su, ASymbol (Entity _ _ tu)) | su == tu ->
return $ Map.insert s t m
(ASymbol (Entity _ _ su), AnUri tu) | su == tu -> return m
(AnUri su, APrefix tu) | showIRICompact su == tu ->
return $ Map.insert s t m
(APrefix su, AnUri tu) | su == showIRICompact tu -> return m
_ -> if u == t then return m else
fail $ "differently mapped symbol: " ++ showDoc s "\nmapped to "
++ showDoc u " and " ++ showDoc t "")
Map.empty
. concatMap (\ (SymbMapItems m us) ->
let ps = map (\ (u, v) -> (u, fromMaybe u v)) us in
case m of
AnyEntity -> map (\ (s, t) -> (AnUri s, AnUri t)) ps
EntityType ty ->
let mS = ASymbol . mkEntity ty
in map (\ (s, t) -> (mS s, mS t)) ps
PrefixO ->
map (\ (s, t) -> (APrefix (showIRICompact s), APrefix $ showIRICompact t)) ps)
mapSen :: OWLMorphism -> Axiom -> Result Axiom
mapSen m a = do
let new = function Rename (MorphMap $ mmaps m) a
return $ function Rename (StringMap $ pmap m) new
morphismUnion :: OWLMorphism -> OWLMorphism -> Result OWLMorphism
morphismUnion mor1 mor2 = do
let ssig1 = osource mor1
tsig1 = otarget mor1
ssig2 = osource mor2
tsig2 = otarget mor2
ssig = addSign ssig1 ssig2
tsig = addSign tsig1 tsig2
m1 = mmaps mor1
m2 = mmaps mor2
intM = Map.intersection m1 m2
pairs = filter (\(a,b) -> a /= b)
$ map (\x -> (Map.findWithDefault (error "1") x m1,
Map.findWithDefault (error "2") x m2))
$ Map.keys intM
case pairs of
[] ->
return $ OWLMorphism {
osource = ssig,
otarget = tsig,
mmaps = Map.union m1 m2,
pmap = Map.union (pmap mor1) $ pmap mor2}
_ -> fail $ "can't unite morphisms:" ++ show pairs