9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett{- |

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettModule : $Header$

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettDescription : Morphisms for Maude

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettCopyright : (c) Martin Kuehl, Uni Bremen 2008

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettMaintainer : mkhl@informatik.uni-bremen.de

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettStability : experimental

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettPortability : portable

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettDefinition of morphisms for Maude.

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett-}

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett{-

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett Ref.

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett ...

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett-}

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblettmodule Maude.Morphism (

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett Morphism(..),

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett fromSignRenamings,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett fromSignsRenamings,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett symbolMap,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett empty,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett identity,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett isIdentity,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett createInclMorph,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett inverse,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett compose,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett isLegal,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett isInclusion,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett mapSentence,

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett renameSorts,

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett union,

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett setTarget,

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett extendMorphismSorts,

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett addQualification

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett) where

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblettimport Maude.AS_Maude

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport Maude.Symbol

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport Maude.Sentence

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport Maude.Meta

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport Maude.Util

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport Maude.Printing

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport Maude.Sign (Sign)

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettimport qualified Maude.Sign as Sign

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblettimport qualified Data.Set as Set

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport qualified Data.Map as Map

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettimport Common.Result (Result)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettimport qualified Common.Result as Result

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettimport Common.Doc as Doc hiding (empty)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettimport Common.DocUtils

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettimport Common.Id (mkSimpleId)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblettimport Data.Maybe

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimbletttype Profile = ([Qid], Qid)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimbletttype QidMap = Map.Map Qid Qid

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimbletttype SortMap = QidMap

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimbletttype OpMap = Map.Map Qid (Map.Map Profile (Qid, Profile))

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimbletttype LabelMap = QidMap

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblettdata Morphism = Morphism {

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett source :: Sign,

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett target :: Sign,

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett sortMap :: SortMap,

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett opMap :: OpMap,

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett labelMap :: LabelMap

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett } deriving (Show, Ord, Eq)

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblettinstance Pretty Morphism where

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett pretty m = Doc.text $ printMorphism (sortMap m) (opMap m) (labelMap m)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett ++ "\n\nTarget:\n" ++ printSign (Sign.sorts sign)

b34e5090387d45b3a35f88eaa23477a83d2a2962Andy Gimblett (Sign.subsorts sign) (Sign.ops sign)

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett where sign = target m

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett-- | create a Morphism from an initial signature and a list of Renamings

d40dd10adffcf341489a1310092fcc99de75f225Andy GimblettfromSignRenamings :: Sign -> [Renaming] -> Morphism

d40dd10adffcf341489a1310092fcc99de75f225Andy GimblettfromSignRenamings sg rnms = applyRenamings (createInclMorph sg sg) rnms

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettapplyRenamings :: Morphism -> [Renaming] -> Morphism

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettapplyRenamings m rnms = foldr applyRenaming2 (foldr applyRenaming1 m rnms) rnms

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett-- | Rename the signature with the operator renaming and creates a morphism

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett-- with only the operator map. Sort renamings have to be applied to this

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett-- morphism.

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettapplyRenaming1 :: Renaming -> Morphism -> Morphism

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettapplyRenaming1 rnm mor = let

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett tgt = target mor

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett omap = opMap mor

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett in case rnm of

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett OpRenaming1 from (To to ats) -> let

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett a = getName from

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett b = getName to

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett in mor {

d40dd10adffcf341489a1310092fcc99de75f225Andy Gimblett target = Sign.renameOp a b ats tgt,

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett opMap = allProfilesRenaming a b tgt omap

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett }

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett OpRenaming2 from ar co (To to ats) -> let

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett a = getName from

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett b = getName to

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett ar' = map getName ar

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett co' = getName co

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett p = (ar', co')

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett in mor {

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett target = Sign.renameOpProfile a ar' co' b ats tgt,

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett opMap = Map.insertWith (Map.union) a (Map.insert p (b, p) Map.empty) omap

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett }

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett _ -> mor

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett-- | Rename a signature with the sort and label renamings, and modify

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett-- the given morphism by renaming the sorts in the profiles.

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettapplyRenaming2 :: Renaming -> Morphism -> Morphism

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettapplyRenaming2 rnm mor = let

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett tgt = target mor

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett smap = sortMap mor

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett omap = opMap mor

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett lmap = labelMap mor

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett in case rnm of

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett SortRenaming from to -> let

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett a = getName from

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett b = getName to

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett in mor {

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett target = Sign.renameSort a b tgt,

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett sortMap = Map.insert a b smap,

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett opMap = renameSortOpMap a b omap

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett }

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett LabelRenaming from to -> let

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett a = getName from

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett b = getName to

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett in mor {

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett labelMap = Map.insert a b lmap

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett }

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett _ -> mor

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett-- | Rename sorts in the profiles of an operator map.

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettrenameSortOpMap :: Qid -> Qid -> OpMap -> OpMap

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy GimblettrenameSortOpMap from to = Map.map f

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett where f = \ x -> Map.map g x

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett where g = \ (q, (ar, co)) -> (q, (map h ar, if co == from

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett then to

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett else co))

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett where h = \ x -> if x == from

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett then to

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett else x

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettallProfilesRenaming :: Qid -> Qid -> Sign -> OpMap -> OpMap

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettallProfilesRenaming from to sg om = om'

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett where om_sg = Sign.ops sg

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett om' = if Map.member from om_sg

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett then Map.insert from (allProfilesRenamingAux to $ fromJust $ Map.lookup from om_sg) om

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett else om

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettallProfilesRenamingAux :: Qid -> Sign.OpDeclSet -> Map.Map Profile (Qid, Profile)

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettallProfilesRenamingAux q = Set.fold (f q) Map.empty

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett where f = \ to (x, y, _) m -> Map.insert (x, y) (to, (x, y)) m

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett-- | extract a Symbol Map from a Morphism

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettsymbolMap :: Morphism -> SymbolMap

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy GimblettsymbolMap mor = Map.unions [(sortMap2symbolMap $ sortMap mor),

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett (opMap2symbolMap $ opMap mor),

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett (labelMap2symbolMap $ labelMap mor)]

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettsortMap2symbolMap :: QidMap -> SymbolMap

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettsortMap2symbolMap = Map.fromList . map f . Map.toList

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett where f = \ (x, y) -> (Sort x, Sort y)

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettopMap2symbolMap :: OpMap -> SymbolMap

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettopMap2symbolMap = Map.fromList . map h . map f . Map.toList

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett where f = \ (x, y) -> map (g x) $ Map.toList y

2cf5a456da8bb3a2bbb695414d8304426e3bd277Andy Gimblett where g = \ q1 ((ar1, co1), (q2, (ar2, co2))) ->

ae6d8241c2ce8132a6e22d9f854edb612c2f637dAndy Gimblett (Operator q1 ar1 co1, Operator q2 ar2 co2)

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett h = \ [a] -> a

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett-- type OpMap = Map.Map Qid (Map.Map Profile (Qid, Profile))

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy Gimblett

b5301fa0ef9e88a488e5cfe8c395a05c2f6884d3Andy GimblettlabelMap2symbolMap :: QidMap -> SymbolMap

labelMap2symbolMap = Map.fromList . map f . Map.toList

where f = \ (x, y) -> (Lab x, Lab y)

-- | create a Morphism from the initial signatures and a list of Renamings

fromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism

fromSignsRenamings sg1 sg2 rnms = foldr insertRenaming2 (foldr insertRenaming1 m rnms) rnms

where m = createInclMorph sg1 sg2

-- | insert a Renaming into a Morphism

insertRenaming1 :: Renaming -> Morphism -> Morphism

insertRenaming1 rename mor = let

tgt = target mor

omap = opMap mor

in case rename of

OpRenaming1 from (To to _) -> let

a = getName from

b = getName to

in mor {

opMap = allProfilesRenaming a b tgt omap

}

OpRenaming2 from ar co (To to _) -> let

a = getName from

b = getName to

ar' = map getName ar

co' = getName co

p = (ar', co')

in mor {

opMap = Map.insertWith (Map.union) a (Map.insert p (b, p) Map.empty) omap

}

_ -> mor

insertRenaming2 :: Renaming -> Morphism -> Morphism

insertRenaming2 rename mor = let

smap = sortMap mor

omap = opMap mor

lmap = labelMap mor

in case rename of

SortRenaming from to -> let

a = getName from

b = getName to

in mor {

sortMap = Map.insert a b smap,

opMap = renameSortOpMap a b omap

}

LabelRenaming from to -> let

a = getName from

b = getName to

in mor {

labelMap = Map.insert a b lmap

}

_ -> mor

-- | the empty Morphism

empty :: Morphism

empty = identity Sign.empty

-- | the identity Morphism

identity :: Sign -> Morphism

identity sign = createInclMorph sign sign

isIdentity :: Morphism -> Bool

isIdentity m = source m == target m

-- | the inclusion Morphism

createInclMorph :: Sign -> Sign -> Morphism

createInclMorph src tgt = Morphism {

source = src,

target = tgt,

sortMap = Map.empty,

opMap = Map.empty,

labelMap = Map.empty

}

-- | the inverse Morphism

inverse :: Morphism -> Result Morphism

inverse mor = let

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

in return Morphism {

source = (target mor),

target = (source mor),

sortMap = inverseMap (sortMap mor),

opMap = inverseOpMap (opMap mor),

labelMap = inverseMap (labelMap mor)

}

inverseOpMap :: OpMap -> OpMap

inverseOpMap om = om

-- | the composition of two Morphisms

-- TODO: Ops don't have labels, so Signs don't have labels. so we can ignore the labelMap. Is that correct?

compose :: Morphism -> Morphism -> Result Morphism

compose f g

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

| otherwise = let

-- map'map takes:

-- mp :: Morphism -> SymbolMap

-- and returns a function |Symbol -> Symbol|

-- by treating each SymbolMap as a function and then combining them

map'map mp = mapAsFunction (mp g) . mapAsFunction (mp f)

-- insert takes:

-- mp :: Morphism -> SymbolMap

-- x :: Symbol

-- and returns a funcion |SymbolMap -> SymbolMap|

-- by applying both SymbolMaps (from |f| and |g|) to |x|, then

-- inserting the resulting renaming into the SymbolMap if there is one

-- and just leaving it (the SymbolMap) alone otherwise.

insert mp x = let y = map'map mp x

in if x == y then id else Map.insert x y

-- compose'map takes:

-- mp :: Morphism -> SymbolMap

-- items :: Sign -> SymbolSet

-- and constructs a combined SymbolMap from both our Morphisms

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

-- if the SymbolMap of |g| is empty, we just use the one from |f|

then mp f

-- otherwise we start with the SymbolSet from |source f|

-- and construct a combined SymbolMap by applying both

-- SymbolMaps (from |f| and |g|) to each item in |insert|

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

-- We want a morphism from |source f| to |target g|,

in return (createInclMorph (source f) $ target g) {

sortMap = compose'map sortMap getSorts -- ,

-- opMap = compose'map opMap getOps -- ,

-- labelMap = compose'map labelMap getLabels

}

-- | check that a Morphism is legal

-- TODO: Ops don't have labels, so Signs don't have labels. so we can ignore the labelMap. Is that correct?

isLegal :: Morphism -> Bool

isLegal mor = let

src = source mor

tgt = target mor

smap = sortMap mor

omap = opMap mor

-- lmap = labelMap mor

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

legal'source = Sign.isLegal src

legal'sortMap = subset smap getSorts

-- legal'opMap = subset omap getOps

legal'opMap = True

-- legal'labelMap = subset lmap getLabels

legal'labelMap = True

legal'target = Sign.isLegal tgt

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

-- | check that a Morphism is an Inclusion

isInclusion :: Morphism -> Bool

-- TODO: Implement Morphism.isInclusion.

isInclusion mor = let

null'sortMap = Map.null (sortMap mor)

null'opMap = Map.null (opMap mor)

null'labelMap = Map.null (labelMap mor)

in all id [null'sortMap, null'opMap, null'labelMap]

-- | translate a Sentence along a Morphism

mapSentence :: Morphism -> Sentence -> Result Sentence

mapSentence mor = let

smap = mapSorts (sortMap mor)

-- omap = mapOps (opMap mor)

lmap = mapLabels (labelMap mor)

in return . lmap . smap -- . omap . smap

union :: Morphism -> Morphism -> Morphism

union m1 m2 = Morphism {

source = Sign.union (source m1) $ source m2,

target = Sign.union (target m1) $ target m2,

sortMap = Map.union (sortMap m1) $ sortMap m2,

opMap = Map.unionWith (Map.union) (opMap m1) $ opMap m2,

labelMap = Map.union (labelMap m1) $ labelMap m2

}

setTarget :: Sign -> Morphism -> Morphism

setTarget sg morph = morph {target = sg}

renameSorts :: Morphism -> [Qid] -> [Qid]

renameSorts m = map f

where sm = sortMap m

f = \ x -> if Map.member x sm

then fromJust $ Map.lookup x sm

else x

extendMorphismSorts :: Morphism -> Qid -> [Qid] -> Morphism

extendMorphismSorts mor sym syms = let

tgt = target mor

smap = sortMap mor

in mor {

target = Sign.renameListSort (createRenaming sym syms) tgt,

sortMap = extendSortMap sym syms smap

}

createRenaming :: Qid -> [Qid] -> [(Qid, Qid)]

createRenaming _ [] = []

createRenaming sym (sym' : syms) = (sym', new_sym) : createRenaming sym syms

where new_sym = mkSimpleId $ show sym ++ "$" ++ show sym'

extendSortMap :: Qid -> [Qid] -> QidMap -> QidMap

extendSortMap _ [] sm = sm

extendSortMap sym (sym' : syms) sort_map = extendSortMap sym syms sort_map'

where new_sym = mkSimpleId $ show sym ++ "$" ++ show sym'

sort_map' = Map.fromList $ extendSortList sym' new_sym $ Map.toList sort_map

extendSortList :: Qid -> Qid -> [(Qid, Qid)] -> [(Qid, Qid)]

extendSortList from to [] = [(from, to)]

extendSortList from to (s@(sym1, sym2) : syms) = if from == sym2

then (sym1, to) : syms

else s : extendSortList from to syms

addQualification :: Morphism -> Qid -> [Qid] -> Morphism

addQualification mor sym syms = let

src = source mor

smap = sortMap mor

in mor {

source = Sign.renameListSort (createRenaming sym syms) src,

sortMap = qualifyMap sym syms smap

}

qualifyMap :: Qid -> [Qid] -> QidMap -> QidMap

qualifyMap _ [] sm = sm

qualifyMap sym (sym' : syms) sort_map = extendSortMap sym syms sort_map'

where new_sym = mkSimpleId $ show sym ++ "$" ++ show sym'

sort_map' = Map.fromList $ qualifySortList sym' new_sym $ Map.toList sort_map

qualifySortList :: Qid -> Qid -> [(Qid, Qid)] -> [(Qid, Qid)]

qualifySortList from to [] = [(from, to)]

qualifySortList from to (s@(sym1, sym2) : syms) = if from == sym1

then (to, sym2) : syms

else s : qualifySortList from to syms

-- | TODO :

-- - compose with the new OpMap

-- - isLegal with the new OpMap

-- - mapSentence with the new OpMap

-- - inverseOpMap (Adrian)

-- - rename ops with profile (Adrian)