81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : morphisms implementation
f11f713bebd8e1e623a0a4361065df256033de47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
967e5f3c25249c779575864692935627004d3f9eChristian MaederStability : provisional
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPortability : portable
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedermapping entities of morphisms
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maederimport Common.Utils (composeMap)
ad187062b0009820118c1b773a232e29b879a2faChristian Maederimport qualified Data.Set as Set
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian MaederdisjointKeys :: (Ord a, Pretty a, Monad m) => Map.Map a b -> Map.Map a c
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian MaederdisjointKeys m1 m2 = let d = Map.keysSet $ Map.intersection m1 m2 in
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder unless (Set.null d) $ fail $ show
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder (sep [ text "overlapping identifiers for types and classes:"
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder-- | map a kind along an identifier map
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapKindI :: IdMap -> Kind -> Kind
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian MaedermapKindI jm = mapKind (\ a -> Map.findWithDefault a a jm)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder-- | map a kind along a signature morphism (variance is preserved)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapKinds :: Morphism -> Kind -> Kind
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian MaedermapKinds = mapKindI . classIdMap
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder-- | only rename the kinds in a type
67d92da5e9610aabad39055a16031154b4dc3748Christian MaedermapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
67d92da5e9610aabad39055a16031154b4dc3748Christian MaedermapKindsOfType jm tm im = foldType mapTypeRec
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder { foldTypeAbs = \ _ -> TypeAbs . mapTypeArg jm tm im
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder , foldKindedType = \ _ t -> KindedType t . Set.map (mapKindI jm) }
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder-- | map type, expand it, and also adjust the kinds
67d92da5e9610aabad39055a16031154b4dc3748Christian MaedermapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
67d92da5e9610aabad39055a16031154b4dc3748Christian MaedermapTypeE jm tm im =
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder mapKindsOfType jm tm im . expandAliases tm . mapType im
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder-- | map a kind along a signature morphism (variance is preserved)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapVarKind jm tm im vk = case vk of
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder VarKind k -> VarKind $ mapKindI jm k
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder Downset ty -> Downset $ mapTypeE jm tm im ty
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapTypeArg jm tm im (TypeArg i v vk rk c s r) =
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder TypeArg i v (mapVarKind jm tm im vk) rk c s r
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapTypeScheme jm tm im (TypeScheme args ty ps) =
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
67d92da5e9610aabad39055a16031154b4dc3748Christian MaedermapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)
a89389521ddf76109168a0b339031575aafbd512Christian MaedergetDatatypeIds :: DataEntry -> Set.Set Id
a89389521ddf76109168a0b339031575aafbd512Christian MaedergetDatatypeIds (DataEntry _ i _ _ _ alts) =
a89389521ddf76109168a0b339031575aafbd512Christian Maeder let getAltIds (Construct _ tys _ sels) = Set.union
a89389521ddf76109168a0b339031575aafbd512Christian Maeder (Set.unions $ map getTypeIds tys)
a89389521ddf76109168a0b339031575aafbd512Christian Maeder $ Set.unions $ concatMap (map getSelIds) sels
a89389521ddf76109168a0b339031575aafbd512Christian Maeder getSelIds (Select _ ty _) = getTypeIds ty
a89389521ddf76109168a0b339031575aafbd512Christian Maeder getTypeIds = idsOf (== 0)
a89389521ddf76109168a0b339031575aafbd512Christian Maeder in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedermapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian MaedermapDataEntry jm tm im fm (DataEntry dm i k args rk alts) =
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder let nDm = Map.map (\ a -> Map.findWithDefault a a im) dm
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder newargs = map (mapTypeArg jm tm im) args
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder in DataEntry nDm i k newargs rk $ Set.map
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian Maeder (mapAlt jm tm im fm nIm newargs
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder $ patToType (Map.findWithDefault i i dm) newargs rk) alts
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian MaedermapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian Maeder -> AltDefn -> AltDefn
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian MaedermapAlt jm tm im fm nIm args dt (Construct mi ts p sels) =
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder let newTs = map (mapTypeE jm tm nIm) ts
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian Maeder newSels = map (map (mapSel jm tm im fm nIm args dt)) sels
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder in case mi of
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder Just i -> let
e77eadd37125110f448dd5ddec7da5b78d35285fChristian Maeder sc = TypeScheme args (getFunType dt p ts) nullRange
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder in Construct (Just j) newTs (getPartiality newTs ty) newSels
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder Nothing -> Construct mi newTs p newSels
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian MaedermapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian Maeder -> Selector -> Selector
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian MaedermapSel jm tm im fm nIm args dt (Select mid t p) =
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder let newT = mapTypeE jm tm nIm t
54ff63bb3b23ef18efbdc51b053a2ca6f348329aChristian Maeder in case mid of
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder Nothing -> Select mid newT p
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder Just i -> let
e77eadd37125110f448dd5ddec7da5b78d35285fChristian Maeder sc = TypeScheme args (getSelType dt p t) nullRange
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
ee93fb771fcf3000d73c8e2f2000adb4b9a5158cChristian Maeder in Select (Just j) newT $ getPartiality [dt] ty
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder{- | get the partiality from a constructor type
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maederwith a given number of curried arguments. -}
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedergetPartiality :: [a] -> Type -> Partiality
d48085f765fca838c1d972d2123601997174583dChristian MaedergetPartiality args t = case getTypeAppl t of
d48085f765fca838c1d972d2123601997174583dChristian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of
d48085f765fca838c1d972d2123601997174583dChristian Maeder [_] -> if isPartialArrow i then Partial else Total
d48085f765fca838c1d972d2123601997174583dChristian Maeder _ : rs -> getPartiality rs res
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder if null args then Partial else error "getPartiality"
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaedermapSentence m s = let
9b30898b139ee02f97ac933b6d935ef0a4206921Christian Maeder tm = filterAliases . typeMap $ mtarget m
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder im = typeIdMap m
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder jm = classIdMap m
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder fm = funMap m
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder f = mapFunSym jm tm im fm
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder in return $ case s of
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder Formula t -> Formula $ mapSen jm tm im fm t
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder ProgEqSen i sc pe ->
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder let (ni, nsc) = f (i, sc)
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder in ProgEqSen ni nsc $ mapEq (f, mapTypeE jm tm im) pe
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder -> (Id, TypeScheme)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapFunSym jm tm im fm (i, sc) =
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder let msc = mapTypeScheme jm tm im sc
c5c193a80459071696b68baf835f1b88f0f8c82eChristian Maeder in Map.findWithDefault (i, msc) (i, sc) fm
967e5f3c25249c779575864692935627004d3f9eChristian MaederideMor :: Env -> Morphism
18b513ff41708f24e1a7407f36b719add813ffeaChristian MaederideMor e = mkMorphism e e
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaedercompMor m1 m2 = let
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder tm1 = typeIdMap m1
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder tm2 = typeIdMap m2
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder ctm = composeMap (typeMap src) tm1 tm2
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder cm1 = classIdMap m1
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu cm2 = classIdMap m2
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder ccm = composeMap (classMap src) cm1 cm2
81d182b21020b815887e9057959228546cf61b6bChristian Maeder fm2 = funMap m2
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder fm1 = funMap m1
242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder tar = mtarget m2
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder src = msource m1
242397ba0f1cc490e892130bf0df239deeecf5daChristian Maeder tm = filterAliases $ typeMap tar
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder emb = mkMorphism src tar
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder in if isInclMor m1 && isInclMor m2 then return emb else do
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder disjointKeys ctm ccm
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder { typeIdMap = ctm
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder , classIdMap = ccm
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder (Map.foldWithKey ( \ p1@(i, sc) p2 ->
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder let p3 = mapFunSym ccm tm tm2 fm2 p2
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder nSc = mapTypeScheme ccm tm ctm sc
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder in if (i, nSc) == p3 then Map.delete p1 else
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder concatMap ( \ (k, os) ->
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder map ( \ o -> ((k, opType o), ())) $ Set.toList os)
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder $ Map.toList $ assumps src }
842eedc62639561781b6c33533d1949693ef6cc5Christian MaedershowEnvDiff :: Env -> Env -> String
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaedershowEnvDiff e1 e2 =
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder (diffEnv e1 e2) ""
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian MaederlegalMor :: Morphism -> Result ()
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaederlegalMor m = let
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder s = msource m
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder t = mtarget m
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder ts = typeIdMap m
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder cs = classIdMap m
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder fs = funMap m in
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder unless (all (`elem` Map.keys (typeMap s)) (Map.keys ts)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder && all (`elem` Map.keys (typeMap t)) (Map.elems ts)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder && all (`elem` Map.keys (classMap s)) (Map.keys cs)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder && all (`elem` Map.keys (classMap t)) (Map.elems cs)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (fail "illegal HasCASL morphism")
967e5f3c25249c779575864692935627004d3f9eChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
ad187062b0009820118c1b773a232e29b879a2faChristian MaedermorphismUnion m1 m2 = do
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder let s1 = msource m1
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder s2 = msource m2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder s <- merge s1 s2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder t <- merge (mtarget m1) $ mtarget m2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder let tm1 = typeMap s1
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder tm2 = typeMap s2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder im1 = typeIdMap m1
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder im2 = typeIdMap m2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder -- unchanged types
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder ut1 = Map.keysSet tm1 Set.\\ Map.keysSet im1
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder ut2 = Map.keysSet tm2 Set.\\ Map.keysSet im2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder ima1 = Map.union im1 $ setToMap ut1
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder ima2 = Map.union im2 $ setToMap ut2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder sAs = filterAliases $ typeMap s
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder tAs = filterAliases $ typeMap t
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder cm1 = classMap s1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder cm2 = classMap s2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder jm1 = classIdMap m1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder jm2 = classIdMap m2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder -- unchanged classes
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder cima1 = Map.union jm1 $ setToMap cut1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder cima2 = Map.union jm2 $ setToMap cut2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder expP = Map.fromList . map ( \ ((i, o), (j, p)) ->
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder ((i, expand tAs o), (j, expand tAs p)))
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder fm1 = expP $ funMap m1
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder fm2 = expP $ funMap m2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder af jm im = Set.unions . map ( \ (i, os) ->
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder Set.map ( \ o -> (i, mapTypeScheme jm tAs im
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder $ expand sAs $ opType o)) os)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder -- unchanged functions
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder fma1 = Map.union fm1 $ setToMap uf1
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder fma2 = Map.union fm2 $ setToMap uf2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder showFun (i, ty) = showId i . (" : " ++) . showDoc ty
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder fail $ "incompatible type mapping to `"
9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder fail $ "incompatible class mapping to `"
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder fail $ "incompatible mapping to '"
9659c509ce5e78adc51d7b02a76274eddcba9338Christian Maeder ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder disjointKeys tma cma
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder return (mkMorphism s t)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder { typeIdMap = tma
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder , classIdMap = cma
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder , funMap = fma }
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian MaedermorphismToSymbMap mor = let
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder src = msource mor
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder tar = mtarget mor
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder im = typeIdMap mor
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder jm = classIdMap mor
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder tm = filterAliases $ typeMap tar
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder classSymMap = Map.foldWithKey ( \ i ti ->
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder k = rawKind ti
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder in Map.insert (idToClassSymbol i k)
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder $ idToClassSymbol j k) Map.empty $ classMap src
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder k = typeKind ti
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder in Map.insert (idToTypeSymbol i k)
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder $ idToTypeSymbol j k) classSymMap $ typeMap src
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder let ty = opType oi
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder in Map.insert (idToOpSymbol i ty)
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder (idToOpSymbol j t2)) m s)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder typeSymMap $ assumps src