michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/tactic): use unprotect/protect idiom for callbacks in the tactic API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-27 18:11:46 -08:00
parent b4a8418d38
commit 3dc7a856f0
4 changed files with 62 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

48
src/library/tactic/cex_builder.cpp
View file

@ -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<counterexample> 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<environment> 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<counterexample> cex, assignment a) {
script_state S = to_script_state(L);
optional<environment> 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<counterexample>(to_environment(L, 3)), to_assignment(L, 4)));
else
return push_environment(L, to_cex_builder(L, 1)(to_name_ext(L, 2), optional<counterexample>(), 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<counterexample>(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<counterexample>(), to_assignment(L, 4));
}
}
static const struct luaL_Reg cex_builder_m[] = {

28
src/library/tactic/proof_builder.cpp
View file

@ -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[] = {

5
src/library/tactic/tactic.cpp
View file

@ -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<proof_state> {
script_state S = to_script_state(L);
optional<proof_state> 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);

7
tests/lua/proof_builder1.lua
View file

@ -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"))