a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- |

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : Morphisms for Maude

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Martin Kuehl, Uni Bremen 2008

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : mkhl@informatik.uni-bremen.de

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : experimental

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederDefinition of morphisms for Maude.

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett-}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Ref.

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ...

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

ad270004874ce1d0697fb30d7309f180553bb315Christian Maedermodule Maude.Morphism (

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Morphism(..),

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach fromRenamings,

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett symbolMap,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett empty,

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett identity,

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett inverse,

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett createInclMorph,

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett mapSentence

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett) where

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport Maude.AS_Maude

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport Maude.Symbol

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Maude.Sentence

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettimport Maude.Meta.HasSorts

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettimport Maude.Meta.HasOps

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport Maude.Meta.HasLabels

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport Maude.Sign (Sign)

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport qualified Maude.Sign as Sign

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport qualified Data.Map as Map

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettimport Common.Result (Result)

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettimport qualified Common.Result as Result

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettimport Common.Doc as Doc hiding (empty)

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettimport Common.DocUtils

9f6d67c9b0e2661e7967b435f17a27687929144fAndy Gimblett

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimbletttype SortMap = SymbolMap

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimbletttype OpMap = SymbolMap

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimbletttype LabelMap = SymbolMap

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettdata Morphism = Morphism {

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett source :: Sign,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett target :: Sign,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sortMap :: SortMap,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett opMap :: OpMap,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett labelMap :: LabelMap

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett } deriving (Show, Ord, Eq)

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettinstance Pretty Morphism where

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett pretty = Doc.text . show

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- | extract a Morphism from a list of Renamings

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettfromRenamings :: [Renaming] -> Morphism

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy GimblettfromRenamings = foldr insertRenaming empty

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- | extract a Symbol Map from a Morphism

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettsymbolMap :: Morphism -> SymbolMap

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettsymbolMap mor = Map.unions [(sortMap mor), (opMap mor), (labelMap mor)]

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- | insert a Renaming into a Morphism

9f6d67c9b0e2661e7967b435f17a27687929144fAndy GimblettinsertRenaming :: Renaming -> Morphism -> Morphism

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettinsertRenaming rename mor = let

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett src = source mor

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett tgt = target mor

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett smap = sortMap mor

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett omap = opMap mor

9f6d67c9b0e2661e7967b435f17a27687929144fAndy Gimblett lmap = labelMap mor

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett in case rename of

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett SortRenaming from to -> let

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett a = sortName from

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett b = sortName to

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett in mor {

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett source = Sign.insertSort from src,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett target = Sign.insertSort to tgt,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett sortMap = Map.insert a b smap

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett }

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett LabelRenaming from to -> let

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett a = labelName from

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett b = labelName to

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett in mor {

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett labelMap = Map.insert a b lmap

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett }

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett OpRenaming1 from (To to _) -> let

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett a = opName from

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett b = opName to

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett in mor {

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett source = Sign.insertOpName from src,

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett target = Sign.insertOpName to tgt,

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett opMap = Map.insert a b omap

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett }

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett OpRenaming2 from _ _ (To to _) -> let

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett a = opName from

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach b = opName to

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett in mor {

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett source = Sign.insertOpName from src,

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett target = Sign.insertOpName to tgt,

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblett opMap = Map.insert a b omap

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett }

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- | the empty Morphism

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettempty :: Morphism

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettempty = identity Sign.empty

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- | the identity Morphism

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettidentity :: Sign -> Morphism

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblettidentity sign = createInclMorph sign sign

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | the inclusion Morphism

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy GimblettcreateInclMorph :: Sign -> Sign -> Morphism

e54c5af823b9775dd2c058185ea5bdf7593950faAndy GimblettcreateInclMorph src tgt = Morphism {

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett source = src,

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett target = tgt,

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett sortMap = Map.empty,

eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder opMap = Map.empty,

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski labelMap = Map.empty

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett }

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski-- | the inverse Morphism

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiinverse :: Morphism -> Result Morphism

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblettinverse mor = let

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett inverseMap = Map.foldWithKey (flip Map.insert) Map.empty

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett in return Morphism {

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett source = (target mor),

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett target = (source mor),

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett sortMap = inverseMap (sortMap mor),

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett opMap = inverseMap (opMap mor),

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder labelMap = inverseMap (labelMap mor)

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski }

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski-- -- | the composition of two Morphisms

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett-- compose :: Morphism -> Morphism -> Result Morphism

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett-- compose f g

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | target f /= source g = fail "target of the first and source of the second morphism are different"

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- | otherwise = let

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- apply mp nam = Map.findWithDefault nam nam mp

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski-- map'map mp = apply (mp g) . apply (mp f)

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski-- insert mp x = let y = map'map mp x

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett-- in if x == y then id else Map.insert x y

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- compose'map mp items = if Map.null (mp g)

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett-- then mp f

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett-- else Set.fold (insert mp) Map.empty $ items (source f)

-- in return Morphism {

-- source = (source f),

-- target = (target g),

-- sortMap = compose'map sortMap getSorts,

-- opMap = compose'map opMap getOps,

-- labelMap = compose'map labelMap getLabels

-- }

-- -- | check that a Morphism is legal

-- isLegal :: Morphism -> Bool

-- isLegal mor = let

-- src = source mor

-- tgt = target mor

-- smap = sortMap mor

-- omap = opMap mor

-- lmap = labelMap mor

-- apply mp nam = Map.findWithDefault nam nam mp

-- subset mp items = Set.isSubsetOf (Set.map (apply mp) $ items src) (items tgt)

-- legal'source = Sign.isLegal src

-- legal'sortMap = subset smap getSorts

-- legal'opMap = subset omap getOps

-- legal'labelMap = subset lmap getLabels

-- legal'target = Sign.isLegal tgt

-- in all id [legal'source, legal'sortMap, legal'opMap, legal'labelMap, legal'target]

-- | translate a Sentence along a Morphism

mapSentence :: Morphism -> Sentence -> Result.Result Sentence

mapSentence mor = let

smap = mapSorts (sortMap mor)

omap = mapOps (opMap mor)

lmap = mapLabels (labelMap mor)

in return . lmap . omap . smap

-- extract the name from a Sort, Op or Label

sortName :: Sort -> Qid

sortName (SortId name) = name

opName :: OpId -> Qid

opName (OpId name) = name

labelName :: LabelId -> Qid

labelName (LabelId name) = name