Merge.hs revision ad270004874ce1d0697fb30d7309f180553bb315
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederMaintainer : maeder@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : experimental
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maedermerging parts of local environment
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport qualified Data.Map as Map
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport qualified Data.Set as Set
df29370ae8d8b41587957f6bcdcb43a3f1927e47Christian Maeder-- | merge together repeated or extended items
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maederclass Mergeable a where
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich merge :: a -> a -> Result a
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichinstance (Ord a, PosItem a, Pretty a, Mergeable b)
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski => Mergeable (Map.Map a b) where
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder merge = mergeMap id merge
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederimproveDiag :: (PosItem a, Pretty a) => a -> Diagnosis -> Diagnosis
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederimproveDiag v d = d { diagString = let f:l = lines $ diagString d in
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder unlines $ (f ++ " of '" ++ showDoc v "'") : l
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , diagPos = getRange v
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermergeMap :: (Ord a, PosItem a, Pretty a) =>
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder (b -> b) -> (b -> b -> Result b)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder -> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)
8410667510a76409aca9bb24ff0eda0420088274Christian MaedermergeMap e f m1 m2 = foldM ( \ m (k, v) ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> return $ Map.insert k (e v) m
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich let Result ds mu = f (e v) w
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder ns = map (improveDiag k) ds
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich in case mu of
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich Nothing -> Result ns $ Nothing
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder Just u -> Result ns $ Just $ Map.insert k u m)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichinstance Mergeable a => Mergeable (Maybe a) where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder merge m1 m2 = case m1 of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Nothing -> return m2
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder Just v1 -> case m2 of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Nothing -> return m1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Just v2 -> do v <- merge v1 v2
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder return $ Just v
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maederinstance Mergeable ClassInfo where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder merge = mergeA "super classes"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederinstance (Pretty a, Eq a) => Mergeable (AnyKind a) where
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder merge = mergeA "super kinds"
cdd280437686b1e2e25e3761d4adf3d4a0a2d11cKlaus LuettichmergeTypeInfo :: TypeInfo -> TypeInfo -> Result TypeInfo
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian MaedermergeTypeInfo t1 t2 =
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder do k <- merge (typeKind t1) $ typeKind t2
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder o <- merge (otherTypeKinds t1) $ otherTypeKinds t2
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maeder s <- merge (superTypes t1) $ superTypes t2
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich return $ TypeInfo k o s d
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus LuettichmergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
363939beade943a02b31004cea09dec34fa8a6d9Christian MaedermergeTypeDefn d1 d2 =
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder case (d1, d2) of
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder (_, DatatypeDefn _) -> return d2
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder (PreDatatype, _) -> fail "expected data type definition"
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder (_, PreDatatype) -> return d1
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder (NoTypeDefn, _) -> return d2
8a28707e9155465c6f2236a06eac6580a65c7025Christian Maeder (_, NoTypeDefn) -> return d1
03ef54c97b3dbc6f829c12e084fbad2e96fcc9a8Christian Maeder (AliasTypeDefn s1, AliasTypeDefn s2) ->
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder do s <- mergeScheme s1 s2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return $ AliasTypeDefn s
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder (_, _) -> mergeA "TypeDefn" d1 d2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Mergeable Vars where
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder merge = mergeA "variables for subtype definition"
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedermergeScheme :: TypeScheme -> TypeScheme -> Result TypeScheme
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermergeScheme s1@(TypeScheme a1 t1 _)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder s2@(TypeScheme a2 t2 _) =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let v1 = genVarsOf t1
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder v2 = genVarsOf t2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder mp a v = foldr ( \ i l ->
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder maybe l (:l) $ findIndex ((== i) . getTypeVar) a)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder [] (map fst v)
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder if t1 == t2 then
776a1a086df734581431e6edb4343ed4c8d34d55Christian Maeder if null a1 && null a2 || isSingle a1 && isSingle a2 then
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else if mp a1 v1 == mp a2 v2 then return s1
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder else fail ("differently bound type variables"
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder ++ expected s1 s2)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder else fail ("wrong type scheme" ++ expected s1 s2)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Mergeable OpAttr where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do t <- mergeTerm Warning t1 t2
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder return $ UnitOpAttr t (p1 `appRange` p2)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder merge a1 a2 = mergeA "attributes" a1 a2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederinstance Mergeable OpBrand where
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder merge b1 b2 = return $ case (b1, b2) of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Pred, _) -> Pred
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (_, Pred) -> Pred
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Op, _) -> Op
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (_, Op) -> Op
4017ebc0f692820736d796af3110c3b3018c108aChristian Maederinstance Mergeable OpDefn where
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder merge d1 d2 = case (d1, d2) of
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder (NoOpDefn b1, NoOpDefn b2) -> do
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder b <- merge b1 b2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder return $ NoOpDefn b
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (SelectData c1 s, SelectData c2 _) -> do
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder c <- merge c1 c2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder return $ SelectData c s
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (Definition b1 e1, Definition b2 e2) -> do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder d <- mergeTerm Hint e1 e2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder b <- merge b1 b2
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder return $ Definition b d
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder (NoOpDefn b1, Definition b2 e2) -> do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder b <- merge b1 b2
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder return $ Definition b e2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (Definition b1 e1, NoOpDefn b2) -> do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder b <- merge b1 b2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return $ Definition b e1
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder (ConstructData _, SelectData _ _) ->
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder fail "illegal selector as constructor redefinition"
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder (SelectData _ _, ConstructData _) ->
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder fail "illegal constructor as selector redefinition"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (ConstructData _, _) -> return d1
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (_, ConstructData _) -> return d2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (SelectData _ _, _) -> return d1
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (_, SelectData _ _) -> return d2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maederinstance Eq a => Mergeable [a] where
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich merge l1 l2 = case l1 of
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder [] -> return l2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder l3 <- merge l l2
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder return $ if any (e==) l2 then l3 else e : l3
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maederinstance Ord a => Mergeable (Set.Set a) where
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder merge s1 s2 = return $ Set.union s1 s2
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedermergeOpInfos :: TypeMap -> OpInfos -> OpInfos -> Result OpInfos
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedermergeOpInfos tm (OpInfos l1) (OpInfos l2) =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder do l <- mergeOps (addUnit tm) l1 l2
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return $ OpInfos l
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermergeOps :: TypeMap -> [OpInfo] -> [OpInfo] -> Result [OpInfo]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedermergeOps _ [] l = return l
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedermergeOps tm (o:os) l2 = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let (es, us) = partition (isUnifiable tm 1
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (opType o) . opType) l2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder l1 <- mergeOps tm os us
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder if null es then return (o : l1)
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder else do r <- mergeOpInfo tm o $ head es
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder return (r : l1)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedermergeOpInfo :: TypeMap -> OpInfo -> OpInfo -> Result OpInfo
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedermergeOpInfo tm o1 o2 =
89f7631cbfbd1bb99fc152b434bd362a7799d295Christian Maeder do let s1 = opType o1
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder s2 = opType o2
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder sc <- if instScheme tm 1 s2 s1 then return s1
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder else if instScheme tm 1 s1 s2 then return s2
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder else fail "overlapping but incompatible type schemes"
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder as <- merge (opAttrs o1) $ opAttrs o2
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich d <- merge (opDefn o1) $ opDefn o2
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return $ OpInfo sc as d
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettichinstance Mergeable Env where
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder merge e1 e2 =
6b6773cf587b74259178641d811746a235faf056Christian Maeder do cMap <- merge (classMap e1) $ classMap e2
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder tMap <- mergeMap id mergeTypeInfo
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder (typeMap e1) $ typeMap e2
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich as <- mergeMap (OpInfos .
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder map (mapOpInfo (id, expandAlias tMap)) . opInfos)
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (mergeOpInfos tMap)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder (assumps e1) $ assumps e2
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder return initialEnv { classMap = cMap
d272062059eea4d7479e1c6e8517469f02f61287Christian Maeder , typeMap = tMap
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder , assumps = as }
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian MaedermergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian MaedermergeA str t1 t2 = if t1 == t2 then return t1 else
7c5c311d67e187280877c45bd89dcba9038bc0a3Christian Maeder fail ("different " ++ str ++ expected t1 t2)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermergeTerm :: DiagKind -> Term -> Term -> Result Term
83394c6b6e6de128e71b67c9251ed7a84485d082Christian MaedermergeTerm k t1 t2 = if t1 == t2 then return t1 else
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Result [Diag k ("different terms" ++ expected t1 t2)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder nullRange] $ Just t2