Merge PR #1040: Efficient fresh name generation

8 files changed, 53 insertions, 49 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5f6d78359..bd5fb1d92 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -587,7 +587,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
     tclTHENLIST
       [
 	(* We first introduce the variables *)
-	tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps));
+	tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps)));
 	(* Then the equation itself *)
 	Proofview.V82.of_tactic (intro_using heq_id);
 	onLastHypId (fun heq_id -> tclTHENLIST [
@@ -1614,7 +1614,7 @@ let prove_principle_for_gen
       let hid =
 	next_ident_away_in_goal
 	  (Id.of_string "prov")
-	  hyps
+	  (Id.Set.of_list hyps)
       in
       tclTHENLIST
 	[
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 409bb89ee..018b51517 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -39,7 +39,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     | decl :: predicates ->
        (match Context.Rel.Declaration.get_name decl with
 	| Name x ->
-	   let id = Namegen.next_ident_away x avoid in
+	   let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in
 	   Hashtbl.add tbl id x;
 	   RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates
 	| Anonymous -> anomaly (Pp.str "Anonymous property binder."))
@@ -285,7 +285,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    let time2 = System.get_time ()  in *)
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
   let new_princ_name =
-    next_ident_away_in_goal (Id.of_string "___________princ_________") []
+    next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty
   in
   let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
   let hook = Lemmas.mk_hook (hook new_principle_type) in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7087a195e..e8e5bfccc 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -120,13 +120,13 @@ let combine_args arg args =
 
 
 let ids_of_binder =  function
-  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> []
-  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> [id]
+  | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty
+  | LetIn (Name id)  | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id
 
 let rec change_vars_in_binder mapping = function
     [] -> []
   | (bt,t)::l ->
-      let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in
+      let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in
       (bt,change_vars mapping t)::
 	(if Id.Map.is_empty new_mapping
 	 then l
@@ -137,27 +137,27 @@ let rec replace_var_by_term_in_binder x_id term = function
   | [] -> []
   | (bt,t)::l ->
       (bt,replace_var_by_term x_id term t)::
-	if Id.List.mem x_id (ids_of_binder bt)
+	if Id.Set.mem x_id (ids_of_binder bt)
 	then l
 	else replace_var_by_term_in_binder x_id term l
 
-let add_bt_names bt = List.append (ids_of_binder bt)
+let add_bt_names bt = Id.Set.union (ids_of_binder bt)
 
 let apply_args ctxt body args =
   let need_convert_id avoid id =
-    List.exists (is_free_in id) args || Id.List.mem id avoid
+    List.exists (is_free_in id) args || Id.Set.mem id avoid
   in
   let need_convert avoid  bt =
-    List.exists (need_convert_id avoid) (ids_of_binder bt)
+    Id.Set.exists (need_convert_id avoid) (ids_of_binder bt)
   in
-  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
+  let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) =
     match na with
-       | Name id when Id.List.mem id avoid ->
+       | Name id when Id.Set.mem id avoid ->
 	   let new_id = Namegen.next_ident_away id avoid in
-	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
+	   Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid
        | _ -> na,mapping,avoid
   in
-  let next_bt_away bt (avoid:Id.t list) =
+  let next_bt_away bt (avoid:Id.Set.t) =
     match bt with
       | LetIn na ->
 	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
@@ -182,15 +182,15 @@ let apply_args ctxt body args =
 	  let new_avoid,new_ctxt',new_body,new_id =
 	    if need_convert_id avoid id
 	    then
-	      let new_avoid =  id::avoid in
+	      let new_avoid =  Id.Set.add id avoid in
 	      let new_id = Namegen.next_ident_away id new_avoid in
-	      let new_avoid' = new_id :: new_avoid in
+	      let new_avoid' = Id.Set.add new_id new_avoid in
 	      let mapping = Id.Map.add id new_id Id.Map.empty in
 	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
 	      let new_body = change_vars mapping body in
 	      new_avoid',new_ctxt',new_body,new_id
 	    else
-	      id::avoid,ctxt',body,id
+	      Id.Set.add id avoid,ctxt',body,id
 	  in
 	  let new_body = replace_var_by_term new_id arg new_body in
 	  let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
@@ -214,7 +214,7 @@ let apply_args ctxt body args =
 	  in
 	  (new_bt,t)::new_ctxt',new_body
   in
-  do_apply []  ctxt body args
+  do_apply Id.Set.empty ctxt body args
 
 
 let combine_app f args =
@@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
+	     (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i)))
 	  )
       in
       let patl_as_term =
@@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
 		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
-		let res_raw_type = Detyping.detype Detyping.Now false [] env (Evd.from_env env) rt_typ in
+		let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkGVar res in
@@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		  match n with
 		    | Name id when List.exists (is_free_in id) args ->
 			(* need to alpha-convert the name *)
-			let new_id = Namegen.next_ident_away id avoid in
+			let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
 			let new_avoid = id:: avoid in
 			let new_b =
 			  replace_var_by_term
@@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
 			let raw_typ_of_id =
-			  Detyping.detype Detyping.Now false []
+			  Detyping.detype Detyping.Now false Id.Set.empty
 			    env_with_pat_ids (Evd.from_env env) typ_of_id
 			in
 			mkGProd (Name id,raw_typ_of_id,acc))
@@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
 		 let typ_as_constr = EConstr.of_constr typ_as_constr in
-		 let typ = Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_as_constr in
+		 let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
                  (* removing trivial holes *) 
                  let pat_as_term = solve_trivial_holes pat_as_term e in 
@@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
 		      let raw_typ_of_id =
-			Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_of_id
+			Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id
 		      in
 		      raw_typ_of_id
 			   )::acc
@@ -1001,7 +1001,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let rt_typ = DAst.make @@
 		       GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
 			    (List.map
-			      (fun p -> Detyping.detype Detyping.Now false []
+			      (fun p -> Detyping.detype Detyping.Now false Id.Set.empty
 				 env (Evd.from_env env)
 				 (EConstr.of_constr p)) params)@(Array.to_list
 				      (Array.make
@@ -1028,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				   match na with
 				     | Anonymous -> acc
 				     | Name id' ->
-					 (id',Detyping.detype Detyping.Now false []
+					 (id',Detyping.detype Detyping.Now false Id.Set.empty
 					    env
                                             (Evd.from_env env)
 					    arg)::acc
 				 else if isVar var_as_constr
-				 then (destVar var_as_constr,Detyping.detype Detyping.Now false []
+				 then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty
 					 env
                                          (Evd.from_env env)
 					 arg)::acc
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 02ee56ac5..0666ab4f1 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -198,7 +198,7 @@ let rec alpha_pat excluded pat =
     | PatVar(Name id) ->
 	if Id.List.mem id excluded
 	then
-	  let new_id = Namegen.next_ident_away id excluded in
+	  let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 	  (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
 	(Id.Map.add id new_id Id.Map.empty)
 	else pat, excluded,Id.Map.empty
@@ -206,7 +206,7 @@ let rec alpha_pat excluded pat =
 	let new_na,new_excluded,map =
 	  match na with
 	    | Name id when Id.List.mem id excluded ->
-		let new_id = Namegen.next_ident_away id excluded in
+		let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 		Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
 	    | _ -> na,excluded,Id.Map.empty
 	in
@@ -261,7 +261,7 @@ let rec alpha_rt excluded rt =
     match DAst.get rt with
       | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt
       | GLambda(Anonymous,k,t,b) ->
-	  let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in
+	  let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in
 	  let new_excluded = new_id :: excluded in
 	  let new_t = alpha_rt new_excluded t in
 	  let new_b = alpha_rt new_excluded b in
@@ -276,7 +276,7 @@ let rec alpha_rt excluded rt =
 	let new_c = alpha_rt excluded c in
 	GLetIn(Anonymous,new_b,new_t,new_c)
     | GLambda(Name id,k,t,b) ->
-	let new_id = Namegen.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 	let t,b =
 	  if Id.equal new_id id
 	  then t, b
@@ -289,7 +289,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	GLambda(Name new_id,k,new_t,new_b)
     | GProd(Name id,k,t,b) ->
-	let new_id = Namegen.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 	let new_excluded = new_id::excluded in
 	let t,b =
 	  if Id.equal new_id id
@@ -302,7 +302,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	GProd(Name new_id,k,new_t,new_b)
     | GLetIn(Name id,b,t,c) ->
-	let new_id = Namegen.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 	let c =
 	  if Id.equal new_id id then c
 	  else change_vars (Id.Map.add id new_id Id.Map.empty) c
@@ -320,7 +320,7 @@ let rec alpha_rt excluded rt =
 	       match na with
 		 | Anonymous -> (na::nal,excluded,mapping)
 		 | Name id ->
-		     let new_id = Namegen.next_ident_away id excluded in
+		     let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in
 		     if Id.equal new_id id
 		     then
 		       na::nal,id::excluded,mapping
@@ -741,7 +741,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
            match evi.evar_body with
            | Evar_defined c ->
            (* we just have to lift the solution in glob_term *)
-              Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c))
+              Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c))
            | Evar_empty -> rt (* the hole was not solved : we do nothing *)
        )
     | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *)
@@ -763,7 +763,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
                 match evi.evar_body with
                 | Evar_defined c ->
                    (* we just have to lift the solution in glob_term *)
-                   Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c))
+                   Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c))
                 | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *)
          in 
          res
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5f4d514f3..1e8854249 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -12,7 +12,7 @@ let mk_equation_id id = Nameops.add_suffix id "_equation"
 let msgnl m =
   ()
 
-let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid)
 
 let fresh_name avoid s = Name (fresh_id avoid s)
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5f8d50da1..299753766 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -131,9 +131,9 @@ let generate_type evd g_to_f f graph i =
 			   | Name id -> Some id
 			   | Anonymous -> None
   in
-  let named_ctxt = List.map_filter filter fun_ctxt in
+  let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in
   let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
-  let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in
+  let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (Id.Set.add res_id named_ctxt) in
   (*i we can then type the argument to be applied to the function [f] i*)
   let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in
   (*i
@@ -189,7 +189,7 @@ let rec generate_fresh_id x avoid i =
   if i == 0
   then []
   else
-    let id = Namegen.next_ident_away_in_goal x avoid in
+    let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in
     id::(generate_fresh_id x (id::avoid) (pred i))
 
 
@@ -239,7 +239,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
        environment and due to the bug #1174, we will need to pose the principle
        using a name
     *)
-    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
+    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") (Id.Set.of_list ids) in
     let ids = principle_id :: ids in
     (* We get the branches of the principle *)
     let branches = List.rev princ_infos.branches in
@@ -396,7 +396,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
 	     p::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
@@ -406,7 +406,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
-	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
+	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
 	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 96200a98a..77c26f8ce 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -767,7 +767,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
     let substindtyp = EConstr.of_constr substindtyp in
-    Detyping.detype Detyping.Now false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
+    Detyping.detype Detyping.Now false avoid (Global.env()) Evd.empty substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
   (* add  to avoid all indentifiers of lcstr1 *)
@@ -851,7 +851,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
   match rdecl with
     | LocalAssum (nme,t) ->
         let t = EConstr.of_constr t in
-        let traw = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in
+        let traw = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in
         DAst.make @@ GProd (nme,Explicit,traw,t2)
     | LocalDef _ -> assert false
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7b63366e8..74c454334 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -115,13 +115,17 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 (* Generic values *)
 let pf_get_new_ids idl g =
   let ids = pf_ids_of_hyps g in
+  let ids = Id.Set.of_list ids in
   List.fold_right
-    (fun id acc -> next_global_ident_away id (acc@ids)::acc)
+    (fun id acc -> next_global_ident_away id (Id.Set.union (Id.Set.of_list acc) ids)::acc)
     idl
     []
 
+let next_ident_away_in_goal ids avoid =
+  next_ident_away_in_goal ids (Id.Set.of_list avoid)
+
 let compute_renamed_type gls c =
-  rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) []
+  rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) []
     (pf_unsafe_type_of gls c)
 let h'_id = Id.of_string "h'"
 let teq_id = Id.of_string "teq"
@@ -1302,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 	with e when CErrors.noncritical e ->
           anomaly (Pp.str "open_new_goal with an unamed theorem.")
   in
-  let na = next_global_ident_away name [] in
+  let na = next_global_ident_away name Id.Set.empty in
   if Termops.occur_existential sigma gls_type then
     CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
   let hook _ _ =