Morphism.hs revision 3f9cd04710597ee787032a371f33861640ab2abe
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederDescription : Morphisms for Maude
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Martin Kuehl, Uni Bremen 2008
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederMaintainer : mkhl@informatik.uni-bremen.de
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : experimental
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiDefinition of morphisms for Maude.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Morphism(..),
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski fromRenamings,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Maude.Sign as Sign
38f350357e92da312d2c344352180b3dc5c1fc8aTill Mossakowskiimport Data.Typeable (Typeable)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Data.Set as Set
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maederimport qualified Data.Map as Map
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Data.Foldable as Fold
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Common.Result as Result
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype SortMap = Map Token Token
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype OpMap = Map Token Token
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskitype LabelMap = Map Token Token
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maederdata Morphism = Morphism {
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder source :: Sign,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target :: Sign,
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski sortMap :: SortMap,
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski opMap :: OpMap,
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski labelMap :: LabelMap
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski } deriving Show--(Show, Eq, Ord, Typeable)
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- | extract a Morphism from a list of Renamings
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskifromRenamings :: [Renaming] -> Morphism
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskifromRenamings = foldr insertRenaming empty
2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski-- | extract a Symbol Map from a Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskisymbolMap :: Morphism -> Map Token Token
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskisymbolMap mor = Map.unions [(sortMap mor), (opMap mor), (labelMap mor)]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | insert a Renaming into a Morphism
38f350357e92da312d2c344352180b3dc5c1fc8aTill MossakowskiinsertRenaming :: Renaming -> Morphism -> Morphism
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill MossakowskiinsertRenaming rename mor = let
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski src = source mor
9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowski tgt = target mor
9a36df4f63e0214bc0b4aef9b388c8d4e48632bbTill Mossakowski smap = sortMap mor
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski omap = opMap mor
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski lmap = labelMap mor
62867c8459918ce0a96960093eb43d758b97a603Till Mossakowski in case rename of
5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski (SortRenaming from to) -> let
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski a = sortName from
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski b = sortName to
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source = Sign.insertSort from src,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target = Sign.insertSort to tgt,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sortMap = Map.insert a b smap
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski (LabelRenaming from to) -> let
0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski a = labelName from
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski b = labelName to
586af0e9490a14dd3075095692b584c652584875Till Mossakowski labelMap = Map.insert a b lmap
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski (OpRenaming1 from (To to _)) -> let
586af0e9490a14dd3075095692b584c652584875Till Mossakowski a = opName from
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder b = opName to
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source = Sign.insertOpName from src,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski opMap = Map.insert a b omap
586af0e9490a14dd3075095692b584c652584875Till Mossakowski (OpRenaming2 from _ _ (To to _)) -> let
70066d44c2dc2f151e44dd0b98955c2dcd35b70bTill Mossakowski a = opName from
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski b = opName to
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source = Sign.insertOpName from src,
586af0e9490a14dd3075095692b584c652584875Till Mossakowski opMap = Map.insert a b omap
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | the empty Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiempty :: Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiempty = identity Sign.empty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | the identity Morphism
586af0e9490a14dd3075095692b584c652584875Till Mossakowskiidentity :: Sign -> Morphism
586af0e9490a14dd3075095692b584c652584875Till Mossakowskiidentity sign = Morphism {
586af0e9490a14dd3075095692b584c652584875Till Mossakowski source = sign,
586af0e9490a14dd3075095692b584c652584875Till Mossakowski target = sign,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- -- | the composition of two Morphisms
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- compose :: Morphism -> Morphism -> Result Morphism
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- compose f g
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | target f /= source g = fail "target of the first and source of the second morphism are different"
8db2d2c5a8df6dd6d7302bc59577150b87237940Till Mossakowski-- | otherwise = let
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- apply mp nam = Map.findWithDefault nam nam mp
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder-- map'map mp = apply (mp g) . apply (mp f)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- insert mp x = let y = map'map mp x
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- in if x == y then id else Map.insert x y
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- compose'map mp items = if Map.null (mp g)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- else Set.fold (insert mp) Map.empty $ items (source f)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- in return Morphism {
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- source = (source f),
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- target = (target g),
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- sortMap = compose'map sortMap getSorts,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- opMap = compose'map opMap getOps,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- labelMap = compose'map labelMap getLabels
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | the inverse of a Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinverse :: Morphism -> Result Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinverse mor = let
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder inverseMap = Map.foldWithKey (flip Map.insert) Map.empty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in return Morphism {
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski source = (target mor),
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski target = (source mor),
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sortMap = inverseMap (sortMap mor),
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski opMap = inverseMap (opMap mor),
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski labelMap = inverseMap (labelMap mor)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- -- | check that a Morphism is legal
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- isLegal :: Morphism -> Bool
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- isLegal mor = let
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- src = source mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- tgt = target mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- smap = sortMap mor
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- omap = opMap mor
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski-- lmap = labelMap mor
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski-- apply mp nam = Map.findWithDefault nam nam mp
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski-- subset mp items = Set.isSubsetOf (Set.map (apply mp) $ items src) (items tgt)
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski-- legal'source = Sign.isLegal src
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- legal'sortMap = subset smap getSorts
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- legal'opMap = subset omap getOps
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- legal'labelMap = subset lmap getLabels
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- legal'target = Sign.isLegal tgt
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- in all id [legal'source, legal'sortMap, legal'opMap, legal'labelMap, legal'target]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- extract the name from a Sort, Op or Label
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaedersortName (SortId name) = name
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaederopName (OpId name) = name
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaederlabelName (LabelId name) = name