From d82df26ff0cf56be692aeca93b9951e4ae9badca Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 9 Sep 2017 12:10:29 +0200 Subject: [PATCH] fix(frontends/lean/elaborator): go back to ignoring implicit args in quote patterns --- src/frontends/lean/elaborator.cpp | 24 +++++++++++++++++++----- src/frontends/lean/elaborator.h | 4 +++- src/frontends/lean/parser.cpp | 3 ++- tests/lean/run/quote_patterns.lean | 7 +++++++ 4 files changed, 31 insertions(+), 7 deletions(-) create mode 100644 tests/lean/run/quote_patterns.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 755d2c9c44..1e7d03b11c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -131,11 +131,11 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const elaborator::elaborator(environment const & env, options const & opts, name const & decl_name, metavar_context const & mctx, local_context const & lctx, bool recover_from_errors, - bool in_pattern): + bool in_pattern, bool in_quote): m_env(env), m_opts(opts), m_decl_name(decl_name), m_ctx(env, opts, mctx, lctx, get_tcm(), transparency_mode::Semireducible), m_recover_from_errors(recover_from_errors), - m_uses_infom(get_global_info_manager() != nullptr), m_in_pattern(in_pattern) { + m_uses_infom(get_global_info_manager() != nullptr), m_in_pattern(in_pattern), m_in_quote(in_quote) { m_coercions = get_elaborator_coercions(opts); } @@ -1269,6 +1269,20 @@ optional elaborator::process_optional_and_auto_params(expr type, expr cons return result_type; } +expr elaborator::post_process_implicit_arg(expr const & arg, expr const & ref) { + if (m_in_pattern && m_in_quote) { + // We ignore implicit arguments in quote patterns so that + // only explicitly given syntax is matched. Note that most + // implicit arguments in standard patterns are ignore via a + // different mechanism in instantiate_pattern_mvars. We cannot + // use the same mechanism for quote patterns because inst-implicit + // arguments are usually not inferable there. + return copy_tag(ref, mk_inaccessible(arg)); + } else { + return arg; + } +} + /* Check if fn args resulting type matches the expected type, and fill first_pass_info & info with information collected in this first pass. Return true iff the types match. @@ -1295,6 +1309,7 @@ void elaborator::first_pass(expr const & fn, buffer const & args, new_arg = mk_metavar(d, ref); if (bi.is_inst_implicit()) info.new_instances.push_back(new_arg); + new_arg = post_process_implicit_arg(new_arg, ref); } else if (i < args.size()) { // explicit argument expr const & arg_ref = args[i]; @@ -1487,9 +1502,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer< new_arg = mk_instance(d, ref); else new_arg = mk_metavar(d, ref); - // implicit arguments are tagged as inaccessible in patterns - if (m_in_pattern) - new_arg = copy_tag(ref, mk_inaccessible(new_arg)); + new_arg = post_process_implicit_arg(new_arg, ref); } else if (i < args.size()) { expr expected_type = d; optional thunk_of; @@ -3697,6 +3710,7 @@ void elaborator::report_error(tactic_state const & s, char const * state_header, void elaborator::ensure_no_unassigned_metavars(expr & e) { // TODO(gabriel): this needs to change e + if (!has_expr_metavar(e)) return; for_each(e, [&](expr const & e, unsigned) { if (!has_expr_metavar(e)) return false; if (is_metavar_decl_ref(e) && !m_ctx.is_assigned(e)) { diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 76df9ff4a5..89fc379aa3 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -97,6 +97,7 @@ private: bool m_no_info{false}; bool m_in_pattern{false}; + bool m_in_quote{false}; expr get_default_numeral_type(); @@ -199,6 +200,7 @@ private: bool is_with_expected_candidate(expr const & fn); std::tuple> elaborate_arg(expr const & arg, expr const & expected_type, expr const & ref); + expr post_process_implicit_arg(expr const & arg, expr const & ref); struct first_pass_info; void first_pass(expr const & fn, buffer const & args, expr const & expected_type, expr const & ref, first_pass_info & info); @@ -292,7 +294,7 @@ private: public: elaborator(environment const & env, options const & opts, name const & decl_name, metavar_context const & mctx, local_context const & lctx, - bool recover_from_errors = true, bool in_pattern = false); + bool recover_from_errors = true, bool in_pattern = false, bool in_quote = false); ~elaborator(); metavar_context const & mctx() const { return m_ctx.mctx(); } local_context const & lctx() const { return m_ctx.lctx(); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index f6405ee329..95dd07a886 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1772,7 +1772,8 @@ expr elaborate_quote(expr e, environment const & env, options const & opts) { metavar_context ctx; local_context lctx; - elaborator elab(env, opts, "_elab_quote", ctx, lctx, /* recover_from_errors */ false, /* in_pattern */ true); + elaborator elab(env, opts, "_elab_quote", ctx, lctx, /* recover_from_errors */ false, + /* in_pattern */ true, /* in_quote */ true); e = elab.elaborate(e); e = elab.finalize(e, /* check_unassigned */ false, /* to_simple_metavar */ true).first; diff --git a/tests/lean/run/quote_patterns.lean b/tests/lean/run/quote_patterns.lean new file mode 100644 index 0000000000..43201128df --- /dev/null +++ b/tests/lean/run/quote_patterns.lean @@ -0,0 +1,7 @@ +meta def f : expr → option (expr × expr × expr) +| `(%%x = %%c*%%y) := some (x, c, y) +| _ := none + +meta def g : expr → nat +| `(%%x = 0) := 2 +| _ := 0