From 0579970fc59d9d9643abef69c7878ae4595a5bf7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2013 14:38:49 -0800 Subject: [PATCH] feat(lua): expose options object in the Lua bindings Signed-off-by: Leonardo de Moura --- src/bindings/lua/CMakeLists.txt | 2 +- src/bindings/lua/options.cpp | 176 ++++++++++++++++++++++++++++++++ src/bindings/lua/options.h | 12 +++ src/shell/lua/leanlua.cpp | 2 + 4 files changed, 191 insertions(+), 1 deletion(-) create mode 100644 src/bindings/lua/options.cpp create mode 100644 src/bindings/lua/options.h diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index 68214a3ff..e9b6deda8 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/src/bindings/lua/CMakeLists.txt @@ -1 +1 @@ -add_library(lua util.cpp name.cpp numerics.cpp) +add_library(lua util.cpp name.cpp numerics.cpp options.cpp) diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp new file mode 100644 index 000000000..7326ee0c7 --- /dev/null +++ b/src/bindings/lua/options.cpp @@ -0,0 +1,176 @@ +/* +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 +#include +#include "util/debug.h" +#include "util/name.h" +#include "util/sexpr/options.h" +#include "bindings/lua/util.h" + +namespace lean { +static int mk_option(lua_State * L); +static int options_gc(lua_State * L); +static int options_tostring(lua_State * L); +static int options_contains(lua_State * L); +static int options_size(lua_State * L); +static int options_empty(lua_State * L); +static int options_get_bool(lua_State * L); +static int options_get_int(lua_State * L); +static int options_get_unsigned(lua_State * L); +static int options_get_double(lua_State * L); +static int options_get_string(lua_State * L); +static int options_update_bool(lua_State * L); +static int options_update_int(lua_State * L); +static int options_update_unsigned(lua_State * L); +static int options_update_double(lua_State * L); +static int options_update_string(lua_State * L); + +static const struct luaL_Reg options_m[] = { + {"__gc", options_gc}, // never throws + {"__tostring", safe_function}, + {"__len", safe_function }, + {"contains", safe_function}, + {"size", safe_function}, + {"empty", safe_function}, + {"get_bool", safe_function}, + {"get_int", safe_function}, + {"get_unsigned", safe_function}, + {"get_double", safe_function}, + {"get_string", safe_function}, + {"update_bool", safe_function}, + {"update_int", safe_function}, + {"update_unsigned", safe_function}, + {"update_double", safe_function}, + {"update_string", safe_function}, + {0, 0} +}; + +void open_options(lua_State * L) { + luaL_newmetatable(L, "options.mt"); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, options_m, 0); + + lua_pushcfunction(L, safe_function); + lua_setglobal(L, "options"); +} + +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"); + lua_setmetatable(L, -2); + return 1; +} + +static int mk_option(lua_State * L) { + // int nargs = lua_gettop(L); + options r; + + // TODO(Leo): optional table argument + + return push_options(L, r); +} + +static name to_key(lua_State * L, unsigned 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; + } +} + +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; +} + +static int options_tostring(lua_State * L) { + std::ostringstream out; + out << to_options(L, 1); + lua_pushfstring(L, out.str().c_str()); + return 1; +} + +static int options_size(lua_State * L) { + lua_pushinteger(L, to_options(L, 1).size()); + return 1; +} + +static int options_contains(lua_State * L) { + lua_pushboolean(L, to_options(L, 1).contains(to_key(L, 2))); + return 1; +} + +static int options_empty(lua_State * L) { + lua_pushboolean(L, to_options(L, 1).empty()); + return 1; +} + +static int options_get_bool(lua_State * L) { + int nargs = lua_gettop(L); + bool defval = nargs < 3 ? false : lua_toboolean(L, 3); + lua_pushboolean(L, to_options(L, 1).get_bool(to_key(L, 2), defval)); + return 1; +} + +static int options_get_int(lua_State * L) { + int nargs = lua_gettop(L); + int defval = nargs < 3 ? 0 : lua_tointeger(L, 3); + lua_pushinteger(L, to_options(L, 1).get_int(to_key(L, 2), defval)); + return 1; +} + +static int options_get_unsigned(lua_State * L) { + int nargs = lua_gettop(L); + unsigned defval = nargs < 3 ? 0 : lua_tointeger(L, 3); + lua_pushnumber(L, to_options(L, 1).get_unsigned(to_key(L, 2), defval)); + return 1; +} + +static int options_get_double(lua_State * L) { + int nargs = lua_gettop(L); + double defval = nargs < 3 ? 0.0 : lua_tonumber(L, 3); + lua_pushnumber(L, to_options(L, 1).get_double(to_key(L, 2), defval)); + return 1; +} + +static int options_get_string(lua_State * L) { + int nargs = lua_gettop(L); + char const * defval = nargs < 3 ? "" : lua_tostring(L, 3); + lua_pushfstring(L, to_options(L, 1).get_string(to_key(L, 2), defval)); + return 1; +} + +static int options_update_bool(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_key(L, 2), static_cast(lua_toboolean(L, 3)))); +} + +static int options_update_int(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_key(L, 2), static_cast(lua_tointeger(L, 3)))); +} + +static int options_update_unsigned(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_key(L, 2), static_cast(lua_tointeger(L, 3)))); +} + +static int options_update_double(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_key(L, 2), lua_tonumber(L, 3))); +} + +static int options_update_string(lua_State * L) { + return push_options(L, to_options(L, 1).update(to_key(L, 2), lua_tostring(L, 3))); +} +} +#endif diff --git a/src/bindings/lua/options.h b/src/bindings/lua/options.h new file mode 100644 index 000000000..cb089e12a --- /dev/null +++ b/src/bindings/lua/options.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 open_options(lua_State * L); +} +#endif diff --git a/src/shell/lua/leanlua.cpp b/src/shell/lua/leanlua.cpp index fe3cfa901..9c52a300d 100644 --- a/src/shell/lua/leanlua.cpp +++ b/src/shell/lua/leanlua.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include #include "bindings/lua/name.h" #include "bindings/lua/numerics.h" +#include "bindings/lua/options.h" int main(int argc, char ** argv) { int status, result; @@ -21,6 +22,7 @@ int main(int argc, char ** argv) { lean::open_name(L); lean::open_mpz(L); lean::open_mpq(L); + lean::open_options(L); for (int i = 1; i < argc; i++) { status = luaL_loadfile(L, argv[i]);