c1d71ac637c449feb0a25369f029397e6a1f241cChristian Maeder{- |

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederModule : $Header$

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederMaintainer : maeder@tzi.de

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : provisional

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederMorphism on 'Env' (as for CASL)

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder-}

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule HasCASL.Morphism where

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowskiimport HasCASL.Le

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.As

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.AsToLe

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport HasCASL.Unify

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport HasCASL.MapTerm

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport HasCASL.AsUtils

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport Common.Id

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport Common.Keywords

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport Common.Result

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport Common.PrettyPrint

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport Common.Lib.Pretty

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichimport qualified Common.Lib.Map as Map

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichtype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettichdata Morphism = Morphism { msource :: Env

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich , mtarget :: Env

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich , classIdMap :: IdMap -- ignore

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich , typeIdMap :: IdMap

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , funMap :: FunMap }

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski deriving (Eq, Show)

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance PrettyPrint Morphism where

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder printText0 ga m =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder let tm = typeIdMap m

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder fm = funMap m

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder ds = Map.foldWithKey ( \ (i, s) (j, t) l ->

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder (printText0 ga i <+> colon <+> printText0 ga s

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski <+> text mapsTo <+>

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder printText0 ga j <+> colon <+> printText0 ga t) : l)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski [] fm

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in (if Map.isEmpty tm then empty

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski else text (typeS ++ sS) <+> printText0 ga tm)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $$ (if Map.isEmpty fm then empty

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder else text (opS ++ sS) <+> fsep (punctuate comma ds))

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $$ nest 1 colon <+> braces (printText0 ga $ msource m)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $$ nest 1 (text mapsTo)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski <+> braces (printText0 ga $ mtarget m)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeScheme :: IdMap -> TypeScheme -> TypeScheme

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeScheme im = mapTypeOfScheme $ mapType im

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescumapSen :: Morphism -> Term -> Term

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai CodescumapSen m = let im = typeIdMap m in

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu mapTerm (mapFunSym im (funMap m), mapType im)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskimapDataEntry :: Morphism -> DataEntry -> DataEntry

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskimapDataEntry m (DataEntry tm i k args alts) =

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski let tim = compIdMap tm $ typeIdMap m

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski in DataEntry tim i k args $ map

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski (mapAlt m tim args (Map.findWithDefault i i tim, args, star)) alts

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski

bba825b39570777866d560bfde3807731131097eKlaus LuettichmapAlt :: Morphism -> IdMap -> [TypeArg] -> DataPat -> AltDefn -> AltDefn

bba825b39570777866d560bfde3807731131097eKlaus LuettichmapAlt m tm args dt c@(Construct mi ts p sels) =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case mi of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just i ->

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder let sc = TypeScheme args

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (getConstrType dt p (map (mapType tm) ts)) []

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski (j, TypeScheme _ ty _) =

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder mapFunSym (typeIdMap m) (funMap m) (i, sc)

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder in Construct (Just j) ts (getPartiality ts ty) sels

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -- do not change (unused) selectors

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Nothing -> c

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSentence :: Morphism -> Sentence -> Result Sentence

0647a6c86b231e391826c7715338ba29cb4934c0Christian MaedermapSentence m s = return $ case s of

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu Formula t -> Formula $ mapSen m t

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu DatatypeSen td -> DatatypeSen $ map (mapDataEntry m) td

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu ProgEqSen i sc pe ->

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu let tm = typeIdMap m

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu fm = funMap m

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu f = mapFunSym tm fm

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (ni, nsc) = f (i, sc)

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu in ProgEqSen ni nsc $ mapEq (f, mapType tm) pe

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu

f2c050360525df494e6115073b0edc4c443a847cMihai CodescumapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)

f2c050360525df494e6115073b0edc4c443a847cMihai CodescumapFunSym im fm (i, sc) =

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu let (j, sc2) = Map.findWithDefault (i, mapTypeScheme im sc)

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu (i, sc) fm in

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski (j , sc2)

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski

0e51a998b1b213654c7a9eca451562041971f100Till MossakowskimkMorphism :: Env -> Env -> Morphism

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichembedMorphism :: Env -> Env -> Morphism

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiembedMorphism = mkMorphism

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederideMor :: Env -> Morphism

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederideMor e = embedMorphism e e

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompIdMap im1 im2 = Map.foldWithKey ( \ i j ->

bba825b39570777866d560bfde3807731131097eKlaus Luettich Map.insert i $ Map.findWithDefault j j im2)

bba825b39570777866d560bfde3807731131097eKlaus Luettich im2 $ im1

bba825b39570777866d560bfde3807731131097eKlaus Luettich

bba825b39570777866d560bfde3807731131097eKlaus LuettichcompMor :: Morphism -> Morphism -> Maybe Morphism

bba825b39570777866d560bfde3807731131097eKlaus LuettichcompMor m1 m2 =

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if isSubEnv (mtarget m1) (msource m2) &&

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder isSubEnv (msource m2) (mtarget m1) then

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder let tm2 = typeIdMap m2

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder fm2 = funMap m2 in Just

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (mkMorphism (msource m1) (mtarget m2))

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder { classIdMap = compIdMap (classIdMap m1) $ classIdMap m2

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder , typeIdMap = compIdMap (typeIdMap m1) tm2

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder , funMap = Map.foldWithKey ( \ p1 p2 ->

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder Map.insert p1

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder $ mapFunSym tm2 fm2 p2) fm2 $ funMap m1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder }

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder else Nothing

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederinclusionMor :: Env -> Env -> Result Morphism

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederinclusionMor e1 e2 =

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if isSubEnv e1 e2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder then return (embedMorphism e1 e2)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder else pplain_error (ideMor initialEnv)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (ptext "Attempt to construct inclusion between non-subsignatures:"

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder $$ ptext "Signature 1:" $$ printText e1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder $$ ptext "Signature 2:" $$ printText e2)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder nullPos

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedersymbMapToMorphism :: Env -> Env -> SymbolMap -> Result Morphism

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder-- consider partial symbol map

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedersymbMapToMorphism sigma1 sigma2 smap = do

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder type_map1 <- Map.foldWithKey myIdMap (return Map.empty) $ typeMap sigma1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fun_map1 <- Map.foldWithKey myAsMap (return Map.empty) $ assumps sigma1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder return (mkMorphism sigma1 sigma2)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder { typeIdMap = type_map1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder , funMap = fun_map1}

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder where

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder myIdMap i k m = do

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder m1 <- m

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sym <- maybeToResult nullPos

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder ("symbMapToMorphism - Could not map type "++showId i "")

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder $ Map.lookup (Symbol { symName = i

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder , symType = TypeAsItemType

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder $ typeKind k

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder , symEnv = sigma1 }) smap

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder return (Map.insert i (symName sym) m1)

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder myAsMap i (OpInfos ots) m = foldr (insFun i) m ots

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder insFun i ot m = do

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder let osc = opType ot

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder m1 <- m

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder sym <- maybeToResult nullPos

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ("symbMapToMorphism - Could not map op "++showId i "")

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder $ Map.lookup (Symbol { symName = i

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder , symType = OpAsItemType osc

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder , symEnv = sigma1 }) smap

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder k <- case symType sym of

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder OpAsItemType sc -> return sc

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder _ -> plain_error (osc)

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder ("symbMapToMorphism - Wrong result symbol type for op"

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ++showId i "") nullPos

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder return (Map.insert (i, osc) (symName sym, k) m1)

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaederlegalEnv :: Env -> Bool

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederlegalEnv _ = True -- maybe a closure test?

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaederlegalMor :: Morphism -> Bool

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederlegalMor m = let s = msource m

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder t = mtarget m

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder ts = typeIdMap m

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder fs = funMap m

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder in

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder all (`elem` (Map.keys $ typeMap s))

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (Map.keys ts)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder && all (`elem` (Map.keys $ typeMap t))

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (Map.elems ts)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder && all ((`elem` (Map.keys $ assumps s)) . fst)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (Map.keys fs)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder && all ((`elem` (Map.keys $ assumps t)) . fst)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (Map.elems fs)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermorphismUnion m1 m2 =

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder do s <- merge (msource m1) $ msource m2

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder t <- merge (mtarget m1) $ mtarget m2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder tm <- foldr ( \ (i, j) rm ->

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder do m <- rm

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich case Map.lookup i m of

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Nothing -> return $ Map.insert i j m

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Just k -> if j == k then return m

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich else do

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Result [Diag Error

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ("incompatible mapping of type id: " ++

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich showId i " to: " ++ showId j " and: "

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ++ showId k "") $ posOfId i] $ Just ()

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich return m)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich (return $ typeIdMap m1) $ Map.toList $ typeIdMap m2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fm <- foldr ( \ (isc@(i, sc), jsc@(j, sc1)) rm -> do

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich let nsc = expand (typeMap t) sc1

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich nisc = (i, expand (typeMap s) sc)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich m <- rm

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich case Map.lookup nisc m of

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Nothing -> return $ Map.insert nisc

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich (j, nsc) m

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Just ksc@(k, sc2) -> if j == k &&

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich nsc == sc2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich then return m

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich else do

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Result [Diag Error

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ("incompatible mapping of op: " ++

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich showFun isc " to: " ++ showFun jsc " and: "

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ++ showFun ksc "") $ posOfId i] $ Just ()

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich return m)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich (return Map.empty) (Map.toList (funMap m1) ++

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich Map.toList (funMap m2))

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich return (mkMorphism s t)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich { typeIdMap = tm

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich , funMap = fm }

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichshowFun :: (Id, TypeScheme) -> ShowS

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichshowFun (i, ty) = showId i . (" : " ++) . showPretty ty

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmorphismToSymbMap :: Morphism -> SymbolMap

797595aad6dfd626bc1c9df52616f1ac4235c669Till MossakowskimorphismToSymbMap mor =

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski let

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski src = msource mor

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski tar = mtarget mor

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich tm = typeIdMap mor

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski let j = Map.findWithDefault i i tm

933baca0720dae81434de384b32a93b47e754d09Christian Maeder k = typeKind ti

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Map.insert (idToTypeSymbol src i k)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ idToTypeSymbol tar j k) Map.empty $ typeMap src

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Map.foldWithKey

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ( \ i (OpInfos l) m ->

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich foldr ( \ oi ->

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich let ty = opType oi

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich (j, t2) = mapFunSym

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich tm (funMap mor) (i, ty)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich in Map.insert (idToOpSymbol src i ty)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich (idToOpSymbol tar j t2)) m l)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich typeSymMap $ assumps src

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich