From 47e6fd091f5fe0ffab5376d763579969dcfa134b Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 21 Oct 2016 16:01:59 -0400 Subject: [PATCH] refactor(frontends/lean): implement show goal function using exceptions --- src/frontends/lean/elaborator.cpp | 10 +++++++--- src/frontends/lean/opt_cmd.cpp | 8 -------- src/frontends/lean/opt_cmd.h | 3 --- src/frontends/lean/parser.cpp | 31 +++++++++++++++++-------------- src/frontends/lean/parser.h | 14 ++++++++++++-- src/shell/lean.cpp | 23 ----------------------- 6 files changed, 36 insertions(+), 53 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 794217aab6..975d538a8e 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2303,9 +2303,7 @@ void elaborator::show_goal(tactic_state const & s, expr const & start_ref, expr return; if (curr_pos->first < line || (curr_pos->first == line && curr_pos->second < col)) return; - m_show_goal_pos = optional(); - get_global_ios().report(message(provider->get_file_name(), *curr_pos, INFORMATION, - (sstream() << mk_pair(s.pp(get_global_ios().get_formatter_factory()), get_global_ios().get_options())).str())); + throw show_goal_exception(*curr_pos, s); } /* Apply the given tactic to the state 's'. @@ -2509,6 +2507,12 @@ void elaborator::ensure_no_unassigned_metavars(expr const & e) { if (!has_expr_metavar(e)) return false; if (is_metavar_decl_ref(e) && !mctx.is_assigned(e)) { tactic_state s = mk_tactic_state_for(e); + if (m_show_goal_pos && get_pos_info_provider()) { + if (auto pos = get_pos_info_provider()->get_pos_info(e)) { + if (pos == m_show_goal_pos) + throw show_goal_exception(*pos, s); + } + } throw_unsolved_tactic_state(s, "don't know how to synthesize placeholder", e); } return true; diff --git a/src/frontends/lean/opt_cmd.cpp b/src/frontends/lean/opt_cmd.cpp index 563d7f2f44..8147a7f2c6 100644 --- a/src/frontends/lean/opt_cmd.cpp +++ b/src/frontends/lean/opt_cmd.cpp @@ -32,14 +32,6 @@ bool has_show_goal(options const & opts, unsigned & line, unsigned & col) { return has_show(opts, "show_goal", line, col); } -options set_show_hole(options const & opts, unsigned line, unsigned col) { - return set_line_col(opts.update(name("show_hole"), true), line, col); -} - -bool has_show_hole(options const & opts, unsigned & line, unsigned & col) { - return has_show(opts, "show_hole", line, col); -} - options set_show_info(options const & opts, unsigned line, unsigned col) { return set_line_col(opts.update(name("show_info"), true), line, col); } diff --git a/src/frontends/lean/opt_cmd.h b/src/frontends/lean/opt_cmd.h index 9144c598ce..cd84d0647a 100644 --- a/src/frontends/lean/opt_cmd.h +++ b/src/frontends/lean/opt_cmd.h @@ -13,9 +13,6 @@ namespace lean { options set_show_goal(options const & opts, unsigned line, unsigned col); bool has_show_goal(options const & opts, unsigned & line, unsigned & col); -options set_show_hole(options const & _opts, unsigned line, unsigned col); -bool has_show_hole(options const & opts, unsigned & line, unsigned & col); - options set_show_info(options const & opts, unsigned line, unsigned col); bool has_show_info(options const & opts, unsigned & line, unsigned & col); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index da450337b3..200e6d454f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -151,19 +151,19 @@ parser::all_id_local_scope::all_id_local_scope(parser & p): static name * g_tmp_prefix = nullptr; -void parser::init_stop_at(options const & opts) { - unsigned col; - m_info_at = false; - m_stop_at = false; - if (has_show_goal(opts, m_stop_at_line, col)) { - m_stop_at = true; - } else if (has_show_hole(opts, m_stop_at_line, col)) { - m_stop_at = true; - } else if (has_show_info(opts, m_info_at_line, m_info_at_col)) { - m_info_at = true; - m_stop_at = true; - m_stop_at_line = m_info_at_line; - } +void parser::enable_show_goal(pos_info const & pos) { + m_stop_at = true; + m_stop_at_line = pos.first; + m_ios.set_options(set_show_goal(m_ios.get_options(), pos.first, pos.second)); +} + +void parser::enable_show_info(pos_info const & pos) { + m_stop_at = true; + m_stop_at_line = pos.first; + m_info_at = true; + m_info_at_line = pos.first; + m_info_at_col = pos.second; + m_ios.set_options(set_show_info(m_ios.get_options(), pos.first, pos.second)); } class parser_message_stream : public message_stream { @@ -202,7 +202,6 @@ parser::parser(environment const & env, io_state const & ios, m_ignore_noncomputable = false; m_ios.set_message_channel(std::make_shared(this, m_ios.get_message_channel_ptr())); m_profile = ios.get_options().get_bool("profile", false); - init_stop_at(ios.get_options()); if (num_threads > 1 && m_profile) throw exception("option --profile cannot be used when theorems are compiled in parallel"); m_in_quote = false; @@ -212,6 +211,8 @@ parser::parser(environment const & env, io_state const & ios, m_id_behavior = id_behavior::ErrorIfUndef; m_found_errors = false; m_used_sorry = false; + m_info_at = false; + m_stop_at = false; updt_options(); m_next_tag_idx = 0; m_next_inst_idx = 1; @@ -328,6 +329,8 @@ void parser::protected_call(std::function && f, std::function && m_env = ex.get_env(); ex.get_exception().rethrow(); } + } catch (show_goal_exception) { + throw; } catch (parser_exception & ex) { CATCH(ios().report(ex), throw); } catch (parser_error & ex) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 4397323791..dbec58dcd1 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "library/io_state.h" #include "library/io_state_stream.h" #include "library/message_builder.h" +#include "library/tactic/tactic_state.h" #include "frontends/lean/scanner.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/local_level_decls.h" @@ -71,6 +72,14 @@ struct snapshot { typedef std::vector snapshot_vector; +class show_goal_exception : public std::exception { +public: + pos_info m_pos; + tactic_state m_state; + + show_goal_exception(pos_info const & pos, tactic_state const & goal) : m_pos(pos), m_state(goal) {} +}; + enum class keep_theorem_mode { All, DiscardImported, DiscardAll }; enum class id_behavior { @@ -200,8 +209,6 @@ class parser : public abstract_parser { friend class parser_message_stream; void add_message(message const & msg) { m_messages = cons(msg, m_messages); } - void init_stop_at(options const & opts); - void replace_theorem(certified_declaration const & thm); environment reveal_theorems_core(buffer const & ds, bool all); public: @@ -211,6 +218,9 @@ public: snapshot const * s = nullptr, snapshot_vector * sv = nullptr); ~parser(); + void enable_show_goal(pos_info const & pos); + void enable_show_info(pos_info const & pos); + bool ignore_noncomputable() const { return m_ignore_noncomputable; } void set_ignore_noncomputable() { m_ignore_noncomputable = true; } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 5035a79737..4df79a6906 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -117,8 +117,6 @@ static void display_help(std::ostream & out) { std::cout << "Frontend query interface:\n"; std::cout << " --line=value line number for query\n"; std::cout << " --col=value column number for query\n"; - std::cout << " --goal display goal at close to given position\n"; - std::cout << " --hole display type of the \"hole\" in the given posivition\n"; std::cout << " --info display information about identifier or token in the given posivition\n"; std::cout << "Exporting data:\n"; std::cout << " --export=file -E export final environment as textual low-level file\n"; @@ -151,8 +149,6 @@ static struct option g_long_options[] = { #endif {"line", required_argument, 0, 'L'}, {"col", required_argument, 0, 'O'}, - {"goal", no_argument, 0, 'G'}, - {"hole", no_argument, 0, 'Z'}, {"info", no_argument, 0, 'I'}, {"dir", required_argument, 0, 'T'}, #ifdef LEAN_DEBUG @@ -265,9 +261,6 @@ int main(int argc, char ** argv) { optional export_txt; optional export_all_txt; optional base_dir; - bool show_goal = false; - bool show_hole = false; - bool show_info = false; while (true) { int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL); if (c == -1) @@ -338,15 +331,6 @@ int main(int argc, char ** argv) { case 'O': column = atoi(optarg); break; - case 'G': - show_goal = true; - break; - case 'Z': - show_hole = true; - break; - case 'I': - show_info = true; - break; case 'E': export_txt = std::string(optarg); break; @@ -371,13 +355,6 @@ int main(int argc, char ** argv) { #if defined(__GNUC__) && !defined(__CLANG__) #pragma GCC diagnostic ignored "-Wmaybe-uninitialized" #endif - if (show_hole && line && column) { - opts = set_show_hole(opts, *line, *column); - } else if (show_goal && line && column) { - opts = set_show_goal(opts, *line, *column); - } else if (show_info && line && column) { - opts = set_show_info(opts, *line, *column); - } #if !defined(LEAN_MULTI_THREAD) lean_assert(num_threads == 1);