diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index d61ca81b1..9dc89bb40 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,4 +1,4 @@ -add_library(tactic goal.cpp) +add_library(tactic goal.cpp cex_builder.cpp) # proof_builder.cpp cex_builder.cpp # proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp diff --git a/src/library/tactic/cex_builder.cpp b/src/library/tactic/cex_builder.cpp index 8a567485c..2fd9a828f 100644 --- a/src/library/tactic/cex_builder.cpp +++ b/src/library/tactic/cex_builder.cpp @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -8,78 +8,33 @@ Author: Leonardo de Moura #include "util/script_state.h" #include "util/luaref.h" #include "library/kernel_bindings.h" -#include "library/tactic/proof_builder.h" #include "library/tactic/cex_builder.h" namespace lean { -cex_builder & cex_builder::operator=(cex_builder const & s) { LEAN_COPY_REF(s); } -cex_builder & cex_builder::operator=(cex_builder && s) { LEAN_MOVE_REF(s); } - -cex_builder mk_cex_builder_for(name const & gname) { - return mk_cex_builder( - [=](name const & n, optional const & cex, assignment const &) -> counterexample { +cex_builder_fn mk_cex_builder_for(name const & gname) { + return cex_builder_fn([=](name const & n, optional const & cex, substitution const &) -> counterexample { if (n != gname || !cex) throw exception(sstream() << "failed to build counterexample for '" << gname << "' goal"); return *cex; }); } -DECL_UDATA(cex_builder) - -static int mk_cex_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_cex_builder(L, - mk_cex_builder([=](name const & n, optional const & cex, assignment const & a) -> counterexample { - script_state S_copy(S); - optional r; - S_copy.exec_protected([&]() { - ref.push(); // push user-fun on the stack - push_name(L, n); - if (cex) - push_environment(L, *cex); - else - lua_pushnil(L); - push_assignment(L, a); - pcall(L, 3, 1, 0); - r = to_environment(L, -1); - lua_pop(L, 1); - }); - return *r; - })); -} - -static int cex_builder_call_core(lua_State * L, cex_builder b, name n, optional cex, assignment a) { - script_state S = to_script_state(L); - optional env; - S.exec_unprotected([&]() { - env = b(n, cex, a); +cex_builder_fn to_cex_builder(lua_State * L, int idx) { + luaL_checktype(L, idx, LUA_TFUNCTION); // user-fun + luaref f(L, idx); + return cex_builder_fn([=](name const & n, optional const & cex, substitution const & s) { + lua_State * L = f.get_state(); + f.push(); + push_name(L, n); + if (cex) + push_environment(L, *cex); + else + lua_pushnil(L); + push_substitution(L, s); + pcall(L, 3, 1, 0); + environment r = to_environment(L, -1); + lua_pop(L, 1); + return r; }); - return push_environment(L, *env); -} - -static int cex_builder_call(lua_State * L) { - if (is_environment(L, 3)) { - return cex_builder_call_core(L, to_cex_builder(L, 1), to_name_ext(L, 2), optional(to_environment(L, 3)), to_assignment(L, 4)); - } else { - return cex_builder_call_core(L, to_cex_builder(L, 1), to_name_ext(L, 2), optional(), to_assignment(L, 4)); - } -} - -static const struct luaL_Reg cex_builder_m[] = { - {"__gc", cex_builder_gc}, // never throws - {"__call", safe_function}, - {0, 0} -}; - -void open_cex_builder(lua_State * L) { - luaL_newmetatable(L, cex_builder_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, cex_builder_m, 0); - - SET_GLOBAL_FUN(cex_builder_pred, "is_cex_builder"); - SET_GLOBAL_FUN(mk_cex_builder, "cex_builder"); } } diff --git a/src/library/tactic/cex_builder.h b/src/library/tactic/cex_builder.h index 3c56907a9..237ac30a9 100644 --- a/src/library/tactic/cex_builder.h +++ b/src/library/tactic/cex_builder.h @@ -1,78 +1,24 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include +#include #include "util/lua.h" -#include "util/debug.h" #include "util/name.h" -#include "util/rc.h" #include "util/optional.h" -#include "kernel/expr.h" #include "kernel/environment.h" -#include "library/tactic/assignment.h" +#include "kernel/metavar.h" namespace lean { -/** - \brief In Lean, a counter-example is encoded using an environment object. -*/ +/** \brief In Lean, a counter-example is encoded using an environment object. */ typedef environment counterexample; +typedef std::function const &, substitution const &)> cex_builder_fn; +/** \brief Return a counterexample builder that expects a counterexample for the given goal. */ +cex_builder_fn mk_cex_builder_for(name const & gname); -/** - \brief Base class for functors that build a counterexample for the main goal based on - a counterexample for a subgoal. -*/ -class cex_builder_cell { - void dealloc() { delete this; } - MK_LEAN_RC(); -public: - cex_builder_cell():m_rc(0) {} - virtual ~cex_builder_cell() {} - virtual counterexample operator()(name const & n, optional const & cex, assignment const & a) const = 0; -}; - -template -class cex_builder_tpl : public cex_builder_cell { - F m_f; -public: - cex_builder_tpl(F && f):m_f(f) {} - virtual counterexample operator()(name const & n, optional const & cex, assignment const & a) const { - return m_f(n, cex, a); - } -}; - -/** - \brief Smart pointer for a counterexample builder functor. -*/ -class cex_builder { -protected: - cex_builder_cell * m_ptr; -public: - cex_builder():m_ptr(nullptr) {} - explicit cex_builder(cex_builder_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); } - cex_builder(cex_builder const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } - cex_builder(cex_builder && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } - ~cex_builder() { if (m_ptr) m_ptr->dec_ref(); } - friend void swap(cex_builder & a, cex_builder & b) { std::swap(a.m_ptr, b.m_ptr); } - cex_builder & operator=(cex_builder const & s); - cex_builder & operator=(cex_builder && s); - - counterexample operator()(name const & n, optional const & cex, assignment const & a) const { return m_ptr->operator()(n, cex, a); } -}; - -template -cex_builder mk_cex_builder(F && f) { - return cex_builder(new cex_builder_tpl(std::forward(f))); -} - -/** - \brief Return a counterexample builder that expects a counterexample for the given goal. -*/ -cex_builder mk_cex_builder_for(name const & gname); - -UDATA_DEFS(cex_builder) -void open_cex_builder(lua_State * L); +/** \brief Convert a Lua function on position \c idx (on the Lua stack) to a cex_builder_fn */ +cex_builder_fn to_cex_builder(lua_State * L, int idx); }