max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(frontends/lean/info_manager): use pos_info

Browse source
This commit is contained in:
Sebastian Ullrich 2017-03-27 14:19:40 +02:00 • committed by Leonardo de Moura
parent 8c1136c1b6
commit e63c1d3347
6 changed files with 38 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/frontends/lean/elaborator.cpp
View file

@ -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);
}

37
src/frontends/lean/info_manager.cpp
View file

@ -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<info_data>(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<info_data>(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<bool (info_data const &)> 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<bool (info_data const &)> 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<info_data> const & ds) {
if (c == col) {
get_line_info_set(pos.first).for_each([&](unsigned c, list<info_data> 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) {

14
src/frontends/lean/info_manager.h
View file

@ -73,8 +73,8 @@ class info_manager : public log_entry_cell {
std::string m_file_name;
rb_map<unsigned, line_info_data_set, unsigned_cmp> 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<bool (info_data const &)> pred = {}) const;
void get_info_record(environment const & env, options const & o, io_state const & ios, pos_info pos,
json & record, std::function<bool (info_data const &)> pred = {}) const;
#endif
};

6
src/frontends/lean/interactive.cpp
View file

@ -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<vm_obj_format_info const *>(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);
}
}

3
src/frontends/lean/parser.cpp
View file

@ -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;
}

3
src/frontends/lean/print_cmd.cpp
View file

@ -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;