Merge.hs revision ee9eddfa6953868fd6fbaff0d9ff68675a13675a
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : hets@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder merging parts of local environment
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Data.List(nub, partition, nubBy)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance (Ord a, PosItem a, PrettyPrint a, Mergeable b)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder => Mergeable (Map.Map a b) where
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski merge = mergeMap merge
23a00c966f2aa8da525d7a7c51933c99964426c0Christian MaederimproveDiag :: (PosItem a, PrettyPrint a) => a -> Diagnosis -> Diagnosis
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederimproveDiag v d = d { diagString = let f:l = lines $ diagString d in
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder unlines $ (f ++ " of '" ++ showPretty v "'") : l
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder , diagPos = getMyPos v
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang , diagKind = case diagKind d of
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder FatalError -> Error
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeMap :: (Ord a, PosItem a, PrettyPrint a) => (b -> b -> Result b)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedermergeMap f m1 m2 = foldM ( \ m (k, v) ->
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Nothing -> return $ Map.insert k v m
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich let Result ds mu = f v w
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich ns = map (improveDiag k) ds
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich in case mu of
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Nothing -> Result ns $ Nothing
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Just u -> Result ns $ Just $ Map.insert k u m)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance Mergeable a => Mergeable (Maybe a) where
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder merge m1 m2 = case m1 of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Nothing -> return m2
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu Just v1 -> case m2 of
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder Nothing -> return m1
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder Just v2 -> do v <- merge v1 v2
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder return $ Just v
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maederinstance Mergeable ClassInfo where
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder merge c1 c2 = if c1 == c2 then
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else fail "merge: non-equal super classes"
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maederinstance Mergeable Kind where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge k1 k2 = if k1 == k2 then return k1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else fail "merge: non-equal kinds"
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeList :: Eq a => [a] -> [a] -> Result [a]
d79e02625778d20a5458078f979ff74aac67db61Christian MaedermergeList l1 l2 = return $ nub (l1 ++ l2)
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaedermergeTypeInfo :: TypeMap -> Int -> TypeInfo -> TypeInfo -> Result TypeInfo
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian MaedermergeTypeInfo tm c t1 t2 =
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder do k <- merge (typeKind t1) $ typeKind t2
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder o <- mergeList (otherTypeKinds t1) $ otherTypeKinds t2
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder s <- mergeList (superTypes t1) $ superTypes t2
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder d <- mergeTypeDefn tm c (typeDefn t1) $ typeDefn t2
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder return $ TypeInfo k o s d
d79e02625778d20a5458078f979ff74aac67db61Christian MaedermergeTypeDefn :: TypeMap -> Int -> TypeDefn -> TypeDefn -> Result TypeDefn
d79e02625778d20a5458078f979ff74aac67db61Christian MaedermergeTypeDefn tm c d1 d2 =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case (d1, d2) of
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (TypeVarDefn, TypeVarDefn) -> return d1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (TypeVarDefn, _) -> fail "merge: TypeVarDefn"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (_, TypeVarDefn) -> fail "merge: TypeVarDefn"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (_, DatatypeDefn _ _ _) -> return d2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (PreDatatype, _) -> fail "expected data type definition"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (_, PreDatatype) -> return d1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- (NoTypeDefn, AliasTypeDefn _) -> fail "merge: AliasTypeDefn"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- (AliasTypeDefn _, NoTypeDefn) -> fail "merge: AliasTypeDefn"
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (NoTypeDefn, _) -> return d2
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (_, NoTypeDefn) -> return d1
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (AliasTypeDefn s1, AliasTypeDefn s2) ->
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder do s <- mergeScheme tm c s1 s2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ AliasTypeDefn s
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Supertype v1 s1 t1, Supertype v2 s2 t2) ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do s <- mergeScheme tm c s1 s2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder v <- merge v1 v2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder t <- merge t1 t2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ Supertype v s t
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (_, _) -> if d1 == d2 then return d1 else
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder fail "merge: TypeDefn"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Mergeable Vars where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder merge t1 t2 = if t1 == t2 then return t1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else fail ("different variables for subtype definition\n\t"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ++ showPretty t1 "\n\t"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ++ showPretty t2 "\n\t")
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermergeScheme :: TypeMap -> Int -> TypeScheme -> TypeScheme -> Result TypeScheme
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeScheme tm c s1 s2 = let b = instScheme tm c s2 s1 in
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder if instScheme tm c s1 s2 then
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder if b then return s1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder else fail ("found scheme is only a subsitution instance"
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder ++ expected s1 s2)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder else if b then
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder fail ("expected scheme is only a subsitution instance"
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder ++ expected s1 s2)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else fail ("wrong type scheme" ++ expected s1 s2)
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian MaedermergeOpInfo :: TypeMap -> Int -> OpInfo -> OpInfo -> Result OpInfo
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeOpInfo tm c o1 o2 =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do sc <- mergeScheme tm c (opType o1) $ opType o2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder as <- mergeAttrs (opAttrs o1) $ opAttrs o2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder d <- mergeOpDefn tm (opDefn o1) $ opDefn o2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return $ OpInfo sc as d
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- instance Mergeable [OpAttr] where
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeAttrs :: [OpAttr] -> [OpAttr] -> Result [OpAttr]
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeAttrs l1 l2 =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let binAttr a = case a of BinOpAttr _ _ -> True
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (l1b, l1u) = partition binAttr l1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (l2b, l2u) = partition binAttr l2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder lb = nubBy ( \ (BinOpAttr b1 _) (BinOpAttr b2 _) -> b1 == b2)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in if null l1u || null l2u then
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return (l1u ++ l2u ++ lb)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else do u <- merge (head l1u) (head l2u)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return (u : lb)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance Mergeable OpAttr where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski do t <- merge t1 t2
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder return $ UnitOpAttr t (p1 ++ p2)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge _ _ = fail "merge: OpAttr"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maederinstance Mergeable OpBrand where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge Pred _ = return Pred
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge _ Pred = return Pred
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge Op _ = return Op
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge _ Op = return Op
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge _ _ = return Fun
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- instance Mergeable OpDefn where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeOpDefn :: TypeMap -> OpDefn -> OpDefn -> Result OpDefn
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeOpDefn _ VarDefn VarDefn = return VarDefn
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeOpDefn _ VarDefn _ = fail "illegal redeclaration of a variable"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeOpDefn _ _ VarDefn = fail "illegal redeclaration as variable"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermergeOpDefn _ (NoOpDefn _) d = return d
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeOpDefn _ d (NoOpDefn _) = return d
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeOpDefn tm d@(ConstructData d1) (ConstructData d2) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski if relatedTypeIds tm d1 d2 then return d else
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski fail ("wrong constructor target type" ++
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski expected d1 d2)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermergeOpDefn tm (SelectData c1 d1) (SelectData c2 d2) =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder if relatedTypeIds tm d1 d2 then
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder do c <- mergeConstrInfos tm c1 c2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ SelectData c d1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else fail ("wrong selector's source type" ++
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder expected d1 d2)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeOpDefn _ (Definition b1 d1) (Definition b2 d2) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do d <- merge d1 d2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder b <- merge b1 b2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ Definition b d
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeOpDefn _ _d1 _d2 = fail "illegal redefinition"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermergeConstrInfos :: TypeMap -> [ConstrInfo] -> [ConstrInfo]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> Result [ConstrInfo]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermergeConstrInfos _ [] c2 = return c2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeConstrInfos tm (c : r) c2 =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do c3 <- mergeConstrInfos tm r c2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if any ( \ d -> isUnifiable tm 0 (constrType c) (constrType d)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski && constrId c == constrId d) c2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder then return c3
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else return (c : c3)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermergeOpInfos :: TypeMap -> Int -> OpInfos -> OpInfos -> Result OpInfos
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermergeOpInfos tm c (OpInfos l1) (OpInfos l2) =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder do l <- mergeOps tm c l1 l2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return $ OpInfos l
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- trace (showPretty l1 "\n+ " ++ showPretty l2 "\n 0" ++ showPretty l "") l
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeOps :: TypeMap -> Int -> [OpInfo] -> [OpInfo] -> Result [OpInfo]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeOps _ _ [] l = return l
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimergeOps tm c (o:os) l2 = do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let (es, us) = partition (isUnifiable (addUnit tm) c
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (opType o) . opType) l2
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder l1 <- mergeOps tm c os us
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder if null es then return (o : l1)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else do r <- mergeOpInfo tm c o $ head es
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return (r : l1)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance Mergeable Env where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder merge e1 e2 =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do cMap <- merge (classMap e1) $ classMap e2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let m = max (counter e1) $ counter e2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder tMap <- mergeMap (mergeTypeInfo Map.empty 0)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (typeMap e1) $ typeMap e2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder as <- mergeMap (mergeOpInfos tMap m)
3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian Maeder (assumps e1) $ assumps e2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return initialEnv { classMap = cMap
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , typeMap = tMap
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder , assumps = as }
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederinstance Mergeable Term where
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder merge t1 t2 = if t1 == t2 then return t1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder else warning t1 ("different terms\n\t"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ++ showPretty t1 "\n\t"
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ++ showPretty t2 "\n\t") nullPos