Morphism.hs revision 18328fcbfe4296582227d42fdcf363f5a0fb8921
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiModule : $Header$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDescription : Morphisms for Maude
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichCopyright : (c) Martin Kuehl, Uni Bremen 2008
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiMaintainer : mkhl@informatik.uni-bremen.de
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiStability : experimental
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiPortability : portable
89118fd658073a87eddf4ead4bb63c6adb30550dTill MossakowskiDefinition of morphisms for Maude.
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Morphism(..),
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski fromRenamingSet,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Maude.Sign hiding (empty, isLegal)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport qualified Maude.Sign as Sign (empty, isLegal)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport qualified Data.Map as Map
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport qualified Data.Set as Set
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport qualified Common.Result as Result
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitype SortMap = Map.Map Qid Qid
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitype OpMap = Map.Map Qid Qid
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskitype LabelMap = Map.Map Qid Qid
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskidata Morphism = Morphism {
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski source :: Sign,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski target :: Sign,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski sortMap :: SortMap,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski opMap :: OpMap,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski labelMap :: LabelMap
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski } deriving (Show, Eq)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | extract a Morphism from a RenamingSet
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskifromRenamingSet :: RenamingSet -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskifromRenamingSet = Set.fold insertRenaming empty
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | insert a Renaming into a Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiinsertRenaming :: Renaming -> Morphism -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiinsertRenaming rename mor = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski src = source mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski tgt = target mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski smap = sortMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski omap = opMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski lmap = labelMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski op nam as cod dom = Op { op'name = nam, op'range = cod, op'domain = dom, op'attrs = as }
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in case rename of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Sort'To {from = a, to = b} -> mor {
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski source = insertSort a src,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski target = insertSort b tgt,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski sortMap = Map.insert a b smap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Op'To {from = a, to = b} -> mor {
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski source = insertOpName a src,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski target = insertOpName b tgt,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski opMap = Map.insert a b omap
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange Op'Type'To {from = a, range = cod, domain = dom, to = b, attrs = as} -> mor {
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski source = insertOp (op a as cod dom) src,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski target = insertOp (op b as cod dom) tgt,
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange opMap = Map.insert a b omap
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange Label'To {from = a, to = b} -> mor {
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange labelMap = Map.insert a b lmap
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange-- | the empty Morphism
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Langeempty :: Morphism
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Langeempty = identity Sign.empty
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Lange-- | the identity Morphism
a22936ffa58b0b92b957098a1ebc75a22cc48f85Christoph Langeidentity :: Sign -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiidentity sign = Morphism {
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski source = sign,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski target = sign,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | the composition of two Morphisms
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskicompose :: Morphism -> Morphism -> Result.Result Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski | (target f) /= (source g) = fail "target of the first and source of the second morphism are different"
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski | otherwise = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski apply mp nam = Map.findWithDefault nam nam mp
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski map'map mp = apply (mp g) . apply (mp f)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski insert mp x = let y = map'map mp x
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in if x == y then id else Map.insert x y
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski compose'map mp items = if Map.null (mp g)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski else Set.fold (insert mp) Map.empty $ items (source f)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in return Morphism {
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski source = (source f),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski target = (target g),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski sortMap = compose'map sortMap sorts,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski opMap = compose'map opMap opNames,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski labelMap = compose'map labelMap labels
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | check that a Morphism is legal
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiisLegal :: Morphism -> Bool
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiisLegal mor = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski src = source mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski tgt = target mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski smap = sortMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski omap = opMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski lmap = labelMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski apply mp nam = Map.findWithDefault nam nam mp
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski subset mp items = Set.isSubsetOf (Set.map (apply mp) $ items src) (items tgt)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski legal'source = Sign.isLegal src
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski legal'sortMap = subset smap sorts
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski legal'opMap = subset omap opNames
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski legal'labelMap = subset lmap labels
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski legal'target = Sign.isLegal tgt
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in all id [legal'source, legal'sortMap, legal'opMap, legal'labelMap, legal'target]