Morphism.hs revision dd8b4c3053e77395ad1a157b3ad4746a97ddf176
e83ed59502a681713982f25c559aae77a4145734Christian MaederModule : $Header$
eb483f2216949400bfef8f6deb5320f071445626Christian MaederDescription : Morphisms for Maude
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Martin Kuehl, Uni Bremen 2008
eb483f2216949400bfef8f6deb5320f071445626Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
eb483f2216949400bfef8f6deb5320f071445626Christian MaederMaintainer : mkhl@informatik.uni-bremen.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
eb483f2216949400bfef8f6deb5320f071445626Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederDefinition of morphisms for Maude.
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Morphism(..),
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder fromRenamings,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder createInclMorph,
e83ed59502a681713982f25c559aae77a4145734Christian Maederimport qualified Maude.Sign as Sign
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Data.Set as Set
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Data.Map as Map
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport qualified Common.Result as Result
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport Common.Doc as Doc hiding (empty)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype SortMap = SymbolMap
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype OpMap = SymbolMap
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype LabelMap = SymbolMap
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederdata Morphism = Morphism {
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder source :: Sign,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder target :: Sign,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sortMap :: SortMap,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder opMap :: OpMap,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder labelMap :: LabelMap
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder } deriving (Show, Ord, Eq)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederinstance Pretty Morphism where
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder pretty = Doc.text . show
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder-- | extract a Morphism from a list of Renamings
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederfromRenamings :: [Renaming] -> Morphism
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian MaederfromRenamings = foldr insertRenaming empty
2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder-- | extract a Symbol Map from a Morphism
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian MaedersymbolMap :: Morphism -> SymbolMap
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian MaedersymbolMap mor = Map.unions [(sortMap mor), (opMap mor), (labelMap mor)]
1320edfb75af112d509a6ce0a4c02425da7fed4dChristian Maeder-- | insert a Renaming into a Morphism
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiinsertRenaming :: Renaming -> Morphism -> Morphism
eb483f2216949400bfef8f6deb5320f071445626Christian MaederinsertRenaming rename mor = let
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder src = source mor
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder tgt = target mor
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder smap = sortMap mor
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder omap = opMap mor
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder lmap = labelMap mor
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder in case rename of
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder SortRenaming from to -> let
e83ed59502a681713982f25c559aae77a4145734Christian Maeder a = getName from
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder b = getName to
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder source = Sign.insertSort from src,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder target = Sign.insertSort to tgt,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder sortMap = Map.insert a b smap
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski LabelRenaming from to -> let
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski a = getName from
e33e3b425e953236b4617870f995d263ac35b883Christian Maeder b = getName to
e83ed59502a681713982f25c559aae77a4145734Christian Maeder labelMap = Map.insert a b lmap
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder OpRenaming1 from (To to _) -> let
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski -- TODO: handle attrs
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski a = getName from
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski b = getName to
e83ed59502a681713982f25c559aae77a4145734Christian Maeder source = Sign.insertOpName from src,
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski opMap = Map.insert a b omap
e83ed59502a681713982f25c559aae77a4145734Christian Maeder OpRenaming2 from _ _ (To to _) -> let
3a3bbc51abf804d91bc9d8e0f2ce745cfae4c9c7Christian Maeder -- TODO: handle attrs
083679daeba30fce9d60f7170a2cfd9f9c80bfb2Till Mossakowski a = getName from
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder b = getName to
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder source = Sign.insertOpName from src,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder opMap = Map.insert a b omap
1865083b72c1307e9040d78c2743abd5a54ee260Christian Maeder-- | the empty Morphism
eb483f2216949400bfef8f6deb5320f071445626Christian Maederempty :: Morphism
eb483f2216949400bfef8f6deb5320f071445626Christian Maederempty = identity Sign.empty
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | the identity Morphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederidentity :: Sign -> Morphism
c58a5efdb3c9fbc80deb1c69716f09c67292a41dChristian Maederidentity sign = createInclMorph sign sign
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | the inclusion Morphism
eb483f2216949400bfef8f6deb5320f071445626Christian MaedercreateInclMorph :: Sign -> Sign -> Morphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedercreateInclMorph src tgt = Morphism {
e83ed59502a681713982f25c559aae77a4145734Christian Maeder source = src,
e83ed59502a681713982f25c559aae77a4145734Christian Maeder target = tgt,
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | the inverse Morphism
1509ea46b471bef1c5e70864fb1cfc0a5280266bChristian Maederinverse :: Morphism -> Result Morphism
eb483f2216949400bfef8f6deb5320f071445626Christian Maederinverse mor = let
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder inverseMap = Map.foldWithKey (flip Map.insert) Map.empty
afbd86903151121381e4e9d22862136817d7f0f0Christian Maeder in return Morphism {
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder source = (target mor),
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder target = (source mor),
e83ed59502a681713982f25c559aae77a4145734Christian Maeder sortMap = inverseMap (sortMap mor),
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder opMap = inverseMap (opMap mor),
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder labelMap = inverseMap (labelMap mor)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | the composition of two Morphisms
e83ed59502a681713982f25c559aae77a4145734Christian Maeder-- TODO: Ops don't have labels, so Signs don't have labels. so we can ignore the labelMap. Is that correct?
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maedercompose :: Morphism -> Morphism -> Result Morphism
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder | target f /= source g = fail "target of the first and source of the second morphism are different"
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder | otherwise = let
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder apply mp nam = Map.findWithDefault nam nam mp
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder map'map mp = apply (mp g) . apply (mp f)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder insert mp x = let y = map'map mp x
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder in if x == y then id else Map.insert x y
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder compose'map mp items = if Map.null (mp g)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder else Set.fold (insert mp) Map.empty $ items (source f)
e83ed59502a681713982f25c559aae77a4145734Christian Maeder in return Morphism {
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder source = (source f),
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder target = (target g),
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder sortMap = compose'map sortMap getSorts,
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder opMap = compose'map opMap getOps -- ,
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- labelMap = compose'map labelMap getLabels
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | check that a Morphism is legal
e83ed59502a681713982f25c559aae77a4145734Christian Maeder-- TODO: Ops don't have labels, so Signs don't have labels. so we can ignore the labelMap. Is that correct?
e83ed59502a681713982f25c559aae77a4145734Christian MaederisLegal :: Morphism -> Bool
e64aab3e57d843884cd489cc3aa130120a400b05Christian MaederisLegal mor = let
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder src = source mor
e83ed59502a681713982f25c559aae77a4145734Christian Maeder tgt = target mor
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder smap = sortMap mor
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder omap = opMap mor
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder -- lmap = labelMap mor
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder apply mp nam = Map.findWithDefault nam nam mp
25a0b76bc87e80c0f697951d9817862755a71d33Christian Maeder subset mp items = Set.isSubsetOf (Set.map (apply mp) $ items src) (items tgt)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder legal'source = Sign.isLegal src
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder legal'sortMap = subset smap getSorts
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder legal'opMap = subset omap getOps
e83ed59502a681713982f25c559aae77a4145734Christian Maeder -- legal'labelMap = subset lmap getLabels
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder legal'labelMap = True
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder legal'target = Sign.isLegal tgt
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder in all id [legal'source, legal'sortMap, legal'opMap, legal'labelMap, legal'target]
e83ed59502a681713982f25c559aae77a4145734Christian Maeder-- | check that a Morphism is an Inclusion
e83ed59502a681713982f25c559aae77a4145734Christian MaederisInclusion :: Morphism -> Bool
e83ed59502a681713982f25c559aae77a4145734Christian MaederisInclusion mor = let
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder null'sortMap = Map.null (sortMap mor)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder null'opMap = Map.null (opMap mor)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder null'labelMap = Map.null (labelMap mor)
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder in all id [null'sortMap, null'opMap, null'labelMap]
eb483f2216949400bfef8f6deb5320f071445626Christian Maeder-- | translate a Sentence along a Morphism
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimapSentence :: Morphism -> Sentence -> Result.Result Sentence
9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaedermapSentence mor = let
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder smap = mapSorts (sortMap mor)
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder omap = mapOps (opMap mor)
61e38a4f194d3adc66646326c938eb9263a2f39bChristian Maeder lmap = mapLabels (labelMap mor)
9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder in return . lmap . omap . smap