From c6ac89d9676075f9a1b15e91ed6a6204a722d405 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Jun 2014 12:25:04 -0700 Subject: [PATCH] refactor(library/tactic/proof_builder): simplify proof builder Signed-off-by: Leonardo de Moura --- src/library/tactic/CMakeLists.txt | 5 +- src/library/tactic/proof_builder.cpp | 99 +++++----------------------- src/library/tactic/proof_builder.h | 64 +++--------------- src/library/tactic/register_module.h | 6 +- 4 files changed, 28 insertions(+), 146 deletions(-) diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 9dc89bb40..fa3282552 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/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 boolean_tactics.cpp apply_tactic.cpp +# proof_state.cpp tactic.cpp apply_tactic.cpp # simplify_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp index eb01fbb0d..a7361a052 100644 --- a/src/library/tactic/proof_builder.cpp +++ b/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 -#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> const & prs) { - return mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { +proof_builder_fn add_proofs(proof_builder_fn const & pb, list> const & prs) { + 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}, - {"size", safe_function}, {"find", safe_function}, {"insert", safe_function}, {"erase", safe_function}, {0, 0} }; -DECL_UDATA(assignment); - -static int mk_assignment(lua_State * L) { - int nargs = lua_gettop(L); - if (nargs == 0) - return push_assignment(L, assignment(metavar_env())); - else - return push_assignment(L, assignment(to_metavar_env(L, 1))); -} - -static int assignment_call(lua_State * L) { - return push_optional_expr(L, to_assignment(L, 1)(to_name_ext(L, 2))); -} - -static const struct luaL_Reg assignment_m[] = { - {"__gc", assignment_gc}, // never throws - {"__call", safe_function}, - {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); +proof_builder_fn to_proof_builder(lua_State * L, int idx) { + luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun + luaref f(L, idx); + return proof_builder_fn([=](proof_map const & m, substitution const & s) { + lua_State * L = f.get_state(); + f.push(); + push_proof_map(L, m); + push_substitution(L, s); + pcall(L, 2, 1, 0); + expr r = to_expr(L, -1); + lua_pop(L, 1); + return r; }); - return push_expr(L, r); } -static const struct luaL_Reg proof_builder_m[] = { - {"__gc", proof_builder_gc}, // never throws - {"__call", safe_function}, - {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"); } } diff --git a/src/library/tactic/proof_builder.h b/src/library/tactic/proof_builder.h index ddb84e553..9f6379e6d 100644 --- a/src/library/tactic/proof_builder.h +++ b/src/library/tactic/proof_builder.h @@ -8,71 +8,25 @@ Author: Leonardo de Moura #include #include #include "util/lua.h" -#include "util/debug.h" #include "util/name.h" -#include "util/splay_map.h" -#include "util/rc.h" +#include "util/rb_map.h" #include "kernel/expr.h" -#include "library/tactic/assignment.h" namespace lean { -typedef splay_map proof_map; - +typedef rb_map 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 - the proofs of the subgoals. + \brief A proof builder creates an inhabitant a goal type (aka + conclusion) using the inhabitants for its subgoals. */ -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, assignment const & a) const = 0; -}; +typedef std::function proof_builder_fn; +proof_builder_fn add_proofs(proof_builder_fn const & pb, list> const & prs); -template -class proof_builder_tpl : public proof_builder_cell { - 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 -proof_builder mk_proof_builder(F && f) { - return proof_builder(new proof_builder_tpl(std::forward(f))); -} - -proof_builder add_proofs(proof_builder const & pb, list> const & prs); - -UDATA_DEFS_CORE(proof_map) -UDATA_DEFS(assignment) -UDATA_DEFS(proof_builder) +/** \brief Convert a Lua function on position \c idx (on the Lua stack) into a proof_builder_fn */ +proof_builder_fn to_proof_builder(lua_State * L, int idx); void open_proof_builder(lua_State * L); } diff --git a/src/library/tactic/register_module.h b/src/library/tactic/register_module.h index 25c6882a4..fe32e7bfd 100644 --- a/src/library/tactic/register_module.h +++ b/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/cex_builder.h" +#include "library/tactic/proof_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_cex_builder(L); + open_proof_builder(L); // open_proof_state(L); // open_tactic(L); // open_apply_tactic(L);