diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index 092770a25..dbac630c1 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/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}) diff --git a/src/bindings/lua/environment.cpp b/src/bindings/lua/environment.cpp index 8133422e0..8a041872b 100644 --- a/src/bindings/lua/environment.cpp +++ b/src/bindings/lua/environment.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #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}, {"has_object", safe_function}, {"check_type", safe_function}, + {"infer_type", safe_function}, {"normalize", safe_function}, {"objects", safe_function}, {"local_objects", safe_function}, diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index db97ee2b0..6095edeee 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/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); diff --git a/src/bindings/lua/type_inferer.cpp b/src/bindings/lua/type_inferer.cpp new file mode 100644 index 000000000..f79c793e4 --- /dev/null +++ b/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 +#include +#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(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}, + {"clear", safe_function}, + {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"); +} +} diff --git a/src/bindings/lua/type_inferer.h b/src/bindings/lua/type_inferer.h new file mode 100644 index 000000000..e02d905da --- /dev/null +++ b/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 +namespace lean { +void open_type_inferer(lua_State * L); +} diff --git a/src/kernel/environment.h b/src/kernel/environment.h index f27ee8bc4..4b4b9d626 100644 --- a/src/kernel/environment.h +++ b/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 /** diff --git a/tests/lua/ty1.lua b/tests/lua/ty1.lua new file mode 100644 index 000000000..d6bf72791 --- /dev/null +++ b/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))