Fast path in computation of frozen evars in Pretyping.

Most of the time, undefined evars are not modified by the considered function,
which leads to the costly recomputation of a trivial partition of evars. We
simply take advantage of physical equality to discriminate when this is
useless and special-case it in the type of frozen evars.

1 files changed, 37 insertions, 16 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2e215b605d..88853045fc 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -257,16 +257,33 @@ type inference_flags = {
    [sigma'] into those already in [sigma] or deriving from an evar in
    [sigma] by restriction, and the evars properly created in [sigma'] *)
 
+type frozen =
+| FrozenId of evar_info Evar.Map.t
+  (** No pending evars. We do not put a set here not to reallocate like crazy,
+      but the actual data of the map is not used, only keys matter. All
+      functions operating on this type must have the same behaviour on
+      [FrozenId map] and [FrozenProgress (Evar.Map.domain map, Evar.Set.empty)] *)
+| FrozenProgress of Evar.Set.t * Evar.Set.t
+  (** Proper partition of the evar map as described above. *)
+
 let frozen_and_pending_holes (sigma, sigma') =
-  let add_derivative_of evk evi acc =
-    match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
-  let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in
-  let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
-  let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
-  (frozen,pending)
+  let undefined0 = Evd.undefined_map sigma in
+  (** Fast path when the undefined evars where not modified *)
+  if undefined0 == Evd.undefined_map sigma' then
+    FrozenId undefined0
+  else
+    let add_derivative_of evk evi acc =
+      match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in
+    let frozen = Evar.Map.fold add_derivative_of undefined0 Evar.Set.empty in
+    let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in
+    let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in
+    FrozenProgress (frozen, pending)
 
 let apply_typeclasses env evdref frozen fail_evar =
-  let filter_frozen evk = Evar.Set.mem evk frozen in
+  let filter_frozen = match frozen with
+  | FrozenId map -> fun evk -> Evar.Map.mem evk map
+  | FrozenProgress (frozen, _) -> fun 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 && not (filter_frozen evk))
@@ -276,7 +293,9 @@ let apply_typeclasses env evdref frozen fail_evar =
     evdref := Typeclasses.resolve_typeclasses
       ~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 =
+let apply_inference_hook hook evdref frozen = match frozen with
+| FrozenId _ -> ()
+| FrozenProgress (_, pending) ->
   evdref := Evar.Set.fold (fun evk sigma ->
     if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
     then
@@ -299,7 +318,9 @@ let check_typeclasses_instances_are_solved env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
   apply_typeclasses env (ref current_sigma) frozen true
 
-let check_extra_evars_are_solved env current_sigma pending =
+let check_extra_evars_are_solved env current_sigma frozen = match frozen with
+| FrozenId _ -> ()
+| FrozenProgress (_, pending) ->
   Evar.Set.iter
     (fun evk ->
       if not (Evd.is_defined current_sigma evk) then
@@ -326,26 +347,26 @@ let check_evars env initial_sigma sigma c =
       | _ -> Constr.iter proc_rec c
   in proc_rec c
 
-let check_evars_are_solved env current_sigma frozen pending =
+let check_evars_are_solved env current_sigma frozen =
   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
+  check_extra_evars_are_solved env current_sigma frozen
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
 let solve_remaining_evars flags env current_sigma init_sigma =
-  let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in
+  let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
   let evdref = ref current_sigma in
   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;
+    apply_inference_hook (Option.get flags.use_hook env) evdref frozen;
   if flags.solve_unification_constraints then apply_heuristics env evdref false;
-  if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
+  if flags.fail_evar then check_evars_are_solved env !evdref frozen;
   !evdref
 
 let check_evars_are_solved env current_sigma init_sigma =
-  let frozen,pending = frozen_and_pending_holes (init_sigma, current_sigma) in
-  check_evars_are_solved env current_sigma frozen pending
+  let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in
+  check_evars_are_solved env current_sigma frozen
 
 let process_inference_flags flags env initial_sigma (sigma,c) =
   let sigma = solve_remaining_evars flags env sigma initial_sigma in