From 93c8e693136e9ba5effd9367587174c2dce81056 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Jan 2017 14:32:10 -0800 Subject: [PATCH] chore(frontends/lean, library): cleanup anonymous instance management --- src/frontends/lean/decl_util.cpp | 3 ++- src/frontends/lean/parser.cpp | 15 ++------------- src/frontends/lean/parser.h | 1 - src/library/class.cpp | 20 ++++++++++++++++++++ src/library/class.h | 4 ++++ src/library/print.cpp | 23 ++++++++--------------- 6 files changed, 36 insertions(+), 30 deletions(-) diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 571a7dcdfa..896fd5906b 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/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 diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index df31a14a39..589af1f8b7 100644 --- a/src/frontends/lean/parser.cpp +++ b/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; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 5cb223edcd..a78664a29b 100644 --- a/src/frontends/lean/parser.h +++ b/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; diff --git a/src/library/class.cpp b/src/library/class.cpp index d6a1dc3208..5a067a1140 100644 --- a/src/library/class.cpp +++ b/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; } } diff --git a/src/library/class.h b/src/library/class.h index d99caeac31..ea15871ea7 100644 --- a/src/library/class.h +++ b/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(); } diff --git a/src/library/print.cpp b/src/library/print.cpp index 6ba521c8c6..5abf92b6a8 100644 --- a/src/library/print.cpp +++ b/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 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 binding_body_fresh(expr const & b, bool preserve_type) { pair 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);