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

5 files changed, 13 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f5eff693f..f1bee65ef 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1087,7 +1087,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* Not "goal_concl_style" means do alpha-conversion avoiding only *)
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
-  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
   let vars = vars_of_env env in
   extern false (scopt,[]) vars r
@@ -1099,14 +1099,14 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
   extern_constr_gen lax goal_concl_style None env sigma t
 
 let extern_type goal_concl_style env sigma t =
-  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
 
 let extern_closed_glob ?lax goal_concl_style env sigma t =
-  let avoid = if goal_concl_style then ids_of_context env else [] in
+  let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r =
     Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
   in
@@ -1177,15 +1177,15 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
       GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
-  | PFix f -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
-  | PCoFix c -> DAst.get (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+  | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
+  | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
   | PSort s -> GSort s
 
 let extern_constr_pattern env sigma pat =
   extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
 
 let extern_rel_context where env sigma sign =
-  let a = detype_rel_context Detyping.Later where [] (names_of_rel_context env,env) sigma sign in
+  let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
   let a = List.map (extended_glob_local_binder_of_decl) a in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6f7c6c827..1cea307d7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -469,8 +469,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
         | _ -> assert false
       in
       let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
-      let ienv = Id.Set.elements env.ids in
-      let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
+      let id = Namegen.next_ident_away (Id.of_string "pat") env.ids in
       let na = (loc, Name id) in
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern lvar env [na] bk tyc in
@@ -1939,13 +1938,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                 | _ ->
                   let fresh =
                     Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
-                  canonize_args t tt (fresh::forbidden_names)
+                  canonize_args t tt (Id.Set.add fresh forbidden_names)
                     ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
                 end
 	      | _ -> assert false in
 	  let _,args_rel =
 	    List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
-	  canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in
+	  canonize_args args_rel l forbidden_names_for_gen [] [] in
 	match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
     | None ->
       [], None in
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d8241c044..09a0ba83c 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -255,7 +255,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   in
   match kind_of_term (whd_all env t) with
     | Prod (na,a,b) ->
-	let na',avoid = find_displayed_name_in all [] na ([],b) in
+	let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in
 	let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in
 	!rigid, Array.to_list v
     | _ -> true, []
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 3d48114ec..0967d21f0 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -577,7 +577,7 @@ let rec subst_notation_constr subst bound raw =
       if r1' == r1 && k' == k then raw else NCast(r1',k')
 
 let subst_interpretation subst (metas,pat) =
-  let bound = List.map fst metas in
+  let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
   (metas,subst_notation_constr subst bound pat)
 
 (**********************************************************************)
@@ -1143,7 +1143,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
      to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
   | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
       let avoid =
-        free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in
+        Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in
       let id' = Namegen.next_ident_away id avoid in
       let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
       let sigma = match t2 with
diff --git a/interp/reserve.ml b/interp/reserve.ml
index a1e5bd0ea..dc0f60dcf 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -110,7 +110,7 @@ let revert_reserved_type t =
     let t = EConstr.Unsafe.to_constr t in
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
     let t = EConstr.of_constr t in
-    let t = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in
+    let t = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =