Morphism.hs revision 551af0e4ba6d96bb24f3555f3b30ed648e22e34a
8a77240a809197c92c0736c431b4b88947a7bac1Christian MaederModule : $Header$
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederDescription : morphisms implementation
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Christian.Maeder@dfki.de
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : provisional
306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedermapping entities of morphisms
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Set as Set
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Map as Map
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Eq Morphism where
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder m1 == m2 = (msource m1, mtarget m1, typeIdMap m1, classIdMap m1, funMap m1)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder == (msource m2, mtarget m2, typeIdMap m2, classIdMap m2, funMap m2)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederdisjointKeys :: (Ord a, Pretty a, Monad m) => Map.Map a b -> Map.Map a c
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederdisjointKeys m1 m2 = let d = Map.keysSet $ Map.intersection m1 m2 in
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski if Set.null d then return () else
922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder (sep [ text "overlapping identifiers for types and classes:"
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder-- | map a kind along an identifier map
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaedermapKindI :: IdMap -> Kind -> Kind
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKindI jm = mapKind $ (\ a -> Map.findWithDefault a a jm)
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder-- | map a kind along a signature morphism (variance is preserved)
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKinds :: Morphism -> Kind -> Kind
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKinds mor = mapKindI $ classIdMap mor
63324a97283728a30932828a612c7b0b0f687624Christian Maeder-- | only rename the kinds in a type
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKindsOfType jm tm im = foldType mapTypeRec
59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder { foldTypeAbs = \ _ a t p -> TypeAbs (mapTypeArg jm tm im a) t p
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , foldKindedType = \ _ t ks p -> KindedType t
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Set.map (mapKindI jm) ks) p }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | map type, expand it, and also adjust the kinds
53310804002cd9e3c9c5844db3b984abcf001788Christian MaedermapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeE jm tm im =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapKindsOfType jm tm im . expandAliases tm . mapType im
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | map a kind along a signature morphism (variance is preserved)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapVarKind jm tm im vk = case vk of
3a87487c048b275c56e502c4a933273788e8d0bbChristian Maeder VarKind k -> VarKind $ mapKindI jm k
2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu Downset ty -> Downset $ mapTypeE jm tm im ty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapTypeArg jm tm im (TypeArg i v vk rk c s r) =
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder TypeArg i v (mapVarKind jm tm im vk) rk c s r
8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill MossakowskimapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
d97cb7d1c9beadc4d9102738da0a88c4efcf8fddChristian MaedermapTypeScheme jm tm im (TypeScheme args ty ps) =
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskimapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)
d97cb7d1c9beadc4d9102738da0a88c4efcf8fddChristian MaedersetToMap = Map.fromAscList . map ( \ a -> (a, a)) . Set.toList
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedergetDatatypeIds :: DataEntry -> Set.Set Id
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedergetDatatypeIds (DataEntry _ i _ _ _ alts) =
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder let getAltIds (Construct _ tys _ sels) = Set.union
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder (Set.unions $ map getTypeIds tys)
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder $ Set.unions $ concatMap (map getSelIds) sels
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder getSelIds (Select _ ty _) = getTypeIds ty
3d86f079b07a6a058cdd6c112d287e01a69d9c0cChristian Maeder getTypeIds = idsOf (== 0)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapDataEntry jm tm im fm de@(DataEntry dm i k args rk alts) =
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder let tim = Map.intersection (compIdMap dm im) $ setToMap $ getDatatypeIds de
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu newargs = map (mapTypeArg jm tm im) args
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder in DataEntry tim i k newargs rk $ Set.map
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder (mapAlt jm tm tim fm newargs
a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder $ patToType (Map.findWithDefault i i tim) args rk) alts
a975722baf6fee1ca3e67df170c732c4abd0a945Christian MaedermapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaedermapAlt jm tm im fm args dt c@(Construct mi ts p sels) =
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder let sc = TypeScheme args
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder (getFunType dt p $ map (mapTypeE jm tm im) ts) nullRange
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder in Construct (Just j) ts (getPartiality ts ty) $
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu map (map (mapSel jm tm im fm args dt)) sels
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaedermapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> Selector
0e51a998b1b213654c7a9eca451562041971f100Till MossakowskimapSel jm tm im fm args dt s@(Select mid t p) = case mid of
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder Just i -> let
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder sc = TypeScheme args (getSelType dt p $ mapTypeE jm tm im t) nullRange
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder in Select (Just j) t $ getPartiality [dt] ty
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder-- | get the partiality from a constructor type
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder-- with a given number of curried arguments
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedergetPartiality :: [a] -> Type -> Partiality
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedergetPartiality args t = case getTypeAppl t of
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder [_] -> if isPartialArrow i then Partial else Total
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder _ : rs -> getPartiality rs res
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder if null args then Partial else error "getPartiality"
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaedermapSentence m s = let
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder tm = filterAliases $ typeMap $ mtarget m
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder im = typeIdMap m
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder jm = classIdMap m
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fm = funMap m
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder f = mapFunSym jm tm im fm
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder in return $ case s of
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Formula t -> Formula $ mapSen jm tm im fm t
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder ProgEqSen i sc pe ->
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder let (ni, nsc) = f (i, sc)
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder in ProgEqSen ni nsc $ mapEq (f, mapTypeE jm tm im) pe
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> (Id, TypeScheme)
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapFunSym jm tm im fm (i, sc) =
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let msc = mapTypeScheme jm tm im sc
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder in Map.findWithDefault (i, msc) (i, msc) fm
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederembedMorphism :: Env -> Env -> Morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederembedMorphism = mkMorphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederideMor :: Env -> Morphism
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederideMor e = embedMorphism e e
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompIdMap im1 im2 = Map.foldWithKey ( \ i j ->
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let k = Map.findWithDefault j j im2 in
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu if i == k then id else Map.insert i k) im2 im1
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaedercompMor m1 m2 =
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder if mtarget m1 == msource m2 then do
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder let tm2 = typeIdMap m2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder im = compIdMap (typeIdMap m1) tm2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder cm2 = classIdMap m2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder cm = compIdMap (classIdMap m1) cm2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder fm2 = funMap m2
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder tar = mtarget m2
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder src = msource m1
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder tm = filterAliases $ typeMap tar
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder ctm = Map.intersection im $ typeMap src
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder ccm = Map.intersection cm $ classMap src
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder disjointKeys ctm ccm
255f43c567972176c2078e3de2fb7a2798bcfde0Christian Maeder return (mkMorphism src tar)
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder { typeIdMap = ctm
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder , classIdMap = ccm
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder , funMap = Map.intersection (Map.foldWithKey ( \ p1 p2 ->
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder let p3 = mapFunSym cm tm tm2 fm2 p2 in
9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder if p1 == p3 then id else Map.insert p1 p3)
24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder fm2 $ funMap m1) $ Map.fromList $
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder concatMap ( \ (k, os) ->
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder map ( \ o -> ((k, mapTypeScheme cm tm im
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder $ opType o), ())) $ Set.toList os)
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder $ Map.toList $ assumps src }
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder else fail "intermediate signatures of morphisms do not match"
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederinclusionMor :: Env -> Env -> Result Morphism
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian MaederinclusionMor e1 e2 =
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder if isSubEnv e1 e2
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder then return (embedMorphism e1 e2)
6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder else Result [Diag Error
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder ("Attempt to construct inclusion between non-subsignatures:\n"
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder ++ showEnvDiff e1 e2) nullRange] Nothing
19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaedershowEnvDiff :: Env -> Env -> String
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaedershowEnvDiff e1 e2 =
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc
a129422b14eea673dc481d2553cec108e35e72efChristian Maeder (diffEnv e1 e2) ""
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederlegalEnv :: Env -> Bool
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederlegalEnv _ = True -- maybe a closure test?
556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederlegalMor :: Morphism -> Bool
3946c010d94321f14139e12061dd4261a3cc7295Christian MaederlegalMor m = let
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich s = msource m
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich t = mtarget m
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ts = typeIdMap m
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich cs = classIdMap m
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fs = funMap m in
6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu all (`elem` Map.keys (typeMap s)) (Map.keys ts)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder && all (`elem` Map.keys (typeMap t)) (Map.elems ts)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder && all (`elem` Map.keys (classMap s)) (Map.keys cs)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder && all (`elem` Map.keys (classMap t)) (Map.elems cs)
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs)
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmorphismUnion :: Morphism -> Morphism -> Result Morphism
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmorphismUnion m1 m2 = do
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich let s1 = msource m1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich s2 = msource m2
da955132262baab309a50fdffe228c9efe68251dCui Jian s <- merge s1 s2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich t <- merge (mtarget m1) $ mtarget m2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich let tm1 = typeMap s1
da955132262baab309a50fdffe228c9efe68251dCui Jian tm2 = typeMap s2
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder im1 = typeIdMap m1
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder im2 = typeIdMap m2
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -- unchanged types
556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ut1 = Map.keysSet tm1 Set.\\ Map.keysSet im1
fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder ut2 = Map.keysSet tm2 Set.\\ Map.keysSet im2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ima1 = Map.union im1 $ setToMap ut1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ima2 = Map.union im2 $ setToMap ut2
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder sAs = filterAliases $ typeMap s
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder tAs = filterAliases $ typeMap t
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder cm1 = classMap s1
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder cm2 = classMap s2
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder jm1 = classIdMap m1
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder jm2 = classIdMap m2
3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder -- unchanged classes
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder cima1 = Map.union jm1 $ setToMap cut1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cima2 = Map.union jm2 $ setToMap cut2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski expP = Map.fromList . map ( \ ((i, o), (j, p)) ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ((i, expand tAs o), (j, expand tAs p)))
6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu fm1 = expP $ funMap m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fm2 = expP $ funMap m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski af jm im = Set.unions . map ( \ (i, os) ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Set.map ( \ o -> (i, mapTypeScheme jm tAs im
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ expand sAs $ opType o)) os)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder -- unchanged functions
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fma1 = Map.union fm1 $ setToMap uf1
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fma2 = Map.union fm2 $ setToMap uf2
3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder showFun (i, ty) = showId i . (" : " ++) . showDoc ty
3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder fail $ "incompatible type mapping to `"
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder fail $ "incompatible class mapping to `"
27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
da955132262baab309a50fdffe228c9efe68251dCui Jian fail $ "incompatible mapping to '"
da955132262baab309a50fdffe228c9efe68251dCui Jian ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
da955132262baab309a50fdffe228c9efe68251dCui Jian disjointKeys tma cma
eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich return (mkMorphism s t)
da955132262baab309a50fdffe228c9efe68251dCui Jian { typeIdMap = tma
a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu , classIdMap = cma
f2c050360525df494e6115073b0edc4c443a847cMihai Codescu , funMap = fma }
b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap
da955132262baab309a50fdffe228c9efe68251dCui JianmorphismToSymbMap mor = let
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder src = msource mor
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder tar = mtarget mor
ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder im = typeIdMap mor
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder jm = classIdMap mor
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder tm = filterAliases $ typeMap tar
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder classSymMap = Map.foldWithKey ( \ i ti ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski k = rawKind ti
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Map.insert (idToClassSymbol src i k)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ idToClassSymbol tar j k) Map.empty $ classMap src
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski typeSymMap = Map.foldWithKey ( \ i ti ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski k = typeKind ti
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder in Map.insert (idToTypeSymbol src i k)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder $ idToTypeSymbol tar j k) classSymMap $ typeMap src
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let ty = opType oi
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Map.insert (idToOpSymbol src i ty)
d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder (idToOpSymbol tar j t2)) m s)
53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder typeSymMap $ assumps src