Merge.hs revision 836e72a3c413366ba9801726f3b249c7791cb9ca
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{- |
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian MaederModule : $Header$
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiMaintainer : hets@tzi.de
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuStability : experimental
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder merging parts of local environment
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder-}
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskimodule HasCASL.Merge where
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.Id
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.PrettyPrint
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport HasCASL.As
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederimport HasCASL.Le
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport HasCASL.AsUtils
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport HasCASL.Unify
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Common.Lib.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Data.List
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport Control.Monad
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport Common.Result
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- for Logic.signature_union
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maederinstance Mergeable Env where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang merge e1 e2 =
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder do cMap <- merge (classMap e1) $ classMap e2
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder tMap <- merge (typeMap e1) $ typeMap e2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let m = max (counter e1) $ counter e2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder as <- mergeAssumps tMap m
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (assumps e1) $ assumps e2
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder return $ Env cMap tMap as (sentences e1 ++ sentences e2)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (envDiags e1 ++ envDiags e2) m
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maederinstance (Ord a, PosItem a, PrettyPrint a, Mergeable b)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder => Mergeable (Map.Map a b) where
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich merge = mergeMap merge
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichimproveDiag :: (PosItem a, PrettyPrint a) => a -> Diagnosis -> Diagnosis
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederimproveDiag v d = d { diagString = let f:l = lines $ diagString d in
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder unlines $ (f ++ " of '" ++ showPretty v "'") : l
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski , diagPos = getMyPos v
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , diagKind = case diagKind d of
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu FatalError -> Error
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder w -> w
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
8e80792f474d154ff11762fac081a422e34f1accChristian MaedermergeMap :: (Ord a, PosItem a, PrettyPrint a) => (b -> b -> Result b)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeMap f m1 m2 = foldM ( \ m (k, v) ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case k `Map.lookup` m of
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Nothing -> return $ Map.insert k v m
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just w ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let Result ds mu = f v w
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder ns = map (improveDiag k) ds
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder in case mu of
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Nothing -> Result ns $ Nothing
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Just u -> Result ns $ Just $ Map.insert k u m)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder m1 (Map.toList m2)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederinstance Mergeable a => Mergeable (Maybe a) where
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder merge m1 m2 = case m1 of
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Nothing -> return m2
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Just v1 -> case m2 of
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Nothing -> return m1
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Just v2 -> do v <- merge v1 v2
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder return $ Just v
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder
e6dccba746efe07338d3107fed512e713fd50b28Christian Maederinstance Mergeable ClassInfo where
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder merge c1 c2 = if c1 == c2 then
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder return c1
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder else fail "merge: non-equal super classes"
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Mergeable Kind where
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder merge k1 k2 = if k1 == k2 then return k1
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder else fail "merge: non-equal kinds"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian MaedermergeList :: Eq a => [a] -> [a] -> Result [a]
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian MaedermergeList l1 l2 = return $ nub (l1 ++ l2)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Mergeable TypeInfo where
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder merge t1 t2 = do k <- merge (typeKind t1) $ typeKind t2
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder o <- mergeList (otherTypeKinds t1) $ otherTypeKinds t2
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder s <- mergeList (superTypes t1) $ superTypes t2
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder d <- merge (typeDefn t1) $ typeDefn t2
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder return $ TypeInfo k o s d
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Mergeable TypeDefn where
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder merge d1 d2 =
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder case (d1, d2) of
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder (TypeVarDefn, TypeVarDefn) -> return d1
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder (TypeVarDefn, _) -> fail "merge: TypeVarDefn"
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (_, TypeVarDefn) -> fail "merge: TypeVarDefn"
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder (PreDatatype, DatatypeDefn _ _ _) -> return d2
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder (PreDatatype, _) -> fail "expected data type definition"
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder (_, PreDatatype) -> return d1
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder-- (NoTypeDefn, AliasTypeDefn _) -> fail "merge: AliasTypeDefn"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-- (AliasTypeDefn _, NoTypeDefn) -> fail "merge: AliasTypeDefn"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (NoTypeDefn, _) -> return d2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (_, NoTypeDefn) -> return d1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (_, _) -> if d1 == d2 then return d1 else
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder fail "merge: TypeDefn"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeAssumps :: TypeMap -> Int -> Assumps -> Assumps -> Result Assumps
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermergeAssumps tm c = mergeMap (mergeOpInfos tm c)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedermergeOpInfos :: TypeMap -> Int -> OpInfos -> OpInfos -> Result OpInfos
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedermergeOpInfos tm c (OpInfos l1) (OpInfos l2) = fmap OpInfos $
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski foldM ( \ l o ->
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let (es, us) = partition (isUnifiable tm c (opType o) . opType) l
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in if null es then return (o:l)
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder else do r <- merge (head es) o
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return (r : us)) l1 l2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maederinstance Mergeable OpInfo where
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder merge o1 o2 =
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder do sc <- merge (opType o1) $ opType o2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder as <- mergeAttrs (opAttrs o1) $ opAttrs o2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder d <- merge (opDefn o1) $ opDefn o2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return $ OpInfo sc as d
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Mergeable TypeScheme where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski merge s1 s2 = if s1 == s2 then return s1
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder else fail ("wrong type scheme"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ++ expected s1 s2)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- instance Mergeable [OpAttr] where
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermergeAttrs :: [OpAttr] -> [OpAttr] -> Result [OpAttr]
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedermergeAttrs l1 l2 =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let binAttr a = case a of BinOpAttr _ _ -> True
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder _ -> False
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (l1b, l1u) = partition binAttr l1
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder (l2b, l2u) = partition binAttr l2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder lb = nubBy ( \ (BinOpAttr b1 _) (BinOpAttr b2 _) -> b1 == b2)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (l1b ++ l2b)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in if null l1u || null l2u then
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder return (l1u ++ l2u ++ lb)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else do u <- merge (head l1u) (head l2u)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return (u : lb)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederinstance Mergeable OpAttr where
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder if t1 == t2 then return $ UnitOpAttr t1 (p1 ++ p2)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder else fail "unequal unit elements"
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder merge _ _ = fail "merge: OpAttr"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederinstance Mergeable OpDefn where
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder merge VarDefn VarDefn = return VarDefn
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder merge VarDefn _ = fail "illegal redeclaration of a variable"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder merge _ VarDefn = fail "illegal redeclaration as variable"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder merge NoOpDefn d = return d
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder merge d NoOpDefn = return d
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder merge d@(ConstructData d1) (ConstructData d2) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder if d1 == d2 then return d else
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder fail ("wrong constructor target type" ++
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder expected d1 d2)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski merge (SelectData c1 d1) (SelectData c2 d2) =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz if d1 == d2 then
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz do c <- mergeConstrInfos c1 c2
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return $ SelectData c d1
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz else fail ("wrong selector's source type" ++
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz expected d1 d2)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz merge (Definition d1) (Definition d2) =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz do d <- merge d1 d2
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return $ Definition d
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz merge _d1 _d2 = fail "illegal redefinition"
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian MaedermergeConstrInfos :: [ConstrInfo] -> [ConstrInfo] -> Result [ConstrInfo]
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzmergeConstrInfos [] c2 = return c2
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzmergeConstrInfos (c : r) c2 =
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz do c3 <- mergeConstrInfos r c2
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz let cs = filter (==c) c2
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz if null cs then
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz return (c : c3)
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz else return c3
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maederinstance Mergeable Term where
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder merge t1 t2 = if t1 == t2 then return t1
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder else fail ("different terms\n\t"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ++ showPretty t1 "\n\t"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ++ showPretty t2 "\n\t")
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder