Morphism.hs revision 563ca0af6c18a2398a687c8a0d0e2e8c4a0972fe
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederDescription : Morphisms for Maude
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederCopyright : (c) Martin Kuehl, Uni Bremen 2008-2009
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : mkhl@informatik.uni-bremen.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederDefinition of morphisms for Maude.
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder Morphism(..),
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder applyRenamings,
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder fromSignRenamings,
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder fromSignsRenamings,
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder -- extendMorphismSorts,
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder extendWithSortRenaming,
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Maude.Sentence (Sentence)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport qualified Maude.Sign as Sign
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Maude.Sentence as Sen
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Data.List (partition)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Data.Maybe (fromJust)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport qualified Data.Set as Set
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederimport qualified Data.Map as Map
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport qualified Common.Result as Result
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport Common.Doc hiding (empty)
0a39036fa485579a7b7c81cdd44a412392571927Christian Maederimport Common.DocUtils (Pretty(..))
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maedertype SortMap = SymbolMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maedertype OpMap = SymbolMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maedertype LabelMap = SymbolMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederdata Morphism = Morphism {
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder source :: Sign,
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder target :: Sign,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder sortMap :: SortMap,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder opMap :: OpMap,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder labelMap :: LabelMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder } deriving (Show, Ord, Eq)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederinstance Pretty Morphism where
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder pretty mor = let
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder pr'pair txt left right = hsep
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder [txt, pretty left, text "to", pretty right]
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder pr'ops src tgt = pr'pair (text "op") src (getName tgt)
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder pr'map fun = vsep . map (uncurry fun) . Map.toList
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder smap = pr'map (pr'pair $ text "sort") $ sortMap mor
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder omap = pr'map pr'ops $ opMap mor
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder lmap = pr'map (pr'pair $ text "label") $ labelMap mor
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder in vsep [ smap, omap, lmap ]
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder -- text "\n\nTarget:" <$$> pretty $ target mor
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder-- | Separate Operator and other Renamings.
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian MaederpartitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian MaederpartitionRenamings = let
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder is'op renaming = case renaming of
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder OpRenaming1 _ _ -> True
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder OpRenaming2 _ _ _ _ -> True
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder in partition is'op
d591a82b32594f0992b27477cacb00b97226c9c8Christian MaederrenamingSymbolsMaybe :: Renaming -> Maybe (Symbol, Symbol)
d591a82b32594f0992b27477cacb00b97226c9c8Christian MaederrenamingSymbolsMaybe rename = case rename of
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder SortRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder LabelRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder OpRenaming1 src (To tgt _) -> Just (asSymbol src, asSymbol tgt)
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder OpRenaming2 src dom cod (To tgt _) -> let
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder src' = getName src
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder tgt' = getName tgt
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder dom' = map asSymbol dom
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder cod' = asSymbol cod
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder in Just (Operator src' dom' cod', Operator tgt' dom' cod')
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- TODO: We are not currently handling TermMaps, right?
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TermMap _ _ -> Nothing
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenamingSymbols :: Renaming -> (Symbol, Symbol)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenamingSymbols = fromJust . renamingSymbolsMaybe
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederapplyRenamings :: Morphism -> [Renaming] -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederapplyRenamings mor rens = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (ops, rest) = partitionRenamings rens
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'ops = flip (foldr applyOpRenaming) ops
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'rest = flip (foldr applyRenaming) rest
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in add'rest . add'ops $ mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | create a Morphism from an initial signature and a list of Renamings
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederfromSignRenamings :: Sign -> [Renaming] -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederfromSignRenamings = applyRenamings . identity
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- TODO: Handle Attrs in Op Renamings.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederapplyOpRenaming :: Renaming -> Morphism -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederapplyOpRenaming rename = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder syms = renamingSymbols rename
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'op mor = mor { opMap = uncurry Map.insert syms $ opMap mor }
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder use'op attrs mor = mor { target = uncurry Sign.renameOp syms attrs $ target mor }
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder in case rename of
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder OpRenaming1 _ (To _ attrs) -> use'op attrs . add'op
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder OpRenaming2 _ _ _ (To _ attrs) -> use'op attrs . add'op
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederapplyRenaming :: Renaming -> Morphism -> Morphism
d591a82b32594f0992b27477cacb00b97226c9c8Christian MaederapplyRenaming rename = let
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder syms = renamingSymbols rename
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder add'sort mor = mor { sortMap = uncurry Map.insert syms $ sortMap mor }
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder use'sort mor = mor { target = uncurry Sign.renameSort syms $ target mor }
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder ren'sort mor = mor { opMap = uncurry renameSortOpMap syms $ opMap mor }
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder add'labl mor = mor { labelMap = uncurry Map.insert syms $ labelMap mor }
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder use'labl mor = mor { target = uncurry Sign.renameLabel syms $ target mor }
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder in case rename of
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder SortRenaming _ _ -> ren'sort . use'sort . add'sort
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LabelRenaming _ _ -> use'labl . add'labl
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder-- | create a Morphism from the initial signatures and a list of Renamings
d591a82b32594f0992b27477cacb00b97226c9c8Christian MaederfromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaederfromSignsRenamings sign1 sign2 rens = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (ops, rest) = partitionRenamings rens
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'ops = flip (foldr insertOpRenaming) ops
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'rest = flip (foldr insertRenaming) rest
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mor = inclusion sign1 sign2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in add'rest . add'ops $ mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- TODO: Handle Attrs in Op Renamings.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederinsertOpRenaming :: Renaming -> Morphism -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederinsertOpRenaming rename = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder syms = renamingSymbols rename
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'op mor = mor { opMap = uncurry Map.insert syms $ opMap mor }
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in case rename of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder OpRenaming1 _ _ -> add'op
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder OpRenaming2 _ _ _ _ -> add'op
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederinsertRenaming :: Renaming -> Morphism -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederinsertRenaming rename = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder syms = renamingSymbols rename
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'sort mor = mor { sortMap = uncurry Map.insert syms $ sortMap mor }
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ren'sort mor = mor { opMap = uncurry renameSortOpMap syms $ opMap mor }
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'labl mor = mor { labelMap = uncurry Map.insert syms $ labelMap mor }
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in case rename of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder SortRenaming _ _ -> ren'sort . add'sort
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LabelRenaming _ _ -> add'labl
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | Rename sorts in the profiles of an operator map.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenameSortOpMap :: Symbol -> Symbol -> OpMap -> OpMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenameSortOpMap from to = Map.map $ mapSorts $ Map.singleton from to
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | extract the SymbolMap of a Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedersymbolMap :: Morphism -> SymbolMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedersymbolMap mor = Map.unions [sortMap mor, opMap mor, labelMap mor]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | the empty Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederempty :: Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederempty = identity Sign.empty
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- | the identity Morphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederidentity :: Sign -> Morphism
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederidentity sign = inclusion sign sign
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | the inclusion Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederinclusion :: Sign -> Sign -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederinclusion src tgt = Morphism {
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder source = src,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder target = tgt,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | the inverse Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederinverse :: Morphism -> Result Morphism
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederinverse mor = let
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder invertMap = Map.foldWithKey (flip Map.insert) Map.empty
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in return Morphism {
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder source = target mor,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder target = source mor,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder sortMap = invertMap $ sortMap mor,
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder opMap = invertMap $ opMap mor,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder labelMap = invertMap $ labelMap mor
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder-- | the composition of two Morphisms
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maedercompose :: Morphism -> Morphism -> Result Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder | target f /= source g = fail
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder "target of the first and source of the second morphism are different"
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder | otherwise = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- Take SymbolMap |mp| of each Morphism.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- Convert each SymbolMap to a function.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- Compose those functions.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder map'map :: (Morphism -> SymbolMap) -> Symbol -> Symbol
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder map'map mp = mapAsFunction (mp g) . mapAsFunction (mp f)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- Map |x| via the composed SymbolMaps |mp| of both Morphisms.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- Insert the renaming mapping into a SymbolMap.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder insert :: (Morphism -> SymbolMap) -> Symbol -> SymbolMap -> SymbolMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder insert mp x = let y = map'map mp x
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in if x == y then id else Map.insert x y
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- Map each symbol in |items| via the combined SymbolMaps |mp|.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder compose'map :: (Morphism -> SymbolMap) -> (Sign -> SymbolSet) -> SymbolMap
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder compose'map mp items = if Map.null (mp g)
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder -- if the SymbolMap of |g| is empty, we use the one from |f|
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski -- otherwise we start with the SymbolSet from |source f|
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- and construct a combined SymbolMap by applying both
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- SymbolMaps (from |f| and |g|) to each item in |insert|
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else Set.fold (insert mp) Map.empty $ items (source f)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder -- We want a morphism from |source f| to |target g|.
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder mor = inclusion (source f) (target g)
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder in return mor {
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder sortMap = compose'map sortMap getSorts,
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder opMap = compose'map opMap getOps,
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder labelMap = compose'map labelMap getLabels
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-- | check that a Morphism is legal
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederisLegal :: Morphism -> Bool
962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederisLegal mor = let
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder src = source mor
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder tgt = target mor
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder smap = sortMap mor
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder omap = opMap mor
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder lmap = labelMap mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder subset mp items = let mapped = Set.map $ mapAsFunction mp
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in Set.isSubsetOf (mapped $ items src) $ items tgt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder lg'source = Sign.isLegal src
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder lg'sortMap = subset smap getSorts
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder lg'opMap = subset omap getOps
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder lg'labelMap = subset lmap getLabels
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder lg'target = Sign.isLegal tgt
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder in all id [lg'source, lg'sortMap, lg'opMap, lg'labelMap, lg'target]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | check that a Morphism is the identity
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederisIdentity :: Morphism -> Bool
46d766efdf8beaaadf3f34d99c305738064e9216Christian MaederisIdentity mor = source mor == target mor
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- | check that a Morphism is an Inclusion
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederisInclusion :: Morphism -> Bool
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederisInclusion mor = let
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder null'sortMap = Map.null (sortMap mor)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder null'opMap = Map.null (opMap mor)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder null'labelMap = Map.null (labelMap mor)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in all id [null'sortMap, null'opMap, null'labelMap]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | translate a Sentence along a Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermapSentence mor = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder smap = mapSorts (sortMap mor)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder omap = mapOps (opMap mor)
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder lmap = mapLabels (labelMap mor)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in return . lmap . omap . smap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederunion :: Morphism -> Morphism -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederunion m1 m2 = let apply func items = func (items m1) (items m2)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in Morphism {
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder source = apply Sign.union source,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder target = apply Sign.union target,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder sortMap = apply Map.union sortMap,
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder opMap = apply Map.union opMap,
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder labelMap = apply Map.union labelMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedersetTarget :: Sign -> Morphism -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedersetTarget sign morph = morph {target = sign}
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederrenameSorts :: Morphism -> Symbols -> Symbols
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederrenameSorts = mapSorts . sortMap
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder-- extendMorphismSorts :: Morphism -> Qid -> [Qid] -> Morphism
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder-- extendMorphismSorts mor sym syms = let
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- tgt = target mor
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- smap = sortMap mor
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- target = Sign.renameListSort (createRenaming sym syms) tgt,
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- sortMap = extendSortMap sym syms smap
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- createRenaming :: Qid -> [Qid] -> [(Qid, Qid)]
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- createRenaming _ [] = []
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- createRenaming sym (sym' : syms) = (sym', new_sym) : createRenaming sym syms
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- where new_sym = mkSimpleId $ show sym ++ "$" ++ show sym'
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- extendSortMap :: Qid -> [Qid] -> QidMap -> QidMap
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- extendSortMap _ [] sm = sm
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- extendSortMap sym (sym' : syms) sort_map = extendSortMap sym syms sort_map'
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- where new_sym = mkSimpleId $ show sym ++ "$" ++ show sym'
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- sort_map' = Map.fromList $ extendSortList sym' new_sym $ Map.toList sort_map
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- extendSortList :: Qid -> Qid -> [(Qid, Qid)] -> [(Qid, Qid)]
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder-- extendSortList from to [] = [(from, to)]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- extendSortList from to (s@(sym1, sym2) : syms) = if from == sym2
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- then (sym1, to) : syms
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- else s : extendSortList from to syms
f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder-- FIXME: Code duplication!
ac142c1b088711f911018d8108a64be80b2f2a58Christian MaederextendWithSortRenaming :: Symbol -> Symbol -> Morphism -> Morphism
f1ef1c750f805c1732b01001f2b157c0077b808eChristian MaederextendWithSortRenaming src tgt = let
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder add'sort mor = mor { sortMap = Map.insert src tgt $ sortMap mor }
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder use'sort mor = mor { target = Sign.renameSort src tgt $ target mor }
d1012ae182d765c4e6986029d210b9e7b48de205Christian Maeder ren'sort mor = mor { opMap = renameSortOpMap src tgt $ opMap mor }
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in ren'sort . use'sort . add'sort
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- - compose with the new OpMap
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-- - isLegal with the new OpMap
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- - mapSentence with the new OpMap