feat(lua): add type_inferer object to Lua API

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

src/bindings/lua/CMakeLists.txt

@@ -1,7 +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 justification.cpp metavar_env.cpp state.cpp
-leanlua_state.cpp frontend_lean.cpp)
+formatter.cpp justification.cpp metavar_env.cpp type_inferer.cpp
+state.cpp leanlua_state.cpp frontend_lean.cpp)
 
 target_link_libraries(lua ${LEAN_LIBS})

src/bindings/lua/environment.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <lua.hpp>
 #include "kernel/environment.h"
 #include "kernel/formatter.h"
+#include "library/type_inferer.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
 #include "bindings/lua/options.h"
@@ -185,6 +186,15 @@ static int environment_local_objects(lua_State * L) {
     return environment_objects_core(L, true);
 }
 
+static int environment_infer_type(lua_State * L) {
+    int nargs = lua_gettop(L);
+    type_inferer inferer(to_environment(L, 1));
+    if (nargs == 2)
+        return push_expr(L, inferer(to_nonnull_expr(L, 2)));
+    else
+        return push_expr(L, inferer(to_nonnull_expr(L, 2), to_context(L, 3)));
+}
+
 static int environment_tostring(lua_State * L) {
     ro_environment env(L, 1);
     std::ostringstream out;
@@ -211,6 +221,7 @@ static const struct luaL_Reg environment_m[] = {
     {"find_object",    safe_function<environment_find_object>},
     {"has_object",     safe_function<environment_has_object>},
     {"check_type",     safe_function<environment_check_type>},
+    {"infer_type",     safe_function<environment_infer_type>},
     {"normalize",      safe_function<environment_normalize>},
     {"objects",        safe_function<environment_objects>},
     {"local_objects",  safe_function<environment_local_objects>},

src/bindings/lua/leanlua_state.cpp

@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/justification.h"
 #include "bindings/lua/metavar_env.h"
 #include "bindings/lua/state.h"
+#include "bindings/lua/type_inferer.h"
 #include "bindings/lua/frontend_lean.h"
 #include "bindings/lua/lean.lua"
 
@@ -181,6 +182,7 @@ struct leanlua_state::imp {
         open_justification(m_state);
         open_metavar_env(m_state);
         open_state(m_state);
+        open_type_inferer(m_state);
         open_frontend_lean(m_state);
         open_thread(m_state);
         open_interrupt(m_state);

src/bindings/lua/type_inferer.cpp

@@ -0,0 +1,59 @@
+/*
+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 "library/type_inferer.h"
+#include "bindings/lua/util.h"
+#include "bindings/lua/expr.h"
+#include "bindings/lua/context.h"
+#include "bindings/lua/environment.h"
+
+namespace lean {
+constexpr char const * type_inferer_mt = "type_inferer";
+type_inferer & to_type_inferer(lua_State * L, int i) { return *static_cast<type_inferer*>(luaL_checkudata(L, i, type_inferer_mt)); }
+DECL_PRED(type_inferer)
+DECL_GC(type_inferer)
+
+static int type_inferer_call(lua_State * L) {
+    int nargs = lua_gettop(L);
+    type_inferer & inferer = to_type_inferer(L, 1);
+    if (nargs == 2)
+        return push_expr(L, inferer(to_nonnull_expr(L, 2)));
+    else
+        return push_expr(L, inferer(to_nonnull_expr(L, 2), to_context(L, 3)));
+}
+
+static int type_inferer_clear(lua_State * L) {
+    to_type_inferer(L, 1).clear();
+    return 0;
+}
+
+static int mk_type_inferer(lua_State * L) {
+    void * mem = lua_newuserdata(L, sizeof(type_inferer));
+    new (mem) type_inferer(to_environment(L, 1));
+    luaL_getmetatable(L, type_inferer_mt);
+    lua_setmetatable(L, -2);
+    return 1;
+}
+
+static const struct luaL_Reg type_inferer_m[] = {
+    {"__gc",            type_inferer_gc}, // never throws
+    {"__call",          safe_function<type_inferer_call>},
+    {"clear",           safe_function<type_inferer_clear>},
+    {0, 0}
+};
+
+void open_type_inferer(lua_State * L) {
+    luaL_newmetatable(L, type_inferer_mt);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, type_inferer_m, 0);
+
+    SET_GLOBAL_FUN(mk_type_inferer,          "type_inferer");
+    SET_GLOBAL_FUN(type_inferer_pred,        "is_type_inferer");
+}
+}

src/bindings/lua/type_inferer.h

@@ -0,0 +1,11 @@
+/*
+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 {
+void open_type_inferer(lua_State * L);
+}

src/kernel/environment.h

@@ -28,6 +28,8 @@ private:
 public:
     environment();
     ~environment();
+
+    friend bool is_eqp(environment const & env1, environment const & env2) { return env1.m_ptr.get() == env2.m_ptr.get(); }
     // =======================================
     // Parent/Child environment management
     /**

tests/lua/ty1.lua

@@ -0,0 +1,12 @@
+local env1 = environment()
+local env2 = environment()
+env1:add_var("N", Type())
+env1:add_var("x", Const("N"))
+env2:add_var("N", Type())
+local x = Const("x")
+local N = Const("N")
+print(env1:infer_type(x))
+local infer1 = type_inferer(env1)
+local infer2 = type_inferer(env2)
+assert(env1:infer_type(x) == infer1(x))
+assert(env2:infer_type(N) == infer2(N))