From bf57f951ea0c0b3c8b7963112ba9fa206e07b26f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 May 2014 13:20:37 -0700 Subject: [PATCH] refactor(util): move Lua named parameter support to a different file Signed-off-by: Leonardo de Moura --- src/library/kernel_bindings.cpp | 1 + src/util/CMakeLists.txt | 11 +++-- src/util/lua.cpp | 71 ---------------------------- src/util/lua.h | 10 +--- src/util/lua_named_param.cpp | 82 +++++++++++++++++++++++++++++++++ src/util/lua_named_param.h | 18 ++++++++ 6 files changed, 108 insertions(+), 85 deletions(-) create mode 100644 src/util/lua_named_param.cpp create mode 100644 src/util/lua_named_param.h diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index badcddfd6..21de2b9a7 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "util/script_state.h" #include "util/list_lua.h" #include "util/pair_lua.h" +#include "util/lua_named_param.h" #include "util/luaref.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 8cbbd2aa8..7dfc3d182 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -4,10 +4,11 @@ else() set(THREAD_CPP "") endif() -add_library(util trace.cpp debug.cpp name.cpp name_set.cpp name_generator.cpp - exception.cpp interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp - safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp realpath.cpp - script_state.cpp script_exception.cpp rb_map.cpp lua.cpp - luaref.cpp stackinfo.cpp lean_path.cpp serializer.cpp lbool.cpp ${THREAD_CPP}) +add_library(util trace.cpp debug.cpp name.cpp name_set.cpp + name_generator.cpp exception.cpp interrupt.cpp hash.cpp escaped.cpp + bit_tricks.cpp safe_arith.cpp ascii.cpp memory.cpp shared_mutex.cpp + realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp + lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp + serializer.cpp lbool.cpp ${THREAD_CPP}) target_link_libraries(util ${LEAN_LIBS}) diff --git a/src/util/lua.cpp b/src/util/lua.cpp index b46d844b1..30da54929 100644 --- a/src/util/lua.cpp +++ b/src/util/lua.cpp @@ -195,76 +195,5 @@ lua_migrate_fn get_migrate_fn(lua_State * L, int i) { } return nullptr; } - -bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value) { - if (lua_istable(L, idx)) { - bool result = def_value; - push_string(L, opt_name); - lua_gettable(L, idx); - if (lua_isboolean(L, -1)) { - result = lua_toboolean(L, -1); - lua_pop(L, 1); - return result; - } else if (lua_isnil(L, -1)) { - lua_pop(L, 1); - return result; - } else { - lua_pop(L, 1); - throw exception(sstream() << "field '" << opt_name << "' must be a Boolean in table at arg #" << idx); - } - } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) { - throw exception(sstream() << "arg #" << idx << " must be a table"); - } else { - return def_value; - } -} - -int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value) { - if (lua_istable(L, idx)) { - int result = def_value; - push_string(L, opt_name); - lua_gettable(L, idx); - if (lua_isnumber(L, -1)) { - result = lua_tointeger(L, -1); - lua_pop(L, 1); - return result; - } else if (lua_isnil(L, -1)) { - lua_pop(L, 1); - return result; - } else { - lua_pop(L, 1); - throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx); - } - } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) { - throw exception(sstream() << "arg #" << idx << " must be a table"); - } else { - return def_value; - } -} - -unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value) { - if (lua_istable(L, idx)) { - long result = def_value; - push_string(L, opt_name); - lua_gettable(L, idx); - if (lua_isnumber(L, -1)) { - long result = lua_tointeger(L, -1); - lua_pop(L, 1); - if (result < 0 || result > std::numeric_limits::max()) - throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx); - return static_cast(result); - } else if (lua_isnil(L, -1)) { - lua_pop(L, 1); - return static_cast(result); - } else { - lua_pop(L, 1); - throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx); - } - } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) { - throw exception(sstream() << "arg #" << idx << " must be a table"); - } else { - return def_value; - } -} } diff --git a/src/util/lua.h b/src/util/lua.h index fcc27cfcd..a97081956 100644 --- a/src/util/lua.h +++ b/src/util/lua.h @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -138,12 +138,4 @@ inline int push_integer(lua_State * L, lua_Integer v) { lua_pushinteger(L, v); r inline int push_number(lua_State * L, lua_Number v) { lua_pushnumber(L, v); return 1; } inline int push_nil(lua_State * L) { lua_pushnil(L); return 1; } // ======================================= - -// ======================================= -// Utilities for simulating Python-like named parameters using Lua tables. -// In the following function \c idx is the position of the Lua table on the Lua stack. -bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value); -int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value); -unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value); -// ======================================= } diff --git a/src/util/lua_named_param.cpp b/src/util/lua_named_param.cpp new file mode 100644 index 000000000..366645e77 --- /dev/null +++ b/src/util/lua_named_param.cpp @@ -0,0 +1,82 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/lua_named_param.h" +#include "util/sstream.h" + +namespace lean { +bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value) { + if (lua_istable(L, idx)) { + bool result = def_value; + push_string(L, opt_name); + lua_gettable(L, idx); + if (lua_isboolean(L, -1)) { + result = lua_toboolean(L, -1); + lua_pop(L, 1); + return result; + } else if (lua_isnil(L, -1)) { + lua_pop(L, 1); + return result; + } else { + lua_pop(L, 1); + throw exception(sstream() << "field '" << opt_name << "' must be a Boolean in table at arg #" << idx); + } + } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) { + throw exception(sstream() << "arg #" << idx << " must be a table"); + } else { + return def_value; + } +} + +int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value) { + if (lua_istable(L, idx)) { + int result = def_value; + push_string(L, opt_name); + lua_gettable(L, idx); + if (lua_isnumber(L, -1)) { + result = lua_tointeger(L, -1); + lua_pop(L, 1); + return result; + } else if (lua_isnil(L, -1)) { + lua_pop(L, 1); + return result; + } else { + lua_pop(L, 1); + throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx); + } + } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) { + throw exception(sstream() << "arg #" << idx << " must be a table"); + } else { + return def_value; + } +} + +unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value) { + if (lua_istable(L, idx)) { + push_string(L, opt_name); + lua_gettable(L, idx); + if (lua_isnumber(L, -1)) { + long result = lua_tointeger(L, -1); + lua_pop(L, 1); + if (result < 0 || result > std::numeric_limits::max()) + throw exception(sstream() << "field '" << opt_name << "' must be a unsigned integer in table at arg #" << idx); + return static_cast(result); + } else if (lua_isnil(L, -1)) { + lua_pop(L, 1); + return static_cast(def_value); + } else { + lua_pop(L, 1); + throw exception(sstream() << "field '" << opt_name << "' must be an integer in table at arg #" << idx); + } + } else if (idx <= lua_gettop(L) && !lua_isnil(L, idx)) { + throw exception(sstream() << "arg #" << idx << " must be a table"); + } else { + return def_value; + } +} +} + diff --git a/src/util/lua_named_param.h b/src/util/lua_named_param.h new file mode 100644 index 000000000..06799facf --- /dev/null +++ b/src/util/lua_named_param.h @@ -0,0 +1,18 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/lua.h" +#include "util/optional.h" + +namespace lean { +// ======================================= +// Utilities for simulating Python-like named parameters using Lua tables. +// In the following function \c idx is the position of the Lua table on the Lua stack. +bool get_bool_named_param(lua_State * L, int idx, char const * opt_name, bool def_value); +int get_int_named_param(lua_State * L, int idx, char const * opt_name, int def_value); +unsigned get_uint_named_param(lua_State * L, int idx, char const * opt_name, unsigned def_value); +}