Morphism.hs revision 51fb5d7edd9369c367dda2f8b15ddd6f8a146606
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : morphisms implementation
f11f713bebd8e1e623a0a4361065df256033de47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
967e5f3c25249c779575864692935627004d3f9eChristian MaederStability : provisional
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPortability : portable
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedermapping entities of morphisms
ad187062b0009820118c1b773a232e29b879a2faChristian Maederimport qualified Data.Set as Set
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederinstance Eq Morphism where
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder m1 == m2 = (msource m1, mtarget m1, typeIdMap m1, classIdMap m1, funMap m1)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder == (msource m2, mtarget m2, typeIdMap m2, classIdMap m2, funMap m2)
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
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder if Set.null d then return () else
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
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder { foldTypeAbs = \ _ a t p -> TypeAbs (mapTypeArg jm tm im a) t p
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder , foldKindedType = \ _ t ks p -> KindedType t
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder (Set.map (mapKindI jm) ks) p }
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 MaedersetToMap :: Ord a => Set.Set a -> Map.Map a a
a89389521ddf76109168a0b339031575aafbd512Christian MaedersetToMap = Map.fromAscList . map ( \ a -> (a, a)) . Set.toList
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
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
1a75698c909ad515d59c76e65bd783f015c21c4dChristian MaedermapDataEntry jm tm im fm de@(DataEntry dm i k args rk alts) =
a89389521ddf76109168a0b339031575aafbd512Christian Maeder let tim = Map.intersection (compIdMap dm im) $ setToMap $ getDatatypeIds de
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder newargs = map (mapTypeArg jm tm im) args
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder in DataEntry tim i k newargs rk $ Set.map
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder (mapAlt jm tm tim fm newargs
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder $ patToType (Map.findWithDefault i i tim) newargs rk) alts
67d92da5e9610aabad39055a16031154b4dc3748Christian MaedermapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian MaedermapAlt jm tm im fm args dt (Construct mi ts p sels) =
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder let newTs = map (mapTypeE jm tm im) ts in case mi of
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder let sc = TypeScheme args (getFunType dt p newTs) nullRange
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder in Construct (Just j) ts (getPartiality ts ty) $
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder map (map (mapSel jm tm im fm args dt)) sels
51fb5d7edd9369c367dda2f8b15ddd6f8a146606Christian Maeder Nothing -> Construct mi newTs p sels
67d92da5e9610aabad39055a16031154b4dc3748Christian MaedermapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> Selector
67d92da5e9610aabad39055a16031154b4dc3748Christian MaedermapSel jm tm im fm args dt s@(Select mid t p) = case mid of
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder Just i -> let
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder sc = TypeScheme args (getSelType dt p $ mapTypeE jm tm im t) nullRange
67d92da5e9610aabad39055a16031154b4dc3748Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder in Select (Just j) t $ getPartiality [dt] ty
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder-- | get the partiality from a constructor type
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- with 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
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian 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)
67d92da5e9610aabad39055a16031154b4dc3748Christian 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
f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder in Map.findWithDefault (i, msc) (i, msc) fm
967e5f3c25249c779575864692935627004d3f9eChristian MaederideMor :: Env -> Morphism
18b513ff41708f24e1a7407f36b719add813ffeaChristian MaederideMor e = mkMorphism e e
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian MaedercompIdMap im1 im2 = if Map.null im2 then im1 else Map.foldWithKey ( \ i j ->
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder let k = Map.findWithDefault j j im2 in
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder if i == k then Map.delete i else Map.insert i k) im2 im1
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian MaedercompMor m1 m2 = if mtarget m1 == msource m2 then
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder let tm1 = typeIdMap m1
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder tm2 = typeIdMap m2
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder im = compIdMap tm1 tm2
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder cm1 = classIdMap m1
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu cm2 = classIdMap m2
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder cm = compIdMap 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
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder ctm = Map.intersection im $ typeMap src
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder ccm = Map.intersection cm $ classMap src
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
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder , funMap = Map.intersection (if Map.null fm2 then fm1 else
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder let p3 = mapFunSym cm tm tm2 fm2 p2 in
d769b9ca726a9b50d661847c0e58c41d6ef334b4Christian Maeder if p1 == p3 then Map.delete p1 else Map.insert p1 p3)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder concatMap ( \ (k, os) ->
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder map ( \ o -> ((k, mapTypeScheme cm tm im
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder $ opType o), ())) $ Set.toList os)
551af0e4ba6d96bb24f3555f3b30ed648e22e34aChristian Maeder $ Map.toList $ assumps src }
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder else fail "intermediate signatures of morphisms do not match"
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiinclusionMor :: Env -> Env -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinclusionMor e1 e2 =
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder if isSubEnv e1 e2
18b513ff41708f24e1a7407f36b719add813ffeaChristian Maeder then return (mkMorphism e1 e2)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder else Result [Diag Error
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder ("Attempt to construct inclusion between non-subsignatures:\n"
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski ++ showEnvDiff e1 e2) nullRange] Nothing
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) ""
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv :: Env -> Bool
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv _ = True -- maybe a closure test?
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalMor :: Morphism -> Bool
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
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder 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)
a95f5379cabb30d3beb0545002cf50e9e4fc2c86Christian Maeder && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs)
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
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder classSymMap = Map.foldWithKey ( \ i ti ->
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder k = rawKind ti
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder in Map.insert (idToClassSymbol src i k)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder $ idToClassSymbol tar j k) Map.empty $ classMap src
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder k = typeKind ti
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in Map.insert (idToTypeSymbol src i k)
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder $ idToTypeSymbol tar j k) classSymMap $ typeMap src
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder let ty = opType oi
1a75698c909ad515d59c76e65bd783f015c21c4dChristian Maeder (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder in Map.insert (idToOpSymbol src i ty)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder (idToOpSymbol tar j t2)) m s)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder typeSymMap $ assumps src