michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(lua): cleanup Lua bindings, and add accessor/tester to expr Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-13 11:46:09 -08:00
parent c4c548dc5d
commit 450128e28b
15 changed files with 272 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/bindings/lua/context.cpp
View file

@ -146,6 +146,8 @@ static const struct luaL_Reg context_m[] = {
{"__len", safe_function<context_size>},
{"is_empty", safe_function<context_is_empty>},
{"size", safe_function<context_size>},
{"extend", safe_function<context_extend>},
{"lookup", safe_function<context_lookup>},
{0, 0}
};
@ -154,16 +156,16 @@ void open_context(lua_State * L) {
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, context_entry_m, 0);
set_global_function<mk_context_entry>(L, "context_entry");
set_global_function<context_entry_pred>(L, "is_context_entry");
SET_GLOBAL_FUN(mk_context_entry, "context_entry");
SET_GLOBAL_FUN(context_entry_pred, "is_context_entry");
luaL_newmetatable(L, context_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, context_m, 0);
set_global_function<mk_context>(L, "context");
set_global_function<context_pred>(L, "is_context");
set_global_function<context_extend>(L, "extend");
set_global_function<context_lookup>(L, "lookup");
SET_GLOBAL_FUN(mk_context, "context");
SET_GLOBAL_FUN(context_pred, "is_context");
SET_GLOBAL_FUN(context_extend, "extend");
SET_GLOBAL_FUN(context_lookup, "lookup");
}
}

8
src/bindings/lua/environment.cpp
View file

@ -247,9 +247,9 @@ void open_environment(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, environment_m, 0);
set_global_function<mk_environment>(L, "environment");
set_global_function<environment_pred>(L, "is_environment");
set_global_function<get_environment>(L, "get_environment");
set_global_function<get_environment>(L, "env");
SET_GLOBAL_FUN(mk_environment, "environment");
SET_GLOBAL_FUN(environment_pred, "is_environment");
SET_GLOBAL_FUN(get_environment, "get_environment");
SET_GLOBAL_FUN(get_environment, "env");
}
}

193
src/bindings/lua/expr.cpp
View file

@ -40,6 +40,13 @@ expr & to_nonnull_expr(lua_State * L, int idx) {
return r;
}
expr & to_app(lua_State * L, int idx) {
expr & r = to_nonnull_expr(L, idx);
if (!is_app(r))
throw exception("Lean application expression expected");
return r;
}
int push_expr(lua_State * L, expr const & e) {
void * mem = lua_newuserdata(L, sizeof(expr));
new (mem) expr(e);
@ -197,13 +204,139 @@ static int expr_is_null(lua_State * L) {
return 1;
}
static int expr_get_kind(lua_State * L) {
lua_pushinteger(L, static_cast<int>(to_nonnull_expr(L, 1).kind()));
return 1;
}
static int expr_is_constant(lua_State * L) {
lua_pushboolean(L, is_constant(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_var(lua_State * L) {
lua_pushboolean(L, is_var(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_app(lua_State * L) {
lua_pushboolean(L, is_app(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_eq(lua_State * L) {
lua_pushboolean(L, is_eq(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_lambda(lua_State * L) {
lua_pushboolean(L, is_lambda(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_pi(lua_State * L) {
lua_pushboolean(L, is_lambda(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_abstraction(lua_State * L) {
lua_pushboolean(L, is_abstraction(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_let(lua_State * L) {
lua_pushboolean(L, is_let(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_value(lua_State * L) {
lua_pushboolean(L, is_value(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_metavar(lua_State * L) {
lua_pushboolean(L, is_metavar(to_nonnull_expr(L, 1)));
return 1;
}
/**
\brief Iterator (closure base function) for application args. See \c expr_args
*/
static int expr_next_arg(lua_State * L) {
expr & e = to_expr(L, lua_upvalueindex(1));
unsigned i = lua_tointeger(L, lua_upvalueindex(2));
if (i >= num_args(e)) {
lua_pushnil(L);
} else {
lua_pushinteger(L, i + 1);
lua_replace(L, lua_upvalueindex(2)); // update closure
push_expr(L, arg(e, i));
}
return 1;
}
static int expr_args(lua_State * L) {
expr & e = to_app(L, 1);
push_expr(L, e); // upvalue(1): expr
lua_pushinteger(L, 0); // upvalue(2): index
lua_pushcclosure(L, &expr_next_arg, 2); // create closure with 2 upvalues
return 1;
}
static int expr_num_args(lua_State * L) {
lua_pushinteger(L, num_args(to_app(L, 1)));
return 1;
}
static int expr_arg(lua_State * L) {
return push_expr(L, arg(to_app(L, 1), luaL_checkinteger(L, 2)));
}
static int expr_fields(lua_State * L) {
expr & e = to_nonnull_expr(L, 1);
switch (e.kind()) {
case expr_kind::Var: lua_pushinteger(L, var_idx(e)); return 1;
case expr_kind::Constant: return push_name(L, const_name(e));
case expr_kind::Type: return push_level(L, ty_level(e));
case expr_kind::Value: return 0;
case expr_kind::App: lua_pushinteger(L, num_args(e)); expr_args(L); return 2;
case expr_kind::Eq: push_expr(L, eq_lhs(e)); push_expr(L, eq_rhs(e)); return 2;
case expr_kind::Lambda:
case expr_kind::Pi: push_name(L, abst_name(e)); push_expr(L, abst_domain(e)); push_expr(L, abst_body(e)); return 3;
case expr_kind::Let: push_name(L, let_name(e)); push_expr(L, let_type(e)); push_expr(L, let_value(e)); push_expr(L, let_body(e)); return 4;
case expr_kind::MetaVar: push_name(L, metavar_name(e)); push_local_context(L, metavar_lctx(e)); return 2;
}
lean_unreachable(); // LCOV_EXCL_LINE
return 0; // LCOV_EXCL_LINE
}
static int expr_pred(lua_State * L) {
lua_pushboolean(L, is_expr(L, 1));
return 1;
}
static const struct luaL_Reg expr_m[] = {
{"__gc", expr_gc}, // never throws
{"__tostring", safe_function<expr_tostring>},
{"__eq", safe_function<expr_eq>},
{"__lt", safe_function<expr_lt>},
{"__call", safe_function<expr_mk_app>},
{"is_null", safe_function<expr_is_null>},
{"__gc", expr_gc}, // never throws
{"__tostring", safe_function<expr_tostring>},
{"__eq", safe_function<expr_eq>},
{"__lt", safe_function<expr_lt>},
{"__call", safe_function<expr_mk_app>},
{"kind", safe_function<expr_get_kind>},
{"is_null", safe_function<expr_is_null>},
{"is_var", safe_function<expr_is_var>},
{"is_constant", safe_function<expr_is_constant>},
{"is_app", safe_function<expr_is_app>},
{"is_eq", safe_function<expr_is_eq>},
{"is_lambda", safe_function<expr_is_lambda>},
{"is_pi", safe_function<expr_is_pi>},
{"is_abstraction", safe_function<expr_is_abstraction>},
{"is_let", safe_function<expr_is_let>},
{"is_value", safe_function<expr_is_value>},
{"is_metavar", safe_function<expr_is_metavar>},
{"fields", safe_function<expr_fields>},
{"args", safe_function<expr_args>},
{"num_args", safe_function<expr_num_args>},
{"arg", safe_function<expr_arg>},
{0, 0}
};
@ -213,22 +346,36 @@ void open_expr(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, expr_m, 0);
set_global_function<expr_mk_constant>(L, "mk_constant");
set_global_function<expr_mk_constant>(L, "Const");
set_global_function<expr_mk_var>(L, "mk_var");
set_global_function<expr_mk_var>(L, "Var");
set_global_function<expr_mk_app>(L, "mk_app");
set_global_function<expr_mk_eq>(L, "mk_eq");
set_global_function<expr_mk_eq>(L, "Eq");
set_global_function<expr_mk_lambda>(L, "mk_lambda");
set_global_function<expr_mk_pi>(L, "mk_pi");
set_global_function<expr_mk_let>(L, "mk_let");
set_global_function<expr_fun>(L, "fun");
set_global_function<expr_fun>(L, "Fun");
set_global_function<expr_pi>(L, "Pi");
set_global_function<expr_let>(L, "Let");
set_global_function<expr_type>(L, "mk_type");
set_global_function<expr_type>(L, "Type");
set_global_function<expr_mk_metavar>(L, "mk_metavar");
SET_GLOBAL_FUN(expr_mk_constant, "mk_constant");
SET_GLOBAL_FUN(expr_mk_constant, "Const");
SET_GLOBAL_FUN(expr_mk_var, "mk_var");
SET_GLOBAL_FUN(expr_mk_var, "Var");
SET_GLOBAL_FUN(expr_mk_app, "mk_app");
SET_GLOBAL_FUN(expr_mk_eq, "mk_eq");
SET_GLOBAL_FUN(expr_mk_eq, "Eq");
SET_GLOBAL_FUN(expr_mk_lambda, "mk_lambda");
SET_GLOBAL_FUN(expr_mk_pi, "mk_pi");
SET_GLOBAL_FUN(expr_mk_let, "mk_let");
SET_GLOBAL_FUN(expr_fun, "fun");
SET_GLOBAL_FUN(expr_fun, "Fun");
SET_GLOBAL_FUN(expr_pi, "Pi");
SET_GLOBAL_FUN(expr_let, "Let");
SET_GLOBAL_FUN(expr_type, "mk_type");
SET_GLOBAL_FUN(expr_type, "Type");
SET_GLOBAL_FUN(expr_mk_metavar, "mk_metavar");
SET_GLOBAL_FUN(expr_pred, "is_expr");
lua_newtable(L);
SET_ENUM("Var", expr_kind::Var);
SET_ENUM("Constant", expr_kind::Constant);
SET_ENUM("Type", expr_kind::Type);
SET_ENUM("Value", expr_kind::Value);
SET_ENUM("App", expr_kind::App);
SET_ENUM("Eq", expr_kind::Eq);
SET_ENUM("Lambda", expr_kind::Lambda);
SET_ENUM("Pi", expr_kind::Pi);
SET_ENUM("Let", expr_kind::Let);
SET_ENUM("MetaVar", expr_kind::MetaVar);
lua_setglobal(L, "expr_kind");
}
}

8
src/bindings/lua/format.cpp
View file

@ -135,9 +135,9 @@ void open_format(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, format_m, 0);
set_global_function<mk_format>(L, "format");
set_global_function<format_line>(L, "line");
set_global_function<format_space>(L, "space");
set_global_function<format_pred>(L, "is_format");
SET_GLOBAL_FUN(mk_format, "format");
SET_GLOBAL_FUN(format_line, "line");
SET_GLOBAL_FUN(format_space, "space");
SET_GLOBAL_FUN(format_pred, "is_format");
}
}

2
src/bindings/lua/formatter.cpp
View file

@ -127,6 +127,6 @@ void open_formatter(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, formatter_m, 0);
set_global_function<formatter_pred>(L, "is_formatter");
SET_GLOBAL_FUN(formatter_pred, "is_formatter");
}
}

10
src/bindings/lua/leanlua_state.cpp
View file

@ -239,7 +239,7 @@ static int print(lua_State * L) {
/** \brief Redefine some functions from the Lua library */
static void open_patch(lua_State * L) {
set_global_function<print>(L, "print");
SET_GLOBAL_FUN(print, "print");
}
constexpr char const * state_mt = "luastate.mt";
@ -326,8 +326,8 @@ static void open_state(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, state_m, 0);
set_global_function<mk_state>(L, "State");
set_global_function<state_pred>(L, "is_State");
SET_GLOBAL_FUN(mk_state, "State");
SET_GLOBAL_FUN(state_pred, "is_State");
}
class leanlua_thread {
@ -432,7 +432,7 @@ static void open_thread(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, thread_m, 0);
set_global_function<mk_thread>(L, "thread");
set_global_function<thread_pred>(L, "is_thread");
SET_GLOBAL_FUN(mk_thread, "thread");
SET_GLOBAL_FUN(thread_pred, "is_thread");
}
}

34
src/bindings/lua/level.cpp
View file

@ -133,11 +133,26 @@ static int level_pred(lua_State * L) {
return 1;
}
static int level_get_kind(lua_State * L) {
lua_pushinteger(L, static_cast<int>(kind(to_level(L, 1))));
return 1;
}
static const struct luaL_Reg level_m[] = {
{"__gc", level_gc}, // never throws
{"__tostring", safe_function<level_tostring>},
{"__eq", safe_function<level_eq>},
{"__lt", safe_function<level_lt>},
{"kind", safe_function<level_get_kind>},
{"is_bottom", safe_function<level_is_bottom>},
{"is_lift", safe_function<level_is_lift>},
{"is_max", safe_function<level_is_max>},
{"is_uvar", safe_function<level_is_uvar>},
{"uvar_name", safe_function<level_name>},
{"lift_of", safe_function<level_lift_of>},
{"lift_offset", safe_function<level_lift_offset>},
{"max_size", safe_function<level_max_size>},
{"max_level", safe_function<level_max_level>},
{0, 0}
};
@ -147,16 +162,13 @@ void open_level(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, level_m, 0);
set_global_function<mk_level>(L, "level");
set_global_function<level_pred>(L, "is_level");
set_global_function<level_is_bottom>(L, "is_bottom");
set_global_function<level_is_lift>(L, "is_lift");
set_global_function<level_is_max>(L, "is_max");
set_global_function<level_is_uvar>(L, "is_uvar");
set_global_function<level_name>(L, "uvar_name");
set_global_function<level_lift_of>(L, "lift_of");
set_global_function<level_lift_offset>(L, "lift_offset");
set_global_function<level_max_size>(L, "max_size");
set_global_function<level_max_level>(L, "max_level");
SET_GLOBAL_FUN(mk_level, "level");
SET_GLOBAL_FUN(level_pred, "is_level");
lua_newtable(L);
SET_ENUM("UVar", level_kind::UVar);
SET_ENUM("Lift", level_kind::Lift);
SET_ENUM("Max", level_kind::Max);
lua_setglobal(L, "level_kind");
}
}

10
src/bindings/lua/local_context.cpp
View file

@ -158,15 +158,15 @@ void open_local_context(lua_State * L) {
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, local_entry_m, 0);
set_global_function<local_entry_mk_lift>(L, "mk_lift");
set_global_function<local_entry_mk_inst>(L, "mk_inst");
set_global_function<local_entry_pred>(L, "is_local_entry");
SET_GLOBAL_FUN(local_entry_mk_lift, "mk_lift");
SET_GLOBAL_FUN(local_entry_mk_inst, "mk_inst");
SET_GLOBAL_FUN(local_entry_pred, "is_local_entry");
luaL_newmetatable(L, local_context_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, local_context_m, 0);
set_global_function<mk_local_context>(L, "local_context");
set_global_function<local_context_pred>(L, "is_local_context");
SET_GLOBAL_FUN(mk_local_context, "local_context");
SET_GLOBAL_FUN(local_context_pred, "is_local_context");
}
}

4
src/bindings/lua/name.cpp
View file

@ -97,7 +97,7 @@ void open_name(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, name_m, 0);
set_global_function<mk_name>(L, "name");
set_global_function<name_pred>(L, "is_name");
SET_GLOBAL_FUN(mk_name, "name");
SET_GLOBAL_FUN(name_pred, "is_name");
}
}

8
src/bindings/lua/numerics.cpp
View file

@ -125,8 +125,8 @@ void open_mpz(lua_State * L) {
luaL_newmetatable(L, mpz_mt);
setfuncs(L, mpz_m, 0);
set_global_function<mk_mpz>(L, "mpz");
set_global_function<mpz_pred>(L, "is_mpz");
SET_GLOBAL_FUN(mk_mpz, "mpz");
SET_GLOBAL_FUN(mpz_pred, "is_mpz");
}
constexpr char const * mpq_mt = "mpq.mt";
@ -242,7 +242,7 @@ void open_mpq(lua_State * L) {
luaL_newmetatable(L, mpq_mt);
setfuncs(L, mpq_m, 0);
set_global_function<mk_mpq>(L, "mpq");
set_global_function<mpq_pred>(L, "is_mpq");
SET_GLOBAL_FUN(mk_mpq, "mpq");
SET_GLOBAL_FUN(mpq_pred, "is_mpq");
}
}

2
src/bindings/lua/object.cpp
View file

@ -191,6 +191,6 @@ void open_object(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, object_m, 0);
set_global_function<object_pred>(L, "is_kernel_object");
SET_GLOBAL_FUN(object_pred, "is_kernel_object");
}
}

10
src/bindings/lua/options.cpp
View file

@ -249,10 +249,10 @@ void open_options(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, options_m, 0);
set_global_function<mk_options>(L, "options");
set_global_function<options_pred>(L, "is_options");
set_global_function<_get_global_options>(L, "get_options");
set_global_function<_set_global_options>(L, "set_options");
set_global_function<_set_global_option>(L, "set_option");
SET_GLOBAL_FUN(mk_options, "options");
SET_GLOBAL_FUN(options_pred, "is_options");
SET_GLOBAL_FUN(_get_global_options, "get_options");
SET_GLOBAL_FUN(_set_global_options, "set_options");
SET_GLOBAL_FUN(_set_global_option, "set_option");
}
}

22
src/bindings/lua/sexpr.cpp
View file

@ -174,11 +174,17 @@ static int sexpr_pred(lua_State * L) {
return 1;
}
static int sexpr_get_kind(lua_State * L) {
lua_pushinteger(L, static_cast<int>(to_sexpr(L, 1).kind()));
return 1;
}
static const struct luaL_Reg sexpr_m[] = {
{"__gc", sexpr_gc}, // never throws
{"__tostring", safe_function<sexpr_tostring>},
{"__eq", safe_function<sexpr_eq>},
{"__lt", safe_function<sexpr_lt>},
{"kind", safe_function<sexpr_get_kind>},
{"is_nil", safe_function<sexpr_is_nil>},
{"is_cons", safe_function<sexpr_is_cons>},
{"is_list", safe_function<sexpr_is_list>},
@ -209,7 +215,19 @@ void open_sexpr(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, sexpr_m, 0);
set_global_function<mk_sexpr>(L, "sexpr");
set_global_function<sexpr_pred>(L, "is_sexpr");
SET_GLOBAL_FUN(mk_sexpr, "sexpr");
SET_GLOBAL_FUN(sexpr_pred, "is_sexpr");
lua_newtable(L);
SET_ENUM("Nil", sexpr_kind::NIL);
SET_ENUM("String", sexpr_kind::STRING);
SET_ENUM("Bool", sexpr_kind::BOOL);
SET_ENUM("Int", sexpr_kind::INT);
SET_ENUM("Double", sexpr_kind::DOUBLE);
SET_ENUM("Name", sexpr_kind::NAME);
SET_ENUM("MPZ", sexpr_kind::MPZ);
SET_ENUM("MPQ", sexpr_kind::MPQ);
SET_ENUM("Cons", sexpr_kind::CONS);
lua_setglobal(L, "sexpr_kind");
}
}

5
src/bindings/lua/util.h
View file

@ -25,4 +25,9 @@ template<lua_CFunction F> void set_global_function(lua_State * L, char const * n
lua_pushcfunction(L, safe_function<F>);
lua_setglobal(L, name);
}
#define SET_GLOBAL_FUN(F, N) set_global_function<F>(L, N)
// Auxiliary macro for creating a Lua table that stores enumeration values
#define SET_ENUM(N, V) lua_pushstring(L, N); lua_pushinteger(L, static_cast<int>(V)); lua_settable(L, -3)
}

27
tests/lua/level1.lua
View file

@ -1,19 +1,22 @@
l = level()
assert(is_bottom(l))
assert(is_level(l))
assert(l:is_bottom())
assert(l:kind() == level_kind.UVar)
l = level(l, 1)
assert(is_level(l))
assert(not is_bottom(l))
assert(is_lift(l))
assert(lift_of(l) == level())
assert(lift_offset(l) == 1)
assert(not l:is_bottom())
assert(l:is_lift())
assert(l:kind() == level_kind.Lift)
assert(l:lift_of() == level())
assert(l:lift_offset() == 1)
l = level("U")
assert(is_uvar(l))
assert(uvar_name(l) == name("U"))
assert(not is_lift(l))
assert(l:is_uvar())
assert(l:uvar_name() == name("U"))
assert(not l:is_lift())
l = level(level("U"), level("M"), level("m"))
assert(is_max(l))
assert(max_size(l) == 3)
assert(max_level(l, 0) == level("U"))
assert(max_level(l, 1) == level("M"))
assert(l:is_max())
assert(l:max_size() == 3)
assert(l:max_level(0) == level("U"))
assert(l:max_level(1) == level("M"))
print(l)
assert(l:kind() == level_kind.Max)