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

feat(library/tactic/proof_state): add report_failure flag to proof state

Browse source 
tactic can use the flag to produce nice error messages
This commit is contained in:
Leonardo de Moura 2015-02-06 16:29:04 -08:00
parent 2126b8ec9a
commit 1557a579ed
3 changed files with 31 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/tactic/proof_state.cpp
View file

@ -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, proof_state::proof_state(goals const & gs, substitution const & s, name_generator const & ngen,
constraints const & postponed, bool 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_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(), if (std::any_of(gs.begin(), gs.end(),
[&](goal const & g) { return s.is_assigned(g.get_mvar()); })) { [&](goal const & g) { return s.is_assigned(g.get_mvar()); })) {
m_goals = filter(gs, [&](goal const & g) { return !s.is_assigned(g.get_mvar()); }); m_goals = filter(gs, [&](goal const & g) { return !s.is_assigned(g.get_mvar()); });

14
src/library/tactic/proof_state.h
View file

@ -22,17 +22,18 @@ class proof_state {
name_generator m_ngen; name_generator m_ngen;
constraints m_postponed; constraints m_postponed;
bool m_relax_main_opaque; bool m_relax_main_opaque;
bool m_report_failure;
format pp_core(std::function<formatter()> const & mk_fmt, options const & opts) const; format pp_core(std::function<formatter()> const & mk_fmt, options const & opts) const;
public: public:
proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed, 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, proof_state(proof_state const & s, goals const & gs, substitution const & subst, name_generator const & ngen,
constraints const & postponed): 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(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(proof_state const & s, goals const & gs, substitution const & subst):
proof_state(s, gs, subst, s.m_ngen) {} proof_state(s, gs, subst, s.m_ngen) {}
proof_state(proof_state const & s, goals const & gs, name_generator const & 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(proof_state const & s, goals const & gs):
proof_state(s, gs, s.m_subst) {} proof_state(s, gs, s.m_subst) {}
proof_state(proof_state const & s, name_generator const & ngen, constraints const & postponed): 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(proof_state const & s, name_generator const & ngen):
proof_state(s, ngen, s.m_postponed) {} 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; } goals const & get_goals() const { return m_goals; }
substitution const & get_subst() const { return m_subst; } substitution const & get_subst() const { return m_subst; }
name_generator const & get_ngen() const { return m_ngen; } name_generator const & get_ngen() const { return m_ngen; }
constraints const & get_postponed() const { return m_postponed; } constraints const & get_postponed() const { return m_postponed; }
bool relax_main_opaque() const { return m_relax_main_opaque; } 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 */ /** \brief Return true iff this state does not have any goals left */
bool is_final_state() const { return empty(m_goals); } bool is_final_state() const { return empty(m_goals); }

27
src/library/tactic/tactic.cpp
View file

@ -97,7 +97,8 @@ tactic then(tactic const & t1, tactic const & t2) {
} }
tactic orelse(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"); 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) { 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); return timeout(t(env, ios, s), ms, check_ms);
}); });
} }
tactic append(tactic const & t1, tactic const & t2) { 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"); return append(t1(env, ios, s), t2(env, ios, s), "APPEND tactical");
}); });
} }
tactic interleave(tactic const & t1, tactic const & t2) { 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"); return interleave(t1(env, ios, s), t2(env, ios, s), "INTERLEAVE tactical");
}); });
} }
tactic par(tactic const & t1, tactic const & t2, unsigned check_ms) { 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); return par(t1(env, ios, s), t2(env, ios, s), check_ms);
}); });
} }
tactic repeat(tactic const & t) { 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 repeat(s1, [=](proof_state const & s2) {
return t(env, ios, s2); return t(env, ios, s2);
}, "REPEAT tactical"); }, "REPEAT tactical");
@ -169,7 +175,8 @@ tactic repeat(tactic const & t) {
} }
tactic repeat_at_most(tactic const & t, unsigned k) { 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 repeat_at_most(s1, [=](proof_state const & s2) {
return t(env, ios, s2); return t(env, ios, s2);
}, k, "REPEAT_AT_MOST tactical"); }, 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) { 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)); return take(k, t(env, ios, s));
}); });
} }
tactic discard(tactic const & t, unsigned k) { 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); auto r = t(env, ios, s);
for (unsigned i = 0; i < k; i++) { for (unsigned i = 0; i < k; i++) {
auto m = r.pull(); auto m = r.pull();