From 3dc7a856f0dd08a0225719e34ed33bfdc377d330 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Nov 2013 18:11:46 -0800 Subject: [PATCH] refactor(library/tactic): use unprotect/protect idiom for callbacks in the tactic API Signed-off-by: Leonardo de Moura --- src/library/tactic/cex_builder.cpp | 48 ++++++++++++++++++---------- src/library/tactic/proof_builder.cpp | 28 ++++++++++++---- src/library/tactic/tactic.cpp | 5 +-- tests/lua/proof_builder1.lua | 7 +++- 4 files changed, 62 insertions(+), 26 deletions(-) diff --git a/src/library/tactic/cex_builder.cpp b/src/library/tactic/cex_builder.cpp index bb271f578..0f1d02675 100644 --- a/src/library/tactic/cex_builder.cpp +++ b/src/library/tactic/cex_builder.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/script_state.h" #include "util/luaref.h" #include "library/kernel_bindings.h" #include "library/tactic/proof_builder.h" @@ -16,29 +17,44 @@ cex_builder & cex_builder::operator=(cex_builder && s) { LEAN_MOVE_REF(cex_build DECL_UDATA(cex_builder) static int mk_cex_builder(lua_State * L) { + script_state S = to_script_state(L); 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 { - 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); - environment r = to_environment(L, -1); - lua_pop(L, 1); - return r; - })); + script_state _S(S); + optional r; + _S.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); + }); + return push_environment(L, *env); } static int cex_builder_call(lua_State * L) { - if (is_environment(L, 3)) - return push_environment(L, to_cex_builder(L, 1)(to_name_ext(L, 2), optional(to_environment(L, 3)), to_assignment(L, 4))); - else - return push_environment(L, to_cex_builder(L, 1)(to_name_ext(L, 2), optional(), to_assignment(L, 4))); + 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[] = { diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp index cff29ab0c..e2856d545 100644 --- a/src/library/tactic/proof_builder.cpp +++ b/src/library/tactic/proof_builder.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/script_state.h" #include "util/exception.h" #include "util/sstream.h" #include "util/luaref.h" @@ -76,22 +77,35 @@ static const struct luaL_Reg assignment_m[] = { DECL_UDATA(proof_builder); static int mk_proof_builder(lua_State * L) { + script_state S = to_script_state(L); 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 { - ref.push(); // push user-fun on the stack - push_proof_map(L, m); - push_assignment(L, a); - pcall(L, 2, 1, 0); - expr r = to_expr(L, -1); - lua_pop(L, 1); + expr r; + script_state _S(S); + _S.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) { - return push_expr(L, to_proof_builder(L, 1)(to_proof_map(L, 2), to_assignment(L, 3))); + 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[] = { diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index ebf92fd53..718014c7c 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -382,12 +382,13 @@ static int tactic_solve(lua_State * L) { static int mk_lua_tactic01(lua_State * L) { luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun + script_state S = to_script_state(L); luaref ref(L, 1); return push_tactic(L, mk_tactic01([=](environment const & env, io_state const & ios, proof_state const & s) -> optional { - script_state S = to_script_state(L); optional r; - S.exec_protected([&]() { + script_state _S(S); + _S.exec_protected([&]() { ref.push(); // push user-fun on the stack push_environment(L, env); push_io_state(L, ios); diff --git a/tests/lua/proof_builder1.lua b/tests/lua/proof_builder1.lua index 64456289f..29b49dc60 100644 --- a/tests/lua/proof_builder1.lua +++ b/tests/lua/proof_builder1.lua @@ -1,5 +1,8 @@ local pb = proof_builder(function(m, a) - return m:find("main") + print("builder...") + local e = m:find("main") + print(e) + return e end) assert(is_proof_builder(pb)) local a = assignment() @@ -11,4 +14,6 @@ m:insert("main", Const("H")) m:insert("subgoal", Const("H1")) m:erase("subgoal") assert(not pcall(function() m:find("subgoal") end)) +print(m:find("main")) +print(pb(m, a)) assert(pb(m, a) == Const("H"))