Morphism.hs revision 1f9274bb2aa44ea236327814dce99946be52e348
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder{- |
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederModule : $Header$
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederDescription : RDF Morphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederCopyright : (c) Francisc-Nicolae Bungiu, Felix Gabriel Mance, 2011
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederMaintainer : f.bungiu@jacobs-university.de
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederStability : provisional
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederPortability : portable
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederMorphisms for RDF
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedermodule RDF.Morphism where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.DocUtils
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder{-}import Common.Doc
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Lib.State
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Lib.MapSet (setToMap)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Result
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport OWL2.AS
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport RDF.AS
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport RDF.Sign
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport RDF.Function
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder--import RDF.StaticAnalysis
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder--import RDF.Symbols
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport RDF.Print ()
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder{-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Control.Monad
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Data.Maybe
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Data.Set as Set
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Data.Map as Map
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata RDFMorphism = RDFMorphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder { osource :: Sign
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , otarget :: Sign
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , mmaps :: MorphMap
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder } deriving (Show, Eq, Ord)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder{-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinclRDFMorphism :: Sign -> Sign -> RDFMorphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinclRDFMorphism s t = RDFMorphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder { osource = s
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , otarget = t
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , mmaps = Map.empty }
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederisRDFInclusion :: RDFMorphism -> Bool
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederisRDFInclusion m = Map.null (mmaps m) && isSubSign (osource m) (otarget m)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedersymMap :: MorphMap -> Map.Map RDFEntity RDFEntity
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedersymMap = Map.mapWithKey (\ (RDFEntity ty _) -> RDFEntity ty)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinducedElems :: MorphMap -> [RDFEntity]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinducedElems = Map.elems . symMap
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinducedSign :: MorphMap -> Sign -> Sign
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinducedSign m = execState (do
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder mapM_ (modEntity Set.delete) $ Map.keys m
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder mapM_ (modEntity Set.insert) $ inducedElems m)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinducedFromMor :: Map.Map RawSymb RawSymb -> Sign -> Result RDFMorphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederinducedFromMor rm sig = do
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder let syms = symOf sig
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder mm <- foldM (\ m p -> case p of
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder (ASymbol s@(RDFEntity _ v), ASymbol (RDFEntity _ u)) ->
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder if Set.member s syms
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder then return $ if u == v then m else Map.insert s u m
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder else fail $ "unknown symbol: " ++ showDoc s "\n" ++ shows sig ""
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (AnUri v, AnUri u) -> case filter (`Set.member` syms)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder $ map (`RDFEntity` v) rdfEntityTypes of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder [] -> fail $ "unknown symbol: " ++ showDoc v "\n" ++ shows sig ""
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder l -> return $ if u == v then m else foldr (`Map.insert` u) m l
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> error "RDF.Morphism.inducedFromMor") Map.empty $ Map.toList rm
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder return RDFMorphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder { osource = sig
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , otarget = inducedSign mm sig
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , mmaps = mm }
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedersymMapOf :: RDFMorphism -> Map.Map RDFEntity RDFEntity
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedersymMapOf mor = Map.union (symMap $ mmaps mor) $ setToMap $ symOf $ osource mor
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Pretty RDFMorphism where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder{-} pretty m = let
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder s = osource m
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder srcD = specBraces $ space <> pretty s
90bf4bf40789422552e566b73738ba5efae144c3Christian Maeder t = otarget m
020928b46741d7f6cf2ef9d5a2359dafd9a28f73Wiebke Herding in if isRDFInclusion m then
020928b46741d7f6cf2ef9d5a2359dafd9a28f73Wiebke Herding if isSubSign t s then
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder fsep [text "identity morphism over", srcD]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder else fsep
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder [ text "inclusion morphism of"
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , srcD
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , text "extended with"
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , pretty $ Set.difference (symOf t) $ symOf s ]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder else fsep
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder [ pretty $ mmaps m
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , colon <+> srcD, mapsto <+> specBraces (space <> pretty t) ]
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederlegalMor :: RDFMorphism -> Result ()
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederlegalMor m = let mm = mmaps m in unless
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (Set.isSubsetOf (Map.keysSet mm) (symOf $ osource m)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder && Set.isSubsetOf (Set.fromList $ inducedElems mm) (symOf $ otarget m))
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder $ fail "illegal RDF morphism"
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercomposeMor :: RDFMorphism -> RDFMorphism -> Result RDFMorphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercomposeMor m1 m2 =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder let nm = Set.fold (\ s@(RDFEntity ty u) -> let
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder t = getIri ty u $ mmaps m1
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder r = getIri ty t $ mmaps m2
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder in if r == u then id else Map.insert s r) Map.empty
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder . symOf $ osource m1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder in return m1
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder { otarget = otarget m2
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder , mmaps = nm }
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercogeneratedSign :: Set.Set RDFEntity -> Sign -> Result RDFMorphism
afbd86903151121381e4e9d22862136817d7f0f0Christian MaedercogeneratedSign s sign =
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder let sig2 = execState (mapM_ (modEntity Set.delete) $ Set.toList s) sign
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder in if isSubSign sig2 sign then return $ inclRDFMorphism sig2 sign else
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder fail "non RDF subsignatures for (co)generatedSign"
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedergeneratedSign :: Set.Set RDFEntity -> Sign -> Result RDFMorphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedergeneratedSign s sign = cogeneratedSign (Set.difference (symOf sign) s) sign
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedermatchesSym :: RDFEntity -> RawSymb -> Bool
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedermatchesSym e@(RDFEntity _ u) r = case r of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder ASymbol s -> s == e
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder AnUri s -> s == u || namePrefix u == localPart s && null (namePrefix s)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederstatSymbItems :: [SymbItems] -> [RawSymb]
afbd86903151121381e4e9d22862136817d7f0f0Christian MaederstatSymbItems = concatMap
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder $ \ (SymbItems m us) -> case m of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Nothing -> map AnUri us
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder Just ty -> map (ASymbol . RDFEntity ty) us
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder
afbd86903151121381e4e9d22862136817d7f0f0Christian MaederstatSymbMapItems :: [SymbMapItems] -> Result (Map.Map RawSymb RawSymb)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederstatSymbMapItems =
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder foldM (\ m (s, t) -> case Map.lookup s m of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Nothing -> return $ Map.insert s t m
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Just u -> case (u, t) of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (AnUri su, ASymbol (RDFEntity _ tu)) | su == tu ->
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder return $ Map.insert s t m
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder (ASymbol (RDFEntity _ su), AnUri tu) | su == tu -> return m
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> if u == t then return m else
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder fail $ "differently mapped symbol: " ++ showDoc s "\nmapped to "
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder ++ showDoc u " and " ++ showDoc t "")
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Map.empty
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder . concatMap (\ (SymbMapItems m us) ->
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder let ps = map (\ (u, v) -> (u, fromMaybe u v)) us in
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder case m of
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Nothing -> map (\ (s, t) -> (AnUri s, AnUri t)) ps
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Just ty ->
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder let mS = ASymbol . RDFEntity ty
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder in map (\ (s, t) -> (mS s, mS t)) ps)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedermapSen :: RDFMorphism -> Axiom -> Result Axiom
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedermapSen m a = return $ function Rename (MorphMap $ mmaps m) a
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-}
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder