@@ -179,7 +179,8 @@ let effect_checking_visitor
179
179
then Ast. EFF_pure
180
180
else Stack. top auth_stack
181
181
in
182
- Stack. push e auth_stack;
182
+ let next = lower_effect_of e curr in
183
+ Stack. push next auth_stack;
183
184
iflog cx
184
185
begin
185
186
fun _ ->
@@ -188,62 +189,40 @@ let effect_checking_visitor
188
189
" entering '%a', adjusting auth effect: '%a' -> '%a'"
189
190
Ast. sprintf_name name
190
191
Ast. sprintf_effect curr
191
- Ast. sprintf_effect e
192
+ Ast. sprintf_effect next
192
193
end
193
194
end;
194
- let report_mismatch declared_effect calculated_effect =
195
- let name = Hashtbl. find cx.ctxt_all_item_names i.id in
196
- err (Some i.id)
197
- " %a claims effect '%a' but calculated effect is '%a'%s"
198
- Ast. sprintf_name name
199
- Ast. sprintf_effect declared_effect
200
- Ast. sprintf_effect calculated_effect
201
- begin
202
- if Stack. is_empty auth_stack
203
- then " "
204
- else
205
- Printf. sprintf " (auth effects are '%s')"
206
- (stk_fold
207
- auth_stack
208
- (fun e s ->
209
- if s = " "
210
- then
211
- Printf. sprintf " %a"
212
- Ast. sprintf_effect e
213
- else
214
- Printf. sprintf " %s, %a" s
215
- Ast. sprintf_effect e) " " )
216
- end
217
- in
218
195
begin
219
196
match i.node.Ast. decl_item with
220
197
Ast. MOD_ITEM_fn f
221
198
when htab_search cx.ctxt_required_items i.id = None ->
222
- let calculated_effect =
199
+ let e =
223
200
match htab_search item_effect i.id with
224
201
None -> Ast. EFF_pure
225
202
| Some e -> e
226
203
in
227
- let declared_effect = f.Ast. fn_aux.Ast. fn_effect in
228
- if calculated_effect <> declared_effect
204
+ let fe = f.Ast. fn_aux.Ast. fn_effect in
205
+ let ae =
206
+ if Stack. is_empty auth_stack
207
+ then None
208
+ else Some (Stack. top auth_stack)
209
+ in
210
+ if e <> fe && (ae <> (Some e))
229
211
then
230
- (* Something's fishy in this case. If the calculated effect
231
- * is equal to one auth'ed by an enclosing scope -- not just
232
- * a lower one -- we accept this mismatch; otherwise we
233
- * complain.
234
- *
235
- * FIXME: this choice of "what constitutes an error" in
236
- * auth/effect mismatches is subjective and could do
237
- * with some discussion. *)
238
212
begin
239
- match
240
- stk_search auth_stack
241
- (fun e ->
242
- if e = calculated_effect then Some e else None )
243
- with
244
- Some _ -> ()
245
- | None ->
246
- report_mismatch declared_effect calculated_effect
213
+ let name = Hashtbl. find cx.ctxt_all_item_names i.id in
214
+ err (Some i.id)
215
+ " %a claims effect '%a' but calculated effect is '%a'%s"
216
+ Ast. sprintf_name name
217
+ Ast. sprintf_effect fe
218
+ Ast. sprintf_effect e
219
+ begin
220
+ match ae with
221
+ Some ae when ae <> fe ->
222
+ Printf. sprintf " (auth effect is '%a')"
223
+ Ast. sprintf_effect ae
224
+ | _ -> " "
225
+ end
247
226
end
248
227
| _ -> ()
249
228
end ;
@@ -260,16 +239,16 @@ let effect_checking_visitor
260
239
then Ast. EFF_pure
261
240
else Stack. top auth_stack
262
241
in
263
- iflog cx
264
- begin
265
- fun _ ->
266
- let name = Hashtbl. find cx.ctxt_all_item_names i.id in
267
- log cx
268
- " leaving '%a', restoring auth effect: '%a' -> '%a'"
269
- Ast. sprintf_name name
270
- Ast. sprintf_effect curr
271
- Ast. sprintf_effect next
272
- end
242
+ iflog cx
243
+ begin
244
+ fun _ ->
245
+ let name = Hashtbl. find cx.ctxt_all_item_names i.id in
246
+ log cx
247
+ " leaving '%a', restoring auth effect: '%a' -> '%a'"
248
+ Ast. sprintf_name name
249
+ Ast. sprintf_effect curr
250
+ Ast. sprintf_effect next
251
+ end
273
252
in
274
253
{ inner with
275
254
Walk. visit_mod_item_pre = visit_mod_item_pre;
0 commit comments