Morphism.hs revision 18b513ff41708f24e1a7407f36b719add813ffea
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederDescription : morphisms implementation
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : provisional
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maedermapping entities of morphisms
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport qualified Data.Set as Set
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport qualified Data.Map as Map
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederinstance Eq Morphism where
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder m1 == m2 = (msource m1, mtarget m1, typeIdMap m1, classIdMap m1, funMap m1)
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder == (msource m2, mtarget m2, typeIdMap m2, classIdMap m2, funMap m2)
ad270004874ce1d0697fb30d7309f180553bb315Christian MaederdisjointKeys :: (Ord a, Pretty a, Monad m) => Map.Map a b -> Map.Map a c
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian MaederdisjointKeys m1 m2 = let d = Map.keysSet $ Map.intersection m1 m2 in
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder if Set.null d then return () else
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder (sep [ text "overlapping identifiers for types and classes:"
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- | map a kind along an identifier map
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermapKindI :: IdMap -> Kind -> Kind
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermapKindI jm = mapKind $ (\ a -> Map.findWithDefault a a jm)
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder-- | map a kind along a signature morphism (variance is preserved)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermapKinds :: Morphism -> Kind -> Kind
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermapKinds mor = mapKindI $ classIdMap mor
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- | only rename the kinds in a type
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedermapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
53301de22afd7190981b363b57c48df86fcb50f7Christian MaedermapKindsOfType jm tm im = foldType mapTypeRec
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder { foldTypeAbs = \ _ a t p -> TypeAbs (mapTypeArg jm tm im a) t p
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder , foldKindedType = \ _ t ks p -> KindedType t
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder (Set.map (mapKindI jm) ks) p }
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder-- | map type, expand it, and also adjust the kinds
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermapTypeE jm tm im =
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder mapKindsOfType jm tm im . expandAliases tm . mapType im
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | map a kind along a signature morphism (variance is preserved)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermapVarKind jm tm im vk = case vk of
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder VarKind k -> VarKind $ mapKindI jm k
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Downset ty -> Downset $ mapTypeE jm tm im ty
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermapTypeArg jm tm im (TypeArg i v vk rk c s r) =
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TypeArg i v (mapVarKind jm tm im vk) rk c s r
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedermapTypeScheme jm tm im (TypeScheme args ty ps) =
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaedermapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaedermapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian MaedersetToMap :: Ord a => Set.Set a -> Map.Map a a
c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian MaedersetToMap = Map.fromAscList . map ( \ a -> (a, a)) . Set.toList
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedergetDatatypeIds :: DataEntry -> Set.Set Id
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedergetDatatypeIds (DataEntry _ i _ _ _ alts) =
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder let getAltIds (Construct _ tys _ sels) = Set.union
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder (Set.unions $ map getTypeIds tys)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ Set.unions $ concatMap (map getSelIds) sels
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder getSelIds (Select _ ty _) = getTypeIds ty
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder getTypeIds = idsOf (== 0)
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedermapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedermapDataEntry jm tm im fm de@(DataEntry dm i k args rk alts) =
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder let tim = Map.intersection (compIdMap dm im) $ setToMap $ getDatatypeIds de
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder newargs = map (mapTypeArg jm tm im) args
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder in DataEntry tim i k newargs rk $ Set.map
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder (mapAlt jm tm tim fm newargs
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder $ patToType (Map.findWithDefault i i tim) args rk) alts
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedermapAlt jm tm im fm args dt c@(Construct mi ts p sels) =
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder let sc = TypeScheme args
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder (getFunType dt p $ map (mapTypeE jm tm im) ts) nullRange
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder in Construct (Just j) ts (getPartiality ts ty) $
add9c81ed5250ba046a8581ff75b2284bd69e219Christian Maeder map (map (mapSel jm tm im fm args dt)) sels
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> Selector
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermapSel jm tm im fm args dt s@(Select mid t p) = case mid of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just i -> let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder sc = TypeScheme args (getSelType dt p $ mapTypeE jm tm im t) nullRange
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in Select (Just j) t $ getPartiality [dt] ty
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | get the partiality from a constructor type
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- with a given number of curried arguments
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergetPartiality :: [a] -> Type -> Partiality
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergetPartiality args t = case getTypeAppl t of
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder [_] -> if isPartialArrow i then Partial else Total
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ : rs -> getPartiality rs res
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder if null args then Partial else error "getPartiality"
639732746d7c3a586790043b452a4cbdd29a3fc3Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
639732746d7c3a586790043b452a4cbdd29a3fc3Christian MaedermapSentence m s = let
639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder tm = filterAliases $ typeMap $ mtarget m
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder im = typeIdMap m
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder jm = classIdMap m
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder fm = funMap m
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder f = mapFunSym jm tm im fm
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder in return $ case s of
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Formula t -> Formula $ mapSen jm tm im fm t
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder ProgEqSen i sc pe ->
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder let (ni, nsc) = f (i, sc)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in ProgEqSen ni nsc $ mapEq (f, mapTypeE jm tm im) pe
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedermapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -> (Id, TypeScheme)
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaedermapFunSym jm tm im fm (i, sc) =
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder let msc = mapTypeScheme jm tm im sc
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder in Map.findWithDefault (i, msc) (i, msc) fm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederideMor :: Env -> Morphism
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederideMor e = mkMorphism e e
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedercompIdMap im1 im2 = Map.foldWithKey ( \ i j ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let k = Map.findWithDefault j j im2 in
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder if i == k then id else Map.insert i k) im2 im1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedercompMor m1 m2 = if mtarget m1 == msource m2 then
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let tm1 = typeIdMap m1
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder tm2 = typeIdMap m2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder im = compIdMap tm1 tm2
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder cm1 = classIdMap m1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder cm2 = classIdMap m2
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder cm = compIdMap cm1 cm2
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder fm2 = funMap m2
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder fm1 = funMap m1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder tar = mtarget m2
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder src = msource m1
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder tm = filterAliases $ typeMap tar
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ctm = Map.intersection im $ typeMap src
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder ccm = Map.intersection cm $ classMap src
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder emb = mkMorphism src tar
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in if Map.null tm1 && Map.null tm2 && Map.null cm1 && Map.null cm2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder && Map.null fm1 && Map.null fm2 then return emb else do
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder disjointKeys ctm ccm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder { typeIdMap = ctm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder , classIdMap = ccm
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder , funMap = Map.intersection (Map.foldWithKey ( \ p1 p2 ->
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder let p3 = mapFunSym cm tm tm2 fm2 p2 in
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder if p1 == p3 then id else Map.insert p1 p3)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder concatMap ( \ (k, os) ->
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder map ( \ o -> ((k, mapTypeScheme cm tm im
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ opType o), ())) $ Set.toList os)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder $ Map.toList $ assumps src }
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder else fail "intermediate signatures of morphisms do not match"
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederinclusionMor :: Env -> Env -> Result Morphism
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederinclusionMor e1 e2 =
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder if isSubEnv e1 e2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder then return (mkMorphism e1 e2)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else Result [Diag Error
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ("Attempt to construct inclusion between non-subsignatures:\n"
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ++ showEnvDiff e1 e2) nullRange] Nothing
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedershowEnvDiff :: Env -> Env -> String
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedershowEnvDiff e1 e2 =
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (diffEnv e1 e2) ""
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederlegalEnv :: Env -> Bool
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederlegalEnv _ = True -- maybe a closure test?
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian MaederlegalMor :: Morphism -> Bool
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederlegalMor m = let
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder s = msource m
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder t = mtarget m
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ts = typeIdMap m
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder cs = classIdMap m
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder fs = funMap m in
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder all (`elem` Map.keys (typeMap s)) (Map.keys ts)
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder && all (`elem` Map.keys (typeMap t)) (Map.elems ts)
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder && all (`elem` Map.keys (classMap s)) (Map.keys cs)
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder && all (`elem` Map.keys (classMap t)) (Map.elems cs)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermorphismUnion m1 m2 = do
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder let s1 = msource m1
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder s2 = msource m2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder s <- merge s1 s2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder t <- merge (mtarget m1) $ mtarget m2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let tm1 = typeMap s1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder tm2 = typeMap s2
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder im1 = typeIdMap m1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder im2 = typeIdMap m2
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder -- unchanged types
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ut1 = Map.keysSet tm1 Set.\\ Map.keysSet im1
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ut2 = Map.keysSet tm2 Set.\\ Map.keysSet im2
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder ima1 = Map.union im1 $ setToMap ut1
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder ima2 = Map.union im2 $ setToMap ut2
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski sAs = filterAliases $ typeMap s
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder tAs = filterAliases $ typeMap t
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder cm1 = classMap s1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder cm2 = classMap s2
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder jm1 = classIdMap m1
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder jm2 = classIdMap m2
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder -- unchanged classes
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder cima1 = Map.union jm1 $ setToMap cut1
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder cima2 = Map.union jm2 $ setToMap cut2
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder expP = Map.fromList . map ( \ ((i, o), (j, p)) ->
09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ((i, expand tAs o), (j, expand tAs p)))
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder fm1 = expP $ funMap m1
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder fm2 = expP $ funMap m2
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder af jm im = Set.unions . map ( \ (i, os) ->
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder Set.map ( \ o -> (i, mapTypeScheme jm tAs im
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder $ expand sAs $ opType o)) os)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- unchanged functions
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder fma1 = Map.union fm1 $ setToMap uf1
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder fma2 = Map.union fm2 $ setToMap uf2
add9c81ed5250ba046a8581ff75b2284bd69e219Christian Maeder showFun (i, ty) = showId i . (" : " ++) . showDoc ty
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder fail $ "incompatible type mapping to `"
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder fail $ "incompatible class mapping to `"
7946f81bdc77b0790ac47ccaf2912a1d55c8336dChristian Maeder ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder fail $ "incompatible mapping to '"
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder disjointKeys tma cma
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder return (mkMorphism s t)
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder { typeIdMap = tma
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder , classIdMap = cma
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder , funMap = fma }
b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermorphismToSymbMap mor = let
add9c81ed5250ba046a8581ff75b2284bd69e219Christian Maeder src = msource mor
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder tar = mtarget mor
d27877901128f04518461d25b96d2d93a13f01e4Christian Maeder im = typeIdMap mor
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder jm = classIdMap mor
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder tm = filterAliases $ typeMap tar
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder classSymMap = Map.foldWithKey ( \ i ti ->
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder k = rawKind ti
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in Map.insert (idToClassSymbol src i k)
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder $ idToClassSymbol tar j k) Map.empty $ classMap src
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder k = typeKind ti
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder in Map.insert (idToTypeSymbol src i k)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder $ idToTypeSymbol tar j k) classSymMap $ typeMap src
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let ty = opType oi
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder in Map.insert (idToOpSymbol src i ty)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (idToOpSymbol tar j t2)) m s)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder typeSymMap $ assumps src