From e63c1d3347747d98cc953d6896ec3b2eb79e2316 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 27 Mar 2017 14:19:40 +0200 Subject: [PATCH] refactor(frontends/lean/info_manager): use pos_info --- src/frontends/lean/elaborator.cpp | 10 ++++---- src/frontends/lean/info_manager.cpp | 37 ++++++++++++++++------------- src/frontends/lean/info_manager.h | 14 ++++++----- src/frontends/lean/interactive.cpp | 6 ++--- src/frontends/lean/parser.cpp | 3 +-- src/frontends/lean/print_cmd.cpp | 3 +-- 6 files changed, 38 insertions(+), 35 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index dac950ccb7..d7a4322e18 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -914,8 +914,8 @@ expr elaborator::visit_const_core(expr const & e) { void elaborator::save_identifier_info(expr const & f) { if (!m_no_info && m_uses_infom && get_pos_info_provider() && (is_constant(f) || is_local(f))) { if (auto p = get_pos_info_provider()->get_pos_info(f)) { - m_info.add_identifier_info(p->first, p->second, is_constant(f) ? const_name(f) : local_pp_name(f)); - m_info.add_type_info(p->first, p->second, infer_type(f)); + m_info.add_identifier_info(*p, is_constant(f) ? const_name(f) : local_pp_name(f)); + m_info.add_type_info(*p, infer_type(f)); } } } @@ -3756,11 +3756,11 @@ static vm_obj tactic_save_type_info(vm_obj const & _e, vm_obj const & ref, vm_ob type_context ctx = mk_type_context_for(s); try { expr type = ctx.infer(e); - get_global_info_manager()->add_type_info(pos->first, pos->second, type); + get_global_info_manager()->add_type_info(*pos, type); if (is_constant(e)) - get_global_info_manager()->add_identifier_info(pos->first, pos->second, const_name(e)); + get_global_info_manager()->add_identifier_info(*pos, const_name(e)); else if (is_local(e)) - get_global_info_manager()->add_identifier_info(pos->first, pos->second, local_pp_name(e)); + get_global_info_manager()->add_identifier_info(*pos, local_pp_name(e)); } catch (exception & ex) { return tactic::mk_exception(ex, s); } diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index bd7b821395..4712f04c33 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -76,13 +76,13 @@ info_data mk_type_info(expr const & e) { return info_data(new type_info_data(e)) info_data mk_identifier_info(name const & full_id) { return info_data(new identifier_info_data(full_id)); } info_data mk_vm_obj_format_info(environment const & env, vm_obj const & thunk) { return info_data(new vm_obj_format_info(env, thunk)); } -void info_manager::add_info(unsigned l, unsigned c, info_data data) { +void info_manager::add_info(pos_info pos, info_data data) { #ifdef LEAN_NO_INFO return; #endif - line_info_data_set line_set = m_line_data[l]; - line_set.insert(c, cons(data, line_set[c])); - m_line_data.insert(l, line_set); + line_info_data_set line_set = m_line_data[pos.first]; + line_set.insert(pos.second, cons(data, line_set[pos.second])); + m_line_data.insert(pos.first, line_set); } line_info_data_set info_manager::get_line_info_set(unsigned l) const { @@ -111,40 +111,45 @@ void info_manager::merge(info_manager const & info) { unsigned i = b.size(); while (i > 0) { --i; - add_info(line, col, b[i]); + add_info({line, col}, b[i]); } }); }); } -void info_manager::add_type_info(unsigned l, unsigned c, expr const & e) { +void info_manager::add_type_info(pos_info pos, expr const & e) { #ifdef LEAN_NO_INFO return; #endif - add_info(l, c, mk_type_info(e)); + add_info(pos, mk_type_info(e)); } -void info_manager::add_identifier_info(unsigned l, unsigned c, name const & full_id) { +void info_manager::add_identifier_info(pos_info pos, name const & full_id) { #ifdef LEAN_NO_INFO return; #endif - add_info(l, c, mk_identifier_info(full_id)); + add_info(pos, mk_identifier_info(full_id)); } -void info_manager::add_vm_obj_format_info(unsigned l, unsigned c, environment const & env, vm_obj const & thunk) { +void info_manager::add_const_info(environment const & env, pos_info pos, name const & full_id) { + add_identifier_info(pos, full_id); + add_type_info(pos, env.get(full_id).get_type()); +} + +void info_manager::add_vm_obj_format_info(pos_info pos, environment const & env, vm_obj const & thunk) { #ifdef LEAN_NO_INFO return; #endif - add_info(l, c, mk_vm_obj_format_info(env, thunk)); + add_info(pos, mk_vm_obj_format_info(env, thunk)); } #ifdef LEAN_JSON -void info_manager::get_info_record(environment const & env, options const & o, io_state const & ios, unsigned line, - unsigned col, json & record, std::function pred) const { +void info_manager::get_info_record(environment const & env, options const & o, io_state const & ios, pos_info pos, + json & record, std::function pred) const { type_context tc(env, o); io_state_stream out = regular(env, ios, tc).update_options(o); - get_line_info_set(line).for_each([&](unsigned c, list const & ds) { - if (c == col) { + get_line_info_set(pos.first).for_each([&](unsigned c, list const & ds) { + if (c == pos.second) { for (auto const & d : ds) { if (!pred || pred(d)) d.report(out, record); @@ -170,7 +175,7 @@ vm_obj tactic_save_info_thunk(vm_obj const & pos, vm_obj const & thunk, vm_obj c try { if (g_info_m) { auto _pos = to_pos_info(pos); - g_info_m->add_vm_obj_format_info(_pos.first, _pos.second, tactic::to_state(s).env(), thunk); + g_info_m->add_vm_obj_format_info(_pos, tactic::to_state(s).env(), thunk); } return tactic::mk_success(tactic::to_state(s)); } catch (exception & ex) { diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index b527d3c95a..c2192a12b2 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -73,8 +73,8 @@ class info_manager : public log_entry_cell { std::string m_file_name; rb_map m_line_data; - void add_info(unsigned l, unsigned c, info_data data); line_info_data_set get_line_info_set(unsigned l) const; + void add_info(pos_info pos, info_data data); public: info_manager() {} info_manager(std::string const & file_name) : m_file_name(file_name) {} @@ -83,16 +83,18 @@ public: bool empty() const { return m_line_data.empty(); } - void add_type_info(unsigned l, unsigned c, expr const & e); - void add_identifier_info(unsigned l, unsigned c, name const & full_id); - void add_vm_obj_format_info(unsigned l, unsigned c, environment const & env, vm_obj const & thunk); + void add_type_info(pos_info pos, expr const & e); + void add_identifier_info(pos_info pos, name const & full_id); + /* Takes type info from global declaration with the given name. */ + void add_const_info(environment const & env, pos_info pos, name const & full_id); + void add_vm_obj_format_info(pos_info pos, environment const & env, vm_obj const & thunk); void instantiate_mvars(metavar_context const & mctx); void merge(info_manager const & info); #ifdef LEAN_JSON - void get_info_record(environment const & env, options const & o, io_state const & ios, unsigned line, - unsigned col, json & record, std::function pred = {}) const; + void get_info_record(environment const & env, options const & o, io_state const & ios, pos_info pos, + json & record, std::function pred = {}) const; #endif }; diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index 30ada1b550..da90d21529 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -137,14 +137,12 @@ void report_info(environment const & env, options const & opts, io_state const & for (auto & infom : info_managers) { if (infom.get_file_name() == m_mod_info.m_mod) { if (e.m_goal_pos) { - infom.get_info_record(env, opts, ios, e.m_goal_pos->first, - e.m_goal_pos->second, record, [](info_data const & d) { + infom.get_info_record(env, opts, ios, *e.m_goal_pos, record, [](info_data const & d) { return dynamic_cast(d.raw()); }); } if (!has_token_info) - infom.get_info_record(env, opts, ios, e.m_token_info.m_pos.first, - e.m_token_info.m_pos.second, record); + infom.get_info_record(env, opts, ios, e.m_token_info.m_pos, record); } } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 233920b641..0fba8b5665 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1863,8 +1863,7 @@ expr parser::parse_id() { name id = check_id_next("", break_at_pos_exception::token_context::expr); expr e = id_to_expr(id, p); if (is_constant(e) && get_global_info_manager()) { - get_global_info_manager()->add_identifier_info(p.first, p.second, const_name(e)); - get_global_info_manager()->add_type_info(p.first, p.second, m_env.get(const_name(e)).get_type()); + get_global_info_manager()->add_const_info(m_env, p, const_name(e)); } return e; } diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index 3f7272d4ca..9cca6b3fd6 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -392,8 +392,7 @@ bool print_id_info(parser & p, message_builder & out, name const & id, bool show if (auto c = head_opt(cs)) if (!tail(cs)) if (auto infom = get_global_info_manager()) { - infom->add_identifier_info(pos.first, pos.second, *c); - infom->add_type_info(pos.first, pos.second, p.env().get(*c).get_type()); + infom->add_const_info(p.env(), pos, *c); } if (found) return true;