From ac4cd3d7338a36a47b64c8d9f3fd617ad87968fc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Nov 2016 15:53:40 -0800 Subject: [PATCH] feat(library/tactic/rewrite_tactic): disable pp.beta at rewrite error msg --- library/init/nat_lemmas.lean | 2 -- src/library/tactic/rewrite_tactic.cpp | 6 ++++-- src/library/tactic/tactic_state.h | 3 +++ tests/lean/bad_error2.lean | 11 +++++++++++ tests/lean/bad_error2.lean.expected.out | 9 +++++++++ 5 files changed, 27 insertions(+), 4 deletions(-) create mode 100644 tests/lean/bad_error2.lean create mode 100644 tests/lean/bad_error2.lean.expected.out diff --git a/library/init/nat_lemmas.lean b/library/init/nat_lemmas.lean index 1968a0818c..612ffdcd7d 100644 --- a/library/init/nat_lemmas.lean +++ b/library/init/nat_lemmas.lean @@ -36,8 +36,6 @@ namespace nat | n m 0 := rfl | n m (succ k) := by simp [add_succ, add_assoc n m k] - set_option trace.app_builder true - protected lemma add_left_cancel : ∀ {n m k : ℕ}, n + m = n + k → m = k | 0 m k := by ctx_simp [nat.zero_add] | (succ n) m k := λ h, diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index f00c17fa53..3dd6440d2e 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/app_builder.h" #include "library/constants.h" #include "library/trace.h" +#include "library/pp_options.h" #include "library/vm/vm_list.h" #include "library/vm/vm_option.h" #include "library/vm/vm_nat.h" @@ -64,12 +65,13 @@ vm_obj rewrite(transparency_mode const & m, bool use_instances, occurrences cons expr pattern = target ? lhs : rhs; expr e_abst = kabstract(ctx, e, pattern, occs); if (closed(e_abst)) { + auto new_s = update_option_if_undef(s, get_pp_beta_name(), false); auto thunk = [=]() { format msg = format("rewrite tactic failed, did not find instance of the pattern in the target expression"); - msg += pp_indented_expr(s, pattern); + msg += pp_indented_expr(new_s, pattern); return msg; }; - return mk_tactic_exception(thunk, s); + return mk_tactic_exception(thunk, new_s); } /* Synthesize type class instances */ if (use_instances) { diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index e0676b469f..665d990d72 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -96,6 +96,9 @@ tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env, \remark It returns s is is_eqp(s.mctx(), mctx) and is_decl_eqp(s.get_main_goal_decl()->get_context(), lctx) */ tactic_state set_mctx_lctx(tactic_state const & s, metavar_context const & mctx, local_context const & lctx); +template tactic_state update_option_if_undef(tactic_state const & s, name const & n, T v) { + return set_options(s, s.get_options().update_if_undef(n, v)); +} bool is_tactic_state(vm_obj const & o); tactic_state const & to_tactic_state(vm_obj const & o); diff --git a/tests/lean/bad_error2.lean b/tests/lean/bad_error2.lean new file mode 100644 index 0000000000..5f1aeeb496 --- /dev/null +++ b/tests/lean/bad_error2.lean @@ -0,0 +1,11 @@ +open nat + +example {k n m : ℕ} (h : k + n ≤ k + m) : n ≤ m := +match le.elim h with +| ⟨w, hw⟩ := @le.intro _ _ w + begin + -- in the following error pp.beta is automatically disabled + rw [nat.add_assoc] at hw, + apply nat.add_left_cancel hw + end +end diff --git a/tests/lean/bad_error2.lean.expected.out b/tests/lean/bad_error2.lean.expected.out new file mode 100644 index 0000000000..838f3039fa --- /dev/null +++ b/tests/lean/bad_error2.lean.expected.out @@ -0,0 +1,9 @@ +bad_error2.lean:8:6: error: rewrite tactic failed, did not find instance of the pattern in the target expression + ?m_1 + ?m_2 + ?m_3 +state: +k n m : ℕ, +h : k + n ≤ k + m, +_match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m, +w : ℕ, +hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w +⊢ n + w = m