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).

1 files changed, 10 insertions, 11 deletions

diff --git a/engine/namegen.mli b/engine/namegen.mli
index 14846a9184..6fde90a39c 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -72,23 +72,22 @@ val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t
     the whole identifier except for the {i subscript}.
 
     E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *)
-val next_ident_away : Id.t -> Id.t list -> Id.t
+val next_ident_away : Id.t -> Id.Set.t -> Id.t
 
 (** Avoid clashing with a name already used in current module *)
-val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
+val next_ident_away_in_goal : Id.t -> Id.Set.t -> Id.t
 
 (** Avoid clashing with a name already used in current module 
    but tolerate overwriting section variables, as in goals *)
-val next_global_ident_away : Id.t -> Id.t list -> Id.t
+val next_global_ident_away : Id.t -> Id.Set.t -> Id.t
 
 (** Default is [default_non_dependent_ident] *)
-val next_name_away  : Name.t -> Id.t list -> Id.t
+val next_name_away  : Name.t -> Id.Set.t -> Id.t
 
-val next_name_away_with_default : string -> Name.t -> Id.t list ->
-  Id.t
+val next_name_away_with_default : string -> Name.t -> Id.Set.t -> Id.t
 
 val next_name_away_with_default_using_types : string -> Name.t ->
-  Id.t list -> types -> Id.t
+  Id.Set.t -> types -> Id.t
 
 val set_reserved_typed_name : (types -> Name.t) -> unit
 
@@ -103,13 +102,13 @@ type renaming_flags =
 val make_all_name_different : env -> evar_map -> env
 
 val compute_displayed_name_in :
-  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val compute_and_force_displayed_name_in :
-  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val compute_displayed_let_name_in :
-  evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list
+  evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
 val rename_bound_vars_as_displayed :
-  evar_map -> Id.t list -> Name.t list -> types -> types
+  evar_map -> Id.Set.t -> Name.t list -> types -> types
 
 (**********************************************************************)
 (* Naming strategy for arguments in Prop when eliminating inductive types *)