feat(lua): expose kernel objects in the Lua API

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

src/bindings/lua/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp
 options.cpp sexpr.cpp format.cpp level.cpp local_context.cpp expr.cpp
-context.cpp environment.cpp leanlua_state.cpp)
+context.cpp object.cpp environment.cpp leanlua_state.cpp)
 
 target_link_libraries(lua ${LEAN_LIBS})

src/bindings/lua/environment.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/name.h"
 #include "bindings/lua/level.h"
 #include "bindings/lua/expr.h"
+#include "bindings/lua/object.h"
 #include "bindings/lua/context.h"
 #include "bindings/lua/environment.h"
 
@@ -51,6 +52,25 @@ static int mk_environment(lua_State * L) {
     return push_environment(L, environment());
 }
 
+static int environment_has_parent(lua_State * L) {
+    ro_environment env(L, 1);
+    lua_pushboolean(L, env->has_parent());
+    return 1;
+}
+
+static int environment_has_children(lua_State * L) {
+    ro_environment env(L, 1);
+    lua_pushboolean(L, env->has_children());
+    return 1;
+}
+
+static int environment_parent(lua_State * L) {
+    ro_environment env(L, 1);
+    if (!env->has_parent())
+        throw exception("environment does not have a parent environment");
+    return push_environment(L, env->parent());
+}
+
 static int environment_add_uvar(lua_State * L) {
     rw_environment env(L, 1);
     int nargs = lua_gettop(L);
@@ -106,6 +126,17 @@ static int environment_add_axiom(lua_State * L) {
     return 0;
 }
 
+static int environment_find_object(lua_State * L) {
+    ro_environment env(L, 1);
+    return push_object(L, env->find_object(to_name_ext(L, 2)));
+}
+
+static int environment_has_object(lua_State * L) {
+    ro_environment env(L, 1);
+    lua_pushboolean(L, env->has_object(to_name_ext(L, 2)));
+    return 1;
+}
+
 static int environment_check_type(lua_State * L) {
     ro_environment env(L, 1);
     int nargs = lua_gettop(L);
@@ -124,6 +155,30 @@ static int environment_normalize(lua_State * L) {
         return push_expr(L, env->normalize(to_nonnull_expr(L, 2), to_context(L, 3)));
 }
 
+static int environment_objects(lua_State * L) {
+    ro_environment env(L, 1);
+    auto it  = env->begin_objects();
+    auto end = env->end_objects();
+    lua_newtable(L);
+    for (int i = 1; it != end; ++it, ++i) {
+        push_object(L, *it);
+        lua_rawseti(L, -2, i);
+    }
+    return 1;
+}
+
+static int environment_local_objects(lua_State * L) {
+    ro_environment env(L, 1);
+    auto it  = env->begin_local_objects();
+    auto end = env->end_local_objects();
+    lua_newtable(L);
+    for (int i = 1; it != end; ++it, ++i) {
+        push_object(L, *it);
+        lua_rawseti(L, -2, i);
+    }
+    return 1;
+}
+
 static int environment_pred(lua_State * L) {
     lua_pushboolean(L, is_environment(L, 1));
     return 1;
@@ -142,6 +197,9 @@ static int environment_tostring(lua_State * L) {
 static const struct luaL_Reg environment_m[] = {
     {"__gc",           environment_gc}, // never throws
     {"__tostring",     safe_function<environment_tostring>},
+    {"has_parent",     safe_function<environment_has_parent>},
+    {"has_children",   safe_function<environment_has_children>},
+    {"parent",         safe_function<environment_parent>},
     {"add_uvar",       safe_function<environment_add_uvar>},
     {"is_ge",          safe_function<environment_is_ge>},
     {"get_uvar",       safe_function<environment_get_uvar>},
@@ -149,8 +207,12 @@ static const struct luaL_Reg environment_m[] = {
     {"add_theorem",    safe_function<environment_add_theorem>},
     {"add_var",        safe_function<environment_add_var>},
     {"add_axiom",      safe_function<environment_add_axiom>},
+    {"find_object",    safe_function<environment_find_object>},
+    {"has_object",     safe_function<environment_has_object>},
     {"check_type",     safe_function<environment_check_type>},
     {"normalize",      safe_function<environment_normalize>},
+    {"objects",        safe_function<environment_objects>},
+    {"local_objects",  safe_function<environment_local_objects>},
     {0, 0}
 };
 

src/bindings/lua/leanlua_state.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/local_context.h"
 #include "bindings/lua/expr.h"
 #include "bindings/lua/context.h"
+#include "bindings/lua/object.h"
 #include "bindings/lua/environment.h"
 #include "bindings/lua/lean.lua"
 
@@ -97,6 +98,7 @@ struct leanlua_state::imp {
         open_local_context(m_state);
         open_expr(m_state);
         open_context(m_state);
+        open_object(m_state);
         open_environment(m_state);
         open_state(m_state);
         open_thread(m_state);

src/bindings/lua/object.cpp

@@ -0,0 +1,178 @@
+/*
+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/object.h"
+#include "bindings/lua/util.h"
+#include "bindings/lua/name.h"
+#include "bindings/lua/level.h"
+#include "bindings/lua/expr.h"
+
+namespace lean {
+constexpr char const * object_mt = "object.mt";
+
+bool is_object(lua_State * L, int idx) {
+    return testudata(L, idx, object_mt);
+}
+
+object & to_object(lua_State * L, int idx) {
+    return *static_cast<object*>(luaL_checkudata(L, idx, object_mt));
+}
+
+object & to_nonnull_object(lua_State * L, int idx) {
+    object & r = to_object(L, idx);
+    if (!r)
+        throw exception("non-null kernel object expected");
+    return r;
+}
+
+int push_object(lua_State * L, object const & o) {
+    void * mem = lua_newuserdata(L, sizeof(object));
+    new (mem) object(o);
+    luaL_getmetatable(L, object_mt);
+    lua_setmetatable(L, -2);
+    return 1;
+}
+
+static int object_gc(lua_State * L) {
+    to_object(L, 1).~object();
+    return 0;
+}
+
+static int object_is_null(lua_State * L) {
+    lua_pushboolean(L, !to_object(L, 1));
+    return 1;
+}
+
+static int object_keyword(lua_State * L) {
+    lua_pushfstring(L, to_nonnull_object(L, 1).keyword());
+    return 1;
+}
+
+static int object_has_name(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).has_name());
+    return 1;
+}
+
+static int object_get_name(lua_State * L) {
+    if (!to_nonnull_object(L, 1).has_name())
+        throw exception("kernel object does not have a name");
+    return push_name(L, to_nonnull_object(L, 1).get_name());
+}
+
+static int object_has_type(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).has_type());
+    return 1;
+}
+
+static int object_get_type(lua_State * L) {
+    if (!to_nonnull_object(L, 1).has_type())
+        throw exception("kernel object does not have a type");
+    return push_expr(L, to_nonnull_object(L, 1).get_type());
+}
+
+static int object_has_cnstr_level(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).has_cnstr_level());
+    return 1;
+}
+
+static int object_get_cnstr_level(lua_State * L) {
+    if (!to_nonnull_object(L, 1).has_cnstr_level())
+        throw exception("kernel object does not have a constraint level");
+    return push_level(L, to_nonnull_object(L, 1).get_cnstr_level());
+}
+
+static int object_is_definition(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).is_definition());
+    return 1;
+}
+
+static int object_is_opaque(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).is_opaque());
+    return 1;
+}
+
+static int object_get_value(lua_State * L) {
+    if (!to_nonnull_object(L, 1).is_definition())
+        throw exception("kernel object is not a definition/theorem");
+    return push_expr(L, to_nonnull_object(L, 1).get_value());
+}
+
+static int object_get_weight(lua_State * L) {
+    if (!to_nonnull_object(L, 1).is_definition())
+        throw exception("kernel object is not a definition");
+    lua_pushinteger(L, to_nonnull_object(L, 1).get_weight());
+    return 1;
+}
+
+static int object_is_axiom(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).is_axiom());
+    return 1;
+}
+
+static int object_is_theorem(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).is_theorem());
+    return 1;
+}
+
+static int object_is_var_decl(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).is_var_decl());
+    return 1;
+}
+
+static int object_is_builtin(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).is_builtin());
+    return 1;
+}
+
+static int object_is_builtin_set(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).is_builtin_set());
+    return 1;
+}
+
+static int object_in_builtin_set(lua_State * L) {
+    lua_pushboolean(L, to_nonnull_object(L, 1).in_builtin_set(to_expr(L, 2)));
+    return 1;
+}
+
+static int object_pred(lua_State * L) {
+    lua_pushboolean(L, is_object(L, 1));
+    return 1;
+}
+
+static const struct luaL_Reg object_m[] = {
+    {"__gc",            object_gc}, // never throws
+    {"is_null",         safe_function<object_is_null>},
+    {"keyword",         safe_function<object_keyword>},
+    {"has_name",        safe_function<object_has_name>},
+    {"get_name",        safe_function<object_get_name>},
+    {"has_type",        safe_function<object_has_type>},
+    {"get_type",        safe_function<object_get_type>},
+    {"has_cnstr_level", safe_function<object_has_cnstr_level>},
+    {"get_cnstr_level", safe_function<object_get_cnstr_level>},
+    {"is_definition",   safe_function<object_is_definition>},
+    {"is_opaque",       safe_function<object_is_opaque>},
+    {"get_value",       safe_function<object_get_value>},
+    {"get_weight",      safe_function<object_get_weight>},
+    {"is_axiom",        safe_function<object_is_axiom>},
+    {"is_theorem",      safe_function<object_is_theorem>},
+    {"is_var_decl",     safe_function<object_is_var_decl>},
+    {"is_builtin",      safe_function<object_is_builtin>},
+    {"is_builtin_set",  safe_function<object_is_builtin_set>},
+    {"in_builtin_set",  safe_function<object_in_builtin_set>},
+    {0, 0}
+};
+
+void open_object(lua_State * L) {
+    luaL_newmetatable(L, object_mt);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, object_m, 0);
+
+    set_global_function<object_pred>(L, "is_kernel_object");
+}
+}

src/bindings/lua/object.h

@@ -0,0 +1,15 @@
+/*
+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 {
+class object;
+void open_object(lua_State * L);
+bool is_object(lua_State * L, int idx);
+object & to_object(lua_State * L, int idx);
+int push_object(lua_State * L, object const & o);
+}

tests/lua/env2.lua

@@ -0,0 +1,16 @@
+env = environment()
+env:add_var("N", Type())
+env:add_var("x", Const("N"))
+for i, v in ipairs(env:objects()) do
+   print(v:get_name())
+end
+assert(not env:find_object("N"):is_null())
+assert(env:find_object("Z"):is_null())
+assert(env:find_object("N"):is_var_decl())
+assert(env:find_object("N"):has_type())
+assert(env:find_object("N"):has_name())
+assert(env:find_object("N"):get_type() == Type())
+assert(env:find_object("N"):get_name() == name("N"))
+assert(env:find_object("x"):get_type() == Const("N"))
+assert(not env:has_parent())
+assert(not env:has_children())