From af2c3b181541fe0baff91bb6fd041fa7c3f712d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Sep 2014 10:25:07 -0700 Subject: [PATCH] fix(frontends/lean/info_manager): bug in save_environment_options, server was displaying old results --- src/frontends/lean/info_manager.cpp | 17 +++++--- src/frontends/lean/info_manager.h | 10 ++++- src/frontends/lean/server.cpp | 8 ++-- tests/lean/interactive/num2.input | 16 ++++++++ .../lean/interactive/num2.input.expected.out | 38 ++++++++++++++++++ tests/lean/interactive/num2.lean | 40 +++++++++++++++++++ 6 files changed, 118 insertions(+), 11 deletions(-) create mode 100644 tests/lean/interactive/num2.input create mode 100644 tests/lean/interactive/num2.input.expected.out create mode 100644 tests/lean/interactive/num2.lean diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index d881d92230..a847fb9152 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -307,12 +307,13 @@ struct info_manager::imp { auto it = m_env_info.begin(); auto end = m_env_info.end(); while (it != end) { - if (it->m_line > l) + if (it->m_line > l) { break; - else if (it->m_line <= l && it->m_iteration < m_iteration) - it = m_env_info.erase(it); - else + } else if (it->m_line <= l && it->m_iteration < m_iteration) { + m_env_info.erase(it++); + } else { ++it; + } } m_env_info.insert(env_info(l, m_iteration, env, o)); } @@ -647,7 +648,11 @@ void info_manager::display(environment const & env, io_state const & ios, unsign unsigned info_manager::get_processed_upto() const { return m_ptr->m_processed_upto; } optional info_manager::get_type_at(unsigned line, unsigned col) const { return m_ptr->get_type_at(line, col); } 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(bool f) { - m_ptr->block_new_info(f); +void info_manager::block_new_info() { + m_ptr->block_new_info(true); +} +void info_manager::start() { + m_ptr->m_iteration++; + m_ptr->block_new_info(false); } } diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index 6c5c7bb864..fa39da8779 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -46,7 +46,15 @@ public: void clear(); void display(environment const & env, io_state const & ios, unsigned line, optional const & col = optional()) const; - void block_new_info(bool f); + /** \brief Block new information from being inserted into this info_manager. + \remark #start_iteration unblocks it. + */ + void block_new_info(); + /** \breif Mark the start of a new information collection cycle. + It also enables new information to be added, i.e., it will undo + the effect of #block_new_info. + */ + void start(); unsigned get_processed_upto() const; }; } diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 4a1065931a..338498536e 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -53,7 +53,7 @@ void server::file::replace_line(unsigned line_num, std::string const & new_line) while (i < old_line.size() && i < new_line.size() && old_line[i] == new_line[i]) i++; #endif - m_info.block_new_info(true); + m_info.block_new_info(); #if 0 // It turns out that is not a good idea to try to "keep" some of the information. // The info_manager will accumulate conflicting information and confuse the frontend. @@ -67,7 +67,7 @@ void server::file::replace_line(unsigned line_num, std::string const & new_line) void server::file::insert_line(unsigned line_num, std::string const & new_line) { lock_guard lk(m_lines_mutex); - m_info.block_new_info(true); + m_info.block_new_info(); m_info.insert_line(line_num+1); while (line_num >= m_lines.size()) m_lines.push_back(""); @@ -83,7 +83,7 @@ void server::file::insert_line(unsigned line_num, std::string const & new_line) void server::file::remove_line(unsigned line_num) { lock_guard lk(m_lines_mutex); - m_info.block_new_info(true); + m_info.block_new_info(); m_info.remove_line(line_num+1); if (line_num >= m_lines.size()) return; @@ -181,7 +181,7 @@ server::worker::worker(environment const & env, io_state const & ios, definition todo_file->m_snapshots.resize(i); s = i == 0 ? m_empty_snapshot : todo_file->m_snapshots[i-1]; lean_assert(s.m_line > 0); - todo_file->m_info.block_new_info(false); + todo_file->m_info.start(); todo_file->m_info.set_processed_upto(s.m_line); num_lines = todo_file->copy_to(block, s.m_line - 1); } diff --git a/tests/lean/interactive/num2.input b/tests/lean/interactive/num2.input new file mode 100644 index 0000000000..b6f69685eb --- /dev/null +++ b/tests/lean/interactive/num2.input @@ -0,0 +1,16 @@ +VISIT num2.lean +WAIT +SET +pp.notation false +FINDP 39 +pos_num.si +REPLACE 23 + definition size (a : pos_num) : pos_num := +WAIT +REPLACE 39 + rec (pos pos_num.one) (λp, pos (pos_num.size p)) a +WAIT +FINDP 39 +pos_num.si +FINDP 26 +pos_num.si diff --git a/tests/lean/interactive/num2.input.expected.out b/tests/lean/interactive/num2.input.expected.out new file mode 100644 index 0000000000..79bf0b8aab --- /dev/null +++ b/tests/lean/interactive/num2.input.expected.out @@ -0,0 +1,38 @@ +-- BEGINWAIT +-- ENDWAIT +-- BEGINSET +-- ENDSET +-- BEGINFINDP +pos_num.bit0|pos_num → pos_num +pos_num.is_inhabited|inhabited pos_num +pos_num.inc|pos_num → pos_num +pos_num.bit1|pos_num → pos_num +pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n) +pos_num.one|pos_num +pos_num.num_bits|pos_num → pos_num +pos_num|Type +-- ENDFINDP +-- BEGINWAIT +-- ENDWAIT +-- BEGINWAIT +-- ENDWAIT +-- BEGINFINDP +pos_num.size|pos_num → pos_num +pos_num.bit0|pos_num → pos_num +pos_num.is_inhabited|inhabited pos_num +pos_num.inc|pos_num → pos_num +pos_num.bit1|pos_num → pos_num +pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n) +pos_num.one|pos_num +pos_num|Type +-- ENDFINDP +-- BEGINFINDP +pos_num.size|pos_num → pos_num +pos_num.bit0|pos_num → pos_num +pos_num.is_inhabited|inhabited pos_num +pos_num.inc|pos_num → pos_num +pos_num.bit1|pos_num → pos_num +pos_num.rec|?C pos_num.one → (Π (a : pos_num), ?C a → ?C (pos_num.bit1 a)) → (Π (a : pos_num), ?C a → ?C (pos_num.bit0 a)) → (Π (n : pos_num), ?C n) +pos_num.one|pos_num +pos_num|Type +-- ENDFINDP diff --git a/tests/lean/interactive/num2.lean b/tests/lean/interactive/num2.lean new file mode 100644 index 0000000000..5a3b2b242f --- /dev/null +++ b/tests/lean/interactive/num2.lean @@ -0,0 +1,40 @@ +---------------------------------------------------------------------------------------------------- +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura +---------------------------------------------------------------------------------------------------- +import logic.classes.inhabited + +-- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. +-- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))). +-- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc). +inductive pos_num : Type := +one : pos_num, +bit1 : pos_num → pos_num, +bit0 : pos_num → pos_num + +theorem pos_num.is_inhabited [instance] : inhabited pos_num := +inhabited.mk pos_num.one + +namespace pos_num + definition inc (a : pos_num) : pos_num := + rec (bit0 one) (λn r, bit0 r) (λn r, bit1 n) a + + definition num_bits (a : pos_num) : pos_num := + rec one (λn r, inc r) (λn r, inc r) a +end pos_num + +inductive num : Type := +zero : num, +pos : pos_num → num + +theorem num.is_inhabited [instance] : inhabited num := +inhabited.mk num.zero + +namespace num + definition inc (a : num) : num := + rec (pos pos_num.one) (λp, pos (pos_num.inc p)) a + + definition num_bits (a : num) : num := + rec (pos pos_num.one) (λp, pos (pos_num.num_bits p)) a +end num