From c8fff453192416edae3dfe434c96486c353b272f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 16 Nov 2013 10:39:17 -0800 Subject: [PATCH] feat(lua): add justification objects to Lua API Signed-off-by: Leonardo de Moura --- src/bindings/lua/CMakeLists.txt | 3 +- src/bindings/lua/justification.cpp | 143 +++++++++++++++++++++++++++++ src/bindings/lua/justification.h | 12 +++ src/bindings/lua/leanlua_state.cpp | 2 + 4 files changed, 159 insertions(+), 1 deletion(-) create mode 100644 src/bindings/lua/justification.cpp create mode 100644 src/bindings/lua/justification.h diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index fd91572b4..b94decdb6 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/src/bindings/lua/CMakeLists.txt @@ -1,6 +1,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 state.cpp leanlua_state.cpp frontend_lean.cpp) +formatter.cpp justification.cpp state.cpp leanlua_state.cpp +frontend_lean.cpp) target_link_libraries(lua ${LEAN_LIBS}) diff --git a/src/bindings/lua/justification.cpp b/src/bindings/lua/justification.cpp new file mode 100644 index 000000000..14a16e222 --- /dev/null +++ b/src/bindings/lua/justification.cpp @@ -0,0 +1,143 @@ +/* +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 "kernel/justification.h" +#include "bindings/lua/util.h" +#include "bindings/lua/options.h" +#include "bindings/lua/expr.h" +#include "bindings/lua/format.h" +#include "bindings/lua/formatter.h" + +namespace lean { +DECL_UDATA(justification) + +static int justification_tostring(lua_State * L) { + std::ostringstream out; + justification & jst = to_justification(L, 1); + if (jst) { + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + out << mk_pair(jst.pp(fmt, opts, nullptr, false), opts); + } else { + out << ""; + } + lua_pushstring(L, out.str().c_str()); + return 1; +} + +static int justification_has_children(lua_State * L) { + lua_pushboolean(L, to_justification(L, 1).has_children()); + return 1; +} + +static int justification_is_null(lua_State * L) { + lua_pushboolean(L, !to_justification(L, 1)); + return 1; +} + +/** + \brief Iterator (closure base function) for justification children. See \c justification_children +*/ +static int justification_next_child(lua_State * L) { + unsigned i = lua_tointeger(L, lua_upvalueindex(2)); + unsigned num = objlen(L, lua_upvalueindex(1)); + if (i > num) { + lua_pushnil(L); + } else { + lua_pushinteger(L, i + 1); + lua_replace(L, lua_upvalueindex(2)); // update i + lua_rawgeti(L, lua_upvalueindex(1), i); // read children[i] + } + return 1; +} + +static int justification_children(lua_State * L) { + buffer children; + to_justification(L, 1).get_children(children); + lua_newtable(L); + int i = 1; + for (auto jcell : children) { + push_justification(L, justification(jcell)); + lua_rawseti(L, -2, i); + i = i + 1; + } + lua_pushinteger(L, 1); + lua_pushcclosure(L, &justification_next_child, 2); // create closure with 2 upvalues + return 1; +} + +static int justification_get_main_expr(lua_State * L) { + return push_expr(L, to_justification(L, 1).get_main_expr()); +} + +static int justification_pp(lua_State * L) { + int nargs = lua_gettop(L); + justification & jst = to_justification(L, 1); + formatter fmt = get_global_formatter(L); + options opts = get_global_options(L); + bool display_children = true; + + if (nargs == 2) { + if (lua_isboolean(L, 2)) { + display_children = lua_toboolean(L, 2); + } else { + luaL_checktype(L, 2, LUA_TTABLE); + + lua_pushstring(L, "formatter"); + lua_gettable(L, 2); + if (is_formatter(L, -1)) + fmt = to_formatter(L, -1); + lua_pop(L, 1); + + lua_pushstring(L, "options"); + lua_gettable(L, 2); + if (is_options(L, -1)) + opts = to_options(L, -1); + lua_pop(L, 1); + + lua_pushstring(L, "display_children"); + lua_gettable(L, 2); + if (lua_isboolean(L, -1)) + display_children = lua_toboolean(L, -1); + lua_pop(L, 1); + } + } + return push_format(L, jst.pp(fmt, opts, nullptr, display_children)); +} + +static int justification_depends_on(lua_State * L) { + lua_pushboolean(L, depends_on(to_justification(L, 1), to_justification(L, 2))); + return 1; +} + +static int mk_assumption_justification(lua_State * L) { + return push_justification(L, mk_assumption_justification(luaL_checkinteger(L, 1))); +} + +static const struct luaL_Reg justification_m[] = { + {"__gc", justification_gc}, // never throws + {"__tostring", safe_function}, + {"is_null", safe_function}, + {"has_children", safe_function}, + {"children", safe_function}, + {"get_main_expr", safe_function}, + {"pp", safe_function}, + {"depends_on", safe_function}, + {0, 0} +}; + +void open_justification(lua_State * L) { + luaL_newmetatable(L, justification_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, justification_m, 0); + + SET_GLOBAL_FUN(mk_assumption_justification, "mk_assumption_justification"); + SET_GLOBAL_FUN(justification_pred, "is_justification"); +} +} diff --git a/src/bindings/lua/justification.h b/src/bindings/lua/justification.h new file mode 100644 index 000000000..e534315c8 --- /dev/null +++ b/src/bindings/lua/justification.h @@ -0,0 +1,12 @@ +/* +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(justification) +void open_justification(lua_State * L); +} diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index 37294ad7b..7887e1bbd 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -30,6 +30,7 @@ Author: Leonardo de Moura #include "bindings/lua/context.h" #include "bindings/lua/object.h" #include "bindings/lua/environment.h" +#include "bindings/lua/justification.h" #include "bindings/lua/state.h" #include "bindings/lua/frontend_lean.h" #include "bindings/lua/lean.lua" @@ -176,6 +177,7 @@ struct leanlua_state::imp { open_context(m_state); open_object(m_state); open_environment(m_state); + open_justification(m_state); open_state(m_state); open_frontend_lean(m_state); open_thread(m_state);