From 339713091f3bbd25a0cb51181c0ec0ed1bb551c2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 11 Feb 2017 14:36:48 +0100 Subject: [PATCH] refactor(frontends/lean): simpler field notation info that also works with implicit parameters --- src/frontends/lean/builtin_exprs.cpp | 28 ++++++++----------- src/frontends/lean/builtin_exprs.h | 1 - src/frontends/lean/elaborator.cpp | 18 ++++-------- src/frontends/lean/elaborator.h | 2 +- tests/lean/interactive/field_info.lean | 4 ++- .../interactive/field_info.lean.expected.out | 1 + 6 files changed, 22 insertions(+), 32 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index a9efdc387d..49df683a17 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -822,22 +822,20 @@ static std::string * g_field_notation_opcode = nullptr; class field_notation_macro_cell : public macro_definition_cell { name m_field; unsigned m_field_idx; - pos_info m_field_pos; public: - field_notation_macro_cell(name const & f, pos_info field_pos):m_field(f), m_field_idx(0), m_field_pos(field_pos) {} + field_notation_macro_cell(name const & f):m_field(f), m_field_idx(0) {} field_notation_macro_cell(unsigned fidx):m_field_idx(fidx) {} virtual name get_name() const { return *g_field_notation_name; } virtual expr check_type(expr const &, abstract_type_context &, bool) const { throw_pn_ex(); } virtual optional expand(expr const &, abstract_type_context &) const { throw_pn_ex(); } - virtual void write(serializer & s) const { s << *g_field_notation_opcode << m_field << m_field_idx << m_field_pos; } + virtual void write(serializer & s) const { s << *g_field_notation_opcode << m_field << m_field_idx; } bool is_anonymous() const { return m_field.is_anonymous(); } name const & get_field_name() const { lean_assert(!is_anonymous()); return m_field; } unsigned get_field_idx() const { lean_assert(is_anonymous()); return m_field_idx; } - optional get_field_pos() const { return is_anonymous() ? optional() : some(m_field_pos); } }; -static expr mk_proj_notation(expr const & e, name const & field, pos_info field_pos) { - macro_definition def(new field_notation_macro_cell(field, field_pos)); +static expr mk_proj_notation(expr const & e, name const & field) { + macro_definition def(new field_notation_macro_cell(field)); return mk_macro(def, 1, &e); } @@ -865,11 +863,6 @@ unsigned get_field_notation_field_idx(expr const & e) { return static_cast(macro_def(e).raw())->get_field_idx(); } -optional get_field_notation_field_pos(expr const & e) { - lean_assert(is_field_notation(e)); - return static_cast(macro_def(e).raw())->get_field_pos(); -} - static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info const & pos) { try { p.check_break_at_pos(break_at_pos_exception::token_context::expr); @@ -880,9 +873,8 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c throw parser_error("invalid projection, index must be greater than 0", num_pos); return p.save_pos(mk_proj_notation(args[0], fidx), pos); } else { - pos_info field_pos = p.pos(); name field = p.check_id_next("invalid '~>' notation, identifier or numeral expected"); - return p.save_pos(mk_proj_notation(args[0], field, field_pos), pos); + return p.save_pos(mk_proj_notation(args[0], field), pos); } } catch (break_at_pos_exception & ex) { expr lhs = args[0]; @@ -901,6 +893,10 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c if (is_constant(fn)) { ex.m_token_info.m_struct = const_name(fn); ex.m_token_info.m_context = break_at_pos_exception::token_context::field; + if (!p.get_complete()) { + // info is stored at position of notation token + ex.m_token_info.m_pos = pos; + } } throw; } @@ -990,12 +986,12 @@ void initialize_builtin_exprs() { [](deserializer & d, unsigned num, expr const * args) { if (num != 1) throw corrupted_stream_exception(); - name fname; unsigned fidx; pos_info fpos; - d >> fname >> fidx >> fpos; + name fname; unsigned fidx; + d >> fname >> fidx; if (fname.is_anonymous()) return mk_proj_notation(args[0], fidx); else - return mk_proj_notation(args[0], fname, fpos); + return mk_proj_notation(args[0], fname); }); } diff --git a/src/frontends/lean/builtin_exprs.h b/src/frontends/lean/builtin_exprs.h index 53e114de60..1fb0dc5e28 100644 --- a/src/frontends/lean/builtin_exprs.h +++ b/src/frontends/lean/builtin_exprs.h @@ -17,7 +17,6 @@ bool is_field_notation(expr const & e); bool is_anonymous_field_notation(expr const & e); name const & get_field_notation_field_name(expr const & e); unsigned get_field_notation_field_idx(expr const & e); -optional get_field_notation_field_pos(expr const & e); bool is_do_failure_eq(expr const & e); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b8f1369bd5..12cdec1a9c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -885,13 +885,11 @@ expr elaborator::visit_const_core(expr const & e) { } /** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */ -void elaborator::save_identifier_info(expr const & f, optional pos) { +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 (!pos) - pos = get_pos_info_provider()->get_pos_info(f); - if (pos) { - m_info.add_identifier_info(pos->first, pos->second, is_constant(f) ? const_name(f) : local_pp_name(f)); - m_info.add_type_info(pos->first, pos->second, infer_type(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)); } } } @@ -2425,13 +2423,7 @@ expr elaborator::visit_field(expr const & e, optional const & expected_typ } expr proj = copy_tag(e, mk_constant(full_fname)); expr new_e = copy_tag(e, mk_app(proj, copy_tag(e, mk_as_is(s)))); - expr r = visit(new_e, expected_type); - if (is_app(r)) { - /* r may be a sorry macro due to error recovery*/ - if (auto pos = get_field_notation_field_pos(e)) - save_identifier_info(app_fn(r), pos); - } - return r; + return visit(new_e, expected_type); } expr elaborator::visit_structure_instance(expr const & e, optional const & _expected_type) { diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 701eeb3080..6a312d8b89 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -184,7 +184,7 @@ private: expr visit_sort(expr const & e); expr visit_const_core(expr const & e); - void save_identifier_info(expr const & f, optional pos = {}); + void save_identifier_info(expr const & f); expr visit_function(expr const & fn, bool has_args, expr const & ref); format mk_app_type_mismatch_error(expr const & t, expr const & arg, expr const & arg_type, expr const & expected_type); format mk_app_arg_mismatch_error(expr const & t, expr const & arg, expr const & expected_arg); diff --git a/tests/lean/interactive/field_info.lean b/tests/lean/interactive/field_info.lean index 056375838d..e6fb9edd44 100644 --- a/tests/lean/interactive/field_info.lean +++ b/tests/lean/interactive/field_info.lean @@ -1,2 +1,4 @@ -def f (n:nat) := n^.to_string +def f (n : ℕ) := n^.to_string --^ "command": "info" +def g (l : list ℕ) := l^.all + --^ "command": "info" diff --git a/tests/lean/interactive/field_info.lean.expected.out b/tests/lean/interactive/field_info.lean.expected.out index 71fa6169d1..ad6a146ba0 100644 --- a/tests/lean/interactive/field_info.lean.expected.out +++ b/tests/lean/interactive/field_info.lean.expected.out @@ -1,2 +1,3 @@ {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"full-id":"nat.to_string","source":{"column":14,"file":"/library/init/data/to_string.lean","line":57},"type":"ℕ → string"},"response":"ok","seq_num":2} +{"record":{"full-id":"list.all","source":{"column":11,"file":"/library/init/data/list/basic.lean","line":147},"type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":4}