refactor(library/tactic): simplify tactic framework, add orelse and try_for combinators/tacticals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<typename F>
 class simple_proof_builder : public proof_builder_cell {
     F m_f;
 public:
-    simple_proof_builder(F && f):m_f(std::forward<F>(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); }
 };
 

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);

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 <utility>
+#include <chrono>
 #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<std::mutex> 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_seq r   = operator()(env, io, s);
-    proof_state_ref final = r->next(env, io);
+    if (!r)
-    if (!final)
+        throw exception("tactic failed to solve input");
-        throw tactic_exception("tactic did not produce any result");
+    proof_state final = head(r);
-    if (!empty(final->get_goals()))
+    assignment a(final.get_menv());
-        throw tactic_exception("tactic did not solve all goals");
-    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 proof_state_seq();
-            return s;
+            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<std::pair<name, expr>> 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 then(tactic t1, tactic t2) {
-    tactic m_t1;
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq {
-    tactic m_t2;
+            tactic _t1(t1);
-public:
+            return map_append(_t1(env, io, s1), [=](proof_state const & s2) {
-    then_tactic(tactic const & t1, tactic const & t2):m_t1(t1), m_t2(t2) {}
+                    check_interrupted();
+                    tactic _t2(t2);
+                    return _t2(env, io, s2);
+                });
+        });
+}
 
-    class result : public tactic_result {
+tactic orelse(tactic t1, tactic t2) {
-        tactic_result_ref              m_r1;
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
-        proof_state_ref                m_s1;
+            tactic _t1(t1);
-        tactic                         m_t2;
+            proof_state_seq r = _t1(env, io, s);
-        tactic_result_ref              m_r2;
+            if (r) {
-    protected:
+                return r;
-        virtual void interrupt() {
+            } else {
-            tactic_result::interrupt();
+                check_interrupted();
-            propagate_interrupt(m_r1);
+                tactic _t2(t2);
-            propagate_interrupt(m_r2);
+                return _t2(env, io, s);
+            }
+        });
 }
-    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) {
+tactic try_for(tactic t, unsigned ms, unsigned check_ms) {
-            if (m_r2) {
+    if (check_ms == 0)
-                proof_state_ref s2 = m_r2->next(env, s);
+        check_ms = 1;
-                if (s2)
+    return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
-                    return s2;
+            tactic _t(t);
-                m_r2.release();
+            proof_state_seq         r;
-                m_s1.release();
+            std::atomic<bool>       done(false);
+            interruptible_thread th([&]() {
+                    try {
+                        r = _t(env, io, s);
+                    } catch (...) {
+                        r = proof_state_seq();
                     }
-            lean_assert(!m_r2);
+                    done = true;
-            lean_assert(!m_s1);
+                });
-            proof_state_ref new_s1(m_r1->next(env, s));
+            try {
-            if (!new_s1)
+                auto start = std::chrono::steady_clock::now();
-                return proof_state_ref(); // done, m_r1 has no more solutions
+                std::chrono::milliseconds d(ms);
-            m_s1.swap(new_s1);
+                std::chrono::milliseconds one(1);
-            tactic_result_ref r2 = m_t2(proof_state(*m_s1));
+                while (!done) {
-            exclusive_update([&]() { m_r2.swap(r2); }); // must protect because interrupt() may be invoked from different thread
+                    auto curr = std::chrono::steady_clock::now();
-            return m_r2->next(env, s);
+                    if (std::chrono::duration_cast<std::chrono::milliseconds>(curr - start) > d)
+                        break;
+                    check_interrupted();
+                    std::this_thread::sleep_for(one);
                 }
-    };
+                th.request_interrupt();
-
+                th.join();
-    virtual tactic_result_ref operator()(proof_state const & s) {
+                return r;
-        return tactic_result_ref(new result(m_t1(s), m_t2));
+            } catch (...) {
+                th.request_interrupt();
+                th.join();
+                throw;
+            }
+        });
 }
-};
-
-tactic then(tactic const & t1, tactic const & t2) { return tactic(new then_tactic(t1, t2)); }
 }

src/library/tactic/tactic.h

@@ -6,41 +6,24 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <algorithm>
+#include <utility>
 #include <memory>
 #include <mutex>
+#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> proof_state_ref;
+typedef lazy_list<proof_state> proof_state_seq;
-class tactic_result;
-typedef std::unique_ptr<tactic_result> tactic_result_ref;
-
-class tactic_result {
-    std::mutex        m_mutex;
-    std::atomic<bool> m_interrupted;
-protected:
-    template<typename F>
-    void exclusive_update(F && f) {
-        std::lock_guard<std::mutex> 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();
-};
 
 class tactic_cell {
     void dealloc() { delete this; }
     MK_LEAN_RC();
 public:
-    virtual ~tactic_cell();
+    tactic_cell():m_rc(0) {}
-    virtual tactic_result_ref operator()(proof_state const & s) = 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) {}
-
+    virtual proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) {
-    class result : public tactic_result {
+        return m_f(env, io, s);
-        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));
     }
 };
 
@@ -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);
 }

src/library/tactic/tactic_exception.h

@@ -7,12 +7,19 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #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(justification const & j):m_justification(j) {}
-    tactic_exception(std::string const & msg):exception(msg) {}
+    virtual ~tactic_exception() {}
-    tactic_exception(sstream const & strm):exception(strm) {}
+    virtual char const * what() const noexcept { return "tactic exception"; }
+    justification const & get_justification() const { return m_justification; }
 };
 }

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 <string>
 #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<bool> * 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 {
+    check_failure(now_tactic(), env, io, ctx, q);
-        now_tactic().solve(env, io, ctx, q);
+    std::cout << "proof 2: " << orelse(fail_tactic(), t).solve(env, io, ctx, q) << "\n";
-        lean_unreachable();
+#ifndef __APPLE__
-    } catch (tactic_exception & ex) {
+    check_failure(try_for(loop_tactic(), 100), env, io, ctx, q);
-        std::cout << "expected error: " << ex.what() << "\n";
+    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<bool> 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() {