Morphism.hs revision e539e3989075e29a9c3e092a6f686dda164bef60
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 -- fromSignRenamings,
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder -- applyRenamings,
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
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder pretty mor = let
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder pr'pair txt left right = hsep
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian 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
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder in vsep [ smap, omap, lmap ]
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder -- text "\n\nTarget:" <$$> pretty $ target mor
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder-- -- | create a Morphism from an initial signature and a list of Renamings
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder-- fromSignRenamings :: Sign -> [Renaming] -> Morphism
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder-- fromSignRenamings sg rnms = applyRenamings (createInclMorph sg sg) rnms
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder-- applyRenamings :: Morphism -> [Renaming] -> Morphism
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- applyRenamings m rnms = foldr applyRenaming2 (foldr applyRenaming1 m rnms) rnms
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- -- | Rename the signature with the operator renaming and creates a morphism
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- -- with only the operator map. Sort renamings have to be applied to this
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- -- morphism.
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- applyRenaming1 :: Renaming -> Morphism -> Morphism
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- applyRenaming1 rnm mor = let
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder-- tgt = target mor
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- omap = opMap mor
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder-- in case rnm of
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder-- OpRenaming1 from (To to ats) -> let
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder-- a = getName from
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder-- b = getName to
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- target = Sign.renameOp a b ats tgt,
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder-- opMap = allProfilesRenaming a b tgt omap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- OpRenaming2 from ar co (To to ats) -> let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- a = getName from
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- b = getName to
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- ar' = map getName ar
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- co' = getName co
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- p = (ar', co')
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- target = Sign.renameOpProfile a ar' b ats tgt,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- opMap = Map.insertWith (Map.union) a (Map.insert p (b, p) Map.empty) omap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- -- | Rename a signature with the sort and label renamings, and modify
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- -- the given morphism by renaming the sorts in the profiles.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- applyRenaming2 :: Renaming -> Morphism -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- applyRenaming2 rnm mor = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- tgt = target mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- smap = sortMap mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- omap = opMap mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- lmap = labelMap mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- in case rnm of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- SortRenaming from to -> let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- a = getName from
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- b = getName to
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder-- target = Sign.renameSort a b tgt,
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder-- sortMap = Map.insert a b smap,
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder-- opMap = renameSortOpMap a b omap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- LabelRenaming from to -> let
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- a = getName from
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder-- b = getName to
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- target = Sign.renameLabel a b tgt,
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- labelMap = Map.insert a b lmap
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- allProfilesRenaming :: Qid -> Qid -> Sign -> OpMap -> OpMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- allProfilesRenaming from to sg om = om'
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- where om_sg = Sign.ops sg
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- om' = if Map.member from om_sg
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- then Map.insert from (allProfilesRenamingAux to $ fromJust $ Map.lookup from om_sg) om
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- allProfilesRenamingAux :: Qid -> Sign.OpDeclSet -> Map.Map Profile (Qid, Profile)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- allProfilesRenamingAux q = Set.fold (f q) Map.empty
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- where f = \ to (x, y, _) m -> Map.insert (x, y) (to, (x, y)) m
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | Separate Operator and other Renamings.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederpartitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederpartitionRenamings = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder is'op renaming = case renaming of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder OpRenaming1 _ _ -> True
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder OpRenaming2 _ _ _ _ -> True
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in partition is'op
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | create a Morphism from the initial signatures and a list of Renamings
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederfromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian 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 MaederrenamingSymbolsMaybe :: Renaming -> Maybe (Symbol, Symbol)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenamingSymbolsMaybe rename = case rename of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder SortRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LabelRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder OpRenaming1 src (To tgt _) -> Just (asSymbol src, asSymbol tgt)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder OpRenaming2 src dom cod (To tgt _) -> let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder src' = getName src
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder tgt' = getName tgt
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder dom' = map asSymbol dom
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder cod' = asSymbol cod
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in Just (Operator src' dom' cod', Operator tgt' dom' cod')
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TermMap _ _ -> Nothing
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenamingSymbols :: Renaming -> (Symbol, Symbol)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenamingSymbols = fromJust . renamingSymbolsMaybe
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- TODO: Handle Attrs in Op Renamings.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederinsertOpRenaming :: Renaming -> Morphism -> Morphism
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederinsertOpRenaming rename = let
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder syms = renamingSymbols rename
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian 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 ren'sort mor = mor { opMap = uncurry renameSortOpMap syms $ opMap mor }
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder add'sort mor = mor { sortMap = uncurry Map.insert syms $ sortMap 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
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- | extract the SymbolMap of a Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedersymbolMap :: Morphism -> SymbolMap
d591a82b32594f0992b27477cacb00b97226c9c8Christian MaedersymbolMap mor = Map.unions [sortMap mor, opMap mor, labelMap mor]
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder-- | the empty Morphism
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maederempty :: Morphism
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maederempty = identity Sign.empty
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | the identity Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maederidentity :: Sign -> Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian 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,
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder-- | the inverse Morphism
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maederinverse :: Morphism -> Result Morphism
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maederinverse mor = let
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski invertMap = Map.foldWithKey (flip Map.insert) Map.empty
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in return Morphism {
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder source = target mor,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder target = source mor,
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder sortMap = invertMap $ sortMap mor,
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder opMap = invertMap $ opMap mor,
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder labelMap = invertMap $ labelMap mor
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder-- | the composition of two Morphisms
09249711700a6acbc40a2e337688b434d7aafa28Christian Maedercompose :: Morphism -> Morphism -> Result Morphism
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder | target f /= source g = fail
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder "target of the first and source of the second morphism are different"
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder | otherwise = let
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -- map'map takes:
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder -- mp :: Morphism -> SymbolMap
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder -- and returns a function |Symbol -> Symbol| by treating
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -- each SymbolMap as a function and then combining them
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder map'map mp = mapAsFunction (mp g) . mapAsFunction (mp f)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- insert takes:
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- mp :: Morphism -> SymbolMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- x :: Symbol
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- and returns a function |SymbolMap -> SymbolMap| by
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- applying both SymbolMaps (from |f| and |g|) to |x|, then
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- inserting the resulting renaming into the SymbolMap if
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder -- there is one and just leaving it (the SymbolMap) alone
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -- otherwise.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder insert mp x = let y = map'map mp x
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in if x == y then id else Map.insert x y
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder -- compose'map takes:
d1012ae182d765c4e6986029d210b9e7b48de205Christian Maeder -- mp :: Morphism -> SymbolMap
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -- items :: Sign -> SymbolSet
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder -- and constructs a combined SymbolMap from both our Morphisms
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder compose'map mp items = if Map.null (mp g)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -- if the SymbolMap of |g| is empty, we use the one from |f|
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -- 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)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- We want a morphism from |source f| to |target g|,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in return (inclusion (source f) $ target g) {
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder sortMap = compose'map sortMap getSorts -- ,
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- opMap = compose'map opMap getOps -- ,
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder -- labelMap = compose'map labelMap getLabels
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | check that a Morphism is legal
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederisLegal :: Morphism -> Bool
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederisLegal mor = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder src = source mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder tgt = target mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder smap = sortMap mor
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder omap = opMap mor
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder lmap = labelMap mor
ad187062b0009820118c1b773a232e29b879a2faChristian 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
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder lg'opMap = subset omap getOps
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder lg'labelMap = subset lmap getLabels
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder lg'target = Sign.isLegal tgt
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder in all id [lg'source, lg'sortMap, lg'opMap, lg'labelMap, lg'target]
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder-- | check that a Morphism is the identity
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederisIdentity :: Morphism -> Bool
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederisIdentity mor = source mor == target mor
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- | check that a Morphism is an Inclusion
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederisInclusion :: Morphism -> Bool
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederisInclusion mor = let
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder null'sortMap = Map.null (sortMap mor)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder null'opMap = Map.null (opMap mor)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder null'labelMap = Map.null (labelMap mor)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder in all id [null'sortMap, null'opMap, null'labelMap]
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- | translate a Sentence along a Morphism
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermapSentence mor = let
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder smap = mapSorts (sortMap mor)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder omap = mapOps (opMap mor)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder lmap = mapLabels (labelMap mor)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in return . lmap . omap . smap
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maederunion :: Morphism -> Morphism -> Morphism
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederunion m1 m2 = let apply func items = func (items m1) (items m2)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in Morphism {
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder source = apply Sign.union source,
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder target = apply Sign.union target,
f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder sortMap = apply Map.union sortMap,
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder opMap = apply Map.union opMap,
f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder labelMap = apply Map.union labelMap
d1012ae182d765c4e6986029d210b9e7b48de205Christian MaedersetTarget :: Sign -> Morphism -> Morphism
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedersetTarget sign morph = morph {target = sign}
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenameSorts :: Morphism -> Symbols -> Symbols
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrenameSorts = mapSorts . sortMap
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- extendMorphismSorts :: Morphism -> Qid -> [Qid] -> Morphism
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- extendMorphismSorts mor sym syms = let
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder-- tgt = target mor
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- smap = sortMap mor
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- target = Sign.renameListSort (createRenaming sym syms) tgt,
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder-- sortMap = extendSortMap sym syms smap
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- createRenaming :: Qid -> [Qid] -> [(Qid, Qid)]
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- createRenaming _ [] = []
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- createRenaming sym (sym' : syms) = (sym', new_sym) : createRenaming sym syms
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- where new_sym = mkSimpleId $ show sym ++ "$" ++ show sym'
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- extendSortMap :: Qid -> [Qid] -> QidMap -> QidMap
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- extendSortMap _ [] sm = sm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- extendSortMap sym (sym' : syms) sort_map = extendSortMap sym syms sort_map'
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- where new_sym = mkSimpleId $ show sym ++ "$" ++ show sym'
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- sort_map' = Map.fromList $ extendSortList sym' new_sym $ Map.toList sort_map
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- extendSortList :: Qid -> Qid -> [(Qid, Qid)] -> [(Qid, Qid)]
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- extendSortList from to [] = [(from, to)]
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- extendSortList from to (s@(sym1, sym2) : syms) = if from == sym2
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder-- then (sym1, to) : syms
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- else s : extendSortList from to syms
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- extendWithSortRenaming :: Qid -> Qid -> Morphism -> Morphism
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- extendWithSortRenaming from to mor = let
ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder-- tgt = target mor
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- smap = sortMap mor
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder-- omap = opMap mor
-- target = Sign.renameSort from to tgt,
-- sortMap = Map.insert from to smap,