michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/norm_num): give better error message when norm_num fails

Browse source
This commit is contained in:
Rob Lewis 2015-10-19 19:35:22 -04:00 committed by Leonardo de Moura
parent eb0b688da8
commit ce1cbcc205
2 changed files with 15 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/library/tactic/norm_num_tactic.cpp
View file

@ -39,16 +39,23 @@ tactic norm_num_tactic() {
pair<expr, expr> 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();

1
tests/lean/extra/num_norm1.lean
View file

@ -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