From c1653a9fb42c0f6f28b68e13aed28b6d667a58ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Oct 2014 17:28:35 -0700 Subject: [PATCH] feat(frontends/lean): only valid proof states should be displayed, closes #275 --- src/frontends/lean/decl_cmds.cpp | 1 + src/frontends/lean/info_manager.cpp | 28 ++++++++++++++++++++++++++++ src/frontends/lean/info_manager.h | 3 +++ src/frontends/lean/parser.cpp | 5 +++++ src/frontends/lean/parser.h | 1 + 5 files changed, 38 insertions(+) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 58b4a7bed..1764c5760 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -442,6 +442,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo } if (!found_cached) { + p.remove_proof_state_info(n_pos, p.pos()); if (is_theorem) { auto type_pos = p.pos_of(type); bool clear_pre_info = false; // we don't want to clear pre_info data until we process the proof. diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 15cacf38d..dc84df73a 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -69,6 +69,7 @@ public: bool is_cheap() const { return m_ptr->is_cheap(); } void display(io_state_stream const & ios, unsigned line) const { m_ptr->display(ios, line); } info_data_cell const * raw() const { return m_ptr; } + info_kind kind() const { return m_ptr->kind(); } }; struct tmp_info_data : public info_data_cell { @@ -444,6 +445,30 @@ struct info_manager::imp { m_line_data[l].insert(mk_proof_state_info(c, ps)); } + void remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col) { + lock_guard lc(m_mutex); + if (m_block_new_info || m_line_data.empty()) + return; + if (end_line >= m_line_data.size()) + end_line = m_line_data.size() - 1; + for (unsigned i = start_line; i <= end_line; i++) { + info_data_set const & curr_set = m_line_data[i]; + if (curr_set.find_if([](info_data const & info) { return info.kind() == info_kind::ProofState; })) { + info_data_set new_curr_set; + curr_set.for_each([&](info_data const & info) { + if (info.kind() == info_kind::ProofState) { + if ((i == start_line && info.get_column() < start_col) || + (i == end_line && info.get_column() >= end_col)) + new_curr_set.insert(info); + } else { + new_curr_set.insert(info); + } + }); + m_line_data[i] = new_curr_set; + } + } + } + static info_data_set instantiate(info_data_set const & s, substitution & subst) { info_data_set r; s.for_each([&](info_data const & d) { @@ -724,4 +749,7 @@ optional info_manager::get_type_at(unsigned line, unsigned col) const { re optional info_manager::get_meta_at(unsigned line, unsigned col) const { return m_ptr->get_meta_at(line, col); } void info_manager::block_new_info() { m_ptr->block_new_info(true); } void info_manager::start_from(unsigned l) { m_ptr->start_from(l); } +void info_manager::remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col) { + m_ptr->remove_proof_state_info(start_line, start_col, end_line, end_col); +} } diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index 9218cfef9..fb50db2bb 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -30,6 +30,9 @@ public: void add_identifier_info(unsigned l, unsigned c, name const & full_id); void add_proof_state_info(unsigned l, unsigned c, proof_state const & e); + /** \brief Remove PROO_STATE info from [(start_line, start_line), (end_line, end_col)) */ + void remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col); + void instantiate(substitution const & s); void merge(info_manager const & m, bool overwrite); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 6c8ce0331..d4d02ed59 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -164,6 +164,11 @@ bool parser::are_info_lines_valid(unsigned start_line, unsigned end_line) const return true; } +void parser::remove_proof_state_info(pos_info const & start, pos_info const & end) { + if (m_info_manager) + m_info_manager->remove_proof_state_info(start.first, start.second, end.first, end.second); +} + expr parser::mk_sorry(pos_info const & p) { m_used_sorry = true; { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 937f51ec5..2b02f8f75 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -226,6 +226,7 @@ public: bool are_info_lines_valid(unsigned start_line, unsigned end_line) const; bool collecting_info() const { return m_info_manager; } + void remove_proof_state_info(pos_info const & start, pos_info const & end); void set_index(declaration_index * i) { m_index = i; } void add_decl_index(name const & n, pos_info const & pos, name const & k, expr const & t);