From 2f75768243c89e466f9e6ea5ba1b6084805704c9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Jun 2015 12:05:00 -0700 Subject: [PATCH] feat(library/tactic/rewrite_tactic): fail when nothing is rewritten fixes #686 --- src/library/tactic/location.cpp | 10 +++++-- src/library/tactic/location.h | 4 ++- src/library/tactic/rewrite_tactic.cpp | 35 +++++++++++++++------- tests/lean/rw_at_failure.lean | 7 +++++ tests/lean/rw_at_failure.lean.expected.out | 1 + 5 files changed, 43 insertions(+), 14 deletions(-) create mode 100644 tests/lean/rw_at_failure.lean create mode 100644 tests/lean/rw_at_failure.lean.expected.out diff --git a/src/library/tactic/location.cpp b/src/library/tactic/location.cpp index aa3b615bd..c511f72e8 100644 --- a/src/library/tactic/location.cpp +++ b/src/library/tactic/location.cpp @@ -112,16 +112,20 @@ deserializer & operator>>(deserializer & d, location & loc) { return d; } -expr replace_occurrences(expr const & e, expr const & t, occurrence const & occ, unsigned idx) { +optional replace_occurrences(expr const & e, expr const & t, occurrence const & occ, unsigned idx) { bool use_cache = occ.is_all(); unsigned occ_idx = 0; - return replace(e, [&](expr const & e, unsigned offset) { + bool replaced = false; + expr r = replace(e, [&](expr const & e, unsigned offset) { if (e == t) { occ_idx++; - if (occ.contains(occ_idx)) + if (occ.contains(occ_idx)) { + replaced = true; return some_expr(mk_var(offset+idx)); + } } return none_expr(); }, use_cache); + return replaced ? some_expr(r) : none_expr(); } } diff --git a/src/library/tactic/location.h b/src/library/tactic/location.h index 44db1268e..c60c5a8e1 100644 --- a/src/library/tactic/location.h +++ b/src/library/tactic/location.h @@ -54,8 +54,10 @@ public: /** \brief Replace occurrences of \c t in \c e with the free variable #vidx. The j-th occurrence is replaced iff occ.contains(j) + + Return none when no occurrence was replaced. */ -expr replace_occurrences(expr const & e, expr const & t, occurrence const & occ, unsigned vidx); +optional replace_occurrences(expr const & e, expr const & t, occurrence const & occ, unsigned vidx); class location { public: diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 60af7b540..0ef17665a 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -1330,6 +1330,16 @@ class rewrite_fn { return e; } + void throw_nothing_rewritten_ex() { + if (m_ps.report_failure()) { + throw_rewrite_exception("invalid 'rewrite' tactic, no occurrence was replaced, " + "this error may occur when the 'at' modifier is used (e.g., 'at {2}'). Lean " + "uses the following semantics: first it finds a matching subterm; then uses the bound " + "arguments to look for further syntactically identical occurrences; and then it replaces " + "the occurrences specified by the 'at' modifier (when provided)"); + } + } + bool process_rewrite_hypothesis(expr const & hyp, expr const & orig_elem, expr const & pattern, occurrence const & occ) { add_target(hyp, true); expr Pa = apply_beta_eta(mlocal_type(hyp)); @@ -1344,21 +1354,22 @@ class rewrite_fn { return false; bool has_dep_elim = inductive::has_dep_elim(m_env, get_eq_name()); unsigned vidx = has_dep_elim ? 1 : 0; - expr Px = replace_occurrences(Pa, a, occ, vidx); - expr Pb = instantiate(Px, vidx, b); - + optional Px = replace_occurrences(Pa, a, occ, vidx); + if (!Px) { + return false; + } + expr Pb = instantiate(*Px, vidx, b); expr A = m_relaxed_tc->infer(a).first; level l1 = sort_level(m_relaxed_tc->ensure_type(Pa).first); level l2 = sort_level(m_relaxed_tc->ensure_type(A).first); expr H; if (has_dep_elim) { expr Haeqx = mk_app(mk_constant(get_eq_name(), {l2}), A, a, mk_var(0)); - expr P = mk_lambda("x", A, mk_lambda("H", Haeqx, Px)); + expr P = mk_lambda("x", A, mk_lambda("H", Haeqx, *Px)); H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, a, P, hyp, b, Heq}); } else { - H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, a, mk_lambda("x", A, Px), hyp, b, Heq}); + H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, a, mk_lambda("x", A, *Px), hyp, b, Heq}); } - expr new_hyp = update_mlocal(hyp, Pb); buffer new_hyps; buffer args; @@ -1396,8 +1407,12 @@ class rewrite_fn { // where M is a metavariable application of a fresh metavariable, and H is a witness (based on M) for P[a]. bool has_dep_elim = inductive::has_dep_elim(m_env, get_eq_name()); unsigned vidx = has_dep_elim ? 1 : 0; - expr Px = replace_occurrences(Pa, a, occ, vidx); - expr Pb = instantiate(Px, vidx, b); + optional Px = replace_occurrences(Pa, a, occ, vidx); + if (!Px) { + throw_nothing_rewritten_ex(); + return false; + } + expr Pb = instantiate(*Px, vidx, b); expr A = m_relaxed_tc->infer(a).first; level l1 = sort_level(m_relaxed_tc->ensure_type(Pa).first); level l2 = sort_level(m_relaxed_tc->ensure_type(A).first); @@ -1405,10 +1420,10 @@ class rewrite_fn { expr H; if (has_dep_elim) { expr Haeqx = mk_app(mk_constant(get_eq_name(), {l2}), A, b, mk_var(0)); - expr P = mk_lambda("x", A, mk_lambda("H", Haeqx, Px)); + expr P = mk_lambda("x", A, mk_lambda("H", Haeqx, *Px)); H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, b, P, M, a, Heq}); } else { - H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, b, mk_lambda("x", A, Px), M, a, Heq}); + H = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, b, mk_lambda("x", A, *Px), M, a, Heq}); } check_term(H); goal new_g(M, Pb); diff --git a/tests/lean/rw_at_failure.lean b/tests/lean/rw_at_failure.lean new file mode 100644 index 000000000..40cc14662 --- /dev/null +++ b/tests/lean/rw_at_failure.lean @@ -0,0 +1,7 @@ +import data.nat +open nat + +example (a b : nat) : a = b → 0 + a = 0 + b := +begin + rewrite zero_add at {2} -- Should fail since nothing is rewritten +end diff --git a/tests/lean/rw_at_failure.lean.expected.out b/tests/lean/rw_at_failure.lean.expected.out new file mode 100644 index 000000000..48ddf64a0 --- /dev/null +++ b/tests/lean/rw_at_failure.lean.expected.out @@ -0,0 +1 @@ +rw_at_failure.lean:6:10: error: invalid 'rewrite' tactic, no occurrence was replaced, this error may occur when the 'at' modifier is used (e.g., 'at {2}'). Lean uses the following semantics: first it finds a matching subterm; then uses the bound arguments to look for further syntactically identical occurrences; and then it replaces the occurrences specified by the 'at' modifier (when provided)