From be4bfc78c493464cb0af40d7fae08ba86295a6f9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Jan 2016 20:49:34 +0100 Subject: Fixing #4256 and #4484 (changes in evar-evar resolution made that new evars were created making in turn that evars formerly recognized as pending were not anymore in the list of pending evars). This also fixes the reopening of #3848. See comments on #4484 for details. --- pretyping/pretyping.ml | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index faba5c756..521fa2247 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -183,22 +183,26 @@ type inference_flags = { expand_evars : bool } +let frozen_holes (sigma, sigma') = + let fold evk _ accu = Evar.Set.add evk accu in + Evd.fold_undefined fold sigma Evar.Set.empty + let pending_holes (sigma, sigma') = let fold evk _ accu = if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu in Evd.fold_undefined fold sigma' Evar.Set.empty -let apply_typeclasses env evdref pending fail_evar = - let filter_pending evk = Evar.Set.mem evk pending in +let apply_typeclasses env evdref frozen fail_evar = + let filter_frozen evk = Evar.Set.mem evk frozen in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () - then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && filter_pending evk) - else (fun evk evi -> Typeclasses.no_goals evk evi && filter_pending evk)) + then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) + else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk))) ~split:true ~fail:fail_evar env !evdref; if Flags.is_program_mode () then (* Try optionally solving the obligations *) evdref := Typeclasses.resolve_typeclasses - ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && filter_pending evk) ~split:true ~fail:false env !evdref + ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env !evdref let apply_inference_hook hook evdref pending = evdref := Evar.Set.fold (fun evk sigma -> @@ -219,9 +223,9 @@ let apply_heuristics env evdref fail_evar = with e when Errors.noncritical e -> let e = Errors.push e in if fail_evar then iraise e -let check_typeclasses_instances_are_solved env current_sigma pending = +let check_typeclasses_instances_are_solved env current_sigma frozen = (* Naive way, call resolution again with failure flag *) - apply_typeclasses env (ref current_sigma) pending true + apply_typeclasses env (ref current_sigma) frozen true let check_extra_evars_are_solved env current_sigma pending = Evar.Set.iter @@ -233,26 +237,28 @@ let check_extra_evars_are_solved env current_sigma pending = | _ -> error_unsolvable_implicit loc env current_sigma evk None) pending -let check_evars_are_solved env current_sigma pending = - check_typeclasses_instances_are_solved env current_sigma pending; +let check_evars_are_solved env current_sigma frozen pending = + check_typeclasses_instances_are_solved env current_sigma frozen; check_problems_are_solved env current_sigma; check_extra_evars_are_solved env current_sigma pending (* Try typeclasses, hooks, unification heuristics ... *) let solve_remaining_evars flags env current_sigma pending = + let frozen = frozen_holes pending in let pending = pending_holes pending in let evdref = ref current_sigma in - if flags.use_typeclasses then apply_typeclasses env evdref pending false; + if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then apply_inference_hook (Option.get flags.use_hook env) evdref pending; if flags.use_unif_heuristics then apply_heuristics env evdref false; - if flags.fail_evar then check_evars_are_solved env !evdref pending; + if flags.fail_evar then check_evars_are_solved env !evdref frozen pending; !evdref let check_evars_are_solved env current_sigma pending = + let frozen = frozen_holes pending in let pending = pending_holes pending in - check_evars_are_solved env current_sigma pending + check_evars_are_solved env current_sigma frozen pending let process_inference_flags flags env initial_sigma (sigma,c) = let sigma = solve_remaining_evars flags env sigma (initial_sigma, sigma) in -- cgit v1.2.3