Merge PR #1040: Efficient fresh name generation

3 files changed, 26 insertions, 27 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index a75fe721f7..1dd29e6eae 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -239,7 +239,7 @@ let visible_ids sigma (nenv, c) =
 let next_name_away_in_cases_pattern sigma env_t na avoid =
   let id = match na with Name id -> id | Anonymous -> default_dependent_ident in
   let visible = visible_ids sigma env_t in
-  let bad id = Id.List.mem id avoid || is_constructor id
+  let bad id = Id.Set.mem id avoid || is_constructor id
                                     || Id.Set.mem id visible in
   next_ident_away_from id bad
 
@@ -253,8 +253,8 @@ let next_name_away_in_cases_pattern sigma env_t na avoid =
      name is taken by finding a free subscript starting from 0 *)
 
 let next_ident_away_in_goal id avoid =
-  let id = if Id.List.mem id avoid then restart_subscript id else id in
-  let bad id = Id.List.mem id avoid || (is_global id && not (is_section_variable id)) in
+  let id = if Id.Set.mem id avoid then restart_subscript id else id in
+  let bad id = Id.Set.mem id avoid || (is_global id && not (is_section_variable id)) in
   next_ident_away_from id bad
 
 let next_name_away_in_goal na avoid =
@@ -271,16 +271,16 @@ let next_name_away_in_goal na avoid =
    beyond the current subscript *)
 
 let next_global_ident_away id avoid =
-  let id = if Id.List.mem id avoid then restart_subscript id else id in
-  let bad id = Id.List.mem id avoid || is_global id in
+  let id = if Id.Set.mem id avoid then restart_subscript id else id in
+  let bad id = Id.Set.mem id avoid || is_global id in
   next_ident_away_from id bad
 
 (* 4- Looks for next fresh name outside a list; if name already used,
    looks for same name with lower available subscript *)
 
 let next_ident_away id avoid =
-  if Id.List.mem id avoid then
-    next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid)
+  if Id.Set.mem id avoid then
+    next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid)
   else id
 
 let next_name_away_with_default default na avoid =
@@ -302,7 +302,7 @@ let next_name_away = next_name_away_with_default default_non_dependent_string
 
 let make_all_name_different env sigma =
   (** FIXME: this is inefficient, but only used in printing *)
-  let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in
+  let avoid = ref (ids_of_named_context_val (named_context_val env)) in
   let sign = named_context_val env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
@@ -310,7 +310,7 @@ let make_all_name_different env sigma =
     (fun decl newenv ->
        let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in
        let id = next_name_away na !avoid in
-       avoid := id::!avoid;
+       avoid := Id.Set.add id !avoid;
        push_rel (RelDecl.set_name (Name id) decl) newenv)
     rels ~init:env0
 
@@ -321,7 +321,7 @@ let make_all_name_different env sigma =
 
 let next_ident_away_for_default_printing sigma env_t id avoid =
   let visible = visible_ids sigma env_t in
-  let bad id = Id.List.mem id avoid || Id.Set.mem id visible in
+  let bad id = Id.Set.mem id avoid || Id.Set.mem id visible in
   next_ident_away_from id bad
 
 let next_name_away_for_default_printing sigma env_t na avoid =
@@ -371,7 +371,7 @@ let compute_displayed_name_in sigma flags avoid na c =
   | _ ->
     let fresh_id = next_name_for_display sigma flags na avoid in
     let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
-    (idopt, fresh_id::avoid)
+    (idopt, Id.Set.add fresh_id avoid)
 
 let compute_and_force_displayed_name_in sigma flags avoid na c =
   match na with
@@ -379,11 +379,11 @@ let compute_and_force_displayed_name_in sigma flags avoid na c =
     (Anonymous,avoid)
   | _ ->
     let fresh_id = next_name_for_display sigma flags na avoid in
-    (Name fresh_id, fresh_id::avoid)
+    (Name fresh_id, Id.Set.add fresh_id avoid)
 
 let compute_displayed_let_name_in sigma flags avoid na c =
   let fresh_id = next_name_for_display sigma flags na avoid in
-  (Name fresh_id, fresh_id::avoid)
+  (Name fresh_id, Id.Set.add fresh_id avoid)
 
 let rename_bound_vars_as_displayed sigma avoid env c =
   let rec rename avoid env c =
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 *)
diff --git a/engine/termops.ml b/engine/termops.ml
index e2bdf72387..b7fa2dc4a4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1071,9 +1071,9 @@ let replace_term_gen sigma eq_fun c by_c in_t =
 let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t
 
 let vars_of_env env =
-  let s =
-    Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s)
-      (named_context env) ~init:Id.Set.empty in
+  let s = Environ.ids_of_named_context_val (Environ.named_context_val env) in
+  if List.is_empty (Environ.rel_context env) then s
+  else
   Context.Rel.fold_outside
     (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s)
     (rel_context env) ~init:s