feat(lua): add justification objects to Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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 <sstream>
+#include <lua.hpp>
+#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 << "<null-justification>";
+    }
+    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<justification_cell*> 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<justification_tostring>},
+    {"is_null",         safe_function<justification_is_null>},
+    {"has_children",    safe_function<justification_has_children>},
+    {"children",        safe_function<justification_children>},
+    {"get_main_expr",   safe_function<justification_get_main_expr>},
+    {"pp",              safe_function<justification_pp>},
+    {"depends_on",      safe_function<justification_depends_on>},
+    {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");
+}
+}

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 <lua.hpp>
+namespace lean {
+UDATA_DEFS(justification)
+void open_justification(lua_State * L);
+}

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);