From cd6bd79d6367c2b80c6030269c1d213ad8cb0624 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Nov 2013 17:19:51 -0800 Subject: [PATCH] refactor(lua): cleanup Lua API, improve performance Signed-off-by: Leonardo de Moura --- src/bindings/lua/context.cpp | 56 +----------------- src/bindings/lua/context.h | 12 +--- src/bindings/lua/environment.cpp | 28 +-------- src/bindings/lua/environment.h | 5 +- src/bindings/lua/expr.cpp | 28 +-------- src/bindings/lua/expr.h | 7 +-- src/bindings/lua/format.cpp | 28 +-------- src/bindings/lua/format.h | 5 +- src/bindings/lua/formatter.cpp | 28 +-------- src/bindings/lua/formatter.h | 5 +- src/bindings/lua/level.cpp | 28 +-------- src/bindings/lua/level.h | 5 +- src/bindings/lua/local_context.cpp | 56 +----------------- src/bindings/lua/local_context.h | 10 +--- src/bindings/lua/name.cpp | 44 +++----------- src/bindings/lua/name.h | 5 +- src/bindings/lua/numerics.cpp | 58 +----------------- src/bindings/lua/numerics.h | 14 ++--- src/bindings/lua/object.cpp | 28 +-------- src/bindings/lua/object.h | 5 +- src/bindings/lua/options.cpp | 28 +-------- src/bindings/lua/options.h | 5 +- src/bindings/lua/sexpr.cpp | 28 +-------- src/bindings/lua/sexpr.h | 5 +- src/bindings/lua/splay_map.cpp | 94 +++++++++++------------------- src/bindings/lua/util.h | 63 ++++++++++++++++++++ src/tests/kernel/expr.cpp | 6 +- 27 files changed, 142 insertions(+), 542 deletions(-) diff --git a/src/bindings/lua/context.cpp b/src/bindings/lua/context.cpp index 7b5358795..b05462090 100644 --- a/src/bindings/lua/context.cpp +++ b/src/bindings/lua/context.cpp @@ -17,28 +17,7 @@ Author: Leonardo de Moura #include "bindings/lua/formatter.h" namespace lean { -constexpr char const * context_entry_mt = "context_entry.mt"; - -bool is_context_entry(lua_State * L, int idx) { - return testudata(L, idx, context_entry_mt); -} - -context_entry & to_context_entry(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, context_entry_mt)); -} - -int push_context_entry(lua_State * L, context_entry const & e) { - void * mem = lua_newuserdata(L, sizeof(context_entry)); - new (mem) context_entry(e); - luaL_getmetatable(L, context_entry_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int context_entry_gc(lua_State * L) { - to_context_entry(L, 1).~context_entry(); - return 0; -} +DECL_UDATA(context_entry) static int mk_context_entry(lua_State * L) { int nargs = lua_gettop(L); @@ -48,11 +27,6 @@ static int mk_context_entry(lua_State * L) { return push_context_entry(L, context_entry(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_expr(L, 3))); } -static int context_entry_pred(lua_State * L) { - lua_pushboolean(L, is_context_entry(L, 1)); - return 1; -} - static int context_entry_get_name(lua_State * L) { return push_name(L, to_context_entry(L, 1).get_name()); } static int context_entry_get_domain(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_domain()); } static int context_entry_get_body(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_body()); } @@ -65,28 +39,7 @@ static const struct luaL_Reg context_entry_m[] = { {0, 0} }; -constexpr char const * context_mt = "context.mt"; - -bool is_context(lua_State * L, int idx) { - return testudata(L, idx, context_mt); -} - -context & to_context(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, context_mt)); -} - -int push_context(lua_State * L, context const & e) { - void * mem = lua_newuserdata(L, sizeof(context)); - new (mem) context(e); - luaL_getmetatable(L, context_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int context_gc(lua_State * L) { - to_context(L, 1).~context(); - return 0; -} +DECL_UDATA(context) static int context_tostring(lua_State * L) { std::ostringstream out; @@ -111,11 +64,6 @@ static int mk_context(lua_State * L) { } } -static int context_pred(lua_State * L) { - lua_pushboolean(L, is_context(L, 1)); - return 1; -} - static int context_extend(lua_State * L) { int nargs = lua_gettop(L); if (nargs != 3 && nargs != 4) diff --git a/src/bindings/lua/context.h b/src/bindings/lua/context.h index 8e48569a8..6fd44aaa9 100644 --- a/src/bindings/lua/context.h +++ b/src/bindings/lua/context.h @@ -7,15 +7,7 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class context_entry; -bool is_context_entry(lua_State * L, int idx); -context_entry & to_context_entry(lua_State * L, int idx); -int push_context_entry(lua_State * L, context_entry const & o); - -class context; -bool is_context(lua_State * L, int idx); -context & to_context(lua_State * L, int idx); -int push_context(lua_State * L, context const & o); - +UDATA_DEFS(context_entry) +UDATA_DEFS(context) void open_context(lua_State * L); } diff --git a/src/bindings/lua/environment.cpp b/src/bindings/lua/environment.cpp index e36496e07..3183c4af7 100644 --- a/src/bindings/lua/environment.cpp +++ b/src/bindings/lua/environment.cpp @@ -19,15 +19,7 @@ Author: Leonardo de Moura #include "bindings/lua/formatter.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)); -} +DECL_UDATA(environment) ro_environment::ro_environment(lua_State * L, int idx): read_only_environment(to_environment(L, idx)) { @@ -37,19 +29,6 @@ rw_environment::rw_environment(lua_State * L, int idx): read_write_environment(to_environment(L, idx)) { } -static int environment_gc(lua_State * L) { - to_environment(L, 1).~environment(); - return 0; -} - -int push_environment(lua_State * L, environment const & env) { - void * mem = lua_newuserdata(L, sizeof(environment)); - new (mem) environment(env); - luaL_getmetatable(L, environment_mt); - lua_setmetatable(L, -2); - return 1; -} - static int mk_environment(lua_State * L) { return push_environment(L, environment()); } @@ -197,11 +176,6 @@ static int environment_local_objects(lua_State * L) { return environment_objects_core(L, true); } -static int environment_pred(lua_State * L) { - lua_pushboolean(L, is_environment(L, 1)); - return 1; -} - static int environment_tostring(lua_State * L) { ro_environment env(L, 1); std::ostringstream out; diff --git a/src/bindings/lua/environment.h b/src/bindings/lua/environment.h index 25bbe1ebd..4edd237da 100644 --- a/src/bindings/lua/environment.h +++ b/src/bindings/lua/environment.h @@ -9,11 +9,8 @@ Author: Leonardo de Moura #include "kernel/threadsafe_environment.h" namespace lean { -class environment; +UDATA_DEFS(environment) void open_environment(lua_State * L); -bool is_environment(lua_State * L, int idx); -int push_environment(lua_State * L, environment const & env); - /** \brief Auxiliary class for setting the Lua registry of a Lua state with an environment object. diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp index df9c9d3e8..6c3e0daf5 100644 --- a/src/bindings/lua/expr.cpp +++ b/src/bindings/lua/expr.cpp @@ -32,15 +32,7 @@ Author: Leonardo de Moura #include "bindings/lua/numerics.h" namespace lean { -constexpr char const * expr_mt = "expr.mt"; - -bool is_expr(lua_State * L, int idx) { - return testudata(L, idx, expr_mt); -} - -expr & to_expr(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, expr_mt)); -} +DECL_UDATA(expr) expr & to_nonnull_expr(lua_State * L, int idx) { expr & r = to_expr(L, idx); @@ -56,19 +48,6 @@ expr & to_app(lua_State * L, int idx) { return r; } -int push_expr(lua_State * L, expr const & e) { - void * mem = lua_newuserdata(L, sizeof(expr)); - new (mem) expr(e); - luaL_getmetatable(L, expr_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int expr_gc(lua_State * L) { - to_expr(L, 1).~expr(); - return 0; -} - static int expr_tostring(lua_State * L) { std::ostringstream out; expr & e = to_expr(L, 1); @@ -293,11 +272,6 @@ static int expr_fields(lua_State * L) { return 0; // LCOV_EXCL_LINE } -static int expr_pred(lua_State * L) { - lua_pushboolean(L, is_expr(L, 1)); - return 1; -} - static int expr_for_each(lua_State * L) { expr & e = to_nonnull_expr(L, 1); // expr luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun diff --git a/src/bindings/lua/expr.h b/src/bindings/lua/expr.h index 7bd8beb78..36ecb648e 100644 --- a/src/bindings/lua/expr.h +++ b/src/bindings/lua/expr.h @@ -7,10 +7,7 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class expr; -void open_expr(lua_State * L); -bool is_expr(lua_State * L, int idx); -expr & to_expr(lua_State * L, int idx); +UDATA_DEFS(expr); expr & to_nonnull_expr(lua_State * L, int idx); -int push_expr(lua_State * L, expr const & o); +void open_expr(lua_State * L); } diff --git a/src/bindings/lua/format.cpp b/src/bindings/lua/format.cpp index 0ffeb0e50..b1ad24202 100644 --- a/src/bindings/lua/format.cpp +++ b/src/bindings/lua/format.cpp @@ -17,23 +17,7 @@ Author: Leonardo de Moura #include "bindings/lua/options.h" namespace lean { -constexpr char const * format_mt = "format.mt"; - -int push_format(lua_State * L, format const & e) { - void * mem = lua_newuserdata(L, sizeof(format)); - new (mem) format(e); - luaL_getmetatable(L, format_mt); - lua_setmetatable(L, -2); - return 1; -} - -bool is_format(lua_State * L, int idx) { - return testudata(L, idx, format_mt); -} - -format & to_format(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, format_mt)); -} +DECL_UDATA(format) format to_format_elem(lua_State * L, int idx) { if (is_format(L, idx)) @@ -50,11 +34,6 @@ format to_format_elem(lua_State * L, int idx) { return format(lua_tostring(L, idx)); } -static int format_gc(lua_State * L) { - to_format(L, 1).~format(); - return 0; -} - static int format_tostring(lua_State * L) { std::ostringstream out; out << mk_pair(to_format(L, 1), get_global_options(L)); @@ -114,11 +93,6 @@ static int format_highlight(lua_State * L) { static int format_line(lua_State * L) { return push_format(L, line()); } static int format_space(lua_State * L) { return push_format(L, space()); } -static int format_pred(lua_State * L) { - lua_pushboolean(L, is_format(L, 1)); - return 1; -} - static const struct luaL_Reg format_m[] = { {"__gc", format_gc}, // never throws {"__tostring", safe_function}, diff --git a/src/bindings/lua/format.h b/src/bindings/lua/format.h index 457f34af7..6013e75f3 100644 --- a/src/bindings/lua/format.h +++ b/src/bindings/lua/format.h @@ -7,9 +7,6 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class format; +UDATA_DEFS(format) void open_format(lua_State * L); -bool is_format(lua_State * L, int idx); -format & to_format(lua_State * L, int idx); -int push_format(lua_State * L, format const & o); } diff --git a/src/bindings/lua/formatter.cpp b/src/bindings/lua/formatter.cpp index 1238a5add..50647ea1e 100644 --- a/src/bindings/lua/formatter.cpp +++ b/src/bindings/lua/formatter.cpp @@ -17,28 +17,7 @@ Author: Leonardo de Moura #include "bindings/lua/state.h" namespace lean { -constexpr char const * formatter_mt = "formatter.mt"; - -bool is_formatter(lua_State * L, int idx) { - return testudata(L, idx, formatter_mt); -} - -formatter & to_formatter(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, formatter_mt)); -} - -int push_formatter(lua_State * L, formatter const & o) { - void * mem = lua_newuserdata(L, sizeof(formatter)); - new (mem) formatter(o); - luaL_getmetatable(L, formatter_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int formatter_gc(lua_State * L) { - to_formatter(L, 1).~formatter(); - return 0; -} +DECL_UDATA(formatter) [[ noreturn ]] void throw_invalid_formatter_call() { throw exception("invalid formatter invocation, the acceptable arguments are: (expr, options?), (context, options?), (context, expr, bool? options?), (kernel object, options?), (environment, options?)"); @@ -78,11 +57,6 @@ static int formatter_call(lua_State * L) { } } -static int formatter_pred(lua_State * L) { - lua_pushboolean(L, is_formatter(L, 1)); - return 1; -} - static const struct luaL_Reg formatter_m[] = { {"__gc", formatter_gc}, // never throws {"__call", safe_function}, diff --git a/src/bindings/lua/formatter.h b/src/bindings/lua/formatter.h index 86568babd..e36e6433a 100644 --- a/src/bindings/lua/formatter.h +++ b/src/bindings/lua/formatter.h @@ -7,11 +7,8 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class formatter; +UDATA_DEFS(formatter) void open_formatter(lua_State * L); -bool is_formatter(lua_State * L, int idx); -formatter & to_formatter(lua_State * L, int idx); -int push_formatter(lua_State * L, formatter const & o); /** \brief Return the formatter object associated with the given Lua State. This procedure checks for options at: diff --git a/src/bindings/lua/level.cpp b/src/bindings/lua/level.cpp index a2e164c97..27b267948 100644 --- a/src/bindings/lua/level.cpp +++ b/src/bindings/lua/level.cpp @@ -14,28 +14,7 @@ Author: Leonardo de Moura #include "bindings/lua/options.h" namespace lean { -constexpr char const * level_mt = "level.mt"; - -bool is_level(lua_State * L, int idx) { - return testudata(L, idx, level_mt); -} - -level & to_level(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, level_mt)); -} - -int push_level(lua_State * L, level const & e) { - void * mem = lua_newuserdata(L, sizeof(level)); - new (mem) level(e); - luaL_getmetatable(L, level_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int level_gc(lua_State * L) { - to_level(L, 1).~level(); - return 0; -} +DECL_UDATA(level) static int level_tostring(lua_State * L) { std::ostringstream out; @@ -119,11 +98,6 @@ static int level_max_level(lua_State * L) { return push_level(L, max_level(to_level(L, 1), luaL_checkinteger(L, 2))); } -static int level_pred(lua_State * L) { - lua_pushboolean(L, is_level(L, 1)); - return 1; -} - static int level_get_kind(lua_State * L) { lua_pushinteger(L, static_cast(kind(to_level(L, 1)))); return 1; diff --git a/src/bindings/lua/level.h b/src/bindings/lua/level.h index dd869e13a..917146ae7 100644 --- a/src/bindings/lua/level.h +++ b/src/bindings/lua/level.h @@ -7,9 +7,6 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class level; +UDATA_DEFS(level) void open_level(lua_State * L); -bool is_level(lua_State * L, int idx); -level & to_level(lua_State * L, int idx); -int push_level(lua_State * L, level const & o); } diff --git a/src/bindings/lua/local_context.cpp b/src/bindings/lua/local_context.cpp index 977c63043..41b74f5d9 100644 --- a/src/bindings/lua/local_context.cpp +++ b/src/bindings/lua/local_context.cpp @@ -12,28 +12,7 @@ Author: Leonardo de Moura #include "bindings/lua/local_context.h" namespace lean { -constexpr char const * local_entry_mt = "local_entry.mt"; - -bool is_local_entry(lua_State * L, int idx) { - return testudata(L, idx, local_entry_mt); -} - -local_entry & to_local_entry(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, local_entry_mt)); -} - -int push_local_entry(lua_State * L, local_entry const & e) { - void * mem = lua_newuserdata(L, sizeof(local_entry)); - new (mem) local_entry(e); - luaL_getmetatable(L, local_entry_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int local_entry_gc(lua_State * L) { - to_local_entry(L, 1).~local_entry(); - return 0; -} +DECL_UDATA(local_entry) static int local_entry_eq(lua_State * L) { lua_pushboolean(L, to_local_entry(L, 1) == to_local_entry(L, 2)); @@ -48,11 +27,6 @@ static int local_entry_mk_inst(lua_State * L) { return push_local_entry(L, mk_inst(luaL_checkinteger(L, 1), to_nonnull_expr(L, 2))); } -static int local_entry_pred(lua_State * L) { - lua_pushboolean(L, is_local_entry(L, 1)); - return 1; -} - static int local_entry_is_lift(lua_State * L) { lua_pushboolean(L, is_local_entry(L, 1) && to_local_entry(L, 1).is_lift()); return 1; @@ -95,28 +69,7 @@ static const struct luaL_Reg local_entry_m[] = { {0, 0} }; -constexpr char const * local_context_mt = "local_context.mt"; - -bool is_local_context(lua_State * L, int idx) { - return testudata(L, idx, local_context_mt); -} - -local_context & to_local_context(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, local_context_mt)); -} - -int push_local_context(lua_State * L, local_context const & e) { - void * mem = lua_newuserdata(L, sizeof(local_context)); - new (mem) local_context(e); - luaL_getmetatable(L, local_context_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int local_context_gc(lua_State * L) { - to_local_context(L, 1).~local_context(); - return 0; -} +DECL_UDATA(local_context) static int mk_local_context(lua_State * L) { int nargs = lua_gettop(L); @@ -140,11 +93,6 @@ static int local_context_is_nil(lua_State * L) { return 1; } -static int local_context_pred(lua_State * L) { - lua_pushboolean(L, is_local_context(L, 1)); - return 1; -} - static const struct luaL_Reg local_context_m[] = { {"__gc", local_context_gc}, {"head", local_context_head}, diff --git a/src/bindings/lua/local_context.h b/src/bindings/lua/local_context.h index a51f20903..e59bb810a 100644 --- a/src/bindings/lua/local_context.h +++ b/src/bindings/lua/local_context.h @@ -8,13 +8,7 @@ Author: Leonardo de Moura #include #include "kernel/expr.h" namespace lean { -bool is_local_entry(lua_State * L, int idx); -local_entry & to_local_entry(lua_State * L, int idx); -int push_local_entry(lua_State * L, local_entry const & o); - -bool is_local_context(lua_State * L, int idx); -local_context & to_local_context(lua_State * L, int idx); -int push_local_context(lua_State * L, local_context const & o); - +UDATA_DEFS(local_entry) +UDATA_DEFS_CORE(local_context) void open_local_context(lua_State * L); } diff --git a/src/bindings/lua/name.cpp b/src/bindings/lua/name.cpp index 82e42774a..7bc980ede 100644 --- a/src/bindings/lua/name.cpp +++ b/src/bindings/lua/name.cpp @@ -7,18 +7,11 @@ Author: Leonardo de Moura #include #include "util/debug.h" #include "util/name.h" +#include "util/sstream.h" #include "bindings/lua/util.h" namespace lean { -constexpr char const * name_mt = "name.mt"; - -bool is_name(lua_State * L, int idx) { - return testudata(L, idx, name_mt); -} - -name & to_name(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, name_mt)); -} +DECL_UDATA(name) name to_name_ext(lua_State * L, int idx) { if (lua_isstring(L, idx)) { @@ -45,36 +38,22 @@ name to_name_ext(lua_State * L, int idx) { } } -int push_name(lua_State * L, name const & n) { - void * mem = lua_newuserdata(L, sizeof(name)); - new (mem) name(n); - luaL_getmetatable(L, name_mt); - lua_setmetatable(L, -2); - return 1; -} - static int mk_name(lua_State * L) { int nargs = lua_gettop(L); name r; for (int i = 1; i <= nargs; i++) { - if (lua_isnil(L, i)) { - // skip - } else if (lua_isuserdata(L, i)) { - r = r + to_name(L, i); - } else if (lua_isstring(L, i)) { - r = name(r, luaL_checkstring(L, i)); - } else { - r = name(r, luaL_checkinteger(L, i)); + switch (lua_type(L, i)) { + case LUA_TNIL: break; // skip + case LUA_TNUMBER: r = name(r, lua_tointeger(L, i)); break; + case LUA_TSTRING: r = name(r, lua_tostring(L, i)); break; + case LUA_TUSERDATA: r = r + to_name(L, i); break; + default: + throw exception(sstream() << "arg #" << i << " must be a hierarchical name, string, or integer"); } } return push_name(L, r); } -static int name_gc(lua_State * L) { - to_name(L, 1).~name(); - return 0; -} - static int name_tostring(lua_State * L) { lua_pushstring(L, to_name(L, 1).to_string().c_str()); return 1; @@ -90,11 +69,6 @@ static int name_lt(lua_State * L) { return 1; } -static int name_pred(lua_State * L) { - lua_pushboolean(L, is_name(L, 1)); - return 1; -} - static int name_hash(lua_State * L) { lua_pushinteger(L, to_name(L, 1).hash()); return 1; diff --git a/src/bindings/lua/name.h b/src/bindings/lua/name.h index c0c845105..9435cc4d4 100644 --- a/src/bindings/lua/name.h +++ b/src/bindings/lua/name.h @@ -7,10 +7,7 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class name; +UDATA_DEFS(name) void open_name(lua_State * L); -bool is_name(lua_State * L, int idx); -name & to_name(lua_State * L, int idx); name to_name_ext(lua_State * L, int idx); -int push_name(lua_State * L, name const & n); } diff --git a/src/bindings/lua/numerics.cpp b/src/bindings/lua/numerics.cpp index 857ce8ec6..866717a23 100644 --- a/src/bindings/lua/numerics.cpp +++ b/src/bindings/lua/numerics.cpp @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "bindings/lua/util.h" namespace lean { -constexpr char const * mpz_mt = "mpz.mt"; +DECL_UDATA(mpz) template static mpz const & to_mpz(lua_State * L) { @@ -28,14 +28,6 @@ static mpz const & to_mpz(lua_State * L) { } } -bool is_mpz(lua_State * L, int idx) { - return testudata(L, idx, mpz_mt); -} - -mpz & to_mpz(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, mpz_mt)); -} - mpz to_mpz_ext(lua_State * L, int idx) { if (lua_isuserdata(L, idx)) { return *static_cast(luaL_checkudata(L, idx, mpz_mt)); @@ -46,20 +38,6 @@ mpz to_mpz_ext(lua_State * L, int idx) { } } -int push_mpz(lua_State * L, mpz const & val) { - void * mem = lua_newuserdata(L, sizeof(mpz)); - new (mem) mpz(val); - luaL_getmetatable(L, mpz_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int mpz_gc(lua_State * L) { - mpz * n = static_cast(luaL_checkudata(L, 1, mpz_mt)); - n->~mpz(); - return 0; -} - static int mpz_tostring(lua_State * L) { mpz * n = static_cast(luaL_checkudata(L, 1, mpz_mt)); std::ostringstream out; @@ -111,11 +89,6 @@ static int mk_mpz(lua_State * L) { return push_mpz(L, arg); } -static int mpz_pred(lua_State * L) { - lua_pushboolean(L, is_mpz(L, 1)); - return 1; -} - static const struct luaL_Reg mpz_m[] = { {"__gc", mpz_gc}, // never throws {"__tostring", safe_function}, @@ -138,7 +111,7 @@ void open_mpz(lua_State * L) { SET_GLOBAL_FUN(mpz_pred, "is_mpz"); } -constexpr char const * mpq_mt = "mpq.mt"; +DECL_UDATA(mpq) template static mpq const & to_mpq(lua_State * L) { @@ -157,14 +130,6 @@ static mpq const & to_mpq(lua_State * L) { return arg; } -bool is_mpq(lua_State * L, int idx) { - return testudata(L, idx, mpq_mt); -} - -mpq & to_mpq(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, mpq_mt)); -} - mpq to_mpq_ext(lua_State * L, int idx) { if (lua_isuserdata(L, idx)) { if (is_mpz(L, idx)) { @@ -179,20 +144,6 @@ mpq to_mpq_ext(lua_State * L, int idx) { } } -int push_mpq(lua_State * L, mpq const & val) { - void * mem = lua_newuserdata(L, sizeof(mpq)); - new (mem) mpq(val); - luaL_getmetatable(L, mpq_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int mpq_gc(lua_State * L) { - mpq * n = static_cast(luaL_checkudata(L, 1, mpq_mt)); - n->~mpq(); - return 0; -} - static int mpq_tostring(lua_State * L) { mpq * n = static_cast(luaL_checkudata(L, 1, mpq_mt)); std::ostringstream out; @@ -244,11 +195,6 @@ static int mk_mpq(lua_State * L) { return push_mpq(L, arg); } -static int mpq_pred(lua_State * L) { - lua_pushboolean(L, is_mpq(L, 1)); - return 1; -} - static const struct luaL_Reg mpq_m[] = { {"__gc", mpq_gc}, // never throws {"__tostring", safe_function}, diff --git a/src/bindings/lua/numerics.h b/src/bindings/lua/numerics.h index e2596f641..36d3fe8ea 100644 --- a/src/bindings/lua/numerics.h +++ b/src/bindings/lua/numerics.h @@ -7,17 +7,11 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class mpz; -void open_mpz(lua_State * L); -bool is_mpz(lua_State * L, int idx); -mpz & to_mpz(lua_State * L, int idx); +UDATA_DEFS(mpz) mpz to_mpz_ext(lua_State * L, int idx); -int push_mpz(lua_State * L, mpz const & val); +void open_mpz(lua_State * L); -class mpq; -void open_mpq(lua_State * L); -bool is_mpq(lua_State * L, int idx); -mpq & to_mpq(lua_State * L, int idx); +UDATA_DEFS(mpq) mpq to_mpq_ext(lua_State * L, int idx); -int push_mpq(lua_State * L, mpq const & val); +void open_mpq(lua_State * L); } diff --git a/src/bindings/lua/object.cpp b/src/bindings/lua/object.cpp index 986397e53..4c6d4bb33 100644 --- a/src/bindings/lua/object.cpp +++ b/src/bindings/lua/object.cpp @@ -17,15 +17,7 @@ Author: Leonardo de Moura #include "bindings/lua/formatter.h" namespace lean { -constexpr char const * object_mt = "object.mt"; - -bool is_object(lua_State * L, int idx) { - return testudata(L, idx, object_mt); -} - -object & to_object(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, object_mt)); -} +DECL_UDATA(object) object & to_nonnull_object(lua_State * L, int idx) { object & r = to_object(L, idx); @@ -34,19 +26,6 @@ object & to_nonnull_object(lua_State * L, int idx) { return r; } -int push_object(lua_State * L, object const & o) { - void * mem = lua_newuserdata(L, sizeof(object)); - new (mem) object(o); - luaL_getmetatable(L, object_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int object_gc(lua_State * L) { - to_object(L, 1).~object(); - return 0; -} - static int object_is_null(lua_State * L) { lua_pushboolean(L, !to_object(L, 1)); return 1; @@ -127,11 +106,6 @@ static int object_in_builtin_set(lua_State * L) { return 1; } -static int object_pred(lua_State * L) { - lua_pushboolean(L, is_object(L, 1)); - return 1; -} - static int object_tostring(lua_State * L) { std::ostringstream out; formatter fmt = get_global_formatter(L); diff --git a/src/bindings/lua/object.h b/src/bindings/lua/object.h index a3d987cd9..ac7c7c62e 100644 --- a/src/bindings/lua/object.h +++ b/src/bindings/lua/object.h @@ -7,9 +7,6 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class object; +UDATA_DEFS(object) void open_object(lua_State * L); -bool is_object(lua_State * L, int idx); -object & to_object(lua_State * L, int idx); -int push_object(lua_State * L, object const & o); } diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp index 82e3044f4..835e66b9d 100644 --- a/src/bindings/lua/options.cpp +++ b/src/bindings/lua/options.cpp @@ -16,23 +16,7 @@ Author: Leonardo de Moura #include "bindings/lua/state.h" namespace lean { -constexpr char const * options_mt = "options.mt"; - -bool is_options(lua_State * L, int idx) { - return testudata(L, idx, options_mt); -} - -options & to_options(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, options_mt)); -} - -int push_options(lua_State * L, options const & o) { - void * mem = lua_newuserdata(L, sizeof(options)); - new (mem) options(o); - luaL_getmetatable(L, options_mt); - lua_setmetatable(L, -2); - return 1; -} +DECL_UDATA(options) static int mk_options(lua_State * L) { options r; @@ -48,11 +32,6 @@ static name to_key(lua_State * L, int idx) { } } -static int options_gc(lua_State * L) { - to_options(L, 1).~options(); - return 0; -} - static int options_tostring(lua_State * L) { std::ostringstream out; out << to_options(L, 1); @@ -166,11 +145,6 @@ static int options_update(lua_State * L) { } } -static int options_pred(lua_State * L) { - lua_pushboolean(L, is_options(L, 1)); - return 1; -} - static char g_options_key; options get_global_options(lua_State * L) { diff --git a/src/bindings/lua/options.h b/src/bindings/lua/options.h index f30c74e3a..90db30373 100644 --- a/src/bindings/lua/options.h +++ b/src/bindings/lua/options.h @@ -7,11 +7,8 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class options; +UDATA_DEFS(options) void open_options(lua_State * L); -bool is_options(lua_State * L, int idx); -options & to_options(lua_State * L, int idx); -int push_options(lua_State * L, options const & o); /** \brief Return the set of options associated with the given Lua State. This procedure checks for options at: diff --git a/src/bindings/lua/sexpr.cpp b/src/bindings/lua/sexpr.cpp index f3b6b9982..6d73cf14b 100644 --- a/src/bindings/lua/sexpr.cpp +++ b/src/bindings/lua/sexpr.cpp @@ -13,28 +13,7 @@ Author: Leonardo de Moura #include "bindings/lua/numerics.h" namespace lean { -constexpr char const * sexpr_mt = "sexpr.mt"; - -int push_sexpr(lua_State * L, sexpr const & e) { - void * mem = lua_newuserdata(L, sizeof(sexpr)); - new (mem) sexpr(e); - luaL_getmetatable(L, sexpr_mt); - lua_setmetatable(L, -2); - return 1; -} - -bool is_sexpr(lua_State * L, int idx) { - return testudata(L, idx, sexpr_mt); -} - -sexpr & to_sexpr(lua_State * L, int idx) { - return *static_cast(lua_touserdata(L, idx)); -} - -static int sexpr_gc(lua_State * L) { - to_sexpr(L, 1).~sexpr(); - return 0; -} +DECL_UDATA(sexpr) static int sexpr_tostring(lua_State * L) { std::ostringstream out; @@ -176,11 +155,6 @@ static int sexpr_to_mpq(lua_State * L) { return push_mpq(L, to_mpq(e)); } -static int sexpr_pred(lua_State * L) { - lua_pushboolean(L, is_sexpr(L, 1)); - return 1; -} - static int sexpr_get_kind(lua_State * L) { lua_pushinteger(L, static_cast(to_sexpr(L, 1).kind())); return 1; diff --git a/src/bindings/lua/sexpr.h b/src/bindings/lua/sexpr.h index 778b1072a..e7aedc349 100644 --- a/src/bindings/lua/sexpr.h +++ b/src/bindings/lua/sexpr.h @@ -7,9 +7,6 @@ Author: Leonardo de Moura #pragma once #include namespace lean { -class sexpr; +UDATA_DEFS(sexpr) void open_sexpr(lua_State * L); -bool is_sexpr(lua_State * L, int idx); -sexpr & to_sexpr(lua_State * L, int idx); -int push_sexpr(lua_State * L, sexpr const & e); } diff --git a/src/bindings/lua/splay_map.cpp b/src/bindings/lua/splay_map.cpp index 2260e1a1b..903a27706 100644 --- a/src/bindings/lua/splay_map.cpp +++ b/src/bindings/lua/splay_map.cpp @@ -12,61 +12,40 @@ Author: Leonardo de Moura namespace lean { typedef splay_map lua_splay_map; -constexpr char const * splay_map_mt = "splay_map.mt"; +DECL_UDATA(lua_splay_map) -bool is_splay_map(lua_State * L, int idx) { - return testudata(L, idx, splay_map_mt); -} - -lua_splay_map & to_splay_map(lua_State * L, int idx) { - return *static_cast(luaL_checkudata(L, idx, splay_map_mt)); -} - -int push_splay_map(lua_State * L, lua_splay_map const & o) { - void * mem = lua_newuserdata(L, sizeof(lua_splay_map)); - new (mem) lua_splay_map(o); - luaL_getmetatable(L, splay_map_mt); - lua_setmetatable(L, -2); - return 1; -} - -static int mk_splay_map(lua_State * L) { +static int mk_lua_splay_map(lua_State * L) { lua_splay_map r; - return push_splay_map(L, r); + return push_lua_splay_map(L, r); } -static int splay_map_gc(lua_State * L) { - to_splay_map(L, 1).~lua_splay_map(); - return 0; -} - -static int splay_map_size(lua_State * L) { - lua_pushinteger(L, to_splay_map(L, 1).size()); +static int lua_splay_map_size(lua_State * L) { + lua_pushinteger(L, to_lua_splay_map(L, 1).size()); return 1; } -static int splay_map_contains(lua_State * L) { - lua_pushboolean(L, to_splay_map(L, 1).contains(lref(L, 2))); +static int lua_splay_map_contains(lua_State * L) { + lua_pushboolean(L, to_lua_splay_map(L, 1).contains(lref(L, 2))); return 1; } -static int splay_map_empty(lua_State * L) { - lua_pushboolean(L, to_splay_map(L, 1).empty()); +static int lua_splay_map_empty(lua_State * L) { + lua_pushboolean(L, to_lua_splay_map(L, 1).empty()); return 1; } -static int splay_map_insert(lua_State * L) { - to_splay_map(L, 1).insert(lref(L, 2), lref(L, 3)); +static int lua_splay_map_insert(lua_State * L) { + to_lua_splay_map(L, 1).insert(lref(L, 2), lref(L, 3)); return 0; } -static int splay_map_erase(lua_State * L) { - to_splay_map(L, 1).erase(lref(L, 2)); +static int lua_splay_map_erase(lua_State * L) { + to_lua_splay_map(L, 1).erase(lref(L, 2)); return 0; } -static int splay_map_find(lua_State * L) { - lua_splay_map & m = to_splay_map(L, 1); +static int lua_splay_map_find(lua_State * L) { + lua_splay_map & m = to_lua_splay_map(L, 1); lref * val = m.splay_find(lref(L, 2)); if (val) { lean_assert(val->get_state() == L); @@ -77,21 +56,16 @@ static int splay_map_find(lua_State * L) { return 1; } -static int splay_map_copy(lua_State * L) { - return push_splay_map(L, to_splay_map(L, 1)); +static int lua_splay_map_copy(lua_State * L) { + return push_lua_splay_map(L, to_lua_splay_map(L, 1)); } -static int splay_map_pred(lua_State * L) { - lua_pushboolean(L, is_splay_map(L, 1)); - return 1; -} - -static int splay_map_for_each(lua_State * L) { +static int lua_splay_map_for_each(lua_State * L) { // Remark: we take a copy of the map to make sure // for_each will not crash if the map is updated while being // traversed. // The copy operation is very cheap O(1). - lua_splay_map m(to_splay_map(L, 1)); // map + lua_splay_map m(to_lua_splay_map(L, 1)); // map luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun m.for_each([&](lref const & k, lref const & v) { lua_pushvalue(L, 2); // push user-fun @@ -102,27 +76,27 @@ static int splay_map_for_each(lua_State * L) { return 0; } -static const struct luaL_Reg splay_map_m[] = { - {"__gc", splay_map_gc}, // never throws - {"__len", safe_function }, - {"contains", safe_function}, - {"size", safe_function}, - {"empty", safe_function}, - {"insert", safe_function}, - {"erase", safe_function}, - {"find", safe_function}, - {"copy", safe_function}, - {"for_each", safe_function}, +static const struct luaL_Reg lua_splay_map_m[] = { + {"__gc", lua_splay_map_gc}, // never throws + {"__len", safe_function }, + {"contains", safe_function}, + {"size", safe_function}, + {"empty", safe_function}, + {"insert", safe_function}, + {"erase", safe_function}, + {"find", safe_function}, + {"copy", safe_function}, + {"for_each", safe_function}, {0, 0} }; void open_splay_map(lua_State * L) { - luaL_newmetatable(L, splay_map_mt); + luaL_newmetatable(L, lua_splay_map_mt); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); - setfuncs(L, splay_map_m, 0); + setfuncs(L, lua_splay_map_m, 0); - SET_GLOBAL_FUN(mk_splay_map, "splay_map"); - SET_GLOBAL_FUN(splay_map_pred, "is_splay_map"); + SET_GLOBAL_FUN(mk_lua_splay_map, "splay_map"); + SET_GLOBAL_FUN(lua_splay_map_pred, "is_splay_map"); } } diff --git a/src/bindings/lua/util.h b/src/bindings/lua/util.h index b25dd2495..39b2537c8 100644 --- a/src/bindings/lua/util.h +++ b/src/bindings/lua/util.h @@ -33,4 +33,67 @@ template void set_global_function(lua_State * L, char const * 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(V)); lua_settable(L, -3) + +#define DECL_PUSH_CORE(NAME, T, TREF) \ +int push_ ## NAME(lua_State * L, TREF val) { \ + void * mem = lua_newuserdata(L, sizeof(T)); \ + new (mem) T(val); \ + luaL_getmetatable(L, NAME ## _mt); \ + lua_setmetatable(L, -2); \ + return 1; \ +} + +#define DECL_PUSH(T) \ +DECL_PUSH_CORE(T, T, T const &) \ +DECL_PUSH_CORE(T, T, T &&) + +#define DECL_GC(T) static int T ## _gc(lua_State * L) { static_cast(lua_touserdata(L, 1))->~T(); return 0; } + +#define DECL_PRED(T) \ +bool is_ ## T(lua_State * L, int idx) { return testudata(L, idx, T ## _mt); } \ +static int T ## _pred(lua_State * L) { \ + lua_pushboolean(L, is_ ## T(L, 1)); \ + return 1; \ +} + +/** + \brief Create basic declarations for adding a new kind of userdata in Lua + T is a Lean object type. + For example, if T == expr, it produces an implementation for the + following declarations + + constexpr char const * expr_mt = "expr"; + expr & to_expr(lua_State * L, int i); + bool is_expr(lua_State * L, int i); + static int expr_pred(lua_State * L); + static int expr_gc(lua_State * L); + int push_expr(lua_State * L, expr const & e); + int push_expr(lua_State * L, expr && e); +*/ +#define DECL_UDATA(T) \ +constexpr char const * T ## _mt = #T; \ +T & to_ ## T(lua_State * L, int i) { return *static_cast(luaL_checkudata(L, i, T ## _mt)); } \ +DECL_PRED(T) \ +DECL_GC(T) \ +DECL_PUSH(T) + +/** + \brief Similar to DECL_UDATA, but it only declares the functions. + + For example, if T == expr, it produces the following declarations: + + class expr; + expr & to_expr(lua_State * L, int i); + bool is_expr(lua_State * L, int i); + int push_expr(lua_State * L, expr const & e); + int push_expr(lua_State * L, expr && e); +*/ +#define UDATA_DEFS_CORE(T) \ +T & to_ ## T(lua_State * L, int i); \ +bool is_ ## T(lua_State * L, int i); \ +int push_ ## T(lua_State * L, T const & e); \ +int push_ ## T(lua_State * L, T && e); +#define UDATA_DEFS(T) \ +class T; \ +UDATA_DEFS_CORE(T) } diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 77a7c246f..07b736296 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -147,8 +147,8 @@ expr mk_big(expr f, unsigned depth, unsigned val) { void tst3() { expr f = Const("f"); - expr r1 = mk_big(f, 18, 0); - expr r2 = mk_big(f, 18, 0); + expr r1 = mk_big(f, 20, 0); + expr r2 = mk_big(f, 20, 0); lean_assert(r1 == r2); } @@ -376,6 +376,8 @@ int main() { std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n"; std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n"; + tst3(); + return 0; tst1(); tst2(); tst3();