hets/HasCASL/Morphism.hs

	Morphism.hs revision 2dfc7b04f2db681992ca04175f2beb0f127c9844
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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                         , mtarget :: Env
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                         , classIdMap :: IdMap  -- ignore
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder          fm = funMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder          ds = Map.foldWithKey ( \ (i, s) (j, t) l ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                (printText0 ga i <+> colon <+> printText0 ga s
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                <+> text mapsTo <+>
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                printText0 ga j <+> colon <+> printText0 ga t) : l)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder               [] fm
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder      in (if Map.isEmpty tm then empty
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         else text (typeS ++ sS) <+> printText0 ga tm)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder         $$ (if Map.isEmpty fm then empty
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             else text (opS ++ sS) <+> fsep (punctuate comma ds))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         $$ nest 1 colon <+> braces (printText0 ga $ msource m)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                    $$ nest 1 (text mapsTo)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             (getConstrType dt p (map (mapType tm) ts)) []
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder          (j, TypeScheme _ ty _) =
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder              mapFunSym (typeIdMap m) (funMap m) (i, sc)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           fm = funMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           f = mapFunSym tm fm
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           (ni, nsc) = f (i, sc)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                   (i, sc) fm in
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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 ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                       Map.insert i $ Map.findWithDefault j j im2)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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 ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                       Map.insert p1
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder     else Result [Diag Error
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder          ("Attempt to construct inclusion between non-subsignatures:"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           ++ "\nSignature 1:\n" ++ showPretty e1 "\nSignature 2:\n"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           ++ showPretty e2 "") nullPos] Nothing
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)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         { typeIdMap = type_map1
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                                  , symType = TypeAsItemType
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                                               $ typeKind k
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                                  , symType = OpAsItemType osc
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                 t = mtarget m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                 ts = typeIdMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                 fs = funMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             in
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             all (`elem` (Map.keys $ typeMap s))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                  (Map.keys ts)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             && all (`elem` (Map.keys $ typeMap t))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                (Map.elems ts)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             && all ((`elem` (Map.keys $ assumps s)) . fst)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                (Map.keys fs)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             && all ((`elem` (Map.keys $ assumps t)) . fst)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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 ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                     do m <- rm
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                        case Map.lookup i m of
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                          Nothing -> return $ Map.insert i j m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                          Just k -> if j == k then return m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                            else do
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                            Result [Diag Error
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                              ("incompatible mapping of type id: " ++
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                               showId i " to: " ++ showId j " and: "
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                               ++ showId k "") $ posOfId i] $ Just ()
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                            return m)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             (return $ typeIdMap m1) $ Map.toList $ typeIdMap m2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder       fm <- foldr ( \ (isc@(i, sc), jsc@(j, sc1)) rm -> do
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                     let nsc = expand (typeMap t) sc1
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder                         nisc = (i, expand (typeMap s) sc)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                     m <- rm
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                     case Map.lookup nisc m of
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                       Nothing -> return $ Map.insert nisc
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                          (j, nsc) m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                       Just ksc@(k, sc2) -> if j == k &&
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                         nsc == sc2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                         then return m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                            else do
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                            Result [Diag Error
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                              ("incompatible mapping of op: " ++
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                               showFun isc " to: " ++ showFun jsc " and: "
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                               ++ showFun ksc "") $ posOfId i] $ Just ()
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                            return m)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             (return Map.empty) (Map.toList (funMap m1) ++
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                                 Map.toList (funMap m2))
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder       return (mkMorphism s t)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                  { typeIdMap = tm
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           k = typeKind ti
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian 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 ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             foldr ( \ oi ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             let ty = opType oi
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder                 (j, t2) = mapFunSym
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                     tm (funMap mor) (i, ty)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder             in Map.insert (idToOpSymbol src i ty)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder                        (idToOpSymbol tar j t2)) m l)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder         typeSymMap $ assumps src