From 84188c5aa1673fdf37a082b2de8562dddf53df3f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Feb 2017 19:00:20 -0800 Subject: [PATCH] feat(frontends/lean/elaborator): add pattern validator in the elaborator MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit @johoelzl We now produce a better message for your example: inductive R : ℕ → Prop | pos : ∀p n, R (p + n) lemma R_id : ∀n, R n → R n | (.p + .n) (R.pos p n) := R.pos p n The new error is: file.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )') .p + .n --- src/frontends/lean/elaborator.cpp | 127 ++++++++++++++++++ src/frontends/lean/elaborator.h | 1 + src/library/equations_compiler/elim_match.cpp | 7 +- src/library/equations_compiler/util.cpp | 10 ++ src/library/equations_compiler/util.h | 3 + tests/lean/eqn_compiler_error_msg.lean | 5 + .../eqn_compiler_error_msg.lean.expected.out | 2 + 7 files changed, 149 insertions(+), 6 deletions(-) create mode 100644 tests/lean/eqn_compiler_error_msg.lean create mode 100644 tests/lean/eqn_compiler_error_msg.lean.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 857bcb8c41..bb30e88176 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -38,13 +38,16 @@ Author: Leonardo de Moura #include "library/protected.h" #include "library/message_builder.h" #include "library/aliases.h" +#include "library/inverse.h" #include "library/vm/vm_name.h" #include "library/vm/vm_expr.h" #include "library/tactic/kabstract.h" +#include "library/tactic/unfold_tactic.h" #include "library/tactic/tactic_state.h" #include "library/tactic/elaborate.h" #include "library/equations_compiler/compiler.h" #include "library/equations_compiler/util.h" +#include "library/inductive_compiler/ginductive.h" #include "frontends/lean/builtin_exprs.h" #include "frontends/lean/brackets.h" #include "frontends/lean/util.h" @@ -2035,6 +2038,129 @@ void elaborator::check_inaccessible_annotations(expr const & lhs) { } } +/* Recursive equation pattern validation.*/ +class validate_equation_lhs_fn : public replace_visitor { + elaborator & m_elab; + expr m_ref; + + type_context & ctx() { return m_elab.m_ctx; } + environment const & env() { return m_elab.env(); } + + optional expand(expr const & e) { + /* We don't simply use whnf because we want to avoid exposing the internal implementation + of definitions compiled using the equation compiler */ + { + /* Try without use delta reduction */ + type_context::transparency_scope scope(ctx(), transparency_mode::None); + expr new_e = ctx().whnf(e); + if (new_e != e) return some_expr(new_e); + } + if (auto new_e = ctx().reduce_projection(e)) + return new_e; + /* Try to unfold using refl equations */ + if (auto new_e = dunfold(ctx(), e)) + return new_e; + /* Last resort, whnf using current setting */ + expr new_e = ctx().whnf(e); + if (new_e != e) return some_expr(new_e); + return none_expr(); + } + + [[ noreturn ]] void throw_invalid_pattern(char const * msg, expr const & e) { + throw elaborator_exception(m_ref, format(msg) + + format(" (possible solution, mark term as inaccessible using '.( )')") + + m_elab.pp_indent(e)); + } + + virtual expr visit_local(expr const & e) override { + return e; + } + + virtual expr visit_lambda(expr const & e) override { + throw_invalid_pattern("invalid occurrence of lambda expression in pattern", e); + } + + virtual expr visit_pi(expr const & e) override { + throw_invalid_pattern("invalid occurrence of pi/forall expression in pattern", e); + } + + virtual expr visit_let(expr const & e) override { + return visit(instantiate(let_body(e), let_value(e))); + } + + virtual expr visit_sort(expr const & e) override { + throw_invalid_pattern("invalid occurrence of sort in pattern", e); + } + + virtual expr visit_meta(expr const & e) override { + throw_invalid_pattern("invalid occurrence of metavariable in pattern", e); + } + + [[ noreturn ]] void throw_invalid_app(expr const & e) { + if (is_constant(e)) + throw_invalid_pattern("invalid constant in pattern, it cannot be reduced to a constructor", e); + else + throw_invalid_pattern("invalid function application in pattern, it cannot be reduced to a constructor", e); + } + + virtual expr visit_app(expr const & e) override { + expr it = e; + while (true) { + if (is_nat_int_char_string_value(ctx(), it)) + return e; + if (!is_app(it) && !is_constant(it)) + return visit(it); + buffer args; + expr const & fn = get_app_args(it, args); + if (!is_constant(fn)) + throw_invalid_app(e); + + if (optional I = is_ginductive_intro_rule(env(), const_name(fn))) { + unsigned num_params = get_ginductive_num_params(env(), *I); + for (unsigned i = num_params; i < args.size(); i++) { + visit(args[i]); + } + return e; + } else if (optional info = has_inverse(env(), const_name(fn))) { + visit(args.back()); + return e; + } else { + if (auto r = expand(it)) { + it = *r; + } else { + throw_invalid_app(e); + } + } + } + } + + virtual expr visit_constant(expr const & e) override { + return visit_app(e); + } + + virtual expr visit_macro(expr const & e) override { + if (is_inaccessible(e)) { + return e; + } else if (auto r = ctx().expand_macro(e)) { + return visit(*r); + } else { + throw_invalid_pattern("invalid occurrence of macro expression in pattern", e); + } + } + +public: + validate_equation_lhs_fn(elaborator & elab, expr const & ref): + m_elab(elab), m_ref(ref) { + } + + void validate(expr const & lhs) { + buffer args; + get_app_args(lhs, args); + for (expr & arg : args) + visit(arg); + } +}; + expr elaborator::visit_equation(expr const & eq) { expr const & lhs = equation_lhs(eq); expr const & rhs = equation_rhs(eq); @@ -2053,6 +2179,7 @@ expr elaborator::visit_equation(expr const & eq) { expr new_lhs_type = instantiate_mvars(infer_type(new_lhs)); expr new_rhs = visit(rhs, some_expr(new_lhs_type)); new_rhs = enforce_type(new_rhs, new_lhs_type, "equation type mismatch", eq); + validate_equation_lhs_fn(*this, lhs).validate(instantiate_mvars(new_lhs)); return copy_tag(eq, mk_equation(new_lhs, new_rhs)); } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 571b55dab4..7054a47df2 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -27,6 +27,7 @@ class elaborator { public: class checkpoint; private: + friend class validate_equation_lhs_fn; typedef std::vector> to_check_sorts; enum class arg_mask { AllExplicit /* @ annotation */, diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 7dcfd92cba..69763b8e86 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -286,12 +286,7 @@ struct elim_match_fn { bool is_value(type_context & ctx, expr const & e) { try { if (!m_use_ite) return false; - if (to_char(ctx, e) || to_string(e)) return true; - if (is_signed_num(e)) { - expr type = ctx.infer(e); - if (ctx.is_def_eq(type, mk_nat_type()) || ctx.is_def_eq(type, mk_int_type())) - return true; - } + if (is_nat_int_char_string_value(ctx, e)) return true; if (optional I_name = is_constructor(e)) return is_nontrivial_enum(*I_name); return false; } catch (exception &) { diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 354eddc9fe..e539f2a849 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -575,6 +575,16 @@ environment mk_simple_equation_lemma_for(environment const & env, options const return add_equation_lemma(env, opts, metavar_context(), ctx.lctx(), is_private, eqn_name, eqn_type, eqn_proof); } +bool is_nat_int_char_string_value(type_context & ctx, expr const & e) { + if (to_char(ctx, e) || to_string(e)) return true; + if (is_signed_num(e)) { + expr type = ctx.infer(e); + if (ctx.is_def_eq(type, mk_nat_type()) || ctx.is_def_eq(type, mk_int_type())) + return true; + } + return false; +} + void initialize_eqn_compiler_util() { register_trace_class("eqn_compiler"); register_trace_class(name{"debug", "eqn_compiler"}); diff --git a/src/library/equations_compiler/util.h b/src/library/equations_compiler/util.h index c594b58fa8..fe6a26b194 100644 --- a/src/library/equations_compiler/util.h +++ b/src/library/equations_compiler/util.h @@ -99,6 +99,9 @@ environment mk_simple_equation_lemma_for(environment const & env, options const name mk_equation_name(name const & f_name, unsigned eqn_idx); +/* Return true iff e is a nat, int, char or string value. */ +bool is_nat_int_char_string_value(type_context & ctx, expr const & e); + void initialize_eqn_compiler_util(); void finalize_eqn_compiler_util(); } diff --git a/tests/lean/eqn_compiler_error_msg.lean b/tests/lean/eqn_compiler_error_msg.lean new file mode 100644 index 0000000000..9e01986291 --- /dev/null +++ b/tests/lean/eqn_compiler_error_msg.lean @@ -0,0 +1,5 @@ +inductive R : ℕ → Prop +| pos : ∀p n, R (p + n) + +lemma R_id : ∀n, R n → R n +| (.p + .n) (R.pos p n) := R.pos p n diff --git a/tests/lean/eqn_compiler_error_msg.lean.expected.out b/tests/lean/eqn_compiler_error_msg.lean.expected.out new file mode 100644 index 0000000000..d195777bc0 --- /dev/null +++ b/tests/lean/eqn_compiler_error_msg.lean.expected.out @@ -0,0 +1,2 @@ +eqn_compiler_error_msg.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )') + .p + .n