feat(library/kernel_bindings): add new global level methods to environment Lua API

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

src/library/kernel_bindings.cpp

@@ -829,6 +829,8 @@ static int environment_trust_lvl(lua_State * L) { return push_integer(L, to_envi
 static int environment_proof_irrel(lua_State * L) { return push_boolean(L, to_environment(L, 1).proof_irrel()); }
 static int environment_eta(lua_State * L) { return push_boolean(L, to_environment(L, 1).eta()); }
 static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); }
+static int environment_add_global_level(lua_State * L) { return push_environment(L, to_environment(L, 1).add_global_level(to_name_ext(L, 2))); }
+static int environment_is_global_level(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_global_level(to_name_ext(L, 2))); }
 static int environment_find(lua_State * L) { return push_optional_definition(L, to_environment(L, 1).find(to_name_ext(L, 2))); }
 static int environment_get(lua_State * L) { return push_definition(L, to_environment(L, 1).get(to_name_ext(L, 2))); }
 static int environment_add(lua_State * L) { return push_environment(L, to_environment(L, 1).add(to_certified_definition(L, 2))); }
@@ -838,16 +840,18 @@ static int mk_empty_environment(lua_State * L) {
 }
 
 static const struct luaL_Reg environment_m[] = {
-    {"__gc",           environment_gc}, // never throws
-    {"is_descendant",  safe_function<environment_is_descendant>},
-    {"trust_lvl",      safe_function<environment_trust_lvl>},
-    {"proof_irrel",    safe_function<environment_proof_irrel>},
-    {"eta",            safe_function<environment_eta>},
-    {"impredicative",  safe_function<environment_impredicative>},
-    {"find",           safe_function<environment_find>},
-    {"get",            safe_function<environment_get>},
-    {"add",            safe_function<environment_add>},
-    {"replace",        safe_function<environment_replace>},
+    {"__gc",             environment_gc}, // never throws
+    {"is_descendant",    safe_function<environment_is_descendant>},
+    {"trust_lvl",        safe_function<environment_trust_lvl>},
+    {"proof_irrel",      safe_function<environment_proof_irrel>},
+    {"eta",              safe_function<environment_eta>},
+    {"impredicative",    safe_function<environment_impredicative>},
+    {"add_global_level", safe_function<environment_add_global_level>},
+    {"is_global_level",  safe_function<environment_is_global_level>},
+    {"find",             safe_function<environment_find>},
+    {"get",              safe_function<environment_get>},
+    {"add",              safe_function<environment_add>},
+    {"replace",          safe_function<environment_replace>},
     {0, 0}
 };
 

tests/lua/env1.lua

@@ -0,0 +1,9 @@
+local env = empty_environment()
+assert(is_environment(env))
+assert(not env:is_global_level("U"))
+local env2 = env:add_global_level("U")
+assert(not env:is_global_level("U"))
+assert(env2:is_global_level("U"))
+assert(env:eta())
+assert(env:proof_irrel())
+assert(env:impredicative())