From d28304f6ba18ad9527a63cd01b39a5ad27526845 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 9 Sep 2017 21:47:17 +0200
Subject: 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).
---
 plugins/extraction/common.ml     | 2 +-
 plugins/extraction/extraction.ml | 1 +
 plugins/extraction/table.ml      | 6 +++---
 3 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9772ebd64..9aec190d0 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -405,7 +405,7 @@ let ref_renaming_fun (k,r) =
     let idg = safe_basename_of_global r in
     match l with
     | [""] -> (* this happens only at toplevel of the monolithic case *)
-      let globs = Id.Set.elements (get_global_ids ()) in
+      let globs = get_global_ids () in
       let id = next_ident_away (kindcase_id k idg) globs in
       Id.to_string id
     | _ -> modular_rename k idg
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 7644b49ce..a227478d0 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -141,6 +141,7 @@ let make_typvar n vl =
     if not (String.contains s '\'') && Unicode.is_basic_ascii s then id
     else id_of_name Anonymous
   in
+  let vl = Id.Set.of_list vl in
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ca98f07e8..30e3b520f 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -750,11 +750,11 @@ let extraction_implicit r l =
 
 let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist"
 
-let modfile_ids = ref []
+let modfile_ids = ref Id.Set.empty
 let modfile_mps = ref MPmap.empty
 
 let reset_modfile () =
-  modfile_ids := Id.Set.elements !blacklist_table;
+  modfile_ids := !blacklist_table;
   modfile_mps := MPmap.empty
 
 let string_of_modfile mp =
@@ -763,7 +763,7 @@ let string_of_modfile mp =
     let id = Id.of_string (raw_string_of_modfile mp) in
     let id' = next_ident_away id !modfile_ids in
     let s' = Id.to_string id' in
-    modfile_ids := id' :: !modfile_ids;
+    modfile_ids := Id.Set.add id' !modfile_ids;
     modfile_mps := MPmap.add mp s' !modfile_mps;
     s'
 
-- 
cgit v1.2.3