From 0276f4c1c06c24d02bce2b01f96a50b681b472f9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Aug 2014 19:13:09 -0700 Subject: [PATCH] feat(frontends/lean): store 'overload' information, remove #setline Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 11 +---------- src/frontends/lean/info_manager.cpp | 10 +++++++--- src/frontends/lean/parser.cpp | 15 ++++++++++++--- src/frontends/lean/parser.h | 2 ++ src/frontends/lean/pp_options.cpp | 5 ++--- src/frontends/lean/pp_options.h | 2 ++ src/frontends/lean/scanner.cpp | 11 ++++------- src/frontends/lean/scanner.h | 2 +- src/frontends/lean/server.cpp | 2 +- src/frontends/lean/token_table.cpp | 2 +- 10 files changed, 33 insertions(+), 29 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index fbb8fd90a..81dfa91b9 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -98,15 +98,6 @@ environment check_cmd(parser & p) { return p.env(); } -environment set_line_cmd(parser & p) { - if (!p.curr_is_numeral()) - throw parser_error("invalid #setline command, numeral expected", p.pos()); - unsigned r = p.get_small_nat(); - p.set_line(r); - p.next(); - return p.env(); -} - environment exit_cmd(parser &) { throw interrupt_parser(); } @@ -300,7 +291,7 @@ cmd_table init_cmd_table() { add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd)); add_cmd(r, cmd_info("coercion", "add a new coercion", coercion_cmd)); add_cmd(r, cmd_info("opaque_hint", "add hints for the elaborator/unifier", opaque_hint_cmd)); - add_cmd(r, cmd_info("#setline", "modify the current line number, it only affects error/report messages", set_line_cmd)); + register_decl_cmds(r); register_inductive_cmd(r); register_structure_cmd(r); diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index f17607a7e..b5c50d7c9 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -30,12 +30,15 @@ void type_info_data::display(io_state_stream const & ios) const { void overload_info_data::display(io_state_stream const & ios) const { ios << "-- OVERLOAD|" << get_line() << "|" << get_column() << "\n"; + options os = ios.get_options(); + os = os.update(get_pp_full_names_option_name(), true); + auto new_ios = ios.update_options(os); for (unsigned i = 0; i < get_num_choices(m_choices); i++) { if (i > 0) ios << "--\n"; - ios << get_choice(m_choices, i) << endl; + new_ios << get_choice(m_choices, i) << endl; } - ios << "-- ACK" << endl; + new_ios << "-- ACK" << endl; } void coercion_info_data::display(io_state_stream const & ios) const { @@ -85,7 +88,8 @@ unsigned info_manager::find(unsigned line, unsigned column) { void info_manager::invalidate(unsigned sline) { lock_guard lc(m_mutex); sort_core(); - m_data.resize(find(sline, 0)); + unsigned i = find(sline, 0); + m_data.resize(i); m_sorted_upto = m_data.size(); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index c61737d3d..7afb30d62 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -85,11 +85,10 @@ parser::parser(environment const & env, io_state const & ios, unsigned line, snapshot_vector * sv, info_manager * im): m_env(env), m_ios(ios), m_ngen(g_tmp_prefix), m_verbose(true), m_use_exceptions(use_exceptions), - m_scanner(strm, strm_name), m_local_level_decls(lds), m_local_decls(eds), + m_scanner(strm, strm_name, line), m_local_level_decls(lds), m_local_decls(eds), m_pos_table(std::make_shared()), m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0), m_snapshot_vector(sv), m_info_manager(im) { - m_scanner.set_line(line); m_num_threads = num_threads; m_no_undef_id_error = false; m_found_errors = false; @@ -838,7 +837,9 @@ expr parser::parse_notation(parse_table t, expr * left) { expr r = instantiate_rev(copy_with_new_pos(a, p), args.size(), args.data()); cs.push_back(r); } - return save_pos(mk_choice(cs.size(), cs.data()), p); + expr r = save_pos(mk_choice(cs.size(), cs.data()), p); + save_overload(r); + return r; } expr parser::parse_nud_notation() { @@ -896,6 +897,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) { new_as.push_back(copy_with_new_pos(mk_constant(e, ls), p)); } r = save_pos(mk_choice(new_as.size(), new_as.data()), p); + save_overload(*r); } if (!r && m_no_undef_id_error) r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p); @@ -1173,6 +1175,13 @@ void parser::save_snapshot() { m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_ios.get_options(), m_scanner.get_line())); } +void parser::save_overload(expr const & e) { + if (!m_info_manager) + return; + auto p = pos_of(e); + m_info_manager->add(std::unique_ptr(new overload_info_data(p.first, p.second, e))); +} + bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads) { parser p(env, ios, in, strm_name, use_exceptions, num_threads); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 51e0fb66d..12c6b884d 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -151,7 +151,9 @@ class parser { void push_local_scope(); void pop_local_scope(); + void save_snapshot(); + void save_overload(expr const & e); public: parser(environment const & env, io_state const & ios, diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp index 748996a91..271be287d 100644 --- a/src/frontends/lean/pp_options.cpp +++ b/src/frontends/lean/pp_options.cpp @@ -53,9 +53,8 @@ static name g_pp_full_names {"pp", "full_names"}; static name g_pp_private_names {"pp", "private_names"}; static name g_pp_metavar_args {"pp", "metavar_args"}; -name const & get_pp_coercion_option_name() { - return g_pp_coercion; -} +name const & get_pp_coercion_option_name() { return g_pp_coercion; } +name const & get_pp_full_names_option_name() { return g_pp_full_names; } list const & get_distinguishing_pp_options() { static options g_universes_true(g_pp_universes, true); diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h index ca7b37826..0031898da 100644 --- a/src/frontends/lean/pp_options.h +++ b/src/frontends/lean/pp_options.h @@ -8,6 +8,8 @@ Author: Leonardo de Moura #include "util/sexpr/options.h" namespace lean { name const & get_pp_coercion_option_name(); +name const & get_pp_full_names_option_name(); + unsigned get_pp_max_depth(options const & opts); unsigned get_pp_max_steps(options const & opts); bool get_pp_notation(options const & opts); diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 7ec37b900..d940d4933 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -78,11 +78,6 @@ bool is_super_sub_script_alnum_unicode(unsigned u) { (0x2090 <= u && u <= 0x209c); } -void scanner::set_line(unsigned p) { - m_line = p; - m_sline = p; -} - void scanner::next() { lean_assert(m_curr != EOF); m_curr = m_stream.get(); @@ -472,11 +467,13 @@ auto scanner::scan(environment const & env) -> token_kind { } } -scanner::scanner(std::istream & strm, char const * strm_name): - m_tokens(nullptr), m_stream(strm), m_spos(0), m_upos(0), m_uskip(0), m_sline(1), m_curr(0), m_pos(0), m_line(1), +scanner::scanner(std::istream & strm, char const * strm_name, unsigned line): + m_tokens(nullptr), m_stream(strm), m_spos(0), m_upos(0), m_uskip(0), m_sline(line), m_curr(0), m_pos(0), m_line(line), m_token_info(nullptr) { m_stream_name = strm_name ? strm_name : "[unknown]"; next(); + m_spos = 0; + m_upos = 0; } std::ostream & operator<<(std::ostream & out, scanner::token_kind k) { diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index 5a8452b45..7c86b5ded 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -68,7 +68,7 @@ protected: token_kind read_quoted_symbol(); public: - scanner(std::istream & strm, char const * strm_name = nullptr); + scanner(std::istream & strm, char const * strm_name = nullptr, unsigned line = 1); int get_line() const { return m_line; } int get_pos() const { return m_pos; } diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 9f3006813..1c5c68418 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -62,12 +62,12 @@ unsigned server::find(unsigned linenum) { } void server::process_from(unsigned linenum) { - m_info.invalidate(linenum); unsigned i = find(linenum); m_snapshots.resize(i); snapshot & s = i == 0 ? m_empty_snapshot : m_snapshots[i-1]; std::string block; lean_assert(s.m_line > 0); + m_info.invalidate(s.m_line-1); for (unsigned j = s.m_line-1; j < m_lines.size(); j++) { block += m_lines[j]; block += '\n'; diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 562d4597d..87bbcd616 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -78,7 +78,7 @@ token_table init_token_table() { "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", - "add_proof_qed", "set_proof_qed", "#setline", "instance", nullptr}; + "add_proof_qed", "set_proof_qed", "instance", nullptr}; std::pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},