feat(util/fresh_name): implement mk_fresh_name using name_generator

src/library/mt_task_queue.cpp

@@ -110,6 +110,7 @@ void mt_task_queue::spawn_worker() {
             reset_thread_local();
             {
                 flet<gtask> _(this_worker->m_current_task, t);
+                set_fresh_name_generator(t->get_name_generator());
                 scoped_current_task scope_cur_task(&t);
                 notify_queue_changed();
                 lock.unlock();

src/util/fresh_name.cpp

@@ -12,49 +12,17 @@ Author: Leonardo de Moura
 #include "util/shared_mutex.h"
 
 namespace lean {
-static name_set *     g_fresh_name_prefixes = nullptr;
-static shared_mutex * g_fresh_name_prefixes_guard = nullptr;
-
-static void register_fresh_name_prefix(name const & p) {
-    exclusive_lock lock(*g_fresh_name_prefixes_guard);
-    g_fresh_name_prefixes->insert(p);
-}
-
-/* CACHE_RESET: NO */
-MK_THREAD_LOCAL_GET_DEF(name, get_prefix);
-/* CACHE_RESET: YES */
-LEAN_THREAD_VALUE(unsigned, g_next_idx, 0);
-
-static bool is_fresh_prefix(name const & p) {
-    if (p == get_prefix())
-        return true;
-    shared_lock lock(*g_fresh_name_prefixes_guard);
-    return g_fresh_name_prefixes->contains(p);
-};
+static name * g_fresh = nullptr;
+MK_THREAD_LOCAL_GET(name_generator, get_name_generator, *g_fresh);
 
 name mk_fresh_name() {
-    name & prefix = get_prefix();
-    if (prefix.is_anonymous()) {
-        // prefix has not been initialized for this thread yet.
-        prefix = name::mk_internal_unique_name();
-        register_fresh_name_prefix(prefix);
-    }
-    /* REMARK: after we implement RESET operation we will not need the following test anymore */
-    if (g_next_idx == std::numeric_limits<unsigned>::max()) {
-        // avoid overflow
-        prefix = name(prefix, g_next_idx);
-        register_fresh_name_prefix(prefix);
-        g_next_idx = 0;
-    }
-    name r(prefix, g_next_idx);
-    g_next_idx++;
-    return r;
+    return get_name_generator().next();
 }
 
 bool is_fresh_name(name const & n) {
     if (n.is_anonymous() || !n.is_numeral())
         return false;
-    else if (is_fresh_prefix(n.get_prefix()))
+    else if (n.get_prefix() == *g_fresh)
         return true;
     else
         return is_fresh_name(n.get_prefix());
@@ -81,19 +49,7 @@ name sanitize_if_fresh(name const & n) {
 
 name mk_tagged_fresh_name(name const & tag) {
     lean_assert(tag.is_atomic());
-    name & prefix = get_prefix();
-    if (prefix.is_anonymous()) {
-        // prefix has not been initialized for this thread yet.
-        prefix = name::mk_internal_unique_name();
-    }
-    if (g_next_idx == std::numeric_limits<unsigned>::max()) {
-        // avoid overflow
-        prefix = name(prefix, g_next_idx);
-        g_next_idx = 0;
-    }
-    name r(tag + prefix, g_next_idx);
-    g_next_idx++;
-    return r;
+    return tag + mk_fresh_name();
 }
 
 bool is_tagged_by(name const & n, name const & tag) {
@@ -123,13 +79,23 @@ optional<name> get_tagged_name_suffix(name const & n, name const & tag) {
     }
 }
 
+name_generator get_fresh_name_generator_snapshot() {
+    return get_name_generator();
+}
+
+void set_fresh_name_generator(name_generator const & g) {
+    get_name_generator() = g;
+}
+
+name_generator mk_fresh_name_generator_child() {
+    return get_name_generator().mk_child();
+}
+
 void initialize_fresh_name() {
-    g_fresh_name_prefixes = new name_set();
-    g_fresh_name_prefixes_guard = new shared_mutex();
+    g_fresh = new name("_fresh");
 }
 
 void finalize_fresh_name() {
-    delete g_fresh_name_prefixes;
-    delete g_fresh_name_prefixes_guard;
+    delete g_fresh;
 }
 }

src/util/fresh_name.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "util/name.h"
+#include "util/name_generator.h"
 
 namespace lean {
 /** \brief Create a unique fresh name. This operation is thread-safe, and it guarantees the names are unique
@@ -24,6 +25,26 @@ optional<name> get_tagged_name_suffix(name const & n, name const & tag);
 bool is_fresh_name(name const & n);
 name sanitize_if_fresh(name const & n);
 
+/* Return a snapshot of the thread local name_generator for fresh names.
+   We use this operation to save the state of the fresh name_generator in the parser snapshots. */
+name_generator get_fresh_name_generator_snapshot();
+
+/* Set the thread local name_generator.
+
+   We use this operation:
+   1- to restore the state of the fresh name_generator when we restore parser snapshots.
+   2- to set the fresh name_generator for a task.
+
+   \pre \c g must have been created using `get_fresh_name_generator_snapshot` or `mk_fresh_name_generator_child`.
+*/
+void set_fresh_name_generator(name_generator const & g);
+
+/* Create a new name_generator that does not create names that may conflict with names
+   generated by the current thread local fresh name_generator.
+
+   We use this operation to set the name_generator before we execute a task. */
+name_generator mk_fresh_name_generator_child();
+
 void initialize_fresh_name();
 void finalize_fresh_name();
 }

src/util/init_module.cpp

@@ -19,10 +19,12 @@ void initialize_util_module() {
     initialize_thread();
     initialize_ascii();
     initialize_name();
+    initialize_name_generator();
     initialize_fresh_name();
 }
 void finalize_util_module() {
     finalize_fresh_name();
+    finalize_name_generator();
     finalize_name();
     finalize_ascii();
     finalize_thread();

src/util/task.h

@@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 */
 #pragma once
+#include <memory>
 #include "util/buffer.h"
 #include "util/thread.h"
 #include "util/cancellable.h"
-#include <memory>
+#include "util/fresh_name.h"
 
 namespace lean {
 
@@ -61,13 +62,19 @@ class gtask_cell : public cancellable {
 
     virtual void execute() {};
 
-    gtask_cell(task_state state) : m_state(state) {}
-
     atomic<task_state>          m_state;
     std::unique_ptr<gtask_data> m_data;
     std::exception_ptr          m_exception;
+    name_generator              m_name_gen;
 
-    gtask_cell(gtask_imp * imp, task_flags flags) : m_state(task_state::Created) {
+    gtask_cell(task_state state) :
+        m_state(state),
+        m_name_gen(mk_fresh_name_generator_child()) {
+    }
+
+    gtask_cell(gtask_imp * imp, task_flags flags) :
+        m_state(task_state::Created),
+        m_name_gen(mk_fresh_name_generator_child()) {
         m_data.reset(new gtask_data(imp, flags));
     }
 
@@ -79,6 +86,8 @@ public:
     bool peek_is_finished() const { return m_state.load() > task_state::Running; }
     std::exception_ptr peek_exception() const;
 
+    name_generator const & get_name_generator() const { return m_name_gen; }
+
     virtual ~gtask_cell() {}
 };