From ce1cbcc2052dd2495690bc1d90dc0606325a98df Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Mon, 19 Oct 2015 19:35:22 -0400 Subject: [PATCH] feat(library/norm_num): give better error message when norm_num fails --- src/library/tactic/norm_num_tactic.cpp | 23 +++++++++++++++-------- tests/lean/extra/num_norm1.lean | 1 - 2 files changed, 15 insertions(+), 9 deletions(-) diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/tactic/norm_num_tactic.cpp index 9e8ac164fb..01a18d476a 100644 --- a/src/library/tactic/norm_num_tactic.cpp +++ b/src/library/tactic/norm_num_tactic.cpp @@ -39,16 +39,23 @@ tactic norm_num_tactic() { pair p2 = mk_norm_num(env, ctx, rhs); expr new_rhs = p2.first; expr new_rhs_pr = p2.second; - /*if (new_lhs != new_rhs) { + auto v_lhs = to_num(new_lhs), v_rhs = to_num(new_rhs); + if (v_lhs && v_rhs) { + if ( *v_lhs == *v_rhs) { + type_checker tc(env); + expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr)); + substitution new_subst = s.get_subst(); + assign(new_subst, g, g_prf); + return some_proof_state(proof_state(s, tail(gs), new_subst)); + } else { std::cout << "lhs: " << new_lhs << ", rhs: " << new_rhs << "\n"; - throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs normal form doesn't match rhs"); + throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs doesn't match rhs"); return none_proof_state(); - }*/ - type_checker tc(env); - expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr)); - substitution new_subst = s.get_subst(); - assign(new_subst, g, g_prf); - return some_proof_state(proof_state(s, tail(gs), new_subst)); + } + } else { + throw_tactic_exception_if_enabled(s, "norm_num tactic failed, one side is not a numeral"); + return none_proof_state(); + } } catch (exception & ex) { throw_tactic_exception_if_enabled(s, ex.what()); return none_proof_state(); diff --git a/tests/lean/extra/num_norm1.lean b/tests/lean/extra/num_norm1.lean index f4c6c9988c..11bcd6c7c7 100644 --- a/tests/lean/extra/num_norm1.lean +++ b/tests/lean/extra/num_norm1.lean @@ -25,7 +25,6 @@ example : (7 : A) = 1 + 6 := by norm_num example : (7 : A) = 6 + 1 := by norm_num example : 33 = 5 + (28 : A) := by norm_num - example : (12 : A) = 0 + (2 + 3) + 7 := by norm_num example : (105 : A) = 70 + (33 + 2) := by norm_num example : (45000000000 : A) = 23000000000 + 22000000000 := by norm_num