967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |

967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$

967e5f3c25249c779575864692935627004d3f9eChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederMaintainer : maeder@tzi.de

967e5f3c25249c779575864692935627004d3f9eChristian MaederStability : provisional

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPortability : portable

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaederMorphism on 'Env' (as for CASL)

967e5f3c25249c779575864692935627004d3f9eChristian Maeder-}

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maedermodule HasCASL.Morphism where

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport HasCASL.Le

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport HasCASL.As

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maederimport HasCASL.AsToLe

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maederimport HasCASL.Unify

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maederimport HasCASL.MapTerm

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederimport HasCASL.AsUtils

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport Common.Id

997c56f3bc74a703043010978e5013fdb074d659Christian Maederimport Common.Keywords

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport Common.Result

9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiimport Common.PrettyPrint

9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskiimport Common.Lib.Pretty

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport qualified Common.Lib.Map as Map

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedertype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maederdata Morphism = Morphism { msource :: Env

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , mtarget :: Env

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , classIdMap :: IdMap -- ignore

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , typeIdMap :: IdMap

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , funMap :: FunMap }

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder deriving (Eq, Show)

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maederinstance PrettyPrint Morphism where

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder printText0 ga m =

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder let tm = typeIdMap m

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder fm = funMap m

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

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder (printText0 ga i <+> colon <+> printText0 ga s

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder <+> text mapsTo <+>

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder printText0 ga j <+> colon <+> printText0 ga t) : l)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder [] fm

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder in (if Map.isEmpty tm then empty

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder else text (typeS ++ sS) <+> printText0 ga tm)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder $$ (if Map.isEmpty fm then empty

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder else text (opS ++ sS) <+> fsep (punctuate comma ds))

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder $$ nest 1 colon <+> braces (printText0 ga $ msource m)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder $$ nest 1 (text mapsTo)

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder <+> braces (printText0 ga $ mtarget m)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme :: IdMap -> TypeScheme -> TypeScheme

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapTypeScheme im = mapTypeOfScheme $ mapType im

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedermapSen :: Morphism -> Term -> Term

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaedermapSen m = let im = typeIdMap m in

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder mapTerm (mapFunSym im (funMap m), mapType im)

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedermapDataEntry :: Morphism -> DataEntry -> DataEntry

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedermapDataEntry m (DataEntry tm i k args alts) =

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder let tim = compIdMap tm $ typeIdMap m

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder in DataEntry tim i k args $ map

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder (mapAlt m tim args (Map.findWithDefault i i tim, args, star)) alts

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedermapAlt :: Morphism -> IdMap -> [TypeArg] -> DataPat -> AltDefn -> AltDefn

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermapAlt m tm args dt c@(Construct mi ts p sels) =

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder case mi of

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder Just i ->

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder let sc = TypeScheme args

d17834302eaa101395b4b806cd73670fd864445fChristian Maeder (getConstrType dt p (map (mapType tm) ts)) []

d17834302eaa101395b4b806cd73670fd864445fChristian Maeder (j, TypeScheme _ ty _) =

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder mapFunSym (typeIdMap m) (funMap m) (i, sc)

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder in Construct (Just j) ts (getPartiality ts ty) sels

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -- do not change (unused) selectors

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder Nothing -> c

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedermapSentence m s = return $ case s of

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Formula t -> Formula $ mapSen m t

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry m) td

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder ProgEqSen i sc pe ->

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder let tm = typeIdMap m

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder fm = funMap m

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder f = mapFunSym tm fm

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder (ni, nsc) = f (i, sc)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder in ProgEqSen ni nsc $ mapEq (f, mapType tm) pe

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapFunSym im fm (i, sc) =

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder let (j, sc2) = Map.findWithDefault (i, mapTypeScheme im sc)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (i, sc) fm in

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (j , sc2)

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaedermkMorphism :: Env -> Env -> Morphism

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederembedMorphism :: Env -> Env -> Morphism

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian MaederembedMorphism = mkMorphism

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaederideMor :: Env -> Morphism

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederideMor e = embedMorphism e e

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap

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

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder Map.insert i $ Map.findWithDefault j j im2)

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder im2 $ im1

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor :: Morphism -> Morphism -> Maybe Morphism

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor m1 m2 =

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder if isSubEnv (mtarget m1) (msource m2) &&

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder isSubEnv (msource m2) (mtarget m1) then

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder let tm2 = typeIdMap m2

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder fm2 = funMap m2 in Just

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (mkMorphism (msource m1) (mtarget m2))

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder { classIdMap = compIdMap (classIdMap m1) $ classIdMap m2

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , typeIdMap = compIdMap (typeIdMap m1) tm2

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder , funMap = Map.foldWithKey ( \ p1 p2 ->

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Map.insert p1

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder $ mapFunSym tm2 fm2 p2) fm2 $ funMap m1

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder }

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder else Nothing

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiinclusionMor :: Env -> Env -> Result Morphism

7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinclusionMor e1 e2 =

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder if isSubEnv e1 e2

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder then return (embedMorphism e1 e2)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder else pplain_error (ideMor initialEnv)

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder (ptext "Attempt to construct inclusion between non-subsignatures:"

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder $$ ptext "Signature 1:" $$ printText e1

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder $$ ptext "Signature 2:" $$ printText e2)

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder nullPos

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedersymbMapToMorphism :: Env -> Env -> SymbolMap -> Result Morphism

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- consider partial symbol map

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedersymbMapToMorphism sigma1 sigma2 smap = do

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder type_map1 <- Map.foldWithKey myIdMap (return Map.empty) $ typeMap sigma1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder fun_map1 <- Map.foldWithKey myAsMap (return Map.empty) $ assumps sigma1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (mkMorphism sigma1 sigma2)

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder { typeIdMap = type_map1

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , funMap = fun_map1}

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder where

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder myIdMap i k m = do

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder m1 <- m

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sym <- maybeToResult nullPos

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ("symbMapToMorphism - Could not map type "++showId i "")

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ Map.lookup (Symbol { symName = i

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , symType = TypeAsItemType

e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder $ typeKind k

e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder , symEnv = sigma1 }) smap

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (Map.insert i (symName sym) m1)

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder myAsMap i (OpInfos ots) m = foldr (insFun i) m ots

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder insFun i ot m = do

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder let osc = opType ot

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder m1 <- m

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sym <- maybeToResult nullPos

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Could not map op "++showId i "")

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ Map.lookup (Symbol { symName = i

e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder , symType = OpAsItemType osc

e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder , symEnv = sigma1 }) smap

dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder k <- case symType sym of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder OpAsItemType sc -> return sc

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder _ -> plain_error (osc)

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Wrong result symbol type for op"

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ++showId i "") nullPos

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return (Map.insert (i, osc) (symName sym, k) m1)

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv :: Env -> Bool

967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv _ = True -- maybe a closure test?

967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalMor :: Morphism -> Bool

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederlegalMor m = let s = msource m

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder t = mtarget m

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder ts = typeIdMap m

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder fs = funMap m

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder in

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

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (Map.keys ts)

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

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (Map.elems ts)

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

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (Map.keys fs)

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

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (Map.elems fs)

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism

7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermorphismUnion m1 m2 =

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

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder t <- merge (mtarget m1) $ mtarget m2

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder tm <- foldr ( \ (i, j) rm ->

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder do m <- rm

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder case Map.lookup i m of

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Nothing -> return $ Map.insert i j m

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just k -> if j == k then return m

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder else do

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Result [Diag Error

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ("incompatible mapping of type id: " ++

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder showId i " to: " ++ showId j " and: "

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ++ showId k "") $ posOfId i] $ Just ()

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return m)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (return $ typeIdMap m1) $ Map.toList $ typeIdMap m2

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fm <- foldr ( \ (isc@(i, sc), jsc@(j, sc1)) rm -> do

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder let nsc = expand (typeMap t) sc1

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder nisc = (i, expand (typeMap s) sc)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder m <- rm

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case Map.lookup nisc m of

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Nothing -> return $ Map.insert nisc

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (j, nsc) m

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Just ksc@(k, sc2) -> if j == k &&

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder nsc == sc2

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder then return m

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder else do

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Result [Diag Error

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ("incompatible mapping of op: " ++

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder showFun isc " to: " ++ showFun jsc " and: "

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ++ showFun ksc "") $ posOfId i] $ Just ()

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder return m)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (return Map.empty) (Map.toList (funMap m1) ++

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Map.toList (funMap m2))

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder return (mkMorphism s t)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder { typeIdMap = tm

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , funMap = fm }

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedershowFun :: (Id, TypeScheme) -> ShowS

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedershowFun (i, ty) = showId i . (" : " ++) . showPretty ty

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder

83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermorphismToSymbMap mor =

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder let

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder src = msource mor

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder tar = mtarget mor

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder tm = typeIdMap mor

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder let j = Map.findWithDefault i i tm

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder k = typeKind ti

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder in Map.insert (idToTypeSymbol src i k)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder $ idToTypeSymbol tar j k) Map.empty $ typeMap src

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder in Map.foldWithKey

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder ( \ i (OpInfos l) m ->

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder foldr ( \ oi ->

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder let ty = opType oi

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (j, t2) = mapFunSym

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder tm (funMap mor) (i, ty)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder in Map.insert (idToOpSymbol src i ty)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder (idToOpSymbol tar j t2)) m l)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder typeSymMap $ assumps src