feat(library/kernel_bindings): add add_decl and type_check functions to Lua API

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

src/kernel/environment.h

@@ -190,7 +190,7 @@ class name_generator;
    Only the type_checker class can create certified definitions.
 */
 class certified_definition {
-    friend certified_definition check(environment const & env, name_generator const & g, definition const & d, bool memoize, name_set const & extra_opaque);
+    friend certified_definition check(environment const & env, definition const & d, name_generator const & g, name_set const & extra_opaque, bool memoize);
     environment_id m_id;
     definition     m_definition;
     certified_definition(environment_id const & id, definition const & d):m_id(id), m_definition(d) {}

src/kernel/type_checker.cpp

@@ -444,6 +444,11 @@ type_checker::type_checker(environment const & env, name_generator const & g, co
 type_checker::type_checker(environment const & env, name_generator const & g, std::unique_ptr<converter> && conv, bool memoize):
     type_checker(env, g, g_no_constraint_handler, std::move(conv), memoize) {}
 
+static name g_tmp_prefix = name::mk_internal_unique_name();
+
+type_checker::type_checker(environment const & env):
+    type_checker(env, name_generator(g_tmp_prefix), g_no_constraint_handler, mk_default_converter(env), true) {}
+
 type_checker::~type_checker() {}
 expr type_checker::infer(expr const & t) { return m_ptr->infer_type(t); }
 expr type_checker::check(expr const & t, param_names const & ps) { return m_ptr->check(t, ps); }
@@ -479,7 +484,7 @@ struct simple_constraint_handler : public constraint_handler {
     virtual void add_cnstr(constraint const & c) { m_cnstrs.push_back(c); }
 };
 
-certified_definition check(environment const & env, name_generator const & g, definition const & d, bool memoize, name_set const & extra_opaque) {
+certified_definition check(environment const & env, definition const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) {
     check_no_mlocal(env, d.get_type());
     if (d.is_definition())
         check_no_mlocal(env, d.get_value());
@@ -514,4 +519,8 @@ certified_definition check(environment const & env, name_generator const & g, de
 
     return certified_definition(env.get_id(), d);
 }
+
+certified_definition check(environment const & env, definition const & d, name_set const & extra_opaque, bool memoize) {
+    return check(env, d, name_generator(g_tmp_prefix), extra_opaque, memoize);
+}
 }

src/kernel/type_checker.h

@@ -61,6 +61,7 @@ public:
     type_checker(environment const & env, name_generator const & g, std::unique_ptr<converter> && conv, bool memoize = true);
     type_checker(environment const & env, name_generator const & g, bool memoize = true):
         type_checker(env, g, mk_default_converter(env), memoize) {}
+    type_checker(environment const & env);
     ~type_checker();
 
     /**
@@ -102,5 +103,7 @@ public:
    \brief Type check the given definition, and return a certified definition if it is type correct.
    Throw an exception if the definition is type incorrect.
 */
-certified_definition check(environment const & env, name_generator const & g, definition const & d, bool memoize, name_set const & extra_opaque);
+certified_definition check(environment const & env, definition const & d,
+                           name_generator const & g, name_set const & extra_opaque = name_set(), bool memoize = true);
+certified_definition check(environment const & env, definition const & d, name_set const & extra_opaque = name_set(), bool memoize = true);
 }

src/library/kernel_bindings.cpp

@@ -1422,7 +1422,9 @@ static void get_type_checker_args(lua_State * L, int idx, optional<module_idx> &
 
 int mk_type_checker(lua_State * L) {
     int nargs = lua_gettop(L);
-    if (nargs <= 2) {
+    if (nargs == 1) {
+        return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1)));
+    } else if (nargs == 2) {
         return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2)));
     } else if (nargs == 3 && is_lua_constraint_handler(L, 3)) {
         return push_type_checker_ref(L, std::make_shared<type_checker>(to_environment(L, 1), to_name_generator(L, 2),
@@ -1473,6 +1475,34 @@ static const struct luaL_Reg type_checker_ref_m[] = {
     {0, 0}
 };
 
+// type_check procedure
+static int type_check(lua_State * L) {
+    int nargs = lua_gettop(L);
+    if (nargs == 2)
+        return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2)));
+    else if (nargs == 3)
+        return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3)));
+    else if (nargs == 4)
+        return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4)));
+    else
+        return push_certified_definition(L, check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4),
+                                                  lua_toboolean(L, 5)));
+}
+
+static int add_declaration(lua_State * L) {
+    int nargs = lua_gettop(L);
+    optional<certified_definition> d;
+    if (nargs == 2)
+        d = check(to_environment(L, 1), to_definition(L, 2));
+    else if (nargs == 3)
+        d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3));
+    else if (nargs == 4)
+        d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4));
+    else
+        d = check(to_environment(L, 1), to_definition(L, 2), to_name_generator(L, 3), to_name_set(L, 4), lua_toboolean(L, 5));
+    return push_environment(L, to_environment(L, 1).add(*d));
+}
+
 static void open_type_checker(lua_State * L) {
     luaL_newmetatable(L, type_checker_ref_mt);
     lua_pushvalue(L, -1);
@@ -1481,6 +1511,9 @@ static void open_type_checker(lua_State * L) {
 
     SET_GLOBAL_FUN(mk_type_checker, "type_checker");
     SET_GLOBAL_FUN(type_checker_ref_pred, "is_type_checker");
+    SET_GLOBAL_FUN(type_check, "type_check");
+    SET_GLOBAL_FUN(type_check, "check");
+    SET_GLOBAL_FUN(add_declaration, "add_decl");
 }
 
 void open_kernel_module(lua_State * L) {

src/tests/kernel/environment.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 using namespace lean;
 
 static environment add_def(environment const & env, definition const & d) {
-    auto cd = check(env, name_generator("test"), d, true, name_set());
+    auto cd = check(env, d, name_generator("test"));
     return env.add(cd);
 }
 

tests/lua/env3.lua

@@ -0,0 +1,21 @@
+function init(env)
+   env = add_decl(env, mk_var_decl("A", Bool))
+   env = add_decl(env, mk_var_decl("And", mk_arrow(Bool, mk_arrow(Bool, Bool))))
+   env = add_decl(env, mk_axiom("p", Const("A")))
+   env = add_decl(env, mk_axiom("q", Const("A")))
+   return env
+end
+local And = Const("And")
+local p   = Const("p")
+local q   = Const("q")
+
+local env = init(empty_environment())
+local t   = type_checker(env)
+assert(t:is_def_eq(p, q))
+assert(t:is_def_eq(And(p, q), And(q, p)))
+
+env = init(empty_environment({proof_irrel=false}))
+t   = type_checker(env)
+assert(not t:is_def_eq(p, q))
+assert(not t:is_def_eq(And(p, q), And(q, p)))
+