feat(library/tactic): add 'idtac' tactic and 'then' tactical

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

src/kernel/environment.h

@@ -35,6 +35,7 @@ public:
     weak_ref to_weak_ref() const { return weak_ref(m_ptr); }
 
     friend bool is_eqp(environment const & env1, environment const & env2) { return env1.m_ptr.get() == env2.m_ptr.get(); }
+    friend void swap(environment & env1, environment & env2) { env1.m_ptr.swap(env2.m_ptr); }
     // =======================================
     // Parent/Child environment management
     /**

src/library/tactic/CMakeLists.txt

@@ -1,2 +1,2 @@
-add_library(tactic goal.cpp tactic.cpp)
+add_library(tactic goal.cpp proof_builder.cpp proof_state.cpp tactic.cpp)
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/goal.cpp

@@ -22,7 +22,7 @@ goal_proof_fn::goal_proof_fn(std::vector<expr> && consts):
     m_constants(consts) {
 }
 
-expr goal_proof_fn::operator()(expr const & pr) {
+expr goal_proof_fn::operator()(expr const & pr) const {
     return abstract(pr, m_constants.size(), m_constants.data());
 }
 

src/library/tactic/goal.h

@@ -36,7 +36,7 @@ class goal_proof_fn {
     std::vector<expr> m_constants;
     goal_proof_fn(std::vector<expr> && constants);
 public:
-    expr operator()(expr const & pr);
+    expr operator()(expr const & pr) const;
 };
 
 /**

src/library/tactic/justification_builder.h

@@ -25,6 +25,7 @@ class justification_builder {
 protected:
     justification_builder_cell * m_ptr;
 public:
+    justification_builder():m_ptr(nullptr) {}
     explicit justification_builder(justification_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
     justification_builder(justification_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     justification_builder(justification_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
@@ -35,4 +36,17 @@ public:
 
     justification operator()(name const & n, justification const & j, environment const & env, assignment const & a) const { return m_ptr->operator()(n, j, env, a); }
 };
+
+template<typename F>
+class simple_justification_builder : public justification_builder_cell {
+    F m_f;
+public:
+    simple_justification_builder(F && f):m_f(std::forward<F>(f)) {}
+    virtual justification operator()(name const & n, justification const & j, environment const & env, assignment const & a) const { return m_f(n, j, env, a); }
+};
+
+template<typename F>
+justification_builder mk_justification_builder(F && f) {
+    return justification_builder(new simple_justification_builder<F>(std::forward<F>(f)));
+}
 }

src/library/tactic/proof_builder.cpp

@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/tactic/proof_builder.h"
+
+namespace lean {
+expr find(proof_map const & m, name const & n) {
+    expr * r = const_cast<proof_map&>(m).splay_find(n);
+    if (r)
+        return *r;
+    else
+        return expr();
+}
+}

src/library/tactic/proof_builder.h

@@ -16,6 +16,8 @@ Author: Leonardo de Moura
 namespace lean {
 typedef splay_map<name, expr, name_quick_cmp> proof_map;
 
+expr find(proof_map const & m, name const & n);
+
 class proof_builder_cell {
     void dealloc() { delete this; }
     MK_LEAN_RC();
@@ -28,6 +30,7 @@ class proof_builder {
 protected:
     proof_builder_cell * m_ptr;
 public:
+    proof_builder():m_ptr(nullptr) {}
     explicit proof_builder(proof_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
     proof_builder(proof_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     proof_builder(proof_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
@@ -38,4 +41,17 @@ public:
 
     expr operator()(proof_map const & p, environment const & env, assignment const & a) const { return m_ptr->operator()(p, env, a); }
 };
+
+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)) {}
+    virtual expr operator()(proof_map const & p, environment const & env, assignment const & a) const { return m_f(p, env, a); }
+};
+
+template<typename F>
+proof_builder mk_proof_builder(F && f) {
+    return proof_builder(new simple_proof_builder<F>(std::forward<F>(f)));
+}
 }

src/library/tactic/proof_state.cpp

@@ -0,0 +1,41 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/sstream.h"
+#include "library/tactic/tactic_exception.h"
+#include "library/tactic/proof_state.h"
+
+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);
+    swap(s1.m_justification_builder, s2.m_justification_builder);
+}
+
+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;
+                           }));
+}
+}

src/library/tactic/proof_state.h

@@ -11,19 +11,25 @@ Author: Leonardo de Moura
 #include "library/tactic/justification_builder.h"
 
 namespace lean {
+typedef list<std::pair<name, goal>> goals;
 class proof_state {
-    environment const           m_env;
-    list<std::pair<name, goal>> m_goals;
+    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<std::pair<name, goal>> 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) {}
+    friend void swap(proof_state & s1, proof_state & s2);
     environment const & get_environment() const { return m_env; }
     list<std::pair<name, goal>> 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; }
     justification_builder const & get_justification_builder() const { return m_justification_builder; }
 };
+void swap(proof_state & s1, proof_state & s2);
+
+proof_state to_proof_state(environment const & env, context const & ctx, expr const & t);
 }

src/library/tactic/tactic.cpp

@@ -12,6 +12,10 @@ tactic_result::~tactic_result() {
 void tactic_result::interrupt() {
     m_result = true;
 }
+void tactic_result::request_interrupt() {
+    std::lock_guard<std::mutex> lock(m_mutex);
+    interrupt();
+}
 
 tactic_cell::~tactic_cell() {
 }
@@ -23,4 +27,70 @@ tactic & tactic::operator=(tactic const & s) {
 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;
+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() {
+            if (m_r2) {
+                proof_state_ref s2 = m_r2->next();
+                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());
+            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();
+        }
+    };
+
+    virtual tactic_result_ref operator()(proof_state const & s) const {
+        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)); }
 }

src/library/tactic/tactic.h

@@ -7,27 +7,39 @@ Author: Leonardo de Moura
 #pragma once
 #include <algorithm>
 #include <memory>
+#include <mutex>
 #include "library/tactic/proof_state.h"
 
 namespace lean {
+typedef std::unique_ptr<proof_state> proof_state_ref;
+class tactic_result;
+typedef std::unique_ptr<tactic_result> tactic_result_ref;
+
 class tactic_result {
-    volatile bool m_result;
+    std::mutex    m_mutex;
+    bool          m_result;
+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(); }
 public:
     tactic_result():m_result(false) {}
     bool interrupted() const { return m_result; }
+    void request_interrupt();
     virtual ~tactic_result();
-    virtual void interrupt();
-    virtual proof_state next() = 0;
+    virtual proof_state_ref next() = 0;
 };
 
-typedef std::unique_ptr<tactic_result> tactic_result_ref;
-
 class tactic_cell {
     void dealloc() { delete this; }
     MK_LEAN_RC();
 public:
     virtual ~tactic_cell();
-    virtual tactic_result_ref operator()(proof_state const & p) const = 0;
+    virtual tactic_result_ref operator()(proof_state const & s) const = 0;
 };
 
 class tactic {
@@ -42,7 +54,9 @@ public:
     tactic & operator=(tactic const & s);
     tactic & operator=(tactic && s);
 
-    tactic_result_ref operator()(proof_state const & p) const { return m_ptr->operator()(p); }
+    tactic_result_ref operator()(proof_state const & s) const { return m_ptr->operator()(s); }
 };
-}
 
+tactic idtac();
+tactic then(tactic const & t1, tactic const & t2);
+}

src/library/tactic/tactic_exception.h

@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/exception.h"
+
+namespace lean {
+class tactic_exception : public exception {
+public:
+    tactic_exception(char const * msg):exception(msg) {}
+    tactic_exception(std::string const & msg):exception(msg) {}
+    tactic_exception(sstream const & strm):exception(strm) {}
+};
+}