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, 9 insertions, 9 deletions

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