c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./HasCASL/Merge.hs
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : union of signature parts
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederStability : experimental
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedermerging parts of local environment
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maedermodule HasCASL.Merge
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder ( merge
1ae7298170b7a26dce9acc6d2c864fb01f0cb347Christian Maeder , mergeTypeInfo
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder , mergeTypeDefn
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder , mergeOpInfo
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder , addUnit
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder ) where
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.Id
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Common.DocUtils
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Result
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.As
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.Le
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.AsUtils
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport HasCASL.PrintLe
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maederimport HasCASL.ClassAna
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport HasCASL.TypeAna
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport HasCASL.Builtin
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport HasCASL.MapTerm
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederimport Data.Maybe
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maederimport Control.Monad (foldM)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedermergeTypeInfo :: ClassMap -> TypeInfo -> TypeInfo -> Result TypeInfo
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian MaedermergeTypeInfo cm t1 t2 = do
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder let o = keepMinKinds cm [otherTypeKinds t1, otherTypeKinds t2]
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder s = Set.union (superTypes t1) $ superTypes t2
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder k <- minRawKind "type raw kind" (typeKind t1) $ typeKind t2
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder return $ TypeInfo k o s d
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian MaedermergeTypeDefn d1 d2 = case (d1, d2) of
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (_, DatatypeDefn _) -> return d2
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (PreDatatype, _) -> fail "expected data type definition"
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (_, PreDatatype) -> return d1
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (NoTypeDefn, _) -> return d2
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (_, NoTypeDefn) -> return d1
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (AliasTypeDefn s1, AliasTypeDefn s2) -> do
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder s <- mergeAlias s1 s2
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder return $ AliasTypeDefn s
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (_, _) -> mergeA "TypeDefn" d1 d2
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaedermergeAlias :: Type -> Type -> Result Type
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian MaedermergeAlias s1 s2 = if eqStrippedType s1 s2 then return s1 else
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder fail $ "wrong type" ++ expected s1 s2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedermergeOpBrand :: OpBrand -> OpBrand -> OpBrand
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedermergeOpBrand b1 b2 = case (b1, b2) of
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (Pred, _) -> Pred
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (_, Pred) -> Pred
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (Op, _) -> Op
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (_, Op) -> Op
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder _ -> Fun
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedermergeOpDefn :: OpDefn -> OpDefn -> Result OpDefn
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedermergeOpDefn d1 d2 = case (d1, d2) of
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (NoOpDefn b1, NoOpDefn b2) -> do
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder let b = mergeOpBrand b1 b2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ NoOpDefn b
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (SelectData c1 s, SelectData c2 _) -> do
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder let c = Set.union c1 c2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ SelectData c s
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (Definition b1 e1, Definition b2 e2) -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder d <- mergeTerm Hint e1 e2
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder let b = mergeOpBrand b1 b2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ Definition b d
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (NoOpDefn b1, Definition b2 e2) -> do
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder let b = mergeOpBrand b1 b2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ Definition b e2
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (Definition b1 e1, NoOpDefn b2) -> do
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder let b = mergeOpBrand b1 b2
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ Definition b e1
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (ConstructData _, SelectData _ _) ->
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder fail "illegal selector as constructor redefinition"
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (SelectData _ _, ConstructData _) ->
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder fail "illegal constructor as selector redefinition"
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (ConstructData _, _) -> return d1
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (_, ConstructData _) -> return d2
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (SelectData _ _, _) -> return d1
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder (_, SelectData _ _) -> return d2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaederaddUnit :: ClassMap -> TypeMap -> TypeMap
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaederaddUnit cm = fromMaybe (error "addUnit") . maybeResult . mergeTypeMap cm bTypes
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
cdb141ee48c3a96e620186de94316c562037a2e0Christian MaedermergeOpInfos :: Set.Set OpInfo -> Set.Set OpInfo -> Result (Set.Set OpInfo)
cdb141ee48c3a96e620186de94316c562037a2e0Christian MaedermergeOpInfos s1 s2 = if Set.null s1 then return s2 else do
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder let (o, os) = Set.deleteFindMin s1
cdb141ee48c3a96e620186de94316c562037a2e0Christian Maeder (es, us) = Set.partition ((opType o ==) . opType) s2
cdb141ee48c3a96e620186de94316c562037a2e0Christian Maeder s <- mergeOpInfos os us
cdb141ee48c3a96e620186de94316c562037a2e0Christian Maeder r <- foldM mergeOpInfo o $ Set.toList es
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder return $ Set.insert r s
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder
cdb141ee48c3a96e620186de94316c562037a2e0Christian MaedermergeOpInfo :: OpInfo -> OpInfo -> Result OpInfo
cdb141ee48c3a96e620186de94316c562037a2e0Christian MaedermergeOpInfo o1 o2 = do
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder let as = Set.union (opAttrs o1) $ opAttrs o2
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder d <- mergeOpDefn (opDefn o1) $ opDefn o2
cdb141ee48c3a96e620186de94316c562037a2e0Christian Maeder return $ OpInfo (opType o1) as d
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedermergeTypeMap :: ClassMap -> TypeMap -> TypeMap -> Result TypeMap
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermergeTypeMap = mergeMap . mergeTypeInfo
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maedermerge :: Env -> Env -> Result Env
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maedermerge e1 e2 = do
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder clMap <- mergeClassMap (classMap e1) $ classMap e2
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder tMap <- mergeTypeMap clMap (typeMap e1) $ typeMap e2
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder let tAs = filterAliases tMap
cdb141ee48c3a96e620186de94316c562037a2e0Christian Maeder as <- mergeMap mergeOpInfos (assumps e1) $ assumps e2
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder bs <- mergeMap (\ i1 i2 -> if i1 == i2 then return i1 else
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder fail "conflicting operation for binder syntax")
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (binders e1) $ binders e2
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder return initialEnv
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder { classMap = clMap
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder , typeMap = tMap
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder , assumps = Map.map (Set.map $ mapOpInfo (id, expandAliases tAs)) as
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder , binders = bs }
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermergeA :: (Pretty a, Eq a) => String -> a -> a -> Result a
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermergeA str t1 t2 = if t1 == t2 then return t1 else
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fail ("different " ++ str ++ expected t1 t2)
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder
15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaedermergeTerm :: DiagKind -> Term -> Term -> Result Term
15bb922b665fcd44c6230a1202785d0c7890e90cChristian MaedermergeTerm k t1 t2 = if t1 == t2 then return t1 else
32a7cc7177ecf70e35ec831ff86887b9acc40dcaChristian Maeder Result [Diag k ("different terms" ++ expected t1 t2) $ getRange t2] $ Just t2