chore(frontends/lean, library): cleanup anonymous instance management

src/frontends/lean/decl_util.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
 #include "library/locals.h"
+#include "library/class.h"
 #include "library/trace.h"
 #include "library/placeholder.h"
 #include "library/protected.h"
@@ -159,7 +160,7 @@ void collect_annonymous_inst_implicit(parser const & p, collected_locals & local
         auto const & entry = entries[i];
         if (is_local(entry.second) && !locals.contains(entry.second) && local_info(entry.second).is_inst_implicit() &&
             // remark: remove the following condition condition, if we want to auto inclusion also for non anonymous ones.
-            p.is_anonymous_inst_name(entry.first)) {
+            is_anonymous_inst_name(entry.first)) {
             bool ok = true;
             for_each(mlocal_type(entry.second), [&](expr const & e, unsigned) {
                     if (!ok) return false; // stop

src/frontends/lean/parser.cpp

@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/module_mgr.h"
 #include "library/export_decl.h"
 #include "library/trace.h"
+#include "library/class.h"
 #include "library/exception.h"
 #include "library/aliases.h"
 #include "library/constants.h"
@@ -87,8 +88,6 @@ bool get_parser_show_errors(options const & opts) {
 
 // ==========================================
 
-static name * g_anonymous_inst_name_prefix = nullptr;
-
 parser::local_scope::local_scope(parser & p, bool save_options):
     m_p(p), m_env(p.env()) {
     m_p.push_local_scope(save_options);
@@ -306,19 +305,11 @@ tag parser::get_tag(expr e) {
 }
 
 name parser::mk_anonymous_inst_name() {
-    name n = g_anonymous_inst_name_prefix->append_after(m_next_inst_idx);
+    name n = ::lean::mk_anonymous_inst_name(m_next_inst_idx);
     m_next_inst_idx++;
     return n;
 }
 
-bool parser::is_anonymous_inst_name(name const & n) const {
-    return
-        n.is_atomic() &&
-        n.is_string() &&
-        strlen(n.get_string()) >= strlen(g_anonymous_inst_name_prefix->get_string()) &&
-        memcmp(n.get_string(), g_anonymous_inst_name_prefix->get_string(), strlen(g_anonymous_inst_name_prefix->get_string())) == 0;
-}
-
 expr parser::save_pos(expr e, pos_info p) {
     auto t = get_tag(e);
     if (!m_pos_table.contains(t))
@@ -2347,7 +2338,6 @@ void initialize_parser() {
     register_bool_option(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT,
                          "(lean parser) import modules in parallel");
     g_tmp_prefix = new name(name::mk_internal_unique_name());
-    g_anonymous_inst_name_prefix = new name("_inst");
     g_documentable_cmds = new name_set();
 
     g_documentable_cmds->insert("definition");
@@ -2365,7 +2355,6 @@ void initialize_parser() {
 }
 
 void finalize_parser() {
-    delete g_anonymous_inst_name_prefix;
     delete g_tmp_prefix;
     delete g_parser_show_errors;
     delete g_parser_parallel_import;

src/frontends/lean/parser.h

@@ -255,7 +255,6 @@ public:
     bool found_errors() const { return m_found_errors; }
 
     name mk_anonymous_inst_name();
-    bool is_anonymous_inst_name(name const & n) const;
 
     unsigned curr_lbp() const;
 

src/library/class.cpp

@@ -247,6 +247,23 @@ unsigned get_instance_fingerprint(environment const & env) {
     return get_attribute_fingerprint(env, get_instance_attr_name());
 }
 
+static name * g_anonymous_inst_name_prefix = nullptr;
+
+name const & get_anonymous_instance_prefix() {
+    return *g_anonymous_inst_name_prefix;
+}
+
+name mk_anonymous_inst_name(unsigned idx) {
+    return g_anonymous_inst_name_prefix->append_after(idx);
+}
+
+bool is_anonymous_inst_name(name const & n) {
+    if (!n.is_atomic() || !n.is_string()) return false;
+    return strncmp(n.get_string(),
+                   g_anonymous_inst_name_prefix->get_string(),
+                   strlen(g_anonymous_inst_name_prefix->get_string())) == 0;
+}
+
 void initialize_class() {
     g_class_attr_name = new name("class");
     g_instance_attr_name = new name("instance");
@@ -264,6 +281,8 @@ void initialize_class() {
                                                  unsigned prio, bool persistent) {
                                                   return add_instance_core(env, d, prio, persistent);
                                               }));
+
+    g_anonymous_inst_name_prefix = new name("_inst");
 }
 
 void finalize_class() {
@@ -271,5 +290,6 @@ void finalize_class() {
     delete g_class_name;
     delete g_class_attr_name;
     delete g_instance_attr_name;
+    delete g_anonymous_inst_name_prefix;
 }
 }

src/library/class.h

@@ -29,6 +29,10 @@ name get_class_name(environment const & env, expr const & e);
 name const & get_instance_attr_name();
 unsigned get_instance_fingerprint(environment const & env);
 
+name const & get_anonymous_instance_prefix();
+name mk_anonymous_inst_name(unsigned idx);
+bool is_anonymous_inst_name(name const & n);
+
 void initialize_class();
 void finalize_class();
 }

src/library/print.cpp

@@ -41,24 +41,19 @@ name pick_unused_name(expr const & t, name const & s) {
     return r;
 }
 
-static name * g_x        = nullptr;
-static name * g_internal = nullptr;
+static name * g_M   = nullptr;
 
 void initialize_print() {
-    g_internal = new name("M");
-    g_x        = new name("x");
+    g_M = new name("M");
 }
 
 void finalize_print() {
-    delete g_x;
-    delete g_internal;
+    delete g_M;
 }
 
 pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
     lean_assert(is_binding(b));
     name n = binding_name(b);
-    if (is_internal_name(n))
-        n = *g_x;
     n = pick_unused_name(binding_body(b), n);
     expr c = mk_local(n, preserve_type ? binding_domain(b) : expr(), binding_info(b));
     return mk_pair(instantiate(binding_body(b), c), c);
@@ -67,21 +62,19 @@ pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type) {
 pair<expr, expr> let_body_fresh(expr const & b, bool preserve_type) {
     lean_assert(is_let(b));
     name n = let_name(b);
-    if (is_internal_name(n))
-        n = *g_x;
     n = pick_unused_name(let_body(b), n);
     expr c = mk_local(n, preserve_type ? let_type(b) : expr());
     return mk_pair(instantiate(let_body(b), c), c);
 }
 
-name fix_internal_name(name const & a) {
+name fix_name(name const & a) {
     if (a.is_atomic()) {
         if (a.is_numeral())
-            return *g_internal;
+            return *g_M;
         else
             return a;
     } else {
-        name p = fix_internal_name(a.get_prefix());
+        name p = fix_name(a.get_prefix());
         if (p == a.get_prefix())
             return a;
         else if (a.is_numeral())
@@ -206,10 +199,10 @@ struct print_expr_fn {
     void print(expr const & a) {
         switch (a.kind()) {
         case expr_kind::Meta:
-            out() << "?" << fix_internal_name(mlocal_name(a));
+            out() << "?" << fix_name(mlocal_name(a));
             break;
         case expr_kind::Local:
-            out() << fix_internal_name(local_pp_name(a));
+            out() << fix_name(local_pp_name(a));
             break;
         case expr_kind::Var:
             out() << "#" << var_idx(a);