From e22ccb4d1ff678ae057e05821bddfb6609db6950 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 3 Jun 2017 19:43:07 -0700 Subject: [PATCH] feat(library/tactic/tactic_state): improve error message for unify and is_def_eq tactics closes #1639 --- src/library/tactic/tactic_state.cpp | 34 ++++- tests/lean/1639.lean | 20 +++ tests/lean/1639.lean.expected.out | 176 ++++++++++++++++++++++++ tests/lean/unify_tac1.lean.expected.out | 5 +- 4 files changed, 228 insertions(+), 7 deletions(-) create mode 100644 tests/lean/1639.lean create mode 100644 tests/lean/1639.lean.expected.out diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 473a8880f3..c545281835 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -426,6 +426,23 @@ vm_obj tactic_mk_instance(vm_obj const & e, vm_obj const & s0) { } } +static vm_obj mk_unify_exception(char const * header, expr const & e1, expr const & e2, tactic_state const & s) { + auto thunk = [=]() { + format r(header); + unsigned indent = get_pp_indent(s.get_options()); + formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); + type_context ctx = mk_type_context_for(s, transparency_mode::All); + formatter fmt = fmtf(s.env(), s.get_options(), ctx); + expr e1_type = ctx.infer(e1); + expr e2_type = ctx.infer(e2); + r += nest(indent, line() + group(fmt(e1) + line() + format(": ") + fmt(e1_type))); + r += line() + format("and"); + r += nest(indent, line() + group(fmt(e2) + line() + format(": ") + fmt(e2_type))); + return r; + }; + return tactic::mk_exception(thunk, s); +} + vm_obj tactic_unify(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & s0) { tactic_state const & s = tactic::to_state(s0); type_context ctx = mk_type_context_for(s, to_transparency_mode(t)); @@ -433,10 +450,12 @@ vm_obj tactic_unify(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_o check_closed("unify", to_expr(e1)); check_closed("unify", to_expr(e2)); bool r = ctx.is_def_eq(to_expr(e1), to_expr(e2)); - if (r) + if (r) { return tactic::mk_success(set_mctx(s, ctx.mctx())); - else - return tactic::mk_exception("unify tactic failed", s); + } else { + return mk_unify_exception("unify tactic failed, failed to unify", + to_expr(e1), to_expr(e2), s); + } } catch (exception & ex) { return tactic::mk_exception(ex, s); } @@ -450,10 +469,13 @@ vm_obj tactic_is_def_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, check_closed("is_def_eq", to_expr(e1)); check_closed("is_def_eq", to_expr(e2)); bool r = ctx.is_def_eq(to_expr(e1), to_expr(e2)); - if (r) + if (r) { return tactic::mk_success(s); - else - return tactic::mk_exception("is_def_eq failed", s); + } else { + return mk_unify_exception("is_def_eq tactic failed, the following expressions are not definitionally equal " + "(remark: is_def_eq tactic does modify the metavariable assignment)", + to_expr(e1), to_expr(e2), s); + } } catch (exception & ex) { return tactic::mk_exception(ex, s); } diff --git a/tests/lean/1639.lean b/tests/lean/1639.lean new file mode 100644 index 0000000000..91ab40cc93 --- /dev/null +++ b/tests/lean/1639.lean @@ -0,0 +1,20 @@ +def some_lets : ℕ → ℕ → ℕ +| 0 v := v +| (nat.succ n) v := let k := some_lets n v + some_lets n v in some_lets n k + +def some_unfolded_lets (n : ℕ) : Σ' v : ℕ , v = some_lets 5 n := +begin + constructor; unfold some_lets; constructor +end + +meta def foo : tactic unit := + do [g] <- tactic.get_goals, + tactic.to_expr (``(1)) >>= tactic.unify g +def some_lifted_lets (n : ℕ) : Σ' (v : ℕ), v = psigma.fst (some_unfolded_lets n) := +begin + constructor; unfold some_unfolded_lets psigma.fst; symmetry; transitivity; symmetry; + { + foo -- unify_reify_rhs_to_let_in + } + +end diff --git a/tests/lean/1639.lean.expected.out b/tests/lean/1639.lean.expected.out new file mode 100644 index 0000000000..6136f4e703 --- /dev/null +++ b/tests/lean/1639.lean.expected.out @@ -0,0 +1,176 @@ +1639.lean:17:4: error: unify tactic failed, failed to unify + ?m_1 + : ?m_2 = + let k : ℕ := + (let k : ℕ := + (let k : ℕ := + (let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k) + + let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k) + + let k : ℕ := + (let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k) + + let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k) + + let k : ℕ := + (let k : ℕ := + (let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k) + + let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k) + + let k : ℕ := + (let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k) + + let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := + (let k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k) + + let k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k +and + 1 : ℕ +state: +n : ℕ +⊢ ?m_1 = + let k : ℕ := + (let k : ℕ := + (let k : ℕ := + (let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k) + + let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k) + + let k : ℕ := + (let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k) + + let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k) + + let k : ℕ := + (let k : ℕ := + (let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k) + + let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k) + + let k : ℕ := + (let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k) + + let k : ℕ := (let k : ℕ := n + n in k) + let k : ℕ := n + n in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := + (let k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k) + + let k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := + (let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, k : ℕ := k + k in k) + + let k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k, + k : ℕ := (let k : ℕ := k + k in k) + let k : ℕ := k + k in k, + k : ℕ := k + k + in k diff --git a/tests/lean/unify_tac1.lean.expected.out b/tests/lean/unify_tac1.lean.expected.out index 197a97230d..8c57fd7ec8 100644 --- a/tests/lean/unify_tac1.lean.expected.out +++ b/tests/lean/unify_tac1.lean.expected.out @@ -1,4 +1,7 @@ -unify_tac1.lean:12:3: error: is_def_eq failed +unify_tac1.lean:12:3: error: is_def_eq tactic failed, the following expressions are not definitionally equal (remark: is_def_eq tactic does modify the metavariable assignment) + p ?m_1 : Prop +and + p a : Prop state: A : Type, a : A,