From 9fd594533d0040076255f1a7bfd7b04a1c70ff24 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Nov 2013 18:39:33 -0800 Subject: [PATCH] refactor(library/tactic): simplify tactic framework, add orelse and try_for combinators/tacticals Signed-off-by: Leonardo de Moura --- src/library/tactic/proof_builder.h | 3 +- src/library/tactic/proof_state.cpp | 2 +- src/library/tactic/tactic.cpp | 176 +++++++++++++------------- src/library/tactic/tactic.h | 63 ++------- src/library/tactic/tactic_exception.h | 13 +- src/tests/library/tactic/tactic.cpp | 61 ++++++++- 6 files changed, 167 insertions(+), 151 deletions(-) diff --git a/src/library/tactic/proof_builder.h b/src/library/tactic/proof_builder.h index c9f4773d3..0f49592fd 100644 --- a/src/library/tactic/proof_builder.h +++ b/src/library/tactic/proof_builder.h @@ -22,6 +22,7 @@ class proof_builder_cell { void dealloc() { delete this; } MK_LEAN_RC(); public: + proof_builder_cell():m_rc(0) {} virtual ~proof_builder_cell() {} virtual expr operator()(proof_map const & p, environment const & env, assignment const & a) const = 0; }; @@ -46,7 +47,7 @@ template class simple_proof_builder : public proof_builder_cell { F m_f; public: - simple_proof_builder(F && f):m_f(std::forward(f)) {} + simple_proof_builder(F && f):m_f(f) {} virtual expr operator()(proof_map const & p, environment const & env, assignment const & a) const { return m_f(p, env, a); } }; diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 628ec6904..b867c28dc 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -38,7 +38,7 @@ proof_state to_proof_state(environment const & env, context const & ctx, expr co [=](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"); + throw exception(sstream() << "failed to find proof for '" << g_main << "' goal"); return fn(p); }); return proof_state(goals(mk_pair(g_main, g)), metavar_env(), p); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 5cff2f8de..39b89077a 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -5,41 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "util/interrupt.h" +#include "util/lazy_list_fn.h" #include "library/tactic/tactic_exception.h" #include "library/tactic/tactic.h" namespace lean { -tactic_result::~tactic_result() { -} -void tactic_result::interrupt() { - m_interrupted = true; -} -void tactic_result::request_interrupt() { - { - std::lock_guard lock(m_mutex); - interrupt(); - } - ::lean::request_interrupt(); -} - -proof_state_ref tactic_result::next(environment const & env, io_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() { -} - tactic & tactic::operator=(tactic const & s) { LEAN_COPY_REF(tactic, s); } @@ -49,15 +21,13 @@ tactic & tactic::operator=(tactic && s) { } expr tactic::solve(environment const & env, io_state const & io, proof_state const & s) { - tactic_result_ref r = operator()(s); - proof_state_ref final = r->next(env, io); - if (!final) - throw tactic_exception("tactic did not produce any result"); - if (!empty(final->get_goals())) - throw tactic_exception("tactic did not solve all goals"); - assignment a(final->get_menv()); + proof_state_seq r = operator()(env, io, s); + if (!r) + throw exception("tactic failed to solve input"); + proof_state final = head(r); + assignment a(final.get_menv()); proof_map m; - return final->get_proof_builder()(m, env, a); + return final.get_proof_builder()(m, env, a); } expr tactic::solve(environment const & env, io_state const & io, context const & ctx, expr const & t) { @@ -65,20 +35,29 @@ expr tactic::solve(environment const & env, io_state const & io, context const & return solve(env, io, s); } -tactic id_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state { return s; }); } +tactic id_tactic() { + return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { + return proof_state_seq(s); + }); +} -tactic fail_tactic() { return mk_tactic([](environment const &, io_state const &, proof_state const &) -> proof_state { throw tactic_exception("failed"); }); } +tactic fail_tactic() { + return mk_tactic([](environment const &, io_state const &, proof_state const &) -> proof_state_seq { + return proof_state_seq(); + }); +} tactic now_tactic() { - return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { if (!empty(s.get_goals())) - throw tactic_exception("nowtac failed"); - return s; + return proof_state_seq(); + else + return proof_state_seq(s); }); } tactic assumption_tactic() { - return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { list> proofs; goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { expr const & c = g.get_conclusion(); @@ -105,54 +84,69 @@ tactic assumption_tactic() { } return p(new_m, env, a); }); - return proof_state(s, new_goals, new_p); + return proof_state_seq(proof_state(s, new_goals, new_p)); }); } -class then_tactic : public tactic_cell { - tactic m_t1; - tactic m_t2; -public: - then_tactic(tactic const & t1, tactic const & t2):m_t1(t1), m_t2(t2) {} - - class result : public tactic_result { - tactic_result_ref m_r1; - proof_state_ref m_s1; - tactic m_t2; - tactic_result_ref m_r2; - protected: - virtual void interrupt() { - tactic_result::interrupt(); - propagate_interrupt(m_r1); - propagate_interrupt(m_r2); - } - public: - result(tactic_result_ref && r1, tactic const & t2):m_r1(std::move(r1)), m_t2(t2) {} - - virtual proof_state_ref next_core(environment const & env, io_state const & s) { - if (m_r2) { - proof_state_ref s2 = m_r2->next(env, s); - if (s2) - return s2; - m_r2.release(); - m_s1.release(); - } - lean_assert(!m_r2); - lean_assert(!m_s1); - 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(env, s); - } - }; - - 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 then(tactic t1, tactic t2) { + return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { + tactic _t1(t1); + return map_append(_t1(env, io, s1), [=](proof_state const & s2) { + check_interrupted(); + tactic _t2(t2); + return _t2(env, io, s2); + }); + }); +} + +tactic orelse(tactic t1, tactic t2) { + return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + tactic _t1(t1); + proof_state_seq r = _t1(env, io, s); + if (r) { + return r; + } else { + check_interrupted(); + tactic _t2(t2); + return _t2(env, io, s); + } + }); +} + +tactic try_for(tactic t, unsigned ms, unsigned check_ms) { + if (check_ms == 0) + check_ms = 1; + return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + tactic _t(t); + proof_state_seq r; + std::atomic done(false); + interruptible_thread th([&]() { + try { + r = _t(env, io, s); + } catch (...) { + r = proof_state_seq(); + } + done = true; + }); + try { + auto start = std::chrono::steady_clock::now(); + std::chrono::milliseconds d(ms); + std::chrono::milliseconds one(1); + while (!done) { + auto curr = std::chrono::steady_clock::now(); + if (std::chrono::duration_cast(curr - start) > d) + break; + check_interrupted(); + std::this_thread::sleep_for(one); + } + th.request_interrupt(); + th.join(); + return r; + } catch (...) { + th.request_interrupt(); + th.join(); + throw; + } + }); +} } diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 43e1ce264..cebd74713 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -6,41 +6,24 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include #include +#include "util/interrupt.h" +#include "util/lazy_list.h" #include "library/io_state.h" #include "library/tactic/proof_state.h" namespace lean { -typedef std::unique_ptr proof_state_ref; -class tactic_result; -typedef std::unique_ptr tactic_result_ref; - -class tactic_result { - std::mutex m_mutex; - std::atomic m_interrupted; -protected: - template - void exclusive_update(F && f) { - std::lock_guard lock(m_mutex); - f(); - } - virtual void interrupt(); - void propagate_interrupt(tactic_result_ref & r) { if (r) r->interrupt(); } - virtual proof_state_ref next_core(environment const & env, io_state const & s) = 0; -public: - tactic_result():m_interrupted(false) {} - void request_interrupt(); - proof_state_ref next(environment const & env, io_state const & s); - virtual ~tactic_result(); -}; +typedef lazy_list proof_state_seq; class tactic_cell { void dealloc() { delete this; } MK_LEAN_RC(); public: - virtual ~tactic_cell(); - virtual tactic_result_ref operator()(proof_state const & s) = 0; + tactic_cell():m_rc(0) {} + virtual ~tactic_cell() {} + virtual proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) = 0; }; class tactic { @@ -55,7 +38,7 @@ public: tactic & operator=(tactic const & s); tactic & operator=(tactic && s); - tactic_result_ref operator()(proof_state const & s) { return m_ptr->operator()(s); } + proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) { return m_ptr->operator()(env, io, s); } expr solve(environment const & env, io_state const & io, proof_state const & s); expr solve(environment const & env, io_state const & io, context const & ctx, expr const & t); @@ -66,29 +49,8 @@ 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, io_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)); + virtual proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) { + return m_f(env, io, s); } }; @@ -99,5 +61,8 @@ tactic id_tactic(); tactic fail_tactic(); tactic now_tactic(); tactic assumption_tactic(); -tactic then(tactic const & t1, tactic const & t2); +tactic then(tactic t1, tactic t2); +tactic orelse(tactic t1, tactic t2); +tactic try_for(tactic t, unsigned ms, unsigned check_ms = g_small_sleep); +tactic repeat(tactic t1); } diff --git a/src/library/tactic/tactic_exception.h b/src/library/tactic/tactic_exception.h index 7ed67bfc3..9236b752b 100644 --- a/src/library/tactic/tactic_exception.h +++ b/src/library/tactic/tactic_exception.h @@ -7,12 +7,19 @@ Author: Leonardo de Moura #pragma once #include #include "util/exception.h" +#include "kernel/justification.h" namespace lean { +/** + \brief Tactic and related components store the reason for + failure in justification objects. +*/ class tactic_exception : public exception { + justification m_justification; public: - tactic_exception(char const * msg):exception(msg) {} - tactic_exception(std::string const & msg):exception(msg) {} - tactic_exception(sstream const & strm):exception(strm) {} + tactic_exception(justification const & j):m_justification(j) {} + virtual ~tactic_exception() {} + virtual char const * what() const noexcept { return "tactic exception"; } + justification const & get_justification() const { return m_justification; } }; } diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index ef930224e..d6c3775ef 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/test.h" +#include "util/interrupt.h" #include "kernel/builtin.h" #include "library/all/all.h" #include "library/tactic/goal.h" @@ -14,6 +16,38 @@ Author: Leonardo de Moura #include "library/tactic/tactic_exception.h" using namespace lean; +tactic loop_tactic() { + return mk_tactic([=](environment const &, io_state const &, proof_state const &) -> proof_state_seq { + while (true) { + check_interrupted(); + } + return proof_state_seq(); + }); +} + +tactic msg_tactic(std::string msg) { + return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { + std::cout << msg << "\n"; + return proof_state_seq(s); + }); +} + +tactic set_tactic(std::atomic * flag) { + return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { + *flag = true; + return proof_state_seq(s); + }); +} + +static void check_failure(tactic t, environment const & env, io_state const & io, context const & ctx, expr const & ty) { + try { + t.solve(env, io, ctx, ty); + lean_unreachable(); + } catch (exception & ex) { + std::cout << "expected error: " << ex.what() << "\n"; + } +} + static void tst1() { environment env; io_state io(options(), mk_simple_formatter()); @@ -30,12 +64,27 @@ static void tst1() { tactic t = then(assumption_tactic(), now_tactic()); std::cout << "proof 1: " << t.solve(env, io, s) << "\n"; std::cout << "proof 2: " << t.solve(env, io, ctx, q) << "\n"; - try { - now_tactic().solve(env, io, ctx, q); - lean_unreachable(); - } catch (tactic_exception & ex) { - std::cout << "expected error: " << ex.what() << "\n"; - } + check_failure(now_tactic(), env, io, ctx, q); + std::cout << "proof 2: " << orelse(fail_tactic(), t).solve(env, io, ctx, q) << "\n"; +#ifndef __APPLE__ + check_failure(try_for(loop_tactic(), 100), env, io, ctx, q); + std::cout << "proof 1: " << try_for(t, 10000).solve(env, io, s) << "\n"; + check_failure(try_for(orelse(try_for(loop_tactic(), 10000), + msg_tactic(std::string("hello world"))), + 100), + env, io, ctx, q); + std::atomic flag1(false); + check_failure(try_for(orelse(try_for(loop_tactic(), 10000), + set_tactic(&flag1)), + 100), + env, io, ctx, q); + lean_assert(!flag1); + check_failure(orelse(try_for(try_for(loop_tactic(), 10000), 100), + set_tactic(&flag1)), + env, io, ctx, q); + lean_assert(flag1); +#endif + std::cout << "done\n"; } int main() {