Morphism.hs revision 3d3889e0cefcdce9b3f43c53aaa201943ac2e895
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederDescription : morphisms implementation
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederMaintainer : Christian.Maeder@dfki.de
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedermapping entities of morphisms
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederimport Common.Utils (composeMap)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport qualified Data.Set as Set
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maederimport qualified Data.Map as Map
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdisjointKeys :: (Ord a, Pretty a, Monad m) => Map.Map a b -> Map.Map a c
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdisjointKeys m1 m2 = let d = Map.keysSet $ Map.intersection m1 m2 in
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder unless (Set.null d) $ fail $ show
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (sep [ text "overlapping identifiers for types and classes:"
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder-- | map a kind along an identifier map
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedermapKindI :: IdMap -> Kind -> Kind
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapKindI jm = mapKind (\ a -> Map.findWithDefault a a jm)
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder-- | map a kind along a signature morphism (variance is preserved)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapKinds :: Morphism -> Kind -> Kind
120efeede54a5f7650cda8e91363bd6832eac9a9Christian MaedermapKinds = mapKindI . classIdMap
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder-- | only rename the kinds in a type
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapKindsOfType jm tm im = foldType mapTypeRec
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { foldTypeAbs = \ _ -> TypeAbs . mapTypeArg jm tm im
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder , foldKindedType = \ _ t -> KindedType t . Set.map (mapKindI jm) }
120efeede54a5f7650cda8e91363bd6832eac9a9Christian Maeder-- | map type, expand it, and also adjust the kinds
ce3928e71520030ad0275b72050a8f4377f9313cChristian MaedermapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapTypeE jm tm im =
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder mapKindsOfType jm tm im . expandAliases tm . mapType im
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder-- | map a kind along a signature morphism (variance is preserved)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapVarKind jm tm im vk = case vk of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder VarKind k -> VarKind $ mapKindI jm k
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Downset ty -> Downset $ mapTypeE jm tm im ty
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian MaedermapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapTypeArg jm tm im (TypeArg i v vk rk c s r) =
d92635f998347112e5d5803301c2abfe7832ab65Christian Maeder TypeArg i v (mapVarKind jm tm im vk) rk c s r
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedermapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapTypeScheme jm tm im (TypeScheme args ty ps) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedermapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedergetDatatypeIds :: DataEntry -> Set.Set Id
024621f43239cfe9629e35d35a8669fad7acbba2Christian MaedergetDatatypeIds (DataEntry _ i _ _ _ alts) =
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian Maeder let getAltIds (Construct _ tys _ sels) = Set.union
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder (Set.unions $ map getTypeIds tys)
d48085f765fca838c1d972d2123601997174583dChristian Maeder $ Set.unions $ concatMap (map getSelIds) sels
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder getSelIds (Select _ ty _) = getTypeIds ty
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder getTypeIds = idsOf (== 0)
d48085f765fca838c1d972d2123601997174583dChristian Maeder in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedermapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian MaedermapDataEntry jm tm im fm (DataEntry dm i k args rk alts) =
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder let nDm = Map.map (\ a -> Map.findWithDefault a a im) dm
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder newargs = map (mapTypeArg jm tm im) args
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder in DataEntry nDm i k newargs rk $ Set.map
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder (mapAlt jm tm im fm nIm newargs
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder $ patToType (Map.findWithDefault i i dm) newargs rk) alts
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaedermapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder -> AltDefn -> AltDefn
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedermapAlt jm tm im fm nIm args dt (Construct mi ts p sels) =
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian Maeder let newTs = map (mapTypeE jm tm nIm) ts
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian Maeder newSels = map (map (mapSel jm tm im fm nIm args dt)) sels
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian Maeder in case mi of
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian Maeder Just i -> let
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder sc = TypeScheme args (getFunType dt p ts) nullRange
ae8052003e1ec7247597f034069db0939a7387e1Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder in Construct (Just j) newTs (getPartiality newTs ty) newSels
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder Nothing -> Construct mi newTs p newSels
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedermapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder -> Selector -> Selector
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian MaedermapSel jm tm im fm nIm args dt (Select mid t p) =
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder let newT = mapTypeE jm tm nIm t
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder in case mid of
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder Nothing -> Select mid newT p
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder Just i -> let
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder sc = TypeScheme args (getSelType dt p t) nullRange
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder in Select (Just j) newT $ getPartiality [dt] ty
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder{- | get the partiality from a constructor type
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maederwith a given number of curried arguments. -}
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian MaedergetPartiality :: [a] -> Type -> Partiality
04a1ed0b360858b85de6f449b84df4eab81b3fc9Christian MaedergetPartiality args t = case getTypeAppl t of
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder [_] -> if isPartialArrow i then Partial else Total
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder _ : rs -> getPartiality rs res
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder if null args then Partial else error "getPartiality"
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian MaedermapSentence m s = let
932f71e6f6f404ac139399c3d6a2b906ba055cbdChristian Maeder tm = filterAliases . typeMap $ mtarget m
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder im = typeIdMap m
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder jm = classIdMap m
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder fm = funMap m
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder f = mapFunSym jm tm im fm
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder in return $ case s of
e997f1724fcc2c5bb49f44e9f45e8354e0f3a2d6Christian Maeder Formula t -> Formula $ mapSen jm tm im fm t
d48085f765fca838c1d972d2123601997174583dChristian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ProgEqSen i sc pe ->
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder let (ni, nsc) = f (i, sc)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder in ProgEqSen ni nsc $ mapEq (f, mapTypeE jm tm im) pe
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -> (Id, TypeScheme)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedermapFunSym jm tm im fm (i, sc) =
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder let msc = mapTypeScheme jm tm im sc
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder in Map.findWithDefault (i, msc) (i, sc) fm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederideMor :: Env -> Morphism
37354e3ed68875fb527338105a610df481f98cb0Christian MaederideMor e = mkMorphism e e
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedercompMor m1 m2 = let
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tm1 = typeIdMap m1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tm2 = typeIdMap m2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ctm = composeMap (typeMap src) tm1 tm2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder cm1 = classIdMap m1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder cm2 = classIdMap m2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ccm = composeMap (classMap src) cm1 cm2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fm2 = funMap m2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fm1 = funMap m1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tar = mtarget m2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder src = msource m1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tm = filterAliases $ typeMap tar
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder emb = mkMorphism src tar
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in if isInclMor m1 && isInclMor m2 then return emb else do
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder disjointKeys ctm ccm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { typeIdMap = ctm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , classIdMap = ccm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Map.foldWithKey ( \ p1@(i, sc) p2 ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let p3 = mapFunSym ccm tm tm2 fm2 p2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder nSc = mapTypeScheme ccm tm ctm sc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in if (i, nSc) == p3 then Map.delete p1 else
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder concatMap ( \ (k, os) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map ( \ o -> ((k, opType o), ())) $ Set.toList os)
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder $ Map.toList $ assumps src }
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaedershowEnvDiff :: Env -> Env -> String
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaedershowEnvDiff e1 e2 =
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian Maeder (diffEnv e1 e2) ""
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaederlegalMor :: Morphism -> Result ()
24f79601ad5e42ce74f4152a36aad257d7c4d7b5Christian MaederlegalMor m = let
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder s = msource m
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder t = mtarget m
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder ts = typeIdMap m
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder cs = classIdMap m
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder fs = funMap m in
79bf169bcae16ce390683c698bae248c1ed6ab13Christian Maeder unless (all (`elem` Map.keys (typeMap s)) (Map.keys ts)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder && all (`elem` Map.keys (typeMap t)) (Map.elems ts)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder && all (`elem` Map.keys (classMap s)) (Map.keys cs)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder && all (`elem` Map.keys (classMap t)) (Map.elems cs)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs))
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder (fail "illegal HasCASL morphism")
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
d50ea352472823a62196db3cf11fae2af6866ab6Christian MaedermorphismUnion m1 m2 = do
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder let s1 = msource m1
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder s2 = msource m2
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder s <- merge s1 s2
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder t <- merge (mtarget m1) $ mtarget m2
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder let tm1 = typeMap s1
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder tm2 = typeMap s2
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder im1 = typeIdMap m1
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder im2 = typeIdMap m2
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder -- unchanged types
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder ut1 = Map.keysSet tm1 Set.\\ Map.keysSet im1
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder ut2 = Map.keysSet tm2 Set.\\ Map.keysSet im2
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder ima1 = Map.union im1 $ setToMap ut1
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder ima2 = Map.union im2 $ setToMap ut2
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder sAs = filterAliases $ typeMap s
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder tAs = filterAliases $ typeMap t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder cm1 = classMap s1
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder cm2 = classMap s2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder jm1 = classIdMap m1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder jm2 = classIdMap m2
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder -- unchanged classes
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2
f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder cima1 = Map.union jm1 $ setToMap cut1
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder cima2 = Map.union jm2 $ setToMap cut2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder expP = Map.fromList . map ( \ ((i, o), (j, p)) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ((i, expand tAs o), (j, expand tAs p)))
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder fm1 = expP $ funMap m1
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder fm2 = expP $ funMap m2
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder af jm im = Set.unions . map ( \ (i, os) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Set.map ( \ o -> (i, mapTypeScheme jm tAs im
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ expand sAs $ opType o)) os)
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder -- unchanged functions
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder fma1 = Map.union fm1 $ setToMap uf1
d50ea352472823a62196db3cf11fae2af6866ab6Christian Maeder fma2 = Map.union fm2 $ setToMap uf2
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder showFun (i, ty) = showId i . (" : " ++) . showDoc ty
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder fail $ "incompatible type mapping to `"
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder fail $ "incompatible class mapping to `"
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder fail $ "incompatible mapping to '"
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder disjointKeys tma cma
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (mkMorphism s t)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { typeIdMap = tma
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder , classIdMap = cma
99edc5256de959957a8c27b05ae4ad4f0572233dChristian Maeder , funMap = fma }
99edc5256de959957a8c27b05ae4ad4f0572233dChristian MaedermorphismToSymbMap :: Morphism -> SymbolMap
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian MaedermorphismToSymbMap mor = let
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder src = msource mor
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder tar = mtarget mor
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder im = typeIdMap mor
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder jm = classIdMap mor
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder tm = filterAliases $ typeMap tar
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder classSymMap = Map.foldWithKey ( \ i ti ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder k = rawKind ti
966e627a1c06b302a06d59d08b8ab45905f3509cChristian Maeder in Map.insert (idToClassSymbol i k)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ idToClassSymbol j k) Map.empty $ classMap src
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder k = typeKind ti
8452387b4c54b8dd36c012b216e0b0c5004ca6f1Christian Maeder in Map.insert (idToTypeSymbol i k)
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder $ idToTypeSymbol j k) classSymMap $ typeMap src
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let ty = opType oi
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in Map.insert (idToOpSymbol i ty)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (idToOpSymbol j t2)) m s)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder typeSymMap $ assumps src