refactor(lua): add goodies for accessing Lean values on the Lua stack

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<name*>(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<name*>(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<mk_name>);

src/bindings/lua/name.h

@@ -7,6 +7,9 @@ Author: Leonardo de Moura
 #ifdef LEAN_USE_LUA
 #include <lua.hpp>
 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

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<unsigned idx>
 static mpz const & to_mpz(lua_State * L) {
     static thread_local mpz arg;
     if (lua_isuserdata(L, idx)) {
-        return *static_cast<mpz*>(luaL_checkudata(L, idx, "mpz.mt"));
+        return *static_cast<mpz*>(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<mpz*>(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<mpz*>(luaL_checkudata(L, 1, "mpz.mt"));
+    mpz * n = static_cast<mpz*>(luaL_checkudata(L, 1, mpz_mt));
     n->~mpz();
     return 0;
 }
 
 static int mpz_tostring(lua_State * L) {
-    mpz * n = static_cast<mpz*>(luaL_checkudata(L, 1, "mpz.mt"));
+    mpz * n = static_cast<mpz*>(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<mk_mpz>);
     lua_setglobal(L, "mpz");
 }
 
+constexpr char const * mpq_mt = "mpq.mt";
+
 template<unsigned idx>
 static mpq const & to_mpq(lua_State * L) {
     static thread_local mpq arg;
     if (lua_isuserdata(L, idx)) {
-        return *static_cast<mpq*>(luaL_checkudata(L, idx, "mpq.mt"));
+        return *static_cast<mpq*>(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<mpq*>(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<mpq*>(luaL_checkudata(L, 1, "mpq.mt"));
+    mpq * n = static_cast<mpq*>(luaL_checkudata(L, 1, mpq_mt));
     n->~mpq();
     return 0;
 }
 
 static int mpq_tostring(lua_State * L) {
-    mpq * n = static_cast<mpq*>(luaL_checkudata(L, 1, "mpq.mt"));
+    mpq * n = static_cast<mpq*>(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<mk_mpq>);

src/bindings/lua/numerics.h

@@ -7,7 +7,14 @@ Author: Leonardo de Moura
 #ifdef LEAN_USE_LUA
 #include <lua.hpp>
 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

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<options*>(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<name*>(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<options*>(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);

src/bindings/lua/options.h

@@ -7,6 +7,9 @@ Author: Leonardo de Moura
 #ifdef LEAN_USE_LUA
 #include <lua.hpp>
 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

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;

src/bindings/lua/util.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <lua.hpp>
 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.
 */