From 8131e35caaacf86cd52262329ab1b0aaa1b8c5b3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 23 Mar 2017 11:29:00 +0100
Subject: Better algorithm for Evarconv.max_undefined_with_candidates.

Instead of crawling the whole undefined evar map, we use the fold_right
function to process evars in decreasing order.
---
 pretyping/evarconv.ml | 28 +++++++++++++++-------------
 1 file changed, 15 insertions(+), 13 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 88ea08c840..d18b437a33 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1196,20 +1196,22 @@ let check_problems_are_solved env evd =
   | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
   | _ -> ()
 
+exception MaxUndefined of (Evar.t * evar_info * constr list)
+
 let max_undefined_with_candidates evd =
-  (* If evar were ordered with highest index first, fold_undefined
-     would be going decreasingly and we could use fold_undefined to
-     find the undefined evar of maximum index (alternatively,
-     max_bindings from ocaml 3.12 could be used); instead we traverse
-     the whole map *)
-  let l = Evd.fold_undefined
-    (fun evk ev_info evars ->
-        match ev_info.evar_candidates with
-        | None -> evars
-        | Some l -> (evk,ev_info,l)::evars) evd [] in
-  match l with
-  | [] -> None
-  | a::l -> Some (List.last (a::l))
+  let fold evk evi () = match evi.evar_candidates with
+  | None -> ()
+  | Some l -> raise (MaxUndefined (evk, evi, l))
+  in
+  (** [fold_right] traverses the undefined map in decreasing order of indices.
+  The evar with candidates of maximum index is thus the first evar with
+  candidates found by a [fold_right] traversal. This has a significant impact on
+  performance. *)
+  try
+    let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in
+    None
+  with MaxUndefined ans ->
+    Some ans
 
 let rec solve_unconstrained_evars_with_candidates ts evd =
   (* max_undefined is supposed to return the most recent, hence
-- 
cgit v1.2.3