From 1557a579eddc37502400eb5f1bb25e53ed237ab8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Feb 2015 16:29:04 -0800 Subject: [PATCH] feat(library/tactic/proof_state): add report_failure flag to proof state tactic can use the flag to produce nice error messages --- src/library/tactic/proof_state.cpp | 5 +++-- src/library/tactic/proof_state.h | 14 ++++++++++---- src/library/tactic/tactic.cpp | 27 ++++++++++++++++++--------- 3 files changed, 31 insertions(+), 15 deletions(-) diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 12851193a..e624f3646 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -31,8 +31,9 @@ bool get_proof_state_goal_names(options const & opts) { } proof_state::proof_state(goals const & gs, substitution const & s, name_generator const & ngen, - constraints const & postponed, bool relax_main_opaque): - m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed), m_relax_main_opaque(relax_main_opaque) { + constraints const & postponed, bool relax_main_opaque, bool report_failure): + m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed), m_relax_main_opaque(relax_main_opaque), + m_report_failure(report_failure) { if (std::any_of(gs.begin(), gs.end(), [&](goal const & g) { return s.is_assigned(g.get_mvar()); })) { m_goals = filter(gs, [&](goal const & g) { return !s.is_assigned(g.get_mvar()); }); diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index b033531b6..e201024c7 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -22,17 +22,18 @@ class proof_state { name_generator m_ngen; constraints m_postponed; bool m_relax_main_opaque; + bool m_report_failure; format pp_core(std::function const & mk_fmt, options const & opts) const; public: proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed, - bool relax_main_opaque); + bool relax_main_opaque, bool report_failure = true); proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen, constraints const & postponed): - proof_state(gs, subst, ngen, postponed, s.relax_main_opaque()) {} + proof_state(gs, subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {} proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen): - proof_state(gs, subst, ngen, s.m_postponed, s.m_relax_main_opaque) {} + proof_state(gs, subst, ngen, s.m_postponed, s.relax_main_opaque(), s.report_failure()) {} proof_state(proof_state const & s, goals const & gs, substitution const & subst): proof_state(s, gs, subst, s.m_ngen) {} proof_state(proof_state const & s, goals const & gs, name_generator const & ngen): @@ -40,15 +41,20 @@ public: proof_state(proof_state const & s, goals const & gs): proof_state(s, gs, s.m_subst) {} proof_state(proof_state const & s, name_generator const & ngen, constraints const & postponed): - proof_state(s.m_goals, s.m_subst, ngen, postponed, s.m_relax_main_opaque) {} + proof_state(s.m_goals, s.m_subst, ngen, postponed, s.relax_main_opaque(), s.report_failure()) {} proof_state(proof_state const & s, name_generator const & ngen): proof_state(s, ngen, s.m_postponed) {} + proof_state update_report_failure(bool f) const { + return m_report_failure == f ? *this : proof_state(m_goals, m_subst, m_ngen, m_postponed, m_relax_main_opaque, f); + } + goals const & get_goals() const { return m_goals; } substitution const & get_subst() const { return m_subst; } name_generator const & get_ngen() const { return m_ngen; } constraints const & get_postponed() const { return m_postponed; } bool relax_main_opaque() const { return m_relax_main_opaque; } + bool report_failure() const { return m_report_failure; } /** \brief Return true iff this state does not have any goals left */ bool is_final_state() const { return empty(m_goals); } diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index b920a416b..1fbf4b4c7 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -97,7 +97,8 @@ tactic then(tactic const & t1, tactic const & t2) { } tactic orelse(tactic const & t1, tactic const & t2) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { + proof_state s = _s.update_report_failure(false); return orelse(t1(env, ios, s), t2(env, ios, s), "ORELSE tactical"); }); } @@ -137,31 +138,36 @@ tactic rotate_right(unsigned n) { } tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { + proof_state s = _s.update_report_failure(false); return timeout(t(env, ios, s), ms, check_ms); }); } tactic append(tactic const & t1, tactic const & t2) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { + proof_state s = _s.update_report_failure(false); return append(t1(env, ios, s), t2(env, ios, s), "APPEND tactical"); }); } tactic interleave(tactic const & t1, tactic const & t2) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { + proof_state s = _s.update_report_failure(false); return interleave(t1(env, ios, s), t2(env, ios, s), "INTERLEAVE tactical"); }); } tactic par(tactic const & t1, tactic const & t2, unsigned check_ms) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { + proof_state s = _s.update_report_failure(false); return par(t1(env, ios, s), t2(env, ios, s), check_ms); }); } tactic repeat(tactic const & t) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s1) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s1) -> proof_state_seq { + proof_state s1 = _s1.update_report_failure(false); return repeat(s1, [=](proof_state const & s2) { return t(env, ios, s2); }, "REPEAT tactical"); @@ -169,7 +175,8 @@ tactic repeat(tactic const & t) { } tactic repeat_at_most(tactic const & t, unsigned k) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s1) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s1) -> proof_state_seq { + proof_state s1 = _s1.update_report_failure(false); return repeat_at_most(s1, [=](proof_state const & s2) { return t(env, ios, s2); }, k, "REPEAT_AT_MOST tactical"); @@ -177,13 +184,15 @@ tactic repeat_at_most(tactic const & t, unsigned k) { } tactic take(tactic const & t, unsigned k) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { + proof_state s = _s.update_report_failure(false); return take(k, t(env, ios, s)); }); } tactic discard(tactic const & t, unsigned k) { - return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + return tactic([=](environment const & env, io_state const & ios, proof_state const & _s) -> proof_state_seq { + proof_state s = _s.update_report_failure(false); auto r = t(env, ios, s); for (unsigned i = 0; i < k; i++) { auto m = r.pull();