Efficient fresh name generation relying on sets.

The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).

3 files changed, 12 insertions, 11 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ea60be31f0..5ef7fac814 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -557,7 +557,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
       let clause = mk_clenv_from_env env sigma n (c,t) in
       clenv_constrain_dep_args hyps_only largs clause
   | ExplicitBindings lbind ->
-      let t = rename_bound_vars_as_displayed sigma [] [] t in
+      let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
       let clause = mk_clenv_from_env env sigma n
 	(c, t)
       in clenv_match_args lbind clause
@@ -605,7 +605,7 @@ let make_evar_clause env sigma ?len t =
   | Some n -> assert (0 <= n); n
   in
   (** FIXME: do the renaming online *)
-  let t = rename_bound_vars_as_displayed sigma [] [] t in
+  let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
   let rec clrec (sigma, holes) n t =
     if n = 0 then (sigma, holes, t)
     else match EConstr.kind sigma t with
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a4d662e0ae..b08051d757 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -64,15 +64,10 @@ let pf_get_hyp_typ gls id =
   id |> pf_get_hyp gls |> NamedDecl.get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
+let pf_ids_set_of_hyps gls = Context.Named.to_vars (pf_hyps gls)
 
 let pf_get_new_id id gls =
-  next_ident_away id (pf_ids_of_hyps gls)
-
-let pf_get_new_ids ids gls =
-  let avoid = pf_ids_of_hyps gls in
-  List.fold_right
-    (fun id acc -> (next_ident_away id (acc@avoid))::acc)
-    ids []
+  next_ident_away id (pf_ids_set_of_hyps gls)
 
 let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
 
@@ -177,8 +172,14 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     ids_of_named_context hyps
 
+  let pf_ids_set_of_hyps gl =
+    (** We only get the identifiers in [hyps] *)
+    let gl = Proofview.Goal.assume gl in
+    let hyps = Proofview.Goal.hyps gl in
+    Context.Named.to_vars hyps
+
   let pf_get_new_id id gl =
-    let ids = pf_ids_of_hyps gl in
+    let ids = pf_ids_set_of_hyps gl in
     next_ident_away id ids
 
   let pf_get_hyp id gl =
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 93bf428fdc..7e6d83b10f 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -48,7 +48,6 @@ val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
-val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
 val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
 
@@ -120,6 +119,7 @@ module New : sig
 
   val pf_get_new_id  : identifier -> 'a Proofview.Goal.t -> identifier
   val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+  val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t
   val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
 
   val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration