hets/HasCASL/Morphism.hs

	Morphism.hs revision 4fb19f237193a3bd6778f8aee3b6dd8da5856665
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