From 1e12ddc7a973255a7f43204b7939b1684b8f4f5c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2013 19:45:15 -0800 Subject: [PATCH] refactor(lua): add goodies for accessing Lean values on the Lua stack Signed-off-by: Leonardo de Moura --- src/bindings/lua/name.cpp | 14 ++++++++---- src/bindings/lua/name.h | 3 +++ src/bindings/lua/numerics.cpp | 40 ++++++++++++++++++++++++++--------- src/bindings/lua/numerics.h | 7 ++++++ src/bindings/lua/options.cpp | 24 +++++++++++++-------- src/bindings/lua/options.h | 3 +++ src/bindings/lua/util.cpp | 12 +++++++++++ src/bindings/lua/util.h | 1 + 8 files changed, 81 insertions(+), 23 deletions(-) diff --git a/src/bindings/lua/name.cpp b/src/bindings/lua/name.cpp index 04ee58c7b..5230968e7 100644 --- a/src/bindings/lua/name.cpp +++ b/src/bindings/lua/name.cpp @@ -11,8 +11,14 @@ Author: Leonardo de Moura #include "bindings/lua/util.h" namespace lean { -static name const & to_name(lua_State * L, unsigned idx) { - return *static_cast(luaL_checkudata(L, idx, "name.mt")); +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)); } static int mk_name(lua_State * L) { @@ -31,7 +37,7 @@ static int mk_name(lua_State * L) { } void * mem = lua_newuserdata(L, sizeof(name)); new (mem) name(r); - luaL_getmetatable(L, "name.mt"); + luaL_getmetatable(L, name_mt); lua_setmetatable(L, -2); return 1; } @@ -65,7 +71,7 @@ static const struct luaL_Reg name_m[] = { }; void open_name(lua_State * L) { - luaL_newmetatable(L, "name.mt"); + luaL_newmetatable(L, name_mt); setfuncs(L, name_m, 0); lua_pushcfunction(L, safe_function); diff --git a/src/bindings/lua/name.h b/src/bindings/lua/name.h index 9f6f5ec21..bad62718f 100644 --- a/src/bindings/lua/name.h +++ b/src/bindings/lua/name.h @@ -7,6 +7,9 @@ Author: Leonardo de Moura #ifdef LEAN_USE_LUA #include namespace lean { +class name; void open_name(lua_State * L); +bool is_name(lua_State * L, int idx); +name & to_name(lua_State * L, int idx); } #endif diff --git a/src/bindings/lua/numerics.cpp b/src/bindings/lua/numerics.cpp index 883cc936c..a8cdaf3e4 100644 --- a/src/bindings/lua/numerics.cpp +++ b/src/bindings/lua/numerics.cpp @@ -13,11 +13,13 @@ Author: Leonardo de Moura #include "bindings/lua/util.h" namespace lean { +constexpr char const * mpz_mt = "mpz.mt"; + template static mpz const & to_mpz(lua_State * L) { static thread_local mpz arg; if (lua_isuserdata(L, idx)) { - return *static_cast(luaL_checkudata(L, idx, "mpz.mt")); + return *static_cast(luaL_checkudata(L, idx, mpz_mt)); } else if (lua_isstring(L, idx)) { char const * str = luaL_checkstring(L, idx); arg = mpz(str); @@ -28,22 +30,30 @@ 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)); +} + static 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"); + 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")); + 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")); + mpz * n = static_cast(luaL_checkudata(L, 1, mpz_mt)); std::ostringstream out; out << *n; lua_pushfstring(L, out.str().c_str()); @@ -108,18 +118,20 @@ static const struct luaL_Reg mpz_m[] = { }; void open_mpz(lua_State * L) { - luaL_newmetatable(L, "mpz.mt"); + luaL_newmetatable(L, mpz_mt); setfuncs(L, mpz_m, 0); lua_pushcfunction(L, safe_function); lua_setglobal(L, "mpz"); } +constexpr char const * mpq_mt = "mpq.mt"; + template static mpq const & to_mpq(lua_State * L) { static thread_local mpq arg; if (lua_isuserdata(L, idx)) { - return *static_cast(luaL_checkudata(L, idx, "mpq.mt")); + return *static_cast(luaL_checkudata(L, idx, mpq_mt)); } else if (lua_isstring(L, idx)) { char const * str = luaL_checkstring(L, idx); arg = mpq(str); @@ -130,22 +142,30 @@ static mpq const & to_mpq(lua_State * L) { } } +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)); +} + static 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"); + 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")); + 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")); + mpq * n = static_cast(luaL_checkudata(L, 1, mpq_mt)); std::ostringstream out; out << *n; lua_pushfstring(L, out.str().c_str()); @@ -210,7 +230,7 @@ static const struct luaL_Reg mpq_m[] = { }; void open_mpq(lua_State * L) { - luaL_newmetatable(L, "mpq.mt"); + luaL_newmetatable(L, mpq_mt); setfuncs(L, mpq_m, 0); lua_pushcfunction(L, safe_function); diff --git a/src/bindings/lua/numerics.h b/src/bindings/lua/numerics.h index 2f100bc74..539ba501b 100644 --- a/src/bindings/lua/numerics.h +++ b/src/bindings/lua/numerics.h @@ -7,7 +7,14 @@ Author: Leonardo de Moura #ifdef LEAN_USE_LUA #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); + +class mpq; void open_mpq(lua_State * L); +bool is_mpq(lua_State * L, int idx); +mpq & to_mpq(lua_State * L, int idx); } #endif diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp index 7c565ded8..e4d717f7f 100644 --- a/src/bindings/lua/options.cpp +++ b/src/bindings/lua/options.cpp @@ -12,12 +12,23 @@ Author: Leonardo de Moura #include "util/sexpr/options.h" #include "util/sexpr/option_declarations.h" #include "bindings/lua/util.h" +#include "bindings/lua/name.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)); +} + static 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"); + luaL_getmetatable(L, options_mt); lua_setmetatable(L, -2); return 1; } @@ -28,20 +39,15 @@ static int mk_option(lua_State * L) { return push_options(L, r); } -static name to_key(lua_State * L, unsigned idx) { +static name to_key(lua_State * L, int idx) { if (lua_isstring(L, idx)) { char const * k = luaL_checkstring(L, idx); return name(k); } else { - name * k = static_cast(luaL_checkudata(L, idx, "name.mt")); - return *k; + return to_name(L, idx); } } -static options & to_options(lua_State * L, unsigned idx) { - return *static_cast(luaL_checkudata(L, idx, "options.mt")); -} - static int options_gc(lua_State * L) { to_options(L, 1).~options(); return 0; @@ -184,7 +190,7 @@ static const struct luaL_Reg options_m[] = { }; void open_options(lua_State * L) { - luaL_newmetatable(L, "options.mt"); + luaL_newmetatable(L, options_mt); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, options_m, 0); diff --git a/src/bindings/lua/options.h b/src/bindings/lua/options.h index cb089e12a..c55eff8f2 100644 --- a/src/bindings/lua/options.h +++ b/src/bindings/lua/options.h @@ -7,6 +7,9 @@ Author: Leonardo de Moura #ifdef LEAN_USE_LUA #include namespace lean { +class options; void open_options(lua_State * L); +bool is_options(lua_State * L, int idx); +options & to_options(lua_State * L, int idx); } #endif diff --git a/src/bindings/lua/util.cpp b/src/bindings/lua/util.cpp index 578c2eedd..f25feedbd 100644 --- a/src/bindings/lua/util.cpp +++ b/src/bindings/lua/util.cpp @@ -27,6 +27,18 @@ void setfuncs(lua_State * L, luaL_Reg const * l, int nup) { lua_pop(L, nup); // remove upvalues } +/** + \brief luaL_testudata replacement. +*/ +bool testudata(lua_State * L, unsigned idx, char const * mt) { + try { + luaL_checkudata(L, idx, mt); + return true; + } catch (...) { + return false; + } +} + int safe_function_wrapper(lua_State * L, lua_CFunction f){ static thread_local std::string _error_msg; char const * error_msg; diff --git a/src/bindings/lua/util.h b/src/bindings/lua/util.h index 4c9f63a34..d401c088d 100644 --- a/src/bindings/lua/util.h +++ b/src/bindings/lua/util.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include namespace lean { void setfuncs(lua_State * L, luaL_Reg const * l, int nup); +bool testudata(lua_State * L, unsigned idx, char const * mt); /** \brief Wrapper for invoking function f, and catching Lean exceptions. */