diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index 6f9bf667a..d50fe0eb6 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/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 leanlua_state.cpp) +context.cpp environment.cpp leanlua_state.cpp) target_link_libraries(lua ${LEAN_LIBS}) diff --git a/src/bindings/lua/environment.cpp b/src/bindings/lua/environment.cpp new file mode 100644 index 000000000..82b455462 --- /dev/null +++ b/src/bindings/lua/environment.cpp @@ -0,0 +1,132 @@ +/* +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 "kernel/environment.h" +#include "bindings/lua/util.h" +#include "bindings/lua/name.h" +#include "bindings/lua/level.h" +#include "bindings/lua/expr.h" +#include "bindings/lua/context.h" + +namespace lean { +constexpr char const * environment_mt = "environment.mt"; + +bool is_environment(lua_State * L, int idx) { + return testudata(L, idx, environment_mt); +} + +environment & to_environment(lua_State * L, int idx) { + return *static_cast(luaL_checkudata(L, idx, environment_mt)); +} + +static int environment_gc(lua_State * L) { + to_environment(L, 1).~environment(); + return 0; +} + +static int mk_environment(lua_State * L) { + void * mem = lua_newuserdata(L, sizeof(environment)); + new (mem) environment(); + luaL_getmetatable(L, environment_mt); + lua_setmetatable(L, -2); + return 1; +} + +static int environment_add_uvar(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + to_environment(L, 1).add_uvar(to_name_ext(L, 2)); + else + to_environment(L, 1).add_uvar(to_name_ext(L, 2), to_level(L, 3)); + return 0; +} + +static int environment_is_ge(lua_State * L) { + lua_pushboolean(L, to_environment(L, 1).is_ge(to_level(L, 2), to_level(L, 3))); + return 1; +} + +static int environment_get_uvar(lua_State * L) { + return push_level(L, to_environment(L, 1).get_uvar(to_name_ext(L, 2))); +} + +static int environment_add_definition(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 3) { + to_environment(L, 1).add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3)); + } else if (nargs == 4) { + if (is_expr(L, 4)) + to_environment(L, 1).add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4)); + else + to_environment(L, 1).add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), lua_toboolean(L, 4)); + } else { + to_environment(L, 1).add_definition(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4), lua_toboolean(L, 5)); + } + return 0; +} + +static int environment_add_theorem(lua_State * L) { + to_environment(L, 1).add_theorem(to_name_ext(L, 2), to_nonnull_expr(L, 3), to_nonnull_expr(L, 4)); + return 0; +} + +static int environment_add_var(lua_State * L) { + to_environment(L, 1).add_var(to_name_ext(L, 2), to_nonnull_expr(L, 3)); + return 0; +} + +static int environment_add_axiom(lua_State * L) { + to_environment(L, 1).add_axiom(to_name_ext(L, 2), to_nonnull_expr(L, 3)); + return 0; +} + +static int environment_check_type(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + return push_expr(L, to_environment(L, 1).infer_type(to_nonnull_expr(L, 2))); + else + return push_expr(L, to_environment(L, 1).infer_type(to_nonnull_expr(L, 2), to_context(L, 3))); +} + +static int environment_normalize(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + return push_expr(L, to_environment(L, 1).normalize(to_nonnull_expr(L, 2))); + else + return push_expr(L, to_environment(L, 1).normalize(to_nonnull_expr(L, 2), to_context(L, 3))); +} + +static int environment_pred(lua_State * L) { + lua_pushboolean(L, is_environment(L, 1)); + return 1; +} + +static const struct luaL_Reg environment_m[] = { + {"__gc", environment_gc}, // never throws + {"add_uvar", safe_function}, + {"is_ge", safe_function}, + {"get_uvar", safe_function}, + {"add_definition", safe_function}, + {"add_theorem", safe_function}, + {"add_var", safe_function}, + {"add_axiom", safe_function}, + {"check_type", safe_function}, + {"normalize", safe_function}, + {0, 0} +}; + +void open_environment(lua_State * L) { + luaL_newmetatable(L, environment_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, environment_m, 0); + + set_global_function(L, "environment"); + set_global_function(L, "is_environment"); +} +} diff --git a/src/bindings/lua/environment.h b/src/bindings/lua/environment.h new file mode 100644 index 000000000..345aa15fa --- /dev/null +++ b/src/bindings/lua/environment.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 +namespace lean { +class environment; +void open_environment(lua_State * L); +bool is_environment(lua_State * L, int idx); +environment & to_environment(lua_State * L, int idx); +int push_environment(lua_State * L, environment const & o); +} diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index c8dc9ee99..5a8de6f0d 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -22,6 +22,7 @@ Author: Leonardo de Moura #include "bindings/lua/local_context.h" #include "bindings/lua/expr.h" #include "bindings/lua/context.h" +#include "bindings/lua/environment.h" #include "bindings/lua/lean.lua" extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); } @@ -50,6 +51,7 @@ struct leanlua_state::imp { lean::open_local_context(m_state); lean::open_expr(m_state); lean::open_context(m_state); + lean::open_environment(m_state); dostring(g_leanlua_extra); } diff --git a/tests/lua/env1.lua b/tests/lua/env1.lua new file mode 100644 index 000000000..f23569d25 --- /dev/null +++ b/tests/lua/env1.lua @@ -0,0 +1,9 @@ +e = environment() +assert(is_environment(e)) +e:add_uvar("M") +print(e:get_uvar("M")) +e:add_var("N", Type()) +N, M = Consts("N M") +e:add_var("a", N) +x, a = Consts("x, a") +print(e:check_type(fun(x, M, a)))