From cda19f5aa67c11e6a212944f2b2840cd62b9fcbb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Mar 2015 20:28:56 -0700 Subject: [PATCH] feat(library/tactic/rewrite_tactic): improve rewrite tactic error messages closes #471 --- src/library/tactic/rewrite_tactic.cpp | 180 +++++++++++++++++++- tests/lean/quasireducible.lean.expected.out | 8 +- tests/lean/rewrite_fail.lean.expected.out | 4 +- 3 files changed, 180 insertions(+), 12 deletions(-) diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 8f543de01..4b333b750 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/rb_map.h" #include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" +#include "kernel/error_msgs.h" #include "kernel/abstract.h" #include "kernel/replace_fn.h" #include "kernel/for_each_fn.h" @@ -41,10 +42,14 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_REWRITER_SYNTACTIC false #endif +#ifndef LEAN_DEFAULT_REWRITER_TRACE +#define LEAN_DEFAULT_REWRITER_TRACE true +#endif namespace lean { static name * g_rewriter_max_iterations = nullptr; static name * g_rewriter_syntactic = nullptr; +static name * g_rewriter_trace = nullptr; unsigned get_rewriter_max_iterations(options const & opts) { return opts.get_unsigned(*g_rewriter_max_iterations, LEAN_DEFAULT_REWRITER_MAX_ITERATIONS); @@ -54,6 +59,10 @@ bool get_rewriter_syntactic(options const & opts) { return opts.get_bool(*g_rewriter_syntactic, LEAN_DEFAULT_REWRITER_SYNTACTIC); } +bool get_rewriter_trace(options const & opts) { + return opts.get_bool(*g_rewriter_trace, LEAN_DEFAULT_REWRITER_TRACE); +} + class unfold_info { list m_names; location m_location; @@ -448,6 +457,7 @@ class rewrite_fn { substitution m_subst; expr m_expr_loc; // auxiliary expression used for error localization + bool m_use_trace; unsigned m_max_iter; buffer> m_lsubst; // auxiliary buffer for pattern matching @@ -825,6 +835,135 @@ class rewrite_fn { some_expr(type), m_expr_loc.get_tag(), cfg, nullptr); } + // target, new_target, H : represents the rewrite (H : target = new_target) for hypothesis + // and (H : new_target = target) for goals + typedef optional> find_result; + + struct failure { + enum kind { Unification, Exception, HasMetavars }; + expr m_elab_lemma; + expr m_subterm; + kind m_kind; + failure(expr const & elab_lemma, expr const & subterm, kind k): + m_elab_lemma(elab_lemma), m_subterm(subterm), m_kind(k) {} + + format pp(formatter const & fmt) const { + format r; + switch (m_kind) { + case Unification: + r = compose(line(), format("-fail to unify equation source")); + r += pp_indent_expr(fmt, m_elab_lemma); + r += compose(line(), format("with subterm")); + r += pp_indent_expr(fmt, m_subterm); + return r; + case Exception: + r = compose(line(), format("-an exception occurred when unifying the subterm")); + r += pp_indent_expr(fmt, m_subterm); + return r; + case HasMetavars: + r = compose(line(), format("-lemma still contains meta-variables")); + r += pp_indent_expr(fmt, m_elab_lemma); + r += compose(line(), format("after the equation source has been unified with subterm")); + r += pp_indent_expr(fmt, m_subterm); + return r; + } + lean_unreachable(); + } + }; + + // Store information for a goal or hypothesis being rewritten + struct target_trace { + bool m_is_hypothesis; + expr m_target; // term being rewritten + list m_failures; // sub-terms that matched but failed to unify + optional m_matched; // sub-term that matched and unified + + target_trace(expr const & t, bool is_hyp): m_is_hypothesis(is_hyp), m_target(t) {} + + format pp(formatter const & fmt) const { + if (m_matched) + return format(); + if (!m_failures) { + if (m_is_hypothesis) + return line() + format("no subterm in the hypothesis '") + fmt(m_target) + format("' matched the pattern"); + else + return line() + format("no subterm in the goal matched the pattern"); + } + format r; + if (m_is_hypothesis) + r = line() + format("matching failures in the hypothesis '") + fmt(m_target) + format("'"); + else + r = line() + format("matching failures in the goal"); + buffer b; + unsigned indent = get_pp_indent(fmt.get_options()); + to_buffer(m_failures, b); + unsigned i = b.size(); + while (i > 0) { + --i; + r += nest(indent, b[i].pp(fmt)); + } + return r; + } + }; + + struct trace { + expr m_lemma; // lemma being used for rewriting + expr m_pattern; // extracted or given pattern + buffer m_targets; // trace for each element we tried to rewrite using m_lemma + + format pp(formatter const & fmt) const { + format r("rewrite step failed using pattern"); + r += pp_indent_expr(fmt, m_pattern); + for (target_trace const & t : m_targets) { + r += t.pp(fmt); + } + return r; + } + }; + + bool m_trace_initialized; + trace m_trace; // temporary object used to store execution trace for a rewrite step + + void clear_trace() { + m_trace_initialized = false; + } + + void init_trace(expr const & lemma, expr const & pattern) { + if (m_use_trace) { + m_trace_initialized = true; + m_trace.m_lemma = lemma; + m_trace.m_pattern = pattern; + m_trace.m_targets.clear(); + } + } + + void add_target(expr const & t, bool is_hyp) { + if (m_use_trace) + m_trace.m_targets.push_back(target_trace(t, is_hyp)); + } + + target_trace & latest_target() { + lean_assert(m_use_trace); + lean_assert(!m_trace.m_targets.empty()); + return m_trace.m_targets.back(); + } + + void add_target_failure(expr const & elab_term, expr const & subterm, failure::kind k) { + if (m_use_trace) { + target_trace & tt = latest_target(); + lean_assert(!tt.m_matched); + tt.m_failures = cons(failure(elab_term, subterm, k), tt.m_failures); + } + } + + void add_target_match(expr const & m) { + if (m_use_trace) { + target_trace & tt = latest_target(); + lean_assert(!tt.m_matched); + tt.m_matched = m; + } + } + // rule, new_t typedef optional> unify_result; @@ -859,8 +998,10 @@ class rewrite_fn { src = app_arg(rule_type); else src = app_arg(app_fn(rule_type)); - if (!m_tc->is_def_eq(t, src, justification(), cs_seq)) + if (!m_tc->is_def_eq(t, src, justification(), cs_seq)) { + add_target_failure(src, t, failure::Unification); return unify_result(); + } cs_seq.linearize(cs); unifier_config cfg; cfg.m_kind = unifier_kind::Liberal; @@ -870,11 +1011,14 @@ class rewrite_fn { substitution new_subst = p->first.first; rule = new_subst.instantiate_all(rule); rule_type = new_subst.instantiate_all(rule_type); - if (has_expr_metavar_strict(rule) || has_expr_metavar_strict(rule_type)) + if (has_expr_metavar_strict(rule) || has_expr_metavar_strict(rule_type)) { + add_target_failure(rule, t, failure::HasMetavars); return unify_result(); // rule was not completely instantiated. + } m_subst = new_subst; expr lhs = app_arg(app_fn(rule_type)); expr rhs = app_arg(rule_type); + add_target_match(t); if (is_goal) { if (symm) { return unify_result(rule, lhs); @@ -890,15 +1034,15 @@ class rewrite_fn { return unify_result(rule, rhs); } } + } else { + add_target_failure(src, t, failure::Unification); + return unify_result(); } } catch (exception&) {} + add_target_failure(orig_elem, t, failure::Exception); return unify_result(); } - // target, new_target, H : represents the rewrite (H : target = new_target) for hypothesis - // and (H : new_target = target) for goals - typedef optional> find_result; - // Search for \c pattern in \c e. If \c t is a match, then try to unify the type of the rule // in the rewrite step \c orig_elem with \c t. // When successful, this method returns the target \c t, the fully elaborated rule \c r, @@ -930,6 +1074,7 @@ class rewrite_fn { } bool process_rewrite_hypothesis(expr const & hyp, expr const & orig_elem, expr const & pattern, occurrence const & occ) { + add_target(hyp, true); expr Pa = mlocal_type(hyp); bool is_goal = false; if (auto it = find_target(Pa, pattern, orig_elem, is_goal)) { @@ -978,6 +1123,7 @@ class rewrite_fn { bool process_rewrite_goal(expr const & orig_elem, expr const & pattern, occurrence const & occ) { expr Pa = m_g.get_type(); + add_target(Pa, false); bool is_goal = true; if (auto it = find_target(Pa, pattern, orig_elem, is_goal)) { expr a, Heq, b; @@ -1043,6 +1189,7 @@ class rewrite_fn { bool process_rewrite_step(expr const & elem, expr const & orig_elem) { lean_assert(is_rewrite_step(elem)); expr pattern = get_pattern(elem); + init_trace(orig_elem, pattern); // regular(m_env, m_ios) << "pattern: " << pattern << "\n"; rewrite_info const & info = get_rewrite_info(elem); unsigned i, num; @@ -1086,6 +1233,7 @@ class rewrite_fn { // Process the given rewrite element/step. This method destructively update // m_g, m_subst, m_ngen. It returns true if it succeeded and false otherwise. bool process_step(expr const & elem) { + clear_trace(); if (is_rewrite_unfold_step(elem)) { return process_unfold_step(elem); } else if (is_rewrite_fold_step(elem)) { @@ -1160,7 +1308,8 @@ public: lean_assert(gs); update_goal(head(gs)); m_subst = m_ps.get_subst(); - m_max_iter = get_rewriter_max_iterations(ios.get_options()); + m_max_iter = get_rewriter_max_iterations(ios.get_options()); + m_use_trace = get_rewriter_trace(ios.get_options()); } proof_state_seq operator()(buffer const & elems) { @@ -1169,8 +1318,18 @@ public: if (!process_step(elem)) { if (m_ps.report_failure()) { proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen); - throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, - [](formatter const &) { return format("invalid 'rewrite' tactic, rewrite step failed"); }); + if (!m_use_trace || !m_trace_initialized) { + throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, + [](formatter const &) { return format("invalid 'rewrite' tactic, rewrite step failed"); }); + } else { + trace saved_trace = m_trace; + throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps, + [=](formatter const & fmt) { + format r = format("invalid 'rewrite' tactic, "); + r += saved_trace.pp(fmt); + return r; + }); + } } return proof_state_seq(); } @@ -1204,6 +1363,9 @@ void initialize_rewrite_tactic() { g_rewriter_syntactic = new name{"rewriter", "syntactic"}; register_bool_option(*g_rewriter_syntactic, LEAN_DEFAULT_REWRITER_SYNTACTIC, "(rewriter tactic) if true tactic will not unfold any constant when performing pattern matching"); + g_rewriter_trace = new name{"rewriter", "trace"}; + register_bool_option(*g_rewriter_trace, LEAN_DEFAULT_REWRITER_TRACE, + "(rewriter tactic) if true tactic will generate a trace for rewrite step failures"); name rewrite_tac_name{"tactic", "rewrite_tac"}; g_rewrite_tac = new expr(Const(rewrite_tac_name)); g_rewrite_reduce_name = new name("rewrite_reduce"); diff --git a/tests/lean/quasireducible.lean.expected.out b/tests/lean/quasireducible.lean.expected.out index 95f52ebe8..a84991154 100644 --- a/tests/lean/quasireducible.lean.expected.out +++ b/tests/lean/quasireducible.lean.expected.out @@ -1,4 +1,6 @@ -quasireducible.lean:11:11: error:invalid 'rewrite' tactic, rewrite step failed +quasireducible.lean:11:11: error:invalid 'rewrite' tactic, rewrite step failed using pattern + f a +no subterm in the goal matched the pattern proof state: a : nat, H : f a = a @@ -10,7 +12,9 @@ H : f a = a quasireducible.lean:11:3: error: failed to add declaration '14.1' to environment, value has metavariables λ (a : nat) (H : f a = a), ?M_1 -quasireducible.lean:16:11: error:invalid 'rewrite' tactic, rewrite step failed +quasireducible.lean:16:11: error:invalid 'rewrite' tactic, rewrite step failed using pattern + f a +no subterm in the goal matched the pattern proof state: a : nat, H : f a = a diff --git a/tests/lean/rewrite_fail.lean.expected.out b/tests/lean/rewrite_fail.lean.expected.out index 1ce25ecd3..522a6790e 100644 --- a/tests/lean/rewrite_fail.lean.expected.out +++ b/tests/lean/rewrite_fail.lean.expected.out @@ -1,4 +1,6 @@ -rewrite_fail.lean:5:15: error:invalid 'rewrite' tactic, rewrite step failed +rewrite_fail.lean:5:15: error:invalid 'rewrite' tactic, rewrite step failed using pattern + a +no subterm in the goal matched the pattern proof state: a b : ℕ, Ha : a = 0,