Morphism.hs revision ed714e0ab59be1431a68f565b19ce3a6863ad747
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiModule : $Header$
d3f2015ae170a15e5b57d4880ded53073d725ac0Till MossakowskiDescription : Morphisms for Maude
e7eefd526faedd63acb8f91de5793368cfe67655Klaus LuettichCopyright : (c) Martin Kuehl, Uni Bremen 2008-2009
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 -- fromSignRenamings,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski -- applyRenamings,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski fromSignsRenamings,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski -- extendMorphismSorts,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski -- extendWithSortRenaming,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport Maude.Sentence (Sentence)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport qualified Maude.Sign as Sign
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowskiimport qualified Maude.Sentence as Sen
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiimport Data.List (partition)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiimport Data.Maybe (fromJust)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiimport qualified Data.Set as Set
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiimport qualified Data.Map as Map
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiimport qualified Common.Result as Result
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiimport Common.Doc hiding (empty)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiimport Common.DocUtils (Pretty(..))
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitype SortMap = SymbolMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitype OpMap = SymbolMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskitype LabelMap = SymbolMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskidata Morphism = Morphism {
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski source :: Sign,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski target :: Sign,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski sortMap :: SortMap,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski opMap :: OpMap,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski labelMap :: LabelMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski } deriving (Show, Ord, Eq)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowskiinstance Pretty Morphism where
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pretty mor = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pr'pair txt left right = hsep
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski [txt, pretty left, text "to", pretty right]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pr'ops src tgt = pr'pair (text "op") src (getName tgt)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski pr'map fun = vsep . map (uncurry fun) . Map.toList
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski smap = pr'map (pr'pair $ text "sort") $ sortMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski omap = pr'map pr'ops $ opMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski lmap = pr'map (pr'pair $ text "label") $ labelMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in vsep [ smap, omap, lmap ]
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski -- text "\n\nTarget:" <$$> pretty $ target mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- -- | create a Morphism from an initial signature and a list of Renamings
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- fromSignRenamings :: Sign -> [Renaming] -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- fromSignRenamings sg rnms = applyRenamings (createInclMorph sg sg) rnms
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- applyRenamings :: Morphism -> [Renaming] -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- applyRenamings m rnms = foldr applyRenaming2 (foldr applyRenaming1 m rnms) rnms
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- -- | Rename the signature with the operator renaming and creates a morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- -- with only the operator map. Sort renamings have to be applied to this
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- -- morphism.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- applyRenaming1 :: Renaming -> Morphism -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- applyRenaming1 rnm mor = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- tgt = target mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- omap = opMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- in case rnm of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- OpRenaming1 from (To to ats) -> let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- a = getName from
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- b = getName to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- target = Sign.renameOp a b ats tgt,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- opMap = allProfilesRenaming a b tgt omap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- OpRenaming2 from ar co (To to ats) -> let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- a = getName from
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- b = getName to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- ar' = map getName ar
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- co' = getName co
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- p = (ar', co')
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- target = Sign.renameOpProfile a ar' b ats tgt,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- opMap = Map.insertWith (Map.union) a (Map.insert p (b, p) Map.empty) omap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- -- | Rename a signature with the sort and label renamings, and modify
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- -- the given morphism by renaming the sorts in the profiles.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- applyRenaming2 :: Renaming -> Morphism -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- applyRenaming2 rnm mor = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- tgt = target mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- smap = sortMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- omap = opMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- lmap = labelMap mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- in case rnm of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- SortRenaming from to -> let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- a = getName from
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- b = getName to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- target = Sign.renameSort a b tgt,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- sortMap = Map.insert a b smap,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- opMap = renameSortOpMap a b omap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- LabelRenaming from to -> let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- a = getName from
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- b = getName to
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- target = Sign.renameLabel a b tgt,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- labelMap = Map.insert a b lmap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- allProfilesRenaming :: Qid -> Qid -> Sign -> OpMap -> OpMap
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- allProfilesRenaming from to sg om = om'
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- where om_sg = Sign.ops sg
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- om' = if Map.member from om_sg
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- then Map.insert from (allProfilesRenamingAux to $ fromJust $ Map.lookup from om_sg) om
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- allProfilesRenamingAux :: Qid -> Sign.OpDeclSet -> Map.Map Profile (Qid, Profile)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- allProfilesRenamingAux q = Set.fold (f q) Map.empty
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- where f = \ to (x, y, _) m -> Map.insert (x, y) (to, (x, y)) m
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | Separate Operator and other Renamings.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskipartitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskipartitionRenamings = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski is'op renaming = case renaming of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski OpRenaming1 _ _ -> True
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski OpRenaming2 _ _ _ _ -> True
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in partition is'op
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- | create a Morphism from the initial signatures and a list of Renamings
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskifromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskifromSignsRenamings sign1 sign2 rens = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (ops, rest) = partitionRenamings rens
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski add'ops = flip (foldr insertOpRenaming) ops
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski add'rest = flip (foldr insertRenaming) rest
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski mor = inclusion sign1 sign2
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in add'rest . add'ops $ mor
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskirenamingSymbolsMaybe :: Renaming -> Maybe (Symbol, Symbol)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskirenamingSymbolsMaybe rename = case rename of
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski SortRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski LabelRenaming src tgt -> Just (asSymbol src, asSymbol tgt)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski OpRenaming1 src (To tgt _) -> Just (asSymbol src, asSymbol tgt)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski OpRenaming2 src dom cod (To tgt _) -> let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski src' = getName src
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski tgt' = getName tgt
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski dom' = map asSymbol dom
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski cod' = asSymbol cod
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in Just (Operator src' dom' cod', Operator tgt' dom' cod')
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski TermMap _ _ -> Nothing
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskirenamingSymbols :: Renaming -> (Symbol, Symbol)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskirenamingSymbols = fromJust . renamingSymbolsMaybe
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski-- TODO: Handle Attrs in Op Renamings.
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiinsertOpRenaming :: Renaming -> Morphism -> Morphism
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till MossakowskiinsertOpRenaming rename = let
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski syms = renamingSymbols rename
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski add'op mor = mor { opMap = uncurry Map.insert syms $ opMap mor }
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski in case rename of
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski OpRenaming1 _ _ -> add'op
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski OpRenaming2 _ _ _ _ -> add'op
30256573a343132354b122097b0ee1215dda1364Till MossakowskiinsertRenaming :: Renaming -> Morphism -> Morphism
30256573a343132354b122097b0ee1215dda1364Till MossakowskiinsertRenaming rename = let
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski syms = renamingSymbols rename
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski ren'sort mor = mor { opMap = uncurry renameSortOpMap syms $ opMap mor }
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski add'sort mor = mor { sortMap = uncurry Map.insert syms $ sortMap mor }
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski add'labl mor = mor { labelMap = uncurry Map.insert syms $ labelMap mor }
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski in case rename of
30256573a343132354b122097b0ee1215dda1364Till Mossakowski SortRenaming _ _ -> ren'sort . add'sort
30256573a343132354b122097b0ee1215dda1364Till Mossakowski LabelRenaming _ _ -> add'labl
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski-- | Rename sorts in the profiles of an operator map.
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskirenameSortOpMap :: Symbol -> Symbol -> OpMap -> OpMap
2c66eeb1cc9ad264525901f10c35c66638f91865Till MossakowskirenameSortOpMap from to = Map.map $ mapSorts $ Map.singleton from to
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | extract the SymbolMap of a Morphism
30256573a343132354b122097b0ee1215dda1364Till MossakowskisymbolMap :: Morphism -> SymbolMap
30256573a343132354b122097b0ee1215dda1364Till MossakowskisymbolMap mor = Map.unions [sortMap mor, opMap mor, labelMap mor]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | the empty Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiempty :: Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiempty = identity Sign.empty
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | the identity Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiidentity :: Sign -> Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiidentity sign = inclusion sign sign
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | the inclusion Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinclusion :: Sign -> Sign -> Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinclusion src tgt = Morphism {
30256573a343132354b122097b0ee1215dda1364Till Mossakowski source = src,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski target = tgt,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | the inverse Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinverse :: Morphism -> Result Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiinverse mor = let
30256573a343132354b122097b0ee1215dda1364Till Mossakowski invertMap = Map.foldWithKey (flip Map.insert) Map.empty
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in return Morphism {
30256573a343132354b122097b0ee1215dda1364Till Mossakowski source = target mor,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski target = source mor,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski sortMap = invertMap $ sortMap mor,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski opMap = invertMap $ opMap mor,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski labelMap = invertMap $ labelMap mor
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | the composition of two Morphisms
30256573a343132354b122097b0ee1215dda1364Till Mossakowskicompose :: Morphism -> Morphism -> Result Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | target f /= source g = fail
30256573a343132354b122097b0ee1215dda1364Till Mossakowski "target of the first and source of the second morphism are different"
30256573a343132354b122097b0ee1215dda1364Till Mossakowski | otherwise = let
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- Take SymbolMap |mp| of each Morphism.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- Convert each SymbolMap to a function.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- Compose those functions.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski map'map :: (Morphism -> SymbolMap) -> Symbol -> Symbol
30256573a343132354b122097b0ee1215dda1364Till Mossakowski map'map mp = mapAsFunction (mp g) . mapAsFunction (mp f)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- Map |x| via the composed SymbolMaps |mp| of both Morphisms.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- Insert the renaming mapping into a SymbolMap.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski insert :: (Morphism -> SymbolMap) -> Symbol -> SymbolMap -> SymbolMap
30256573a343132354b122097b0ee1215dda1364Till Mossakowski insert mp x = let y = map'map mp x
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in if x == y then id else Map.insert x y
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- Map each symbol in |items| via the combined SymbolMaps |mp|.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski compose'map :: (Morphism -> SymbolMap) -> (Sign -> SymbolSet) -> SymbolMap
30256573a343132354b122097b0ee1215dda1364Till Mossakowski compose'map mp items = if Map.null (mp g)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- if the SymbolMap of |g| is empty, we use the one from |f|
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- otherwise we start with the SymbolSet from |source f|
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- and construct a combined SymbolMap by applying both
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- SymbolMaps (from |f| and |g|) to each item in |insert|
30256573a343132354b122097b0ee1215dda1364Till Mossakowski else Set.fold (insert mp) Map.empty $ items (source f)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski -- We want a morphism from |source f| to |target g|.
30256573a343132354b122097b0ee1215dda1364Till Mossakowski mor = inclusion (source f) (target g)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in return mor {
30256573a343132354b122097b0ee1215dda1364Till Mossakowski sortMap = compose'map sortMap getSorts,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski opMap = compose'map opMap getOps,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski labelMap = compose'map labelMap getLabels
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | check that a Morphism is legal
30256573a343132354b122097b0ee1215dda1364Till MossakowskiisLegal :: Morphism -> Bool
30256573a343132354b122097b0ee1215dda1364Till MossakowskiisLegal mor = let
30256573a343132354b122097b0ee1215dda1364Till Mossakowski src = source mor
30256573a343132354b122097b0ee1215dda1364Till Mossakowski tgt = target mor
30256573a343132354b122097b0ee1215dda1364Till Mossakowski smap = sortMap mor
30256573a343132354b122097b0ee1215dda1364Till Mossakowski omap = opMap mor
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lmap = labelMap mor
30256573a343132354b122097b0ee1215dda1364Till Mossakowski subset mp items = let mapped = Set.map $ mapAsFunction mp
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in Set.isSubsetOf (mapped $ items src) $ items tgt
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lg'source = Sign.isLegal src
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lg'sortMap = subset smap getSorts
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lg'opMap = subset omap getOps
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lg'labelMap = subset lmap getLabels
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lg'target = Sign.isLegal tgt
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in all id [lg'source, lg'sortMap, lg'opMap, lg'labelMap, lg'target]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | check that a Morphism is the identity
30256573a343132354b122097b0ee1215dda1364Till MossakowskiisIdentity :: Morphism -> Bool
30256573a343132354b122097b0ee1215dda1364Till MossakowskiisIdentity mor = source mor == target mor
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | check that a Morphism is an Inclusion
30256573a343132354b122097b0ee1215dda1364Till MossakowskiisInclusion :: Morphism -> Bool
30256573a343132354b122097b0ee1215dda1364Till MossakowskiisInclusion mor = let
30256573a343132354b122097b0ee1215dda1364Till Mossakowski null'sortMap = Map.null (sortMap mor)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski null'opMap = Map.null (opMap mor)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski null'labelMap = Map.null (labelMap mor)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in all id [null'sortMap, null'opMap, null'labelMap]
30256573a343132354b122097b0ee1215dda1364Till Mossakowski-- | translate a Sentence along a Morphism
30256573a343132354b122097b0ee1215dda1364Till MossakowskimapSentence :: Morphism -> Sentence -> Result Sentence
30256573a343132354b122097b0ee1215dda1364Till MossakowskimapSentence mor = let
30256573a343132354b122097b0ee1215dda1364Till Mossakowski smap = mapSorts (sortMap mor)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski omap = mapOps (opMap mor)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski lmap = mapLabels (labelMap mor)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in return . lmap . omap . smap
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiunion :: Morphism -> Morphism -> Morphism
30256573a343132354b122097b0ee1215dda1364Till Mossakowskiunion m1 m2 = let apply func items = func (items m1) (items m2)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski in Morphism {
30256573a343132354b122097b0ee1215dda1364Till Mossakowski source = apply Sign.union source,
30256573a343132354b122097b0ee1215dda1364Till Mossakowski target = apply Sign.union target,
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder sortMap = apply Map.union sortMap,
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder opMap = apply Map.union opMap,
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder labelMap = apply Map.union labelMap
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaedersetTarget :: Sign -> Morphism -> Morphism
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaedersetTarget sign morph = morph {target = sign}
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaederrenameSorts :: Morphism -> Symbols -> Symbols
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian MaederrenameSorts = mapSorts . sortMap
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder-- extendMorphismSorts :: Morphism -> Qid -> [Qid] -> Morphism
4b41220e2b76251e0bb0760c016e79994bb2c2bbChristian Maeder-- extendMorphismSorts mor sym syms = let
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa-- tgt = target mor
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa-- smap = sortMap mor
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa-- target = Sign.renameListSort (createRenaming sym syms) tgt,
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa-- sortMap = extendSortMap sym syms smap
dd29aea0190ac8707f2a0896a4a4b8bb2aac13ffEugen Kuksa-- createRenaming :: Qid -> [Qid] -> [(Qid, Qid)]
-- target = Sign.renameSort from to tgt,
-- sortMap = Map.insert from to smap,