Merge.hs revision ad187062b0009820118c1b773a232e29b879a2fa
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- |
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederModule : $Header$
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederDescription : union of signature parts
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederMaintainer : Christian.Maeder@dfki.de
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederStability : experimental
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskimerging parts of local environment
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-}
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedermodule HasCASL.Merge where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.Id
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.DocUtils
85ebda7270c6883b503d3bde4757033c09c25644Christian Maederimport Common.Result
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport HasCASL.As
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport HasCASL.Le
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport HasCASL.AsUtils
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzimport HasCASL.TypeAna
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport HasCASL.PrintLe()
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzimport HasCASL.Unify
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.Builtin
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.MapTerm
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Data.Map as Map
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Data.Set as Set
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maederimport Control.Monad(foldM)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederimport Data.List
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder-- | merge together repeated or extended items
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maederclass Mergeable a where
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder merge :: a -> a -> Result a
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederinstance (Ord a, PosItem a, Pretty a, Mergeable b)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder => Mergeable (Map.Map a b) where
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder merge = mergeMap id merge
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederimproveDiag :: (PosItem a, Pretty a) => a -> Diagnosis -> Diagnosis
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederimproveDiag v d = d { diagString = let f:l = lines $ diagString d in
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder unlines $ (f ++ " of '" ++ showDoc v "'") : l
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder , diagPos = getRange v
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder }
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskimergeMap :: (Ord a, PosItem a, Pretty a) =>
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski (b -> b) -> (b -> b -> Result b)
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski -> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)
6abfd7000f15635fd29746bd841b4c36819e552bTill MossakowskimergeMap e f m1 m2 = foldM ( \ m (k, v) ->
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski case k `Map.lookup` m of
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski Nothing -> return $ Map.insert k (e v) m
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski Just w ->
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski let Result ds mu = f (e v) w
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski ns = map (improveDiag k) ds
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder in case mu of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Nothing -> Result ns $ Nothing
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Just u -> Result ns $ Just $ Map.insert k u m)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Map.empty (Map.toList m1 ++ Map.toList m2)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskiinstance Mergeable a => Mergeable (Maybe a) where
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder merge m1 m2 = case m1 of
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder Nothing -> return m2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Just v1 -> case m2 of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Nothing -> return m1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Just v2 -> do v <- merge v1 v2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder return $ Just v
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance Mergeable ClassInfo where
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder merge = mergeA "super classes"
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance (Pretty a, Ord a) => Mergeable (AnyKind a) where
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder merge = mergeA "super kinds"
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedermergeTypeInfo :: TypeInfo -> TypeInfo -> Result TypeInfo
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaedermergeTypeInfo t1 t2 =
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder do k <- merge (typeKind t1) $ typeKind t2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder o <- merge (otherTypeKinds t1) $ otherTypeKinds t2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder s <- merge (superTypes t1) $ superTypes t2
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder return $ TypeInfo k o s d
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedermergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedermergeTypeDefn d1 d2 =
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder case (d1, d2) of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (_, DatatypeDefn _) -> return d2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (PreDatatype, _) -> fail "expected data type definition"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (_, PreDatatype) -> return d1
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski (NoTypeDefn, _) -> return d2
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski (_, NoTypeDefn) -> return d1
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski (AliasTypeDefn s1, AliasTypeDefn s2) ->
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski do s <- mergeAlias s1 s2
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski return $ AliasTypeDefn s
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski (_, _) -> mergeA "TypeDefn" d1 d2
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskiinstance Mergeable Vars where
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich merge = mergeA "variables for subtype definition"
da955132262baab309a50fdffe228c9efe68251dCui Jian
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedermergeAlias :: Type -> Type -> Result Type
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedermergeAlias s1 s2 = if s1 == s2 then return s1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder else fail $ "wrong type" ++ expected s1 s2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Mergeable OpAttr where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder do t <- mergeTerm Warning t1 t2
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder return $ UnitOpAttr t (p1 `appRange` p2)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder merge a1 a2 = mergeA "attributes" a1 a2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Mergeable OpBrand where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder merge b1 b2 = return $ case (b1, b2) of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Pred, _) -> Pred
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (_, Pred) -> Pred
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (Op, _) -> Op
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz (_, Op) -> Op
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz _ -> Fun
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulzinstance Mergeable OpDefn where
831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz merge d1 d2 = case (d1, d2) of
831b0d8f47480be51d14f2cf122913507859f9c3Ewaryst Schulz (NoOpDefn b1, NoOpDefn b2) -> do
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz b <- merge b1 b2
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz return $ NoOpDefn b
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz (SelectData c1 s, SelectData c2 _) -> do
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz c <- merge c1 c2
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz return $ SelectData c s
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz (Definition b1 e1, Definition b2 e2) -> do
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz d <- mergeTerm Hint e1 e2
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz b <- merge b1 b2
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz return $ Definition b d
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz (NoOpDefn b1, Definition b2 e2) -> do
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz b <- merge b1 b2
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz return $ Definition b e2
295566c1778f463b624caf1be714b70d808e2a51Ewaryst Schulz (Definition b1 e1, NoOpDefn b2) -> do
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz b <- merge b1 b2
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder return $ Definition b e1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (ConstructData _, SelectData _ _) ->
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder fail "illegal selector as constructor redefinition"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (SelectData _ _, ConstructData _) ->
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder fail "illegal constructor as selector redefinition"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (ConstructData _, _) -> return d1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (_, ConstructData _) -> return d2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (SelectData _ _, _) -> return d1
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder (_, SelectData _ _) -> return d2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederinstance Eq a => Mergeable [a] where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder merge l1 l2 = case l1 of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder [] -> return l2
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder e : l -> do
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder l3 <- merge l l2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder return $ if any (e==) l2 then l3 else e : l3
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
07baaf27fc0029203075ed916999006dcc619ef0Christian Maederinstance Ord a => Mergeable (Set.Set a) where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder merge s1 s2 = return $ Set.union s1 s2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedermergeOpInfos :: TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -> Result (Set.Set OpInfo)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedermergeOpInfos tm s1 s2 = mergeOps (addUnit tm) s1 s2
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder
07baaf27fc0029203075ed916999006dcc619ef0Christian MaedermergeOps :: TypeMap -> Set.Set OpInfo -> Set.Set OpInfo
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -> Result (Set.Set OpInfo)
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedermergeOps tm s1 s2 = if Set.null s1 then return s2 else do
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder let (o, os) = Set.deleteFindMin s1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder (es, us) = Set.partition (isUnifiable tm 1 (opType o) . opType) s2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder s <- mergeOps tm os us
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder r <- foldM (mergeOpInfo tm) o $ Set.toList es
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder return $ Set.insert r s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedermergeOpInfo :: TypeMap -> OpInfo -> OpInfo -> Result OpInfo
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaedermergeOpInfo tm o1 o2 =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder do let s1 = opType o1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder s2 = opType o2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder sc <- if instScheme tm 1 s2 s1 then return s1
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder else if instScheme tm 1 s1 s2 then return s2
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder else fail "overlapping but incompatible type schemes"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder as <- merge (opAttrs o1) $ opAttrs o2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder d <- merge (opDefn o1) $ opDefn o2
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski return $ OpInfo sc as d
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder
999f839e42d594e4ae288208fec398626837c41cTill Mossakowskiinstance Mergeable Env where
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski merge e1 e2 =
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski do cMap <- merge (classMap e1) $ classMap e2
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski tMap <- mergeMap id mergeTypeInfo
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder (typeMap e1) $ typeMap e2
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder case filterAliases tMap of
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski tAs -> do
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski as <- mergeMap (Set.map $ mapOpInfo (id, expandAliases tAs))
(mergeOpInfos tMap)
(assumps e1) $ assumps e2
return initialEnv { classMap = cMap
, typeMap = tMap
, assumps = as }
mergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
mergeA str t1 t2 = if t1 == t2 then return t1 else
fail ("different " ++ str ++ expected t1 t2)
mergeTerm :: DiagKind -> Term -> Term -> Result Term
mergeTerm k t1 t2 = if t1 == t2 then return t1 else
Result [Diag k ("different terms" ++ expected t1 t2)
nullRange] $ Just t2