chore(library): remove unique_id

src/library/CMakeLists.txt

@@ -16,6 +16,6 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   eval_helper.cpp messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
   documentation.cpp check.cpp parray.cpp process.cpp
   pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp
-  context_cache.cpp unique_id.cpp elab_context.cpp
+  context_cache.cpp elab_context.cpp
   scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp pos_info_provider.cpp
   derive_attribute.cpp)

src/library/init_module.cpp

@@ -45,7 +45,6 @@ Author: Leonardo de Moura
 #include "library/parray.h"
 #include "library/profiling.h"
 #include "library/time_task.h"
-#include "library/unique_id.h"
 #include "library/error_msgs.h"
 #include "library/formatter.h"
 #include "library/pos_info_provider.h"
@@ -79,7 +78,6 @@ void finalize_library_core_module() {
 }
 
 void initialize_library_module() {
-    initialize_unique_id();
     initialize_local_context();
     initialize_metavar_context();
     initialize_fingerprint();
@@ -153,6 +151,5 @@ void finalize_library_module() {
     finalize_fingerprint();
     finalize_metavar_context();
     finalize_local_context();
-    finalize_unique_id();
 }
 }

src/library/unique_id.cpp

@@ -1,54 +0,0 @@
-/*
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
-*/
-#include <limits>
-#include "runtime/thread.h"
-#include "runtime/exception.h"
-#include "library/unique_id.h"
-
-namespace lean {
-static unsigned g_next_thread_id       = 0;
-static mutex *  g_next_thread_id_guard = nullptr;
-
-LEAN_THREAD_VALUE(unsigned, g_thread_id, std::numeric_limits<unsigned>::max());
-LEAN_THREAD_VALUE(unsigned, g_next_idx, 0);
-
-unique_id::unique_id():
-    m_thread_id(std::numeric_limits<unsigned>::max()),
-    m_id(0) {
-}
-
-bool unique_id::is_valid() const {
-    return m_thread_id != std::numeric_limits<unsigned>::max();
-}
-
-unique_id mk_unique_id() {
-    if (g_thread_id == std::numeric_limits<unsigned>::max()) {
-        lock_guard<mutex> lock(*g_next_thread_id_guard);
-        g_thread_id = g_next_thread_id;
-        g_next_thread_id++;
-        if (g_next_thread_id == std::numeric_limits<unsigned>::max()) {
-            g_next_thread_id--;
-            throw exception("failed to generate unique id, too many threads");
-        }
-    }
-    unique_id r(g_thread_id, g_next_idx);
-    g_next_idx++;
-    if (g_next_idx == std::numeric_limits<unsigned>::max()) {
-        g_next_idx--;
-        throw exception("failed to generate unique unique id, too many ids have been generated");
-    }
-    return r;
-}
-
-void initialize_unique_id() {
-    g_next_thread_id_guard = new mutex();
-    register_thread_local_reset_fn([]() { g_next_idx = 0; });
-}
-
-void finalize_unique_id() {
-    delete g_next_thread_id_guard;
-}
-}

src/library/unique_id.h

@@ -1,46 +0,0 @@
-/*
-Copyright (c) 2018 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/pair.h"
-
-namespace lean {
-class unique_id {
-    unsigned m_thread_id;
-    unsigned m_id;
-    unique_id(unsigned i1, unsigned i2):m_thread_id(i1), m_id(i2) {}
-    friend unique_id mk_unique_id();
-    friend bool operator==(unique_id const & t1, unique_id const & t2) {
-        return t1.m_thread_id == t2.m_thread_id && t1.m_id == t2.m_id;
-    }
-public:
-    /* Use `mk_unique_id()`, this constructor produces and invalid id.
-       It can be used to represent uninitialized ids. */
-    unique_id();
-    bool is_valid() const;
-};
-
-inline bool operator!=(unique_id const & t1, unique_id const & t2) {
-    return !(t1 == t2);
-}
-
-/* Create a global unique id (modulo reset_thread_local).
-
-   Assumptions:
-   - We do not create more than 2^32 - 1 threads.
-     This is fine because we create a small set of threads
-     when we start the process, and then we create only tasks.
-
-   - Each thread does not create more than 2^32 ids.
-     This is fine because we reset the thread local counters
-     after each \c reset_thread_local operation.
-
-   That being said, if the assumptions above are violated
-   \c mk_unique_id throws an exception */
-unique_id mk_unique_id();
-
-void initialize_unique_id();
-void finalize_unique_id();
-}