From 669c4130b1594d25a8768ea5cc89cf413703d628 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 31 Mar 2017 10:51:12 +0200 Subject: [PATCH] fix(frontends/lean/builtin_expr): no field notation after @/@@ --- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/parser.cpp | 19 ++++++++++--------- src/frontends/lean/parser.h | 8 +++++--- tests/lean/run/no_field_access.lean | 6 ++++++ 4 files changed, 22 insertions(+), 13 deletions(-) create mode 100644 tests/lean/run/no_field_access.lean diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 2e5d432e6d..131babce83 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -599,7 +599,7 @@ static expr parse_calc_expr(parser_state & p, unsigned, expr const *, pos_info c static expr parse_explicit_core(parser_state & p, pos_info const & pos, bool partial) { if (!p.curr_is_identifier()) throw parser_error(sstream() << "invalid '" << (partial ? "@@" : "@") << "', identifier expected", p.pos()); - expr fn = p.parse_id(); + expr fn = p.parse_id(/* allow_field_notation */ false); if (is_choice(fn)) { sstream s; s << "invalid '" << (partial ? "@@" : "@") << "', function is overloaded, use fully qualified names (overloads: "; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index eb9ba33234..233ba73252 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1701,7 +1701,7 @@ class patexpr_to_expr_fn : public replace_visitor { } virtual expr visit_local(expr const & e) override { - return m_p.id_to_expr(local_pp_name(e), m_p.pos_of(e), true, m_locals); + return m_p.id_to_expr(local_pp_name(e), m_p.pos_of(e), true, true, m_locals); } public: @@ -1727,7 +1727,8 @@ static void check_no_levels(levels const & ls, pos_info const & p) { "parameter or a constant bound to parameters in a section", p); } -optional parser::resolve_local(name const & id, pos_info const & p, list const & extra_locals) { +optional parser::resolve_local(name const & id, pos_info const & p, list const & extra_locals, + bool allow_field_notation) { /* Remark: (auxiliary) local constants many not be atomic. Example: when elaborating @@ -1751,7 +1752,7 @@ optional parser::resolve_local(name const & id, pos_info const & p, list parser::resolve_local(name const & id, pos_info const & p, list const & extra_locals) { +expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only, bool allow_field_notation, list const & extra_locals) { buffer lvl_buffer; levels ls; bool explicit_levels = false; @@ -1782,7 +1783,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only, return save_pos(mk_local(id, save_pos(mk_expr_placeholder(), p)), p); } - if (auto r = resolve_local(id, p, extra_locals)) { + if (auto r = resolve_local(id, p, extra_locals, allow_field_notation)) { check_no_levels(ls, p); return *r; } @@ -1834,9 +1835,9 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only, r = save_pos(local, p); } } - if (!r && !id.is_atomic() && id.is_string()) { + if (!r && allow_field_notation && !id.is_atomic() && id.is_string()) { try { - expr s = id_to_expr(id.get_prefix(), p, resolve_only, extra_locals); + expr s = id_to_expr(id.get_prefix(), p, resolve_only, allow_field_notation, extra_locals); auto field_pos = p; field_pos.second += id.get_prefix().utf8_size(); r = save_pos(mk_field_notation_compact(s, id.get_string()), field_pos); @@ -1914,11 +1915,11 @@ name parser::check_constant_next(char const * msg) { return to_constant(id, msg, p); } -expr parser::parse_id() { +expr parser::parse_id(bool allow_field_notation) { auto p = pos(); lean_assert(curr_is_identifier()); name id = check_id_next("", break_at_pos_exception::token_context::expr); - expr e = id_to_expr(id, p); + expr e = id_to_expr(id, p, /* resolve_only */ false, allow_field_notation); if (is_constant(e) && get_global_info_manager()) { get_global_info_manager()->add_const_info(m_env, p, const_name(e)); } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 5514df9e0f..85035a3900 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -164,7 +164,8 @@ class parser : public abstract_parser { std::shared_ptr mk_snapshot(); - optional resolve_local(name const & id, pos_info const & p, list const & extra_locals); + optional resolve_local(name const & id, pos_info const & p, list const & extra_locals, + bool allow_field_notation = true); friend class module_parser; friend class patexpr_to_expr_fn; @@ -354,7 +355,8 @@ public: void parse_close_binder_info(binder_info const & bi) { return parse_close_binder_info(optional(bi)); } /** \brief Convert an identifier into an expression (constant or local constant) based on the current scope */ - expr id_to_expr(name const & id, pos_info const & p, bool resolve_only = false, list const & extra_locals = list()); + expr id_to_expr(name const & id, pos_info const & p, bool resolve_only = false, bool allow_field_notation = true, + list const & extra_locals = list()); expr parse_expr(unsigned rbp = 0); /** \brief Parse an (optionally) qualified expression. @@ -381,7 +383,7 @@ public: /* \brief Set pattern mode, and invoke fn. The new locals are stored in new_locals */ expr parse_pattern(std::function const & fn, buffer & new_locals); - expr parse_id(); + expr parse_id(bool allow_field_notation = true); expr parse_led(expr left); expr parse_scoped_expr(unsigned num_params, expr const * ps, local_environment const & lenv, unsigned rbp = 0); diff --git a/tests/lean/run/no_field_access.lean b/tests/lean/run/no_field_access.lean new file mode 100644 index 0000000000..a0a2a7dd33 --- /dev/null +++ b/tests/lean/run/no_field_access.lean @@ -0,0 +1,6 @@ +namespace foo +constant bar : ℕ → ℕ +end foo + +noncomputable def foo : ℕ → ℕ +| x := @foo.bar x -- should not use field notation with '@'