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

11 files changed, 54 insertions, 51 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7455587c0..af28e2a6b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -113,8 +113,8 @@ let rec relocate_index sigma n1 n2 k t =
 
 type 'a rhs =
     { rhs_env    : env;
-      rhs_vars   : Id.t list;
-      avoid_ids  : Id.t list;
+      rhs_vars   : Id.Set.t;
+      avoid_ids  : Id.Set.t;
       it         : 'a option}
 
 type 'a equation =
@@ -553,7 +553,7 @@ let extract_rhs pb =
 let occur_in_rhs na rhs =
   match na with
     | Anonymous -> false
-    | Name id -> Id.List.mem id rhs.rhs_vars
+    | Name id -> Id.Set.mem id rhs.rhs_vars
 
 let is_dep_patt_in eqn pat = match DAst.get pat with
   | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
@@ -747,8 +747,8 @@ let get_names env sigma sign eqns =
   (* Otherwise, we take names from the parameters of the constructor but
      avoiding conflicts with user ids *)
   let allvars =
-    List.fold_left (fun l (_,_,eqn) -> List.union Id.equal l eqn.rhs.avoid_ids)
-      [] eqns in
+    List.fold_left (fun l (_,_,eqn) -> Id.Set.union l eqn.rhs.avoid_ids)
+      Id.Set.empty eqns in
   let names3,_ =
     List.fold_left2
       (fun (l,avoid) d na ->
@@ -757,7 +757,7 @@ let get_names env sigma sign eqns =
 	     (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid))
 	     d na
 	 in
-         (na::l,(Name.get_id na)::avoid))
+         (na::l,Id.Set.add (Name.get_id na) avoid))
       ([],allvars) (List.rev sign) names2 in
   names3,aliasname
 
@@ -999,8 +999,8 @@ let add_assert_false_case pb tomatch =
   in
   [ { patterns = pats;
       rhs = { rhs_env = pb.env;
-	      rhs_vars = [];
-	      avoid_ids = [];
+	      rhs_vars = Id.Set.empty;
+	      avoid_ids = Id.Set.empty;
 	      it = None };
       alias_stack = Anonymous::aliasnames;
       eqn_loc = None;
@@ -1570,10 +1570,12 @@ let matx_of_eqns env eqns =
   let build_eqn (loc,(ids,lpat,rhs)) =
     let initial_lpat,initial_rhs = lpat,rhs in
     let initial_rhs = rhs in
+    let avoid = Context.Named.to_vars (named_context env) in
+    let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
     let rhs =
       { rhs_env = env;
         rhs_vars = free_glob_vars initial_rhs;
-	avoid_ids = ids@(ids_of_named_context (named_context env));
+	avoid_ids = avoid;
 	it = Some initial_rhs } in
     { patterns = initial_lpat;
       alias_stack = [];
@@ -1751,7 +1753,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
 let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd env sigma t Anonymous) avoid in
-    DAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in
+    DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
     match EConstr.kind sigma (whd_all env sigma t) with
     | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc
@@ -1781,7 +1783,7 @@ let build_inversion_problem loc env sigma tms t =
       let d = LocalAssum (alias_of_pat pat,typ) in
       let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in
       pat::patl,acc_sign,acc in
-  let avoid0 = ids_of_context env in
+  let avoid0 = vars_of_env env in
   (* [patl] is a list of patterns revealing the substructure of
      constructors present in the constraints on the type of the
      multiple terms t1..tn that are matched in the original problem;
@@ -1823,7 +1825,7 @@ let build_inversion_problem loc env sigma tms t =
       rhs = { rhs_env = pb_env;
               (* we assume all vars are used; in practice we discard dependent
 		 vars so that the field rhs_vars is normally not used *)
-              rhs_vars = List.map fst subst;
+              rhs_vars = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty subst;
               avoid_ids = avoid;
 	      it = Some (lift n t) } } in
   (* [catch_all] is a catch-all default clause of the auxiliary
@@ -1841,7 +1843,7 @@ let build_inversion_problem loc env sigma tms t =
           eqn_loc = None;
           used = ref false;
           rhs = { rhs_env = pb_env;
-                  rhs_vars = [];
+                  rhs_vars = Id.Set.empty;
 	          avoid_ids = avoid0;
 	          it = None } } ] in
   (* [pb] is the auxiliary pattern-matching serving as skeleton for the
@@ -2085,7 +2087,7 @@ let prime avoid name =
 
 let make_prime avoid prevname =
   let previd, id = prime !avoid prevname in
-    avoid := id :: !avoid;
+    avoid := Id.Set.add id !avoid;
     previd, id
 
 let eq_id avoid id =
@@ -2113,7 +2115,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	    Name n -> name, avoid
 	  | Anonymous ->
 	      let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
-		Name id, id :: avoid
+		Name id, Id.Set.add id avoid
 	in
 	  ((DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
 	   (List.map (fun x -> mkRel 1) realargs), 1, avoid)
@@ -2157,7 +2159,7 @@ let constr_of_pat env evdref arsign pat avoid =
 		pat', sign, app, apptype, realargs, n, avoid
 	    | Name id ->
 		let sign = LocalAssum (alias, lift m ty) :: sign in
-		let avoid = id :: avoid in
+		let avoid = Id.Set.add id avoid in
 		let sign, i, avoid =
 		  try
 		    let env = push_rel_context sign env in
@@ -2168,7 +2170,7 @@ let constr_of_pat env evdref arsign pat avoid =
 		      (lift 1 app) (* aliased term *)
 		    in
 		    let neq = eq_id avoid id in
-		      LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid
+		      LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid
 		  with Reduction.NotConvertible -> sign, 1, avoid
 		in
 		  (* Mark the equality as a hole *)
@@ -2182,7 +2184,7 @@ let constr_of_pat env evdref arsign pat avoid =
 let eq_id avoid id =
   let hid = Id.of_string ("Heq_" ^ Id.to_string id) in
   let hid' = next_ident_away hid !avoid in
-    avoid := hid' :: !avoid;
+    avoid := Id.Set.add hid' !avoid;
     hid'
 
 let is_topvar sigma t =
@@ -2278,7 +2280,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	     (fun (idents, newpatterns, pats) pat arsign ->
 		let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in
 		  (idents, pat' :: newpatterns, cpat :: pats))
-	      ([], [], []) eqn.patterns sign
+	      (Id.Set.empty, [], []) eqn.patterns sign
 	 in
 	 let newpatterns = List.rev newpatterns and opats = List.rev pats in
 	 let rhs_rels, pats, signlen =
@@ -2379,8 +2381,8 @@ let abstract_tomatch env sigma tomatchs tycon =
 	       let name = next_ident_away (Id.of_string "filtered_var") names in
 		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
 	       LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx,
-	       name :: names, tycon)
-      ([], [], [], tycon) tomatchs
+	       Id.Set.add name names, tycon)
+      ([], [], Id.Set.empty, tycon) tomatchs
   in List.rev prev, ctx, tycon
 
 let build_dependent_signature env evdref avoid tomatchs arsign =
@@ -2502,7 +2504,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
     let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *)
       (* Build the dependent arity signature, the equalities which makes
 	 the first part of the predicate and their instantiations. *)
-    let avoid = [] in
+    let avoid = Id.Set.empty in
       build_dependent_signature env evdref avoid tomatchs arsign
 
   in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 428f64b99..7bdc604b8 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -49,16 +49,16 @@ val constr_of_pat :
            Evd.evar_map ref ->
            rel_context ->
            Glob_term.cases_pattern ->
-           Names.Id.t list ->
+           Names.Id.Set.t ->
            Glob_term.cases_pattern *
            (rel_context * constr *
             (types * constr list) * Glob_term.cases_pattern) *
-           Names.Id.t list
+           Names.Id.Set.t
 
 type 'a rhs =
     { rhs_env    : env;
-      rhs_vars   : Id.t list;
-      avoid_ids  : Id.t list;
+      rhs_vars   : Id.Set.t;
+      avoid_ids  : Id.Set.t;
       it         : 'a option}
 
 type 'a equation =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index fc0a650bc..7cfd2e27d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -205,7 +205,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 	| _ -> subco ())
       | Prod (name, a, b), Prod (name', a', b') ->
 	  let name' = 
-	    Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env))
+	    Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.vars_of_env env))
 	  in
 	  let env' = push_rel (LocalAssum (name', a')) env in
 	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index ca7f633dc..0973d73ee 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -178,7 +178,7 @@ let push_binder na1 na2 t ctx =
   let id2 = match na2 with
   | Name id2 -> id2
   | Anonymous ->
-     let avoid = List.map pi2 ctx in
+     let avoid = Id.Set.of_list (List.map pi2 ctx) in
      Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in
   (na1, id2, t) :: ctx
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 5e1430741..d81b88660 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -221,12 +221,12 @@ let lookup_name_as_displayed env sigma t s =
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | Cast (c,_,_) -> lookup avoid n c
     | _ -> None
-  in lookup (ids_of_named_context (named_context env)) 1 t
+  in lookup (Context.Named.to_vars (named_context env)) 1 t
 
 let lookup_index_as_renamed env sigma t n =
   let rec lookup n d c = match EConstr.kind sigma c with
     | Prod (name,_,c') ->
-	  (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
+	  (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with
                (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if Int.equal n 0 then
@@ -236,7 +236,7 @@ let lookup_index_as_renamed env sigma t n =
 		 else
 		   lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-	  (match compute_displayed_name_in sigma RenamingForGoal [] name c' with
+	  (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with
              | (Name _,_) -> lookup n (d+1) c'
              | (Anonymous,_) ->
 		 if Int.equal n 0 then
@@ -578,7 +578,7 @@ and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
     Array.fold_left2
       (fun (avoid, env, l) na ty ->
 	 let id = next_name_away na avoid in
-	 (id::avoid, add_name (Name id) None ty env, id::l))
+	 (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
       (avoid, env, []) names tys in
   let n = Array.length tys in
   let v = Array.map3
@@ -594,7 +594,7 @@ and detype_cofix d flags avoid env sigma n (names,tys,bodies) =
     Array.fold_left2
       (fun (avoid, env, l) na ty ->
 	 let id = next_name_away na avoid in
-	 (id::avoid, add_name (Name id) None ty env, id::l))
+	 (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
       (avoid, env, []) names tys in
   let ntys = Array.length tys in
   let v = Array.map2
@@ -615,14 +615,14 @@ and share_names d flags n l avoid env sigma c t =
           | _ -> na in
         let t' = detype d flags avoid env sigma t in
 	let id = next_name_away na avoid in
-        let avoid = id::avoid and env = add_name (Name id) None t env in
+        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
         share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
     (* May occur for fix built interactively *)
     | LetIn (na,b,t',c), _ when n > 0 ->
         let t'' = detype d flags avoid env sigma t' in
         let b' = detype d flags avoid env sigma b in
 	let id = next_name_away na avoid in
-        let avoid = id::avoid and env = add_name (Name id) (Some b) t' env in
+        let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
         share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
@@ -631,7 +631,7 @@ and share_names d flags n l avoid env sigma c t =
     | _, Prod (na',t',c') when n > 0 ->
         let t'' = detype d flags avoid env sigma t' in
 	let id = next_name_away na' avoid in
-        let avoid = id::avoid and env = add_name (Name id) None t' env in
+        let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
         share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
@@ -822,7 +822,7 @@ let rec subst_glob_constr subst = DAst.map (function
   | GRef (ref,u) as raw ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-         DAst.get (detype Now false [] (Global.env()) Evd.empty (EConstr.of_constr t))
+         DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t))
 
   | GSort _
   | GVar _
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 67c852af3..b70bfd83c 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -35,16 +35,16 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr
    [isgoal] tells if naming must avoid global-level synonyms as intro does 
    [ctx] gives the names of the free variables *)
 
-val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr
+val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> constr -> glob_constr
 
-val detype : 'a delay -> ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> 'a glob_constr_g
+val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g
 
 val detype_sort : evar_map -> sorts -> glob_sort
 
-val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
+val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> 
   evar_map -> rel_context -> 'a glob_decl_g list
 
-val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr
+val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
 
 (** look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_displayed  : env -> evar_map -> constr -> Id.t -> int option
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 7f5a780f9..9fed28bb3 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -72,7 +72,7 @@ let define_pure_evar_as_product evd evk =
   let open Context.Named.Declaration in
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
+  let id = next_ident_away idx (Context.Named.to_vars (evar_context evi)) in
   let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
   let s = destSort evd concl in
   let evd1,(dom,u1) =
@@ -127,7 +127,7 @@ let define_pure_evar_as_lambda env evd evk =
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
   | _ -> error_not_product env evd typ in
-  let avoid = ids_of_named_context (evar_context evi) in
+  let avoid = Context.Named.to_vars (evar_context evi) in
   let id =
     next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
   let newenv = push_named (LocalAssum (id, dom)) evenv in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ef0fb8ea6..8652a4146 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -679,6 +679,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let filter1 = evar_filter evi1 in
   let src = subterm_source evk1 evi1.evar_source in
   let ids1 = List.map get_id (named_context_of_val sign1) in
+  let avoid = Context.Named.to_vars (named_context_of_val sign1) in
   let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
   let open Context.Rel.Declaration in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
@@ -700,9 +701,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
       (push_named_context_val d' sign, Filter.extend 1 filter,
        (mkRel 1)::(List.map (lift 1) inst_in_env),
        (mkRel 1)::(List.map (lift 1) inst_in_sign),
-       push_rel d env,evd,id::avoid))
+       push_rel d env,evd,Id.Set.add id avoid))
       rel_sign
-      (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
+      (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid)
   in
   let evd,ev2ty_in_sign =
     let s = Retyping.get_sort_of env evd ty_in_env in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index e1576b971..7804cc679 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -273,17 +273,17 @@ let free_glob_vars =
     | _ -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in
   fun rt ->
     let vs = vars Id.Set.empty Id.Set.empty rt in
-    Id.Set.elements vs
+    vs
 
 let glob_visible_short_qualid c =
   let rec aux acc c = match DAst.get c with
     | GRef (c,_) ->
         let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in
         let dir,id = Libnames.repr_qualid  qualid in
-        if DirPath.is_empty dir then id :: acc else acc
+        if DirPath.is_empty dir then Id.Set.add id acc else acc
     | _ ->
         fold_glob_constr aux acc c
-  in aux [] c
+  in aux Id.Set.empty c
 
 let warn_variable_collision =
   let open Pp in
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index bacc8fbe4..49ea9727c 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -43,11 +43,11 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
 val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool
-val free_glob_vars : 'a glob_constr_g -> Id.t list
+val free_glob_vars : 'a glob_constr_g -> Id.Set.t
 val bound_glob_vars : glob_constr -> Id.Set.t
 (* Obsolete *)
 val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option
-val glob_visible_short_qualid : 'a glob_constr_g -> Id.t list
+val glob_visible_short_qualid : 'a glob_constr_g -> Id.Set.t
 
 (* Renaming free variables using a renaming map; fails with
    [UnsoundRenaming] if applying the renaming would introduce
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f090921e5..59cb43302 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1616,7 +1616,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let id =
     let t = match ty with Some t -> t | None -> get_type_of env sigma c in
     let x = id_of_name_using_hdchar (Global.env()) sigma t name in
-    let ids = ids_of_named_context (named_context env) in
+    let ids = Context.Named.to_vars (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context_val x (named_context_val env) then
       user_err ~hdr:"Unification.make_abstraction_core"