refactor(library/tactic/proof_builder): simplify proof builder

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

src/library/tactic/CMakeLists.txt

@@ -1,7 +1,6 @@
-add_library(tactic goal.cpp cex_builder.cpp)
+add_library(tactic goal.cpp cex_builder.cpp proof_builder.cpp)
 
-#  proof_builder.cpp cex_builder.cpp
+# proof_state.cpp tactic.cpp apply_tactic.cpp
-# proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp
 # simplify_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/proof_builder.cpp

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <utility>
-#include "util/script_state.h"
 #include "util/exception.h"
 #include "util/sstream.h"
 #include "util/luaref.h"
@@ -20,13 +19,13 @@ expr find(proof_map const & m, name const & n) {
     throw exception(sstream() << "proof for goal '" << n << "' not found");
 }
 
-proof_builder add_proofs(proof_builder const & pb, list<std::pair<name, expr>> const & prs) {
+proof_builder_fn add_proofs(proof_builder_fn const & pb, list<std::pair<name, expr>> const & prs) {
-    return mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
+    return proof_builder_fn([=](proof_map const & m, substitution const & s) -> expr {
             proof_map new_m(m);
             for (auto const & np : prs) {
                 new_m.insert(np.first, np.second);
             }
-            return pb(new_m, a);
+            return pb(new_m, s);
         });
 }
 
@@ -40,11 +39,6 @@ static int mk_proof_map(lua_State * L) {
         return push_proof_map(L, to_proof_map(L, 1));
 }
 
-static int proof_map_len(lua_State * L) {
-    lua_pushinteger(L, to_proof_map(L, 1).size());
-    return 1;
-}
-
 static int proof_map_find(lua_State * L) {
     return push_expr(L, find(to_proof_map(L, 1), to_name_ext(L, 2)));
 }
@@ -61,74 +55,27 @@ static int proof_map_erase(lua_State * L) {
 
 static const struct luaL_Reg proof_map_m[] = {
     {"__gc",            proof_map_gc}, // never throws
-    {"__len",           safe_function<proof_map_len>},
-    {"size",            safe_function<proof_map_len>},
     {"find",            safe_function<proof_map_find>},
     {"insert",          safe_function<proof_map_insert>},
     {"erase",           safe_function<proof_map_erase>},
     {0, 0}
 };
 
-DECL_UDATA(assignment);
+proof_builder_fn to_proof_builder(lua_State * L, int idx) {
-
+    luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun
-static int mk_assignment(lua_State * L) {
+    luaref f(L, idx);
-    int nargs = lua_gettop(L);
+    return proof_builder_fn([=](proof_map const & m, substitution const & s) {
-    if (nargs == 0)
+            lua_State * L = f.get_state();
-        return push_assignment(L, assignment(metavar_env()));
+            f.push();
-    else
+            push_proof_map(L, m);
-        return push_assignment(L, assignment(to_metavar_env(L, 1)));
+            push_substitution(L, s);
-}
+            pcall(L, 2, 1, 0);
-
+            expr r = to_expr(L, -1);
-static int assignment_call(lua_State * L) {
+            lua_pop(L, 1);
-    return push_optional_expr(L, to_assignment(L, 1)(to_name_ext(L, 2)));
+            return r;
-}
-
-static const struct luaL_Reg assignment_m[] = {
-    {"__gc",            assignment_gc}, // never throws
-    {"__call",          safe_function<assignment_call>},
-    {0, 0}
-};
-
-DECL_UDATA(proof_builder);
-
-static int mk_proof_builder(lua_State * L) {
-    script_state::weak_ref S = to_script_state(L).to_weak_ref();
-    luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun
-    luaref ref(L, 1);
-    return push_proof_builder(L,
-                              mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
-                                      expr r;
-                                      script_state S_copy(S);
-                                      S_copy.exec_protected([&]() {
-                                              ref.push(); // push user-fun on the stack
-                                              push_proof_map(L, m);
-                                              push_assignment(L, a);
-                                              pcall(L, 2, 1, 0);
-                                              r = to_expr(L, -1);
-                                              lua_pop(L, 1);
-                                          });
-                                      return r;
-                                  }));
-}
-
-static int proof_builder_call(lua_State * L) {
-    proof_builder pb = to_proof_builder(L, 1);
-    proof_map m      = to_proof_map(L, 2);
-    assignment a     = to_assignment(L, 3);
-    expr r;
-    script_state S   = to_script_state(L);
-    S.exec_unprotected([&]() {
-            r = pb(m, a);
         });
-    return push_expr(L, r);
 }
 
-static const struct luaL_Reg proof_builder_m[] = {
-    {"__gc",            proof_builder_gc}, // never throws
-    {"__call",          safe_function<proof_builder_call>},
-    {0, 0}
-};
-
 void open_proof_builder(lua_State * L) {
     luaL_newmetatable(L, proof_map_mt);
     lua_pushvalue(L, -1);
@@ -137,21 +84,5 @@ void open_proof_builder(lua_State * L) {
 
     SET_GLOBAL_FUN(proof_map_pred, "is_proof_map");
     SET_GLOBAL_FUN(mk_proof_map, "proof_map");
-
-    luaL_newmetatable(L, assignment_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, assignment_m, 0);
-
-    SET_GLOBAL_FUN(assignment_pred, "is_assignment");
-    SET_GLOBAL_FUN(mk_assignment, "assignment");
-
-    luaL_newmetatable(L, proof_builder_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, proof_builder_m, 0);
-
-    SET_GLOBAL_FUN(proof_builder_pred, "is_proof_builder");
-    SET_GLOBAL_FUN(mk_proof_builder, "proof_builder");
 }
 }

src/library/tactic/proof_builder.h

@@ -8,71 +8,25 @@ Author: Leonardo de Moura
 #include <utility>
 #include <algorithm>
 #include "util/lua.h"
-#include "util/debug.h"
 #include "util/name.h"
-#include "util/splay_map.h"
+#include "util/rb_map.h"
-#include "util/rc.h"
 #include "kernel/expr.h"
-#include "library/tactic/assignment.h"
 
 namespace lean {
-typedef splay_map<name, expr, name_quick_cmp> proof_map;
+typedef rb_map<name, expr, name_quick_cmp> proof_map;
-
 /**
-   \brief Return the proof for the goal named \c n in the \c proof_map \c m.
+   \brief Return the proof (of inhabitated type) for the goal named \c n in the \c proof_map \c m.
    Throw an exception if \c m does not contain a proof for \c n.
 */
 expr find(proof_map const & m, name const & n);
-
 /**
-   \brief Base class for functors that build a proof for the main goal based on
+   \brief A proof builder creates an inhabitant a goal type (aka
-   the proofs of the subgoals.
+   conclusion) using the inhabitants for its subgoals.
 */
-class proof_builder_cell {
+typedef std::function<expr(proof_map const &, substitution const &)> proof_builder_fn;
-    void dealloc() { delete this; }
+proof_builder_fn add_proofs(proof_builder_fn const & pb, list<std::pair<name, expr>> const & prs);
-    MK_LEAN_RC();
-public:
-    proof_builder_cell():m_rc(0) {}
-    virtual ~proof_builder_cell() {}
-    virtual expr operator()(proof_map const & p, assignment const & a) const = 0;
-};
 
-template<typename F>
+/** \brief Convert a Lua function on position \c idx (on the Lua stack) into a proof_builder_fn */
-class proof_builder_tpl : public proof_builder_cell {
+proof_builder_fn to_proof_builder(lua_State * L, int idx);
-    F m_f;
-public:
-    proof_builder_tpl(F && f):m_f(f) {}
-    virtual expr operator()(proof_map const & p, assignment const & a) const { return m_f(p, a); }
-};
-
-/**
-   \brief Smart pointer for a proof builder functor.
-*/
-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; }
-    ~proof_builder() { if (m_ptr) m_ptr->dec_ref(); }
-    friend void swap(proof_builder & a, proof_builder & b) { std::swap(a.m_ptr, b.m_ptr); }
-    proof_builder & operator=(proof_builder const & s) { LEAN_COPY_REF(s); }
-    proof_builder & operator=(proof_builder && s) { LEAN_MOVE_REF(s); }
-
-    expr operator()(proof_map const & p, assignment const & a) const { return m_ptr->operator()(p, a); }
-};
-
-template<typename F>
-proof_builder mk_proof_builder(F && f) {
-    return proof_builder(new proof_builder_tpl<F>(std::forward<F>(f)));
-}
-
-proof_builder add_proofs(proof_builder const & pb, list<std::pair<name, expr>> const & prs);
-
-UDATA_DEFS_CORE(proof_map)
-UDATA_DEFS(assignment)
-UDATA_DEFS(proof_builder)
 void open_proof_builder(lua_State * L);
 }

src/library/tactic/register_module.h

@@ -7,8 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/script_state.h"
 #include "library/tactic/goal.h"
-// #include "library/tactic/proof_builder.h"
+#include "library/tactic/proof_builder.h"
-// #include "library/tactic/cex_builder.h"
 // #include "library/tactic/proof_state.h"
 // #include "library/tactic/tactic.h"
 // #include "library/tactic/apply_tactic.h"
@@ -17,8 +16,7 @@ Author: Leonardo de Moura
 namespace lean {
 inline void open_tactic_module(lua_State * L) {
     open_goal(L);
-    // open_proof_builder(L);
+    open_proof_builder(L);
-    // open_cex_builder(L);
     // open_proof_state(L);
     // open_tactic(L);
     // open_apply_tactic(L);