Morphism.hs revision 97889f5e2d475855c8f06f4190aff9cf459a998b
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiModule : $Header$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDescription : Morphisms for Maude
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiCopyright : (c) Martin Kuehl, Uni Bremen 2008-2009
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiMaintainer : mkhl@informatik.uni-bremen.de
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiStability : experimental
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiPortability : portable
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDefinition of morphisms for Maude.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Morphism(..),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski applyRenamings,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fromSignRenamings,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fromSignsRenamings,
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu qualifySorts,
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu extendWithSortRenaming,
356f33e31a1cf98a878f069e9e2e1cbea4a06e81Ewaryst Schulzimport Maude.Sentence (Sentence)
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzimport qualified Maude.Sign as Sign
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzimport qualified Maude.Sentence as Sen
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzimport Data.List (partition)
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzimport Data.Maybe (fromJust)
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzimport qualified Data.Set as Set
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzimport qualified Data.Map as Map
356f33e31a1cf98a878f069e9e2e1cbea4a06e81Ewaryst Schulzimport qualified Common.Result as Result
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzimport Common.Doc hiding (empty)
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzimport Common.DocUtils (Pretty(..))
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Langetype SortMap = SymbolMap
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescutype OpMap = SymbolMap
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescutype LabelMap = SymbolMap
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescudata Morphism = Morphism {
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu source :: Sign,
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu target :: Sign,
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu sortMap :: SortMap,
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu opMap :: OpMap,
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu labelMap :: LabelMap
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu } deriving (Show, Ord, Eq)
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescuinstance Pretty Morphism where
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu pretty mor = let
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu pr'pair txt left right = hsep
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu [txt, pretty left, text "to", pretty right]
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu pr'ops src tgt = pr'pair (text "op") src (getName tgt)
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu pr'map fun = vsep . map (uncurry fun) . Map.toList
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu smap = pr'map (pr'pair $ text "sort") $ sortMap mor
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu omap = pr'map pr'ops $ opMap mor
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu lmap = pr'map (pr'pair $ text "label") $ labelMap mor
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu in vsep [ smap, omap, lmap ]
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu -- text "\n\nTarget:" <$$> pretty $ target mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Separate Operator and other Renamings.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskipartitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskipartitionRenamings = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski is'op renaming = case renaming of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski OpRenaming1 _ _ -> True
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski OpRenaming2 _ _ _ _ -> True
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in partition is'op
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskirenamingSymbolsMaybe :: Renaming -> Maybe (Symbol, Symbol)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskirenamingSymbolsMaybe rename = case rename of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski SortRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski LabelRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski OpRenaming1 src (To tgt _) -> Just (asSymbol src, asSymbol tgt)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski OpRenaming2 src dom cod (To tgt _) -> let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski src' = getName src
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski tgt' = getName tgt
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski dom' = map asSymbol dom
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski cod' = asSymbol cod
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in Just (Operator src' dom' cod', Operator tgt' dom' cod')
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- TODO: We are not currently handling TermMaps, right?
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski TermMap _ _ -> Nothing
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskirenamingSymbols :: Renaming -> (Symbol, Symbol)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskirenamingSymbols = fromJust . renamingSymbolsMaybe
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiapplyRenamings :: Morphism -> [Renaming] -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiapplyRenamings mor rens = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (ops, rest) = partitionRenamings rens
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'ops = flip (foldr applyOpRenaming) ops
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'rest = flip (foldr applyRenaming) rest
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in add'rest . add'ops $ mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | create a Morphism from an initial signature and a list of Renamings
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskifromSignRenamings :: Sign -> [Renaming] -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskifromSignRenamings = applyRenamings . identity
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- TODO: Handle Attrs in Op Renamings.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiapplyOpRenaming :: Renaming -> Morphism -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiapplyOpRenaming rename = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski syms = renamingSymbols rename
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'op mor = mor { opMap = uncurry Map.insert syms $ opMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski use'op attrs mor = mor { target = uncurry Sign.renameOp syms attrs $ target mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in case rename of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski OpRenaming1 _ (To _ attrs) -> use'op attrs . add'op
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski OpRenaming2 _ _ _ (To _ attrs) -> use'op attrs . add'op
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiapplyRenaming :: Renaming -> Morphism -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiapplyRenaming rename = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski syms = renamingSymbols rename
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'sort mor = mor { sortMap = uncurry Map.insert syms $ sortMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski use'sort mor = mor { target = uncurry Sign.renameSort syms $ target mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ren'sort mor = mor { opMap = uncurry renameSortOpMap syms $ opMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'labl mor = mor { labelMap = uncurry Map.insert syms $ labelMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski use'labl mor = mor { target = uncurry Sign.renameLabel syms $ target mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in case rename of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski SortRenaming _ _ -> ren'sort . use'sort . add'sort
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski LabelRenaming _ _ -> use'labl . add'labl
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | create a Morphism from the initial signatures and a list of Renamings
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskifromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskifromSignsRenamings sign1 sign2 rens = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (ops, rest) = partitionRenamings rens
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'ops = flip (foldr insertOpRenaming) ops
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'rest = flip (foldr insertRenaming) rest
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski mor = inclusion sign1 sign2
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in add'rest . add'ops $ mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- TODO: Handle Attrs in Op Renamings.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinsertOpRenaming :: Renaming -> Morphism -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinsertOpRenaming rename = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski syms = renamingSymbols rename
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'op mor = mor { opMap = uncurry Map.insert syms $ opMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in case rename of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski OpRenaming1 _ _ -> add'op
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski OpRenaming2 _ _ _ _ -> add'op
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinsertRenaming :: Renaming -> Morphism -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiinsertRenaming rename = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski syms = renamingSymbols rename
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'sort mor = mor { sortMap = uncurry Map.insert syms $ sortMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ren'sort mor = mor { opMap = uncurry renameSortOpMap syms $ opMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'labl mor = mor { labelMap = uncurry Map.insert syms $ labelMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in case rename of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski SortRenaming _ _ -> ren'sort . add'sort
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski LabelRenaming _ _ -> add'labl
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | Rename sorts in the profiles of an operator map.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskirenameSortOpMap :: Symbol -> Symbol -> OpMap -> OpMap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskirenameSortOpMap from to = Map.map $ mapSorts $ Map.singleton from to
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | extract the SymbolMap of a Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskisymbolMap :: Morphism -> SymbolMap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskisymbolMap mor = Map.unions [sortMap mor, opMap mor, labelMap mor]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | the empty Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiempty :: Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiempty = identity Sign.empty
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | the identity Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiidentity :: Sign -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiidentity sign = inclusion sign sign
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | the inclusion Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinclusion :: Sign -> Sign -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinclusion src tgt = Morphism {
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski source = src,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski target = tgt,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | the inverse Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinverse :: Morphism -> Result Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinverse mor = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski invertMap = Map.foldWithKey (flip Map.insert) Map.empty
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in return Morphism {
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski source = target mor,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski target = source mor,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski sortMap = invertMap $ sortMap mor,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski opMap = invertMap $ opMap mor,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski labelMap = invertMap $ labelMap mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | the composition of two Morphisms
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskicompose :: Morphism -> Morphism -> Result Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | target f /= source g = fail
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski "target of the first and source of the second morphism are different"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | otherwise = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Take SymbolMap |mp| of each Morphism.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Convert each SymbolMap to a function.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Compose those functions.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski map'map :: (Morphism -> SymbolMap) -> Symbol -> Symbol
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski map'map mp = mapAsFunction (mp g) . mapAsFunction (mp f)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Map |x| via the composed SymbolMaps |mp| of both Morphisms.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Insert the renaming mapping into a SymbolMap.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski insert :: (Morphism -> SymbolMap) -> Symbol -> SymbolMap -> SymbolMap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski insert mp x = let y = map'map mp x
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in if x == y then id else Map.insert x y
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- Map each symbol in |items| via the combined SymbolMaps |mp|.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski compose'map :: (Morphism -> SymbolMap) -> (Sign -> SymbolSet) -> SymbolMap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski compose'map mp items = if Map.null (mp g)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- if the SymbolMap of |g| is empty, we use the one from |f|
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- otherwise we start with the SymbolSet from |source f|
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- and construct a combined SymbolMap by applying both
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- SymbolMaps (from |f| and |g|) to each item in |insert|
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski else Set.fold (insert mp) Map.empty $ items (source f)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski -- We want a morphism from |source f| to |target g|.
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski mor = inclusion (source f) (target g)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in return mor {
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski sortMap = compose'map sortMap getSorts,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski opMap = compose'map opMap getOps,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski labelMap = compose'map labelMap getLabels
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | check that a Morphism is legal
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisLegal :: Morphism -> Bool
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisLegal mor = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski src = source mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski tgt = target mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski smap = sortMap mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski omap = opMap mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski lmap = labelMap mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski subset mp items = let mapped = Set.map $ mapAsFunction mp
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in Set.isSubsetOf (mapped $ items src) $ items tgt
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski lg'source = Sign.isLegal src
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski lg'sortMap = subset smap getSorts
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski lg'opMap = subset omap getOps
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski lg'labelMap = subset lmap getLabels
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski lg'target = Sign.isLegal tgt
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in all id [lg'source, lg'sortMap, lg'opMap, lg'labelMap, lg'target]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | check that a Morphism is the identity
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisIdentity :: Morphism -> Bool
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisIdentity mor = source mor == target mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | check that a Morphism is an Inclusion
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisInclusion :: Morphism -> Bool
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiisInclusion mor = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski null'sortMap = Map.null (sortMap mor)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski null'opMap = Map.null (opMap mor)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski null'labelMap = Map.null (labelMap mor)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in all id [null'sortMap, null'opMap, null'labelMap]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- | translate a Sentence along a Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskimapSentence :: Morphism -> Sentence -> Result Sentence
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskimapSentence mor = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski smap = mapSorts (sortMap mor)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski omap = mapOps (opMap mor)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski lmap = mapLabels (labelMap mor)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in return . lmap . omap . smap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunion :: Morphism -> Morphism -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiunion m1 m2 = let apply func items = func (items m1) (items m2)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in Morphism {
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski source = apply Sign.union source,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski target = apply Sign.union target,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski sortMap = apply Map.union sortMap,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski opMap = apply Map.union opMap,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski labelMap = apply Map.union labelMap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskisetTarget :: Sign -> Morphism -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskisetTarget sign morph = morph {target = sign}
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskirenameSorts :: Morphism -> Symbols -> Symbols
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskirenameSorts = mapSorts . sortMap
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiqualifySorts :: Morphism -> Qid -> Symbols -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiqualifySorts mor qid syms = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski insert symb = Map.insert symb $ qualify qid symb
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski smap = foldr insert Map.empty syms
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski q'tgt m = m { target = mapSorts smap $ target m }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski q'smap m = m { sortMap = mapSorts smap $ sortMap m }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in q'tgt . q'smap $ mor
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski-- FIXME: Code duplication!
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiextendWithSortRenaming :: Symbol -> Symbol -> Morphism -> Morphism
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiextendWithSortRenaming src tgt = let
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski add'sort mor = mor { sortMap = Map.insert src tgt $ sortMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski use'sort mor = mor { target = Sign.renameSort src tgt $ target mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ren'sort mor = mor { opMap = renameSortOpMap src tgt $ opMap mor }
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in ren'sort . use'sort . add'sort