diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index c19ed5737..68214a3ff 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/src/bindings/lua/CMakeLists.txt @@ -1 +1 @@ -add_library(lua name.cpp numerics.cpp) +add_library(lua util.cpp name.cpp numerics.cpp) diff --git a/src/bindings/lua/name.cpp b/src/bindings/lua/name.cpp index 5b247853b..a5d63220b 100644 --- a/src/bindings/lua/name.cpp +++ b/src/bindings/lua/name.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "util/debug.h" #include "util/name.h" +#include "bindings/lua/util.h" namespace lean { static int name_gc(lua_State * L); @@ -81,7 +82,7 @@ static int name_lt(lua_State * L) { void init_name(lua_State * L) { luaL_newmetatable(L, "name.mt"); - luaL_setfuncs(L, name_m, 0); + setfuncs(L, name_m, 0); lua_pushcfunction(L, mk_name); lua_setglobal(L, "name"); diff --git a/src/bindings/lua/numerics.cpp b/src/bindings/lua/numerics.cpp index a232d84b7..c19c50d1a 100644 --- a/src/bindings/lua/numerics.cpp +++ b/src/bindings/lua/numerics.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "util/debug.h" #include "util/numerics/mpz.h" #include "util/numerics/mpq.h" +#include "bindings/lua/util.h" namespace lean { template @@ -99,7 +100,7 @@ public: static void init(lua_State * L) { luaL_newmetatable(L, M); - luaL_setfuncs(L, m, 0); + setfuncs(L, m, 0); lua_pushcfunction(L, mk); lua_setglobal(L, N); diff --git a/src/bindings/lua/util.cpp b/src/bindings/lua/util.cpp new file mode 100644 index 000000000..72665a950 --- /dev/null +++ b/src/bindings/lua/util.cpp @@ -0,0 +1,25 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#ifdef LEAN_USE_LUA +#include +namespace lean { +/** + \brief luaL_setfuncs replacement. The function luaL_setfuncs is only available in Lua 5.2. +*/ +void setfuncs(lua_State * L, luaL_Reg const * l, int nup) { + luaL_checkstack(L, nup, "too many upvalues"); + for (; l->name != NULL; l++) { + // fill the table with given functions + for (int i = 0; i < nup; i++) // copy upvalues to the top + lua_pushvalue(L, -nup); + lua_pushcclosure(L, l->func, nup); // closure with those upvalues + lua_setfield(L, -(nup + 2), l->name); + } + lua_pop(L, nup); // remove upvalues +} +} +#endif diff --git a/src/bindings/lua/util.h b/src/bindings/lua/util.h new file mode 100644 index 000000000..b48233736 --- /dev/null +++ b/src/bindings/lua/util.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#ifdef LEAN_USE_LUA +#include +namespace lean { +void setfuncs(lua_State * L, luaL_Reg const * l, int nup); +} +#endif