hets/HasCASL/Merge.hs

	Merge.hs revision f42bcc750a9a02cb4f753b70679f9aacf1b338d7


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule      :  $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription :  union of signature parts
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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
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
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport Control.Monad(foldM)
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport Data.List
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
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaederaddUnit cm = maybe (error "addUnit") id . 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
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaedermergeTypeMap cm = mergeMap $ mergeTypeInfo cm
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maedermerge :: Env -> Env -> Result Env
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maedermerge e1 e2 = do
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder    cMap <- mergeMap mergeClassInfo (classMap e1) $ classMap e2
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder    let clMap = Map.map (\ ci -> ci { classKinds =
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder                          keepMinKinds cMap [classKinds ci] }) cMap
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
31a189d4cff554f78407cdc422480e84e99a6ec6Christian 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