Morphism.hs revision ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiModule : $Header$
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiDescription : morphisms implementation
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiMaintainer : Christian.Maeder@dfki.de
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiStability : provisional
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiPortability : portable
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimapping entities of morphisms
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.Utils (composeMap)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.Lib.Rel (setToMap)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Data.Set as Set
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Data.Map as Map
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskidisjointKeys :: (Ord a, Pretty a, Monad m) => Map.Map a b -> Map.Map a c
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskidisjointKeys m1 m2 = let d = Map.keysSet $ Map.intersection m1 m2 in
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski unless (Set.null d) $ fail $ show
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (sep [ text "overlapping identifiers for types and classes:"
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski-- | map a kind along an identifier map
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKindI :: IdMap -> Kind -> Kind
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKindI jm = mapKind (\ a -> Map.findWithDefault a a jm)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | map a kind along a signature morphism (variance is preserved)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKinds :: Morphism -> Kind -> Kind
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKinds = mapKindI . classIdMap
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | only rename the kinds in a type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKindsOfType jm tm im = foldType mapTypeRec
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { foldTypeAbs = \ _ -> TypeAbs . mapTypeArg jm tm im
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , foldKindedType = \ _ t -> KindedType t . Set.map (mapKindI jm) }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | map type, expand it, and also adjust the kinds
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeE :: 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
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski VarKind k -> VarKind $ mapKindI jm k
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Downset ty -> Downset $ mapTypeE jm tm im ty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeArg jm tm im (TypeArg i v vk rk c s r) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski TypeArg i v (mapVarKind jm tm im vk) rk c s r
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeScheme jm tm im (TypeScheme args ty ps) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till MossakowskigetDatatypeIds :: DataEntry -> Set.Set Id
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till MossakowskigetDatatypeIds (DataEntry _ i _ _ _ alts) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let getAltIds (Construct _ tys _ sels) = Set.union
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Set.unions $ map getTypeIds tys)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ Set.unions $ concatMap (map getSelIds) sels
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski getSelIds (Select _ ty _) = getTypeIds ty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski getTypeIds = idsOf (== 0)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapDataEntry jm tm im fm (DataEntry dm i k args rk alts) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let nDm = Map.map (\ a -> Map.findWithDefault a a im) dm
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski newargs = map (mapTypeArg jm tm im) args
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in DataEntry nDm i k newargs rk $ Set.map
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (mapAlt jm tm im fm nIm newargs
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ patToType (Map.findWithDefault i i dm) newargs rk) alts
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> AltDefn -> AltDefn
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapAlt jm tm im fm nIm args dt (Construct mi ts p sels) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let newTs = map (mapTypeE jm tm nIm) ts
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski newSels = map (map (mapSel jm tm im fm nIm args dt)) sels
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in case mi of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just i -> let
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sc = TypeScheme args (getFunType dt p ts) nullRange
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Construct (Just j) newTs (getPartiality newTs ty) newSels
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Nothing -> Construct mi newTs p newSels
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> IdMap -> [TypeArg] -> Type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> Selector -> Selector
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSel jm tm im fm nIm args dt (Select mid t p) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let newT = mapTypeE jm tm nIm t
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in case mid of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Nothing -> Select mid newT p
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just i -> let
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sc = TypeScheme args (getSelType dt p t) nullRange
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Select (Just j) newT $ getPartiality [dt] ty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | get the partiality from a constructor type
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- with a given number of curried arguments
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskigetPartiality :: [a] -> Type -> Partiality
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskigetPartiality args t = case getTypeAppl t of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (TypeName i _ _, [_, res]) | isArrow i -> case args of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski [_] -> if isPartialArrow i then Partial else Total
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski _ : rs -> getPartiality rs res
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (TypeName i _ _, [_]) | i == lazyTypeId ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski if null args then Partial else error "getPartiality"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSentence :: Morphism -> Sentence -> Result Sentence
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapSentence m s = let
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tm = filterAliases . typeMap $ mtarget m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski im = typeIdMap m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski jm = classIdMap m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fm = funMap m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski f = mapFunSym jm tm im fm
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in return $ case s of
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Formula t -> Formula $ mapSen jm tm im fm t
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ProgEqSen i sc pe ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let (ni, nsc) = f (i, sc)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in ProgEqSen ni nsc $ mapEq (f, mapTypeE jm tm im) pe
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -> (Id, TypeScheme)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapFunSym jm tm im fm (i, sc) =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let msc = mapTypeScheme jm tm im sc
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Map.findWithDefault (i, msc) (i, sc) fm
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiideMor :: Env -> Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiideMor e = mkMorphism e e
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskicompMor :: Morphism -> Morphism -> Result Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskicompMor m1 m2 =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let tm1 = typeIdMap m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tm2 = typeIdMap m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ctm = composeMap (typeMap src) tm1 tm2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cm1 = classIdMap m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cm2 = classIdMap m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ccm = composeMap (classMap src) cm1 cm2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fm2 = funMap m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fm1 = funMap m1
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski tar = mtarget m2
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski src = msource m1
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski tm = filterAliases $ typeMap tar
f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski emb = mkMorphism src tar
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in if isInclMor m1 && isInclMor m2 then return emb else do
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski disjointKeys ctm ccm
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { typeIdMap = ctm
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , classIdMap = ccm
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Map.foldWithKey ( \ p1@(i, sc) p2 ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let p3 = mapFunSym ccm tm tm2 fm2 p2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski nSc = mapTypeScheme ccm tm ctm sc
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in if (i, nSc) == p3 then Map.delete p1 else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski concatMap ( \ (k, os) ->
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski map ( \ o -> ((k, opType o), ())) $ Set.toList os)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ Map.toList $ assumps src }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskishowEnvDiff :: Env -> Env -> String
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskishowEnvDiff e1 e2 =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ showDoc e2 "\nDifference\n" ++ showDoc
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (diffEnv e1 e2) ""
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskilegalEnv :: Env -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskilegalEnv _ = True -- maybe a closure test?
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskilegalMor :: Morphism -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskilegalMor m = let
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski s = msource m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski t = mtarget m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ts = typeIdMap m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cs = classIdMap m
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fs = funMap m in
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski all (`elem` Map.keys (typeMap s)) (Map.keys ts)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski && all (`elem` Map.keys (typeMap t)) (Map.elems ts)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski && all (`elem` Map.keys (classMap s)) (Map.keys cs)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski && all (`elem` Map.keys (classMap t)) (Map.elems cs)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimorphismUnion :: Morphism -> Morphism -> Result Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimorphismUnion m1 m2 = do
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let s1 = msource m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski s2 = msource m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski s <- merge s1 s2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski t <- merge (mtarget m1) $ mtarget m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let tm1 = typeMap s1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tm2 = typeMap s2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski im1 = typeIdMap m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski im2 = typeIdMap m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- unchanged types
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ut1 = Map.keysSet tm1 Set.\\ Map.keysSet im1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ut2 = Map.keysSet tm2 Set.\\ Map.keysSet im2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ima1 = Map.union im1 $ setToMap ut1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ima2 = Map.union im2 $ setToMap ut2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sAs = filterAliases $ typeMap s
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tAs = filterAliases $ typeMap t
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cm1 = classMap s1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cm2 = classMap s2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski jm1 = classIdMap m1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski jm2 = classIdMap m2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- unchanged classes
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 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)))
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 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)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- unchanged functions
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fma1 = Map.union fm1 $ setToMap uf1
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fma2 = Map.union fm2 $ setToMap uf2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski showFun (i, ty) = showId i . (" : " ++) . showDoc ty
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fail $ "incompatible type mapping to `"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fail $ "incompatible class mapping to `"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fail $ "incompatible mapping to '"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski disjointKeys tma cma
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (mkMorphism s t)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski { typeIdMap = tma
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , classIdMap = cma
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , funMap = fma }
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimorphismToSymbMap :: Morphism -> SymbolMap
e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimorphismToSymbMap mor = let
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski src = msource mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tar = mtarget mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski im = typeIdMap mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski jm = classIdMap mor
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tm = filterAliases $ typeMap tar
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski 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
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Map.insert (idToTypeSymbol src i k)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ 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)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (idToOpSymbol tar j t2)) m s)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski typeSymMap $ assumps src