From d28304f6ba18ad9527a63cd01b39a5ad27526845 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 Sep 2017 21:47:17 +0200
Subject: 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).
---
 proofs/clenv.ml    |  4 ++--
 proofs/tacmach.ml  | 17 +++++++++--------
 proofs/tacmach.mli |  2 +-
 3 files changed, 12 insertions(+), 11 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3


From b772c323f62b322c9b0a4ab90c7de8b1e2066bae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 10 Sep 2017 02:21:03 +0200
Subject: Efficient computation of the names contained in an environment.

---
 proofs/tacmach.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b08051d757..a8ec4d8ca3 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -64,7 +64,8 @@ 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_ids_set_of_hyps gls =
+  Environ.ids_of_named_context_val (Environ.named_context_val (pf_env gls))
 
 let pf_get_new_id id gls =
   next_ident_away id (pf_ids_set_of_hyps gls)
@@ -175,8 +176,8 @@ module New = struct
   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 env = Proofview.Goal.env gl in
+    Environ.ids_of_named_context_val (Environ.named_context_val env)
 
   let pf_get_new_id id gl =
     let ids = pf_ids_set_of_hyps gl in
-- 
cgit v1.2.3