From 680ec8abba0814ba01a375170b39508fce2cfb1d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2013 15:31:55 -0800 Subject: [PATCH] refactor(library/tactic): reorganize tactic API, add assumption_tactic Signed-off-by: Leonardo de Moura --- src/library/tactic/goal.h | 2 + src/library/tactic/proof_state.cpp | 35 +++++----- src/library/tactic/proof_state.h | 22 +++++-- src/library/tactic/tactic.cpp | 99 +++++++++++++++++++++-------- src/library/tactic/tactic.h | 55 +++++++++++++--- src/tests/library/tactic/tactic.cpp | 19 ++++++ 6 files changed, 175 insertions(+), 57 deletions(-) diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 30c4094c8..d8fa4300c 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -18,9 +18,11 @@ class goal { list> m_hypotheses; expr m_conclusion; public: + goal() {} goal(list> const & h, expr const & c); list> const & get_hypotheses() const { return m_hypotheses; } expr const & get_conclusion() const { return m_conclusion; } + operator bool() const { return m_conclusion; } }; /** diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 33a54883b..a9c2b4d8c 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura namespace lean { void swap(proof_state & s1, proof_state & s2) { - swap(s1.m_env, s2.m_env); swap(s1.m_goals, s2.m_goals); swap(s1.m_menv, s2.m_menv); swap(s1.m_proof_builder, s2.m_proof_builder); @@ -20,22 +19,22 @@ void swap(proof_state & s1, proof_state & s2) { static name g_main("main"); proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) { - auto p = to_goal(env, ctx, t); - goal g = p.first; - goal_proof_fn fn = p.second; - return proof_state(env, - goals(mk_pair(g_main, g)), - metavar_env(), - mk_proof_builder([=](proof_map const & m, environment const &, assignment const &) -> expr { - expr p = find(m, g_main); - if (!p) - throw tactic_exception(sstream() << "failed to find proof for '" << g_main << "' goal"); - return fn(p); - }), - mk_justification_builder([](name const & n, justification const & j, environment const &, assignment const &) -> justification { - if (n != g_main) - throw tactic_exception(sstream() << "unknown goal name '" << n << "'"); - return j; - })); + auto gfn = to_goal(env, ctx, t); + goal g = gfn.first; + goal_proof_fn fn = gfn.second; + proof_builder p = mk_proof_builder( + [=](proof_map const & m, environment const &, assignment const &) -> expr { + expr p = find(m, g_main); + if (!p) + throw tactic_exception(sstream() << "failed to find proof for '" << g_main << "' goal"); + return fn(p); + }); + justification_builder j = mk_justification_builder( + [](name const & n, justification const & j, environment const &, assignment const &) -> justification { + if (n != g_main) + throw tactic_exception(sstream() << "unknown goal name '" << n << "'"); + return j; + }); + return proof_state(goals(mk_pair(g_main, g)), metavar_env(), p, j); } } diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 32d8e4947..2590b8477 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -13,17 +13,17 @@ Author: Leonardo de Moura namespace lean { typedef list> goals; class proof_state { - environment m_env; goals m_goals; metavar_env m_menv; proof_builder m_proof_builder; justification_builder m_justification_builder; public: proof_state() {} - proof_state(environment const & env, list> const & gs, metavar_env const & menv, proof_builder const & p, justification_builder const & j): - m_env(env), m_goals(gs), m_menv(menv), m_proof_builder(p), m_justification_builder(j) {} + proof_state(list> const & gs, metavar_env const & menv, proof_builder const & p, justification_builder const & j): + m_goals(gs), m_menv(menv), m_proof_builder(p), m_justification_builder(j) {} + proof_state(proof_state const & s, goals const & gs, proof_builder const & p): + m_goals(gs), m_menv(s.m_menv), m_proof_builder(p), m_justification_builder(s.m_justification_builder) {} friend void swap(proof_state & s1, proof_state & s2); - environment const & get_environment() const { return m_env; } list> const & get_goals() const { return m_goals; } metavar_env const & get_menv() const { return m_menv; } proof_builder const & get_proof_builder() const { return m_proof_builder; } @@ -32,4 +32,18 @@ public: void swap(proof_state & s1, proof_state & s2); proof_state to_proof_state(environment const & env, context const & ctx, expr const & t); + +template +goals map_goals(proof_state const & s, F && f) { + return map_filter(s.get_goals(), [=](std::pair const & in, std::pair & out) -> bool { + goal new_goal = f(in.first, in.second); + if (new_goal) { + out.first = in.first; + out.second = new_goal; + return true; + } else { + return false; + } + }); +} } diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 23237b328..27bf23d26 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -4,17 +4,37 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include +#include "util/interrupt.h" +#include "library/tactic/tactic_exception.h" #include "library/tactic/tactic.h" namespace lean { tactic_result::~tactic_result() { } void tactic_result::interrupt() { - m_result = true; + m_interrupted = true; } void tactic_result::request_interrupt() { - std::lock_guard lock(m_mutex); - interrupt(); + { + std::lock_guard lock(m_mutex); + interrupt(); + } + ::lean::request_interrupt(); +} + +proof_state_ref tactic_result::next(environment const & env, state const & s) { + try { + return next_core(env, s); + } catch (interrupted &) { + if (m_interrupted) { + // promote to tactic_exception if tactic is marked as interrupted + throw tactic_exception("interrupted"); + } else { + // if tactic was not interrupted, then continue propagating interrupted exception + throw; + } + } } tactic_cell::~tactic_cell() { @@ -28,25 +48,6 @@ tactic & tactic::operator=(tactic && s) { LEAN_MOVE_REF(tactic, s); } -class id_tactic : public tactic_cell { -public: - class result : public tactic_result { - proof_state_ref m_r; - public: - result(proof_state const & s):m_r(new proof_state(s)) {} - - virtual proof_state_ref next() { - return proof_state_ref(std::move(m_r)); - } - }; - - virtual tactic_result_ref operator()(proof_state const & s) const { - return tactic_result_ref(new result(s)); - } -}; - -tactic idtac() { return tactic(new id_tactic()); } - class then_tactic : public tactic_cell { tactic m_t1; tactic m_t2; @@ -67,9 +68,9 @@ public: public: result(tactic_result_ref && r1, tactic const & t2):m_r1(std::move(r1)), m_t2(t2) {} - virtual proof_state_ref next() { + virtual proof_state_ref next_core(environment const & env, state const & s) { if (m_r2) { - proof_state_ref s2 = m_r2->next(); + proof_state_ref s2 = m_r2->next(env, s); if (s2) return s2; m_r2.release(); @@ -77,20 +78,64 @@ public: } lean_assert(!m_r2); lean_assert(!m_s1); - proof_state_ref new_s1(m_r1->next()); + proof_state_ref new_s1(m_r1->next(env, s)); if (!new_s1) return proof_state_ref(); // done, m_r1 has no more solutions m_s1.swap(new_s1); tactic_result_ref r2 = m_t2(proof_state(*m_s1)); exclusive_update([&]() { m_r2.swap(r2); }); // must protect because interrupt() may be invoked from different thread - return m_r2->next(); + return m_r2->next(env, s); } }; - virtual tactic_result_ref operator()(proof_state const & s) const { + virtual tactic_result_ref operator()(proof_state const & s) { return tactic_result_ref(new result(m_t1(s), m_t2)); } }; tactic then(tactic const & t1, tactic const & t2) { return tactic(new then_tactic(t1, t2)); } + +tactic id_tactic() { return mk_tactic([](environment const &, state const &, proof_state const & s) -> proof_state { return s; }); } + +tactic fail_tactic() { return mk_tactic([](environment const &, state const &, proof_state const &) -> proof_state { throw tactic_exception("failed"); }); } + +tactic now_tactic() { + return mk_tactic([](environment const &, state const &, proof_state const & s) -> proof_state { + if (!empty(s.get_goals())) + throw tactic_exception("nowtac failed"); + return s; + }); +} + +tactic assumption_tactic() { + return mk_tactic([](environment const &, state const &, proof_state const & s) -> proof_state { + list> proofs; + goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { + expr const & c = g.get_conclusion(); + expr pr; + for (auto const & p : g.get_hypotheses()) { + check_interrupted(); + if (p.second == c) { + pr = mk_constant(p.first); + break; + } + } + if (pr) { + proofs.emplace_front(ng, pr); + return goal(); + } else { + return g; + } + }); + proof_builder p = s.get_proof_builder(); + proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { + proof_map new_m(m); + for (auto const & np : proofs) { + new_m.insert(np.first, np.second); + } + return p(new_m, env, a); + }); + return proof_state(s, new_goals, new_p); + }); +} } diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 139b3952d..1bb255b8c 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include "library/state.h" #include "library/tactic/proof_state.h" namespace lean { @@ -16,8 +17,8 @@ class tactic_result; typedef std::unique_ptr tactic_result_ref; class tactic_result { - std::mutex m_mutex; - bool m_result; + std::mutex m_mutex; + std::atomic m_interrupted; protected: template void exclusive_update(F && f) { @@ -26,12 +27,12 @@ protected: } virtual void interrupt(); void propagate_interrupt(tactic_result_ref & r) { if (r) r->interrupt(); } + virtual proof_state_ref next_core(environment const & env, state const & s) = 0; public: - tactic_result():m_result(false) {} - bool interrupted() const { return m_result; } + tactic_result():m_interrupted(false) {} void request_interrupt(); + proof_state_ref next(environment const & env, state const & s); virtual ~tactic_result(); - virtual proof_state_ref next() = 0; }; class tactic_cell { @@ -39,7 +40,7 @@ class tactic_cell { MK_LEAN_RC(); public: virtual ~tactic_cell(); - virtual tactic_result_ref operator()(proof_state const & s) const = 0; + virtual tactic_result_ref operator()(proof_state const & s) = 0; }; class tactic { @@ -54,9 +55,47 @@ public: tactic & operator=(tactic const & s); tactic & operator=(tactic && s); - tactic_result_ref operator()(proof_state const & s) const { return m_ptr->operator()(s); } + tactic_result_ref operator()(proof_state const & s) { return m_ptr->operator()(s); } }; -tactic idtac(); +template +class simple_tactic_cell : public tactic_cell { + F m_f; +public: + simple_tactic_cell(F && f):m_f(f) {} + + class result : public tactic_result { + simple_tactic_cell * m_cell; + proof_state m_in; + public: + result(simple_tactic_cell * c, proof_state const & in):m_cell(c), m_in(in) { + lean_assert(m_cell); + m_cell->inc_ref(); + } + virtual ~result() { if (m_cell) m_cell->dec_ref(); } + virtual proof_state_ref next_core(environment const & env, state const & io) { + if (m_cell) { + proof_state_ref r(new proof_state(m_cell->m_f(env, io, m_in))); + m_cell = nullptr; + return std::move(r); + } else { + return proof_state_ref(); + } + } + }; + + virtual tactic_result_ref operator()(proof_state const & s) { + return tactic_result_ref(new result(this, s)); + } +}; + + +template +tactic mk_tactic(F && f) { return tactic(new simple_tactic_cell(std::forward(f))); } + +tactic id_tactic(); +tactic fail_tactic(); +tactic now_tactic(); +tactic assumption_tactic(); tactic then(tactic const & t1, tactic const & t2); } diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index 98d0ff59d..668ac7343 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/test.h" +#include "kernel/builtin.h" +#include "library/all/all.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" #include "library/tactic/justification_builder.h" @@ -12,6 +14,23 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" using namespace lean; +static void tst1() { + environment env; + import_all(env); + env.add_var("p", Bool); + env.add_var("q", Bool); + expr p = Const("p"); + expr q = Const("q"); + context ctx; + ctx = extend(ctx, "H1", p); + ctx = extend(ctx, "H2", q); + // proof_state s1 = to_proof_state(env, ctx, mk_var(0)); + // tactic t = then(assumption_tactic(), now_tactic()); + // tactic_result_ref r = t(s1); + // proof_state_ref s2 = r->next(); +} + int main() { + tst1(); return has_violations() ? 1 : 0; }