fix(library/type_context,library/blast/blast): blast uses multiple type_context objects, this commit makes sure all of them use the same local name generator

src/library/blast/blast.cpp

@@ -33,6 +33,7 @@ class blastenv {
     environment                m_env;
     io_state                   m_ios;
     name_generator             m_ngen;
+    tmp_local_generator        m_tmp_local_generator;
     name_set                   m_lemma_hints;
     name_set                   m_unfold_hints;
     name_map<level>            m_uvar2uref;    // map global universe metavariables to blast uref's
@@ -46,41 +47,17 @@ class blastenv {
 
     class tctx : public type_context {
         blastenv &         m_benv;
-        unsigned           m_next_local_idx;
         std::vector<state> m_stack;
     public:
         tctx(blastenv & benv):
-            type_context(benv.m_env, benv.m_ios),
-            m_benv(benv), m_next_local_idx(0) {}
+            type_context(benv.m_env, benv.m_ios, benv.m_tmp_local_generator),
+            m_benv(benv) {}
 
         virtual bool is_extra_opaque(name const & n) const {
             // TODO(Leo): class and instances
             return m_benv.m_not_reducible_pred(n) || m_benv.m_projection_info.contains(n);
         }
 
-        name mk_tmp_name() {
-            unsigned idx = m_next_local_idx;
-            m_next_local_idx++;
-            return name(*g_tmp_prefix, idx);
-        }
-
-        virtual expr mk_tmp_local(expr const & type, binder_info const & bi) {
-            name n = mk_tmp_name();
-            return blast::mk_local(n, n, type, bi);
-        }
-
-        virtual expr mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi) {
-            name n = mk_tmp_name();
-            return blast::mk_local(n, pp_n, type, bi);
-        }
-
-        virtual bool is_tmp_local(expr const & e) const {
-            if (!is_local(e))
-                return false;
-            name const & n = mlocal_name(e);
-            return !n.is_atomic() && n.get_prefix() == *g_tmp_prefix;
-        }
-
         virtual bool is_uvar(level const & l) const {
             return blast::is_uref(l);
         }
@@ -582,8 +559,8 @@ scope_debug::~scope_debug() {}
     and blast meta-variables are stored in the blast state */
 class tmp_tctx : public tmp_type_context {
 public:
-    tmp_tctx(environment const & env, io_state const & ios):
-        tmp_type_context(env, ios) {}
+    tmp_tctx(environment const & env, io_state const & ios, tmp_local_generator & gen):
+        tmp_type_context(env, ios, gen) {}
 
     /** \brief Return the type of a local constant (local or not).
         \remark This method allows the customer to store the type of local constants
@@ -618,7 +595,7 @@ public:
 tmp_type_context * blastenv::mk_tmp_type_context() {
     tmp_type_context * r;
     if (m_tmp_ctx_pool.empty()) {
-        r = new tmp_tctx(m_env, m_ios);
+        r = new tmp_tctx(m_env, m_ios, m_tmp_local_generator);
     } else {
         r = m_tmp_ctx_pool.back();
         m_tmp_ctx_pool.pop_back();

src/library/fun_info_manager.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <algorithm>
 #include "kernel/for_each_fn.h"
 #include "kernel/instantiate.h"
 #include "library/fun_info_manager.h"

src/library/init_module.cpp

@@ -45,7 +45,6 @@ Author: Leonardo de Moura
 #include "library/norm_num.h"
 #include "library/class_instance_resolution.h"
 #include "library/type_context.h"
-#include "library/tmp_type_context.h"
 
 namespace lean {
 void initialize_library_module() {
@@ -90,11 +89,9 @@ void initialize_library_module() {
     initialize_norm_num();
     initialize_class_instance_resolution();
     initialize_type_context();
-    initialize_tmp_type_context();
 }
 
 void finalize_library_module() {
-    finalize_tmp_type_context();
     finalize_type_context();
     finalize_class_instance_resolution();
     finalize_norm_num();

src/library/tmp_type_context.cpp

@@ -8,23 +8,28 @@ Author: Leonardo de Moura
 #include "library/idx_metavar.h"
 
 namespace lean {
-static name * g_prefix = nullptr;
-
-tmp_type_context::tmp_type_context(environment const & env, io_state const & ios, reducible_behavior b):
-    type_context(env, ios) {
+void tmp_type_context::init(environment const & env, reducible_behavior b) {
     switch (b) {
     case UnfoldReducible:      m_opaque_pred = mk_not_reducible_pred(env);      break;
     case UnfoldQuasireducible: m_opaque_pred = mk_not_quasireducible_pred(env); break;
     case UnfoldSemireducible:  m_opaque_pred = mk_irreducible_pred(env);        break;
     }
-    m_next_local_idx = 0;
+}
+
+tmp_type_context::tmp_type_context(environment const & env, io_state const & ios, reducible_behavior b):
+    type_context(env, ios) {
+    init(env, b);
+}
+
+tmp_type_context::tmp_type_context(environment const & env, io_state const & ios, tmp_local_generator & gen, reducible_behavior b):
+    type_context(env, ios, gen) {
+    init(env, b);
 }
 
 tmp_type_context::~tmp_type_context() {
 }
 
 void tmp_type_context::clear() {
-    m_next_local_idx = 0;
     m_uassignment.clear();
     m_eassignment.clear();
     m_trail.clear();
@@ -43,27 +48,6 @@ void tmp_type_context::set_next_mvar_idx(unsigned next_idx) {
     m_eassignment.resize(next_idx);
 }
 
-expr tmp_type_context::mk_tmp_local(expr const & type, binder_info const & bi) {
-    unsigned idx = m_next_local_idx;
-    m_next_local_idx++;
-    name n(*g_prefix, idx);
-    return lean::mk_local(n, n, type, bi);
-}
-
-expr tmp_type_context::mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi) {
-    unsigned idx = m_next_local_idx;
-    m_next_local_idx++;
-    name n(*g_prefix, idx);
-    return lean::mk_local(n, pp_n, type, bi);
-}
-
-bool tmp_type_context::is_tmp_local(expr const & e) const {
-    if (!is_local(e))
-        return false;
-    name const & n = mlocal_name(e);
-    return !n.is_atomic() && n.get_prefix() == *g_prefix;
-}
-
 bool tmp_type_context::is_uvar(level const & l) const {
     return is_idx_metauniv(l);
 }
@@ -129,7 +113,6 @@ expr tmp_type_context::mk_mvar(expr const & type) {
 void tmp_type_context::push() {
     m_scopes.push_back(scope());
     scope & s = m_scopes.back();
-    s.m_old_next_local_idx = m_next_local_idx;
     s.m_uassignment_sz     = m_uassignment.size();
     s.m_eassignment_sz     = m_eassignment.size();
     s.m_trail_sz           = m_trail.size();
@@ -138,7 +121,6 @@ void tmp_type_context::push() {
 void tmp_type_context::pop() {
     lean_assert(!m_scopes.empty());
     scope const & s  = m_scopes.back();
-    m_next_local_idx = s.m_old_next_local_idx;
     unsigned old_sz  = s.m_trail_sz;
     unsigned i = m_trail.size();
     while (i > old_sz) {
@@ -159,12 +141,4 @@ void tmp_type_context::commit() {
     lean_assert(!m_scopes.empty());
     m_scopes.pop_back();
 }
-
-void initialize_tmp_type_context() {
-    g_prefix = new name(name::mk_internal_unique_name());
-}
-
-void finalize_tmp_type_context() {
-    delete g_prefix;
-}
 }

src/library/tmp_type_context.h

@@ -29,7 +29,6 @@ namespace lean {
     \remark The local context is set using the method set_context from type_context.
 */
 class tmp_type_context : public type_context {
-    unsigned                          m_next_local_idx;
     name_predicate                    m_opaque_pred;
     std::vector<optional<level>>      m_uassignment;
     std::vector<optional<expr>>       m_eassignment;
@@ -42,8 +41,10 @@ class tmp_type_context : public type_context {
         unsigned m_trail_sz;
     };
     std::vector<scope>                m_scopes;
+    void init(environment const & env, reducible_behavior b);
 public:
     tmp_type_context(environment const & env, io_state const & ios, reducible_behavior b = UnfoldReducible);
+    tmp_type_context(environment const & env, io_state const & ios, tmp_local_generator & gen, reducible_behavior b = UnfoldReducible);
     virtual ~tmp_type_context();
 
     /** \brief Reset the state: backtracking stack, indices and assignment. */
@@ -62,9 +63,6 @@ public:
     void set_next_mvar_idx(unsigned next_idx);
 
     virtual bool is_extra_opaque(name const & n) const { return m_opaque_pred(n); }
-    virtual expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info());
-    virtual expr mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi = binder_info());
-    virtual bool is_tmp_local(expr const & e) const;
     virtual bool is_uvar(level const & l) const;
     virtual bool is_mvar(expr const & e) const;
     virtual optional<level> get_assignment(level const & u) const;
@@ -92,7 +90,4 @@ public:
         return static_cast<bool>(m_eassignment[idx]);
     }
 };
-
-void initialize_tmp_type_context();
-void finalize_tmp_type_context();
 }

src/library/type_context.cpp

@@ -51,6 +51,32 @@ bool get_class_trans_instances(options const & o) {
     return o.get_bool(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES);
 }
 
+tmp_local_generator::tmp_local_generator():
+    m_next_local_idx(0) {}
+
+name tmp_local_generator::mk_fresh_name() {
+    unsigned idx = m_next_local_idx;
+    m_next_local_idx++;
+    return name(*g_prefix, idx);
+}
+
+expr tmp_local_generator::mk_tmp_local(expr const & type, binder_info const & bi) {
+    name n = mk_fresh_name();
+    return lean::mk_local(n, n, type, bi);
+}
+
+expr tmp_local_generator::mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi) {
+    name n = mk_fresh_name();
+    return lean::mk_local(n, pp_n, type, bi);
+}
+
+bool tmp_local_generator::is_tmp_local(expr const & e) const {
+    if (!is_local(e))
+        return false;
+    name const & n = mlocal_name(e);
+    return !n.is_atomic() && n.get_prefix() == *g_prefix;
+}
+
 struct type_context::ext_ctx : public extension_context {
     type_context & m_owner;
 
@@ -79,11 +105,14 @@ struct type_context::ext_ctx : public extension_context {
     }
 };
 
-type_context::type_context(environment const & env, io_state const & ios, bool multiple_instances):
+type_context::type_context(environment const & env, io_state const & ios, tmp_local_generator * gen,
+                           bool gen_owner, bool multiple_instances):
     m_env(env),
     m_ios(ios),
     m_ngen(*g_prefix),
     m_ext_ctx(new ext_ctx(*this)),
+    m_local_gen(gen),
+    m_local_gen_owner(gen_owner),
     m_proj_info(get_projection_info_map(env)) {
     m_pip                   = nullptr;
     m_ci_multiple_instances = multiple_instances;
@@ -97,6 +126,8 @@ type_context::type_context(environment const & env, io_state const & ios, bool m
 }
 
 type_context::~type_context() {
+    if (m_local_gen_owner)
+        delete m_local_gen;
 }
 
 void type_context::set_local_instances(list<expr> const & insts) {
@@ -1678,7 +1709,6 @@ default_type_context::default_type_context(environment const & env, io_state con
     type_context(env, ios, multiple_instances),
     m_not_reducible_pred(mk_not_reducible_pred(env)) {
     m_ignore_if_zero = false;
-    m_next_local_idx = 0;
     m_next_uvar_idx  = 0;
     m_next_mvar_idx  = 0;
     set_local_instances(insts);
@@ -1686,27 +1716,6 @@ default_type_context::default_type_context(environment const & env, io_state con
 
 default_type_context::~default_type_context() {}
 
-expr default_type_context::mk_tmp_local(expr const & type, binder_info const & bi) {
-    unsigned idx = m_next_local_idx;
-    m_next_local_idx++;
-    name n(*g_prefix, idx);
-    return lean::mk_local(n, n, type, bi);
-}
-
-expr default_type_context::mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi) {
-    unsigned idx = m_next_local_idx;
-    m_next_local_idx++;
-    name n(*g_prefix, idx);
-    return lean::mk_local(n, pp_n, type, bi);
-}
-
-bool default_type_context::is_tmp_local(expr const & e) const {
-    if (!is_local(e))
-        return false;
-    name const & n = mlocal_name(e);
-    return !n.is_atomic() && n.get_prefix() == *g_prefix;
-}
-
 bool default_type_context::is_uvar(level const & l) const {
     if (!is_meta(l))
         return false;

src/library/type_context.h

@@ -17,6 +17,23 @@ bool get_class_trace_instances(options const & o);
 unsigned get_class_instance_max_depth(options const & o);
 bool get_class_trans_instances(options const & o);
 
+class tmp_local_generator {
+    unsigned m_next_local_idx;
+    name mk_fresh_name();
+public:
+    tmp_local_generator();
+
+    /** \brief Create a temporary local constant */
+    virtual expr mk_tmp_local(expr const & type, binder_info const & bi);
+
+    /** \brief Create a temporary local constant using the given pretty print name.
+        The pretty printing name has not semantic significance. */
+    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi);
+
+    /** \brief Return true if \c e was created using \c mk_tmp_local */
+    virtual bool is_tmp_local(expr const & e) const;
+};
+
 /** \brief Light-weight type inference, normalization and definitional equality.
     It is simpler and more efficient version of the kernel type checker.
     It does not generate unification constraints.
@@ -104,6 +121,8 @@ class type_context {
     io_state                        m_ios;
     name_generator                  m_ngen;
     std::unique_ptr<ext_ctx>        m_ext_ctx;
+    tmp_local_generator *           m_local_gen;
+    bool                            m_local_gen_owner;
     // postponed universe constraints
     std::vector<pair<level, level>> m_postponed;
     name_map<projection_info>       m_proj_info;
@@ -274,8 +293,14 @@ class type_context {
     optional<expr> mk_class_instance_core(expr const & type);
     optional<expr> check_ci_cache(expr const & type) const;
     void cache_ci_result(expr const & type, expr const & inst);
+    type_context(environment const & env, io_state const & ios, tmp_local_generator * gen,
+                 bool gen_owner, bool multiple_instances);
 public:
-    type_context(environment const & env, io_state const & ios, bool multiple_instances = false);
+    type_context(environment const & env, io_state const & ios, bool multiple_instances = false):
+        type_context(env, ios, new tmp_local_generator(), true, multiple_instances) {}
+    type_context(environment const & env, io_state const & ios, tmp_local_generator & gen,
+                 bool multiple_instances = false):
+        type_context(env, ios, &gen, false, multiple_instances) {}
     virtual ~type_context();
 
     void set_local_instances(list<expr> const & insts);
@@ -289,11 +314,15 @@ public:
     virtual bool is_extra_opaque(name const & n) const = 0;
 
     /** \brief Create a temporary local constant */
-    virtual expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()) = 0;
+    expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()) {
+        return m_local_gen->mk_tmp_local(type, bi);
+    }
 
     /** \brief Create a temporary local constant using the given pretty print name.
         The pretty printing name has not semantic significance. */
-    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) = 0;
+    expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) {
+        return m_local_gen->mk_tmp_local(pp_name, type, bi);
+    }
 
     /** \brief Create a temporary local constant based on the domain of the given binding (lambda/Pi) expression */
     expr mk_tmp_local_from_binding(expr const & b) {
@@ -301,7 +330,9 @@ public:
     }
 
     /** \brief Return true if \c e was created using \c mk_tmp_local */
-    virtual bool is_tmp_local(expr const & e) const = 0;
+    bool is_tmp_local(expr const & e) const {
+        return m_local_gen->is_tmp_local(e);
+    }
 
     /** \brief Return true if \c l represents a universe unification variable.
         \remark This is supposed to be a subset of is_meta(l).
@@ -467,7 +498,6 @@ class default_type_context : public type_context {
     };
     assignment                m_assignment;
     std::vector<assignment>   m_trail;
-    unsigned                  m_next_local_idx;
     unsigned                  m_next_uvar_idx;
     unsigned                  m_next_mvar_idx;
 
@@ -499,9 +529,6 @@ public:
     virtual ~default_type_context();
     virtual bool is_extra_opaque(name const & n) const { return m_not_reducible_pred(n); }
     virtual bool ignore_universe_def_eq(level const & l1, level const & l2) const;
-    virtual expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info());
-    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info());
-    virtual bool is_tmp_local(expr const & e) const;
     virtual bool is_uvar(level const & l) const;
     virtual bool is_mvar(expr const & e) const;
     virtual optional<level> get_assignment(level const & u) const;