Cross Reference: /hets/HasCASL/Merge.hs
Merge.hs revision f3a94a197960e548ecd6520bb768cb0d547457bb
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule : $Header$
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : maeder@tzi.de
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederStability : experimental
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedermerging parts of local environment
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maedermodule HasCASL.Merge where
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.Id
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Common.PrettyPrint
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Result
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.As
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.Le
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.AsUtils
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport HasCASL.PrintLe()
04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport HasCASL.Unify
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport HasCASL.Builtin
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport HasCASL.MapTerm
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport qualified Common.Lib.Map as Map
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport Control.Monad(foldM)
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport Data.List
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder-- | merge together repeated or extended items
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederclass Mergeable a where
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder merge :: a -> a -> Result a
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederinstance (Ord a, PosItem a, PrettyPrint a, Mergeable b)
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder => Mergeable (Map.Map a b) where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge = mergeMap id merge
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian MaederimproveDiag :: (PosItem a, PrettyPrint a) => a -> Diagnosis -> Diagnosis
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian MaederimproveDiag v d = d { diagString = let f:l = lines $ diagString d in
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder unlines $ (f ++ " of '" ++ showPretty v "'") : l
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder , diagPos = get_pos v
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder }
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeMap :: (Ord a, PosItem a, PrettyPrint a) =>
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (b -> b) -> (b -> b -> Result b)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder -> Map.Map a b -> Map.Map a b -> Result (Map.Map a b)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeMap e f m1 m2 = foldM ( \ m (k, v) ->
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder case k `Map.lookup` m of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Nothing -> return $ Map.insert k (e v) m
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Just w ->
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder let Result ds mu = f (e v) w
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder ns = map (improveDiag k) ds
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder in case mu of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Nothing -> Result ns $ Nothing
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Just u -> Result ns $ Just $ Map.insert k u m)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Map.empty (Map.toList m1 ++ Map.toList m2)
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederinstance Mergeable a => Mergeable (Maybe a) where
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder merge m1 m2 = case m1 of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Nothing -> return m2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Just v1 -> case m2 of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Nothing -> return m1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Just v2 -> do v <- merge v1 v2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ Just v
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederinstance Mergeable ClassInfo where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge = mergeA "super classes"
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederinstance Mergeable Kind where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge = mergeA "super kinds"
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeTypeInfo :: TypeInfo -> TypeInfo -> Result TypeInfo
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeTypeInfo t1 t2 =
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder do k <- merge (typeKind t1) $ typeKind t2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder o <- merge (otherTypeKinds t1) $ otherTypeKinds t2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder s <- merge (superTypes t1) $ superTypes t2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder d <- mergeTypeDefn (typeDefn t1) $ typeDefn t2
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder return $ TypeInfo k o s d
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeTypeDefn :: TypeDefn -> TypeDefn -> Result TypeDefn
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeTypeDefn d1 d2 =
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder case (d1, d2) of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (TypeVarDefn 0, TypeVarDefn _) -> return d2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (TypeVarDefn _, TypeVarDefn 0) -> return d1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (TypeVarDefn c1, TypeVarDefn c2) -> do
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder c <- mergeA "TypeVarDefn" c1 c2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ TypeVarDefn c
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (TypeVarDefn _, _) -> fail "merge: TypeVarDefn"
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (_, TypeVarDefn _) -> fail "merge: TypeVarDefn"
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (_, DatatypeDefn _) -> return d2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (PreDatatype, _) -> fail "expected data type definition"
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (_, PreDatatype) -> return d1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (NoTypeDefn, _) -> return d2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (_, NoTypeDefn) -> return d1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (AliasTypeDefn s1, AliasTypeDefn s2) ->
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder do s <- mergeScheme s1 s2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ AliasTypeDefn s
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (Supertype v1 s1 t1, Supertype v2 s2 t2) ->
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder do s <- mergeScheme s1 s2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder v <- merge v1 v2
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder t <- mergeTerm Warning t1 t2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ Supertype v s t
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (_, _) -> mergeA "TypeDefn" d1 d2
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederinstance Mergeable Vars where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge = mergeA "variables for subtype definition"
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeScheme :: TypeScheme -> TypeScheme -> Result TypeScheme
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeScheme s1@(TypeScheme a1 t1 _)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder s2@(TypeScheme a2 t2 _) =
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder let v1 = genVarsOf t1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder v2 = genVarsOf t2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder mp v = mapArg $ zip v [(1::Int)..]
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder in
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder if t1 == t2 then
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder if null a1 && null a2 || isSingle a1 && isSingle a2 then
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return s1
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder else if map (mp v1) a1 == map (mp v2) a2 then return s1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder else fail ("differently bound type variables"
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder ++ expected s1 s2)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder else fail ("wrong type scheme" ++ expected s1 s2)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
04dada28736b4a237745e92063d8bdd49a362debChristian Maederinstance Mergeable OpAttr where
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder merge (UnitOpAttr t1 p1) (UnitOpAttr t2 p2) =
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder do t <- mergeTerm Warning t1 t2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ UnitOpAttr t (p1 ++ p2)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge a1 a2 = mergeA "attributes" a1 a2
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maederinstance Mergeable OpBrand where
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder merge Pred _ = return Pred
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder merge _ Pred = return Pred
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder merge Op _ = return Op
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder merge _ Op = return Op
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder merge _ _ = return Fun
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Mergeable OpDefn where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge VarDefn VarDefn = return VarDefn
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge VarDefn _ = fail "illegal redeclaration of a variable"
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge _ VarDefn = fail "illegal redeclaration as variable"
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge (NoOpDefn _) d = return d
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge d (NoOpDefn _) = return d
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder merge (ConstructData d1) (ConstructData _d2) = do
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder-- d <- mergeA "constructor target type" d1 d2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ ConstructData d1
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder merge (SelectData c1 d1) (SelectData c2 _d2) = do
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder-- d <- mergeA "selector source type" d1 d2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder c <- merge c1 c2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ SelectData c d1
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge (Definition b1 d1) (Definition b2 d2) =
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder do d <- mergeTerm Hint d1 d2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder b <- merge b1 b2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ Definition b d
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge _d1 _d2 = fail "illegal redefinition"
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Eq a => Mergeable [a] where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge [] l2 = return l2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder merge (e:l1) l2 = do
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder l3 <- merge l1 l2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder return $ if any (e==) l2 then l3
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder else e:l3
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedermergeOpInfos :: TypeMap -> OpInfos -> OpInfos -> Result OpInfos
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedermergeOpInfos tm (OpInfos l1) (OpInfos l2) =
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder do l <- mergeOps (addUnit tm) l1 l2
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder return $ OpInfos l
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedermergeOps :: TypeMap -> [OpInfo] -> [OpInfo] -> Result [OpInfo]
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedermergeOps _ [] l = return l
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedermergeOps tm (o:os) l2 = do
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder let (es, us) = partition (isUnifiable tm 1
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (opType o) . opType) l2
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder l1 <- mergeOps tm os us
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder if null es then return (o : l1)
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder else do r <- mergeOpInfo tm o $ head es
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return (r : l1)
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaedermergeOpInfo :: TypeMap -> OpInfo -> OpInfo -> Result OpInfo
962d5c684e2b86d1f9c556c096b426e10cc74026Christian MaedermergeOpInfo tm o1 o2 =
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder do let s1 = opType o1
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder s2 = opType o2
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder sc <- if instScheme tm 1 s2 s1 then return s1
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder else if instScheme tm 1 s1 s2 then return s2
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder else fail "overlapping but incompatible type schemes"
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder as <- merge (opAttrs o1) $ opAttrs o2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder d <- merge (opDefn o1) $ opDefn o2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return $ OpInfo sc as d
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederinstance Mergeable Env where
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder merge e1 e2 =
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder do cMap <- merge (classMap e1) $ classMap e2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder tMap <- mergeMap id mergeTypeInfo
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (typeMap e1) $ typeMap e2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder as <- mergeMap (OpInfos .
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder map (mapOpInfo (id, expandAlias tMap)) . opInfos)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (mergeOpInfos tMap)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (assumps e1) $ assumps e2
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder return initialEnv { classMap = cMap
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder , typeMap = tMap
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder , assumps = as }
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermergeA :: (PrettyPrint a, Eq a) => String -> a -> a -> Result a
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian 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
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder Result [Diag k ("different terms" ++ expected t1 t2)
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder []] $ Just t2