diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index b5e2b3e862..299d3657d1 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/src/bindings/lua/CMakeLists.txt @@ -2,6 +2,7 @@ add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp lref.cpp splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp local_context.cpp expr.cpp context.cpp object.cpp environment.cpp formatter.cpp justification.cpp metavar_env.cpp type_inferer.cpp -io_state.cpp goal.cpp leanlua_state.cpp frontend_lean.cpp) +io_state.cpp goal.cpp proof_builder.cpp leanlua_state.cpp +frontend_lean.cpp) target_link_libraries(lua ${LEAN_LIBS}) diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index 1949c7aed5..838845f169 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -34,6 +34,7 @@ Author: Leonardo de Moura #include "bindings/lua/justification.h" #include "bindings/lua/metavar_env.h" #include "bindings/lua/goal.h" +#include "bindings/lua/proof_builder.h" #include "bindings/lua/io_state.h" #include "bindings/lua/type_inferer.h" #include "bindings/lua/frontend_lean.h" @@ -187,6 +188,7 @@ struct leanlua_state::imp { open_state(m_state); open_type_inferer(m_state); open_goal(m_state); + open_proof_builder(m_state); open_frontend_lean(m_state); open_thread(m_state); open_interrupt(m_state); diff --git a/src/bindings/lua/proof_builder.cpp b/src/bindings/lua/proof_builder.cpp new file mode 100644 index 0000000000..c97d8ae2c8 --- /dev/null +++ b/src/bindings/lua/proof_builder.cpp @@ -0,0 +1,124 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "library/tactic/proof_builder.h" +#include "bindings/lua/util.h" +#include "bindings/lua/name.h" +#include "bindings/lua/expr.h" +#include "bindings/lua/metavar_env.h" +#include "bindings/lua/lref.h" + +namespace lean { +DECL_UDATA(proof_map) + +static int mk_proof_map(lua_State * L) { + return push_proof_map(L, proof_map()); +} + +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))); +} + +static int proof_map_insert(lua_State * L) { + to_proof_map(L, 1).insert(to_name_ext(L, 2), to_expr(L, 3)); + return 0; +} + +static int proof_map_erase(lua_State * L) { + to_proof_map(L, 1).erase(to_name_ext(L, 2)); + return 0; +} + +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_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) { + luaL_checktype(L, 1, LUA_TFUNCTION); // user-fun + lref 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); + 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))); +} + +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); + lua_setfield(L, -2, "__index"); + setfuncs(L, proof_map_m, 0); + + 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/bindings/lua/proof_builder.h b/src/bindings/lua/proof_builder.h new file mode 100644 index 0000000000..6433d48acc --- /dev/null +++ b/src/bindings/lua/proof_builder.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +namespace lean { +UDATA_DEFS(proof_map) +UDATA_DEFS(assignment) +UDATA_DEFS(proof_builder) +void open_proof_builder(lua_State * L); +} diff --git a/tests/lua/proof_builder1.lua b/tests/lua/proof_builder1.lua new file mode 100644 index 0000000000..64456289f0 --- /dev/null +++ b/tests/lua/proof_builder1.lua @@ -0,0 +1,14 @@ +local pb = proof_builder(function(m, a) + return m:find("main") + end) +assert(is_proof_builder(pb)) +local a = assignment() +assert(is_assignment(a)) +local m = proof_map() +assert(#m == 0) +assert(is_proof_map(m)) +m:insert("main", Const("H")) +m:insert("subgoal", Const("H1")) +m:erase("subgoal") +assert(not pcall(function() m:find("subgoal") end)) +assert(pb(m, a) == Const("H"))