diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 62 |
1 files changed, 35 insertions, 27 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5383101b4..6dbf7915b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -142,19 +142,27 @@ type inference_flags = { expand_evars : bool } -let apply_typeclasses env evdref fail_evar = +let fold_pending_holes f (sigma,sigma') = + Evd.fold_undefined + (fun evk _ acc -> if Evd.mem sigma evk then acc else f evk acc) + sigma' + +let is_pending_hole (sigma,sigma') evk = + Evd.is_undefined sigma' evk && not (Evd.mem sigma evk) + +let apply_typeclasses env evdref pending fail_evar = evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () - then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals) + then (fun evk evi -> is_pending_hole pending evk && Typeclasses.no_goals_or_obligations evk evi) + else (fun evk evi -> is_pending_hole pending evk && Typeclasses.no_goals evk evi)) ~split:true ~fail:fail_evar env !evdref; if Flags.is_program_mode () then (* Try optionally solving the obligations *) evdref := Typeclasses.resolve_typeclasses - ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref + ~filter:(fun evk evi -> is_pending_hole pending evk && Typeclasses.all_evars evk evi) ~split:true ~fail:false env !evdref -let apply_inference_hook hook initial_sigma evdref = - evdref := fold_undefined (fun evk evi sigma -> - if not (Evd.mem initial_sigma evk) && - is_undefined sigma evk (* i.e. not defined by side-effect *) +let apply_inference_hook hook evdref pending = + evdref := fold_pending_holes (fun evk sigma -> + if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then try let c = hook sigma evk in @@ -162,7 +170,7 @@ let apply_inference_hook hook initial_sigma evdref = with Exit -> sigma else - sigma) !evdref !evdref + sigma) pending !evdref let apply_heuristics env evdref fail_evar = (* Resolve eagerly, potentially making wrong choices *) @@ -171,39 +179,39 @@ let apply_heuristics env evdref fail_evar = with e when Errors.noncritical e -> let e = Errors.push e in if fail_evar then raise e -let check_typeclasses_instances_are_solved env sigma = +let check_typeclasses_instances_are_solved env current_sigma pending = (* Naive way, call resolution again with failure flag *) - apply_typeclasses env (ref sigma) true + apply_typeclasses env (ref current_sigma) pending true -let check_extra_evars_are_solved env initial_sigma sigma = - Evd.fold_undefined - (fun evk evi () -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in +let check_extra_evars_are_solved env current_sigma pending = + fold_pending_holes + (fun evk () -> + if not (Evd.is_defined current_sigma evk) then + let (loc,k) = evar_source evk current_sigma in match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () | _ -> - let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in - error_unsolvable_implicit loc env sigma evi k None) sigma () + let evi = nf_evar_info current_sigma (Evd.find_undefined current_sigma evk) in + error_unsolvable_implicit loc env current_sigma evi k None) pending () -let check_evars_are_solved env initial_sigma sigma = - check_typeclasses_instances_are_solved env sigma; - check_problems_are_solved env sigma; - check_extra_evars_are_solved env initial_sigma sigma +let check_evars_are_solved env current_sigma pending = + check_typeclasses_instances_are_solved env current_sigma pending; + 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 initial_sigma sigma = - let evdref = ref sigma in - if flags.use_typeclasses then apply_typeclasses env evdref false; +let solve_remaining_evars flags env current_sigma pending = + let evdref = ref current_sigma in + if flags.use_typeclasses then apply_typeclasses env evdref pending false; if Option.has_some flags.use_hook then - apply_inference_hook (Option.get flags.use_hook env) initial_sigma evdref; + 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 initial_sigma !evdref; + if flags.fail_evar then check_evars_are_solved env !evdref pending; !evdref let process_inference_flags flags env initial_sigma (sigma,c) = - let sigma = solve_remaining_evars flags env initial_sigma sigma in + let sigma = solve_remaining_evars flags env sigma (initial_sigma,sigma) in let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c |