From 861be072d851d6f03a17e3a62f51924e41765e34 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Nov 2013 11:32:33 -0800 Subject: [PATCH] feat(bindings/lua): add proof_state to Lua API Signed-off-by: Leonardo de Moura --- src/bindings/lua/CMakeLists.txt | 2 +- src/bindings/lua/goal.h | 3 +- src/bindings/lua/leanlua_state.cpp | 2 + src/bindings/lua/proof_builder.h | 3 +- src/bindings/lua/proof_state.cpp | 218 +++++++++++++++++++++++++++++ src/bindings/lua/proof_state.h | 14 ++ tests/lua/proof_state1.lua | 27 ++++ 7 files changed, 266 insertions(+), 3 deletions(-) create mode 100644 src/bindings/lua/proof_state.cpp create mode 100644 src/bindings/lua/proof_state.h create mode 100644 tests/lua/proof_state1.lua diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index aab549086..0ca02d379 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/src/bindings/lua/CMakeLists.txt @@ -3,6 +3,6 @@ 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 proof_builder.cpp cex_builder.cpp -leanlua_state.cpp frontend_lean.cpp) +proof_state.cpp leanlua_state.cpp frontend_lean.cpp) target_link_libraries(lua ${LEAN_LIBS}) diff --git a/src/bindings/lua/goal.h b/src/bindings/lua/goal.h index 00a4a7e96..dabac273f 100644 --- a/src/bindings/lua/goal.h +++ b/src/bindings/lua/goal.h @@ -6,8 +6,9 @@ Author: Leonardo de Moura */ #pragma once #include +#include "library/tactic/goal.h" namespace lean { -UDATA_DEFS(hypotheses) +UDATA_DEFS_CORE(hypotheses) UDATA_DEFS(goal) void open_goal(lua_State * L); } diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index 718519bf2..9067fc27e 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -36,6 +36,7 @@ Author: Leonardo de Moura #include "bindings/lua/goal.h" #include "bindings/lua/proof_builder.h" #include "bindings/lua/cex_builder.h" +#include "bindings/lua/proof_state.h" #include "bindings/lua/io_state.h" #include "bindings/lua/type_inferer.h" #include "bindings/lua/frontend_lean.h" @@ -191,6 +192,7 @@ struct leanlua_state::imp { open_goal(m_state); open_proof_builder(m_state); open_cex_builder(m_state); + open_proof_state(m_state); open_frontend_lean(m_state); open_thread(m_state); open_interrupt(m_state); diff --git a/src/bindings/lua/proof_builder.h b/src/bindings/lua/proof_builder.h index 6433d48ac..f5c08c7f5 100644 --- a/src/bindings/lua/proof_builder.h +++ b/src/bindings/lua/proof_builder.h @@ -6,8 +6,9 @@ Author: Leonardo de Moura */ #pragma once #include +#include "library/tactic/proof_builder.h" namespace lean { -UDATA_DEFS(proof_map) +UDATA_DEFS_CORE(proof_map) UDATA_DEFS(assignment) UDATA_DEFS(proof_builder) void open_proof_builder(lua_State * L); diff --git a/src/bindings/lua/proof_state.cpp b/src/bindings/lua/proof_state.cpp new file mode 100644 index 000000000..6112f1d04 --- /dev/null +++ b/src/bindings/lua/proof_state.cpp @@ -0,0 +1,218 @@ +/* +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_state.h" +#include "bindings/lua/util.h" +#include "bindings/lua/name.h" +#include "bindings/lua/options.h" +#include "bindings/lua/formatter.h" +#include "bindings/lua/format.h" +#include "bindings/lua/expr.h" +#include "bindings/lua/context.h" +#include "bindings/lua/environment.h" +#include "bindings/lua/metavar_env.h" +#include "bindings/lua/goal.h" +#include "bindings/lua/proof_builder.h" +#include "bindings/lua/cex_builder.h" + +namespace lean { +DECL_UDATA(goals) + +static int mk_goals(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_goals(L, goals()); + } else if (nargs == 2) { + return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), goals())); + } else if (nargs == 3) { + return push_goals(L, goals(mk_pair(to_name_ext(L, 1), to_goal(L, 2)), to_goals(L, 3))); + } else { + throw exception("goals functions expects 0 (empty list), 2 (name & goal for singleton goal list), or 3 (name & goal & goal list) arguments"); + } +} + +static int goals_is_nil(lua_State * L) { + lua_pushboolean(L, !to_goals(L, 1)); + return 1; +} + +static int goals_head(lua_State * L) { + goals const & hs = to_goals(L, 1); + if (!hs) + throw exception("head method expects a non-empty goal list"); + push_name(L, head(hs).first); + push_goal(L, head(hs).second); + return 2; +} + +static int goals_tail(lua_State * L) { + goals const & hs = to_goals(L, 1); + if (!hs) + throw exception("tail method expects a non-empty goal list"); + push_goals(L, tail(hs)); + return 1; +} + +static int goals_next(lua_State * L) { + goals & hs = to_goals(L, lua_upvalueindex(1)); + if (hs) { + push_goals(L, tail(hs)); + lua_replace(L, lua_upvalueindex(1)); + push_name(L, head(hs).first); + push_goal(L, head(hs).second); + return 2; + } else { + lua_pushnil(L); + return 1; + } +} + +static int goals_items(lua_State * L) { + goals & hs = to_goals(L, 1); + push_goals(L, hs); // upvalue(1): goals + lua_pushcclosure(L, &safe_function, 1); // create closure with 1 upvalue + return 1; +} + +static int goals_len(lua_State * L) { + lua_pushinteger(L, length(to_goals(L, 1))); + return 1; +} + +static const struct luaL_Reg goals_m[] = { + {"__gc", goals_gc}, // never throws + {"__len", safe_function}, + {"size", safe_function}, + {"pairs", safe_function}, + {"is_nil", safe_function}, + {"empty", safe_function}, + {"head", safe_function}, + {"tail", safe_function}, + {0, 0} +}; + +DECL_UDATA(proof_state) + +static int mk_proof_state(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_proof_state(L, proof_state()); + } else if (nargs == 4) { + return push_proof_state(L, proof_state(to_goals(L, 1), to_metavar_env(L, 2), to_proof_builder(L, 3), to_cex_builder(L, 4))); + } else if (nargs == 3) { + return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_proof_builder(L, 3))); + } else { + throw exception("proof_state expectes 0, 3, or 4 arguments"); + } +} + +static int to_proof_state(lua_State * L) { + return push_proof_state(L, to_proof_state(to_environment(L, 1), to_context(L, 2), to_expr(L, 3))); +} + +static int proof_state_tostring(lua_State * L) { + std::ostringstream out; + proof_state & s = to_proof_state(L, 1); + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(s.pp(fmt, opts), opts); + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int proof_state_get_precision(lua_State * L) { + lua_pushinteger(L, static_cast(to_proof_state(L, 1).get_precision())); + return 1; +} + +static int proof_state_get_goals(lua_State * L) { + return push_goals(L, to_proof_state(L, 1).get_goals()); +} + +static int proof_state_get_menv(lua_State * L) { + return push_metavar_env(L, to_proof_state(L, 1).get_menv()); +} + +static int proof_state_get_proof_builder(lua_State * L) { + return push_proof_builder(L, to_proof_state(L, 1).get_proof_builder()); +} + +static int proof_state_get_cex_builder(lua_State * L) { + return push_cex_builder(L, to_proof_state(L, 1).get_cex_builder()); +} + +static int proof_state_is_proof_final_state(lua_State * L) { + lua_pushboolean(L, to_proof_state(L, 1).is_proof_final_state()); + return 1; +} + +static int proof_state_is_cex_final_state(lua_State * L) { + lua_pushboolean(L, to_proof_state(L, 1).is_cex_final_state()); + return 1; +} + +static int proof_state_pp(lua_State * L) { + int nargs = lua_gettop(L); + proof_state & s = to_proof_state(L, 1); + if (nargs == 1) { + return push_format(L, s.pp(get_global_formatter(L), get_global_options(L))); + } else if (nargs == 2) { + if (is_formatter(L, 2)) + return push_format(L, s.pp(to_formatter(L, 2), get_global_options(L))); + else + return push_format(L, s.pp(get_global_formatter(L), to_options(L, 2))); + } else { + return push_format(L, s.pp(to_formatter(L, 2), to_options(L, 3))); + } +} + +static const struct luaL_Reg proof_state_m[] = { + {"__gc", proof_state_gc}, // never throws + {"__tostring", safe_function}, + {"pp", safe_function}, + {"get_precision", safe_function}, + {"get_goals", safe_function}, + {"get_menv", safe_function}, + {"get_proof_builder", safe_function}, + {"get_cex_builder", safe_function}, + {"precision", safe_function}, + {"goals", safe_function}, + {"menv", safe_function}, + {"proof_builder", safe_function}, + {"cex_builder", safe_function}, + {"is_proof_final_state", safe_function}, + {"is_cex_final_state", safe_function}, + {0, 0} +}; + +void open_proof_state(lua_State * L) { + luaL_newmetatable(L, goals_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, goals_m, 0); + + SET_GLOBAL_FUN(goals_pred, "is_goals"); + SET_GLOBAL_FUN(mk_goals, "goals"); + + luaL_newmetatable(L, proof_state_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, proof_state_m, 0); + + SET_GLOBAL_FUN(proof_state_pred, "is_proof_state"); + SET_GLOBAL_FUN(mk_proof_state, "proof_state"); + SET_GLOBAL_FUN(to_proof_state, "to_proof_state"); + + lua_newtable(L); + SET_ENUM("Precise", precision::Precise); + SET_ENUM("Over", precision::Over); + SET_ENUM("Under", precision::Under); + SET_ENUM("UnderOver", precision::UnderOver); + lua_setglobal(L, "precision"); +} +} diff --git a/src/bindings/lua/proof_state.h b/src/bindings/lua/proof_state.h new file mode 100644 index 000000000..725d0cbd8 --- /dev/null +++ b/src/bindings/lua/proof_state.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 +#include "library/tactic/proof_state.h" +namespace lean { +UDATA_DEFS_CORE(goals) +UDATA_DEFS(proof_state) +void open_proof_state(lua_State * L); +} diff --git a/tests/lua/proof_state1.lua b/tests/lua/proof_state1.lua new file mode 100644 index 000000000..8867b1f77 --- /dev/null +++ b/tests/lua/proof_state1.lua @@ -0,0 +1,27 @@ +local ps = proof_state() +local env = environment() +local Bool = Const("Bool") +env:add_var("p", Bool) +env:add_var("q", Bool) +local p, q = Consts("p, q") +local ctx = context() +ctx = ctx:extend("H1", p) +ctx = ctx:extend("H2", q) +ps = to_proof_state(env, ctx, p) +print(ps) +for n, g in ps:goals():pairs() do + assert(is_goal(g)) + print(n, g) +end +assert(#(ps:goals()) == 1) +assert(ps:goals():tail():is_nil()) +assert(ps:goals():head() == name("main")) +assert(not ps:goals():empty()) +assert(ps:precision() == precision.Precise) +local menv = ps:menv() +local pb = ps:proof_builder() +local cb = ps:cex_builder() +assert(not ps:is_proof_final_state()) +assert(not ps:is_cex_final_state()) + +