From a6f6f49b5f1908d34008c4bcee9ec252bdc19985 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Nov 2013 10:32:15 -0800 Subject: [PATCH] refactor(frontends/lua): add lua_migrate_fn, and make copy_values modular copy_values is not a big if-then-else anymore. Before this change, whenever we added a new kind of userdata, we would have to update copy_values. Signed-off-by: Leonardo de Moura --- src/frontends/lua/leanlua_state.cpp | 26 ++----------------------- src/library/kernel_bindings.cpp | 30 +++++++++++++++++++++++++++++ src/util/lua.cpp | 26 +++++++++++++++++++++++++ src/util/lua.h | 14 ++++++++++++++ src/util/name.cpp | 5 +++++ src/util/numerics/mpq.cpp | 7 +++++++ src/util/numerics/mpz.cpp | 7 +++++++ src/util/sexpr/format.cpp | 5 +++++ src/util/sexpr/options.cpp | 5 +++++ src/util/sexpr/sexpr.cpp | 5 +++++ 10 files changed, 106 insertions(+), 24 deletions(-) diff --git a/src/frontends/lua/leanlua_state.cpp b/src/frontends/lua/leanlua_state.cpp index 60cdbd836..1a8e998a1 100644 --- a/src/frontends/lua/leanlua_state.cpp +++ b/src/frontends/lua/leanlua_state.cpp @@ -222,30 +222,8 @@ static void copy_values(lua_State * src, int first, int last, lua_State * tgt) { break; } case LUA_TUSERDATA: - if (is_expr(src, i)) { - push_expr(tgt, to_expr(src, i)); - } else if (is_context(src, i)) { - push_context(tgt, to_context(src, i)); - } else if (is_environment(src, i)) { - push_environment(tgt, to_environment(src, i)); - } else if (is_name(src, i)) { - push_name(tgt, to_name(src, i)); - } else if (is_mpz(src, i)) { - push_mpz(tgt, to_mpz(src, i)); - } else if (is_mpq(src, i)) { - push_mpq(tgt, to_mpq(src, i)); - } else if (is_options(src, i)) { - push_options(tgt, to_options(src, i)); - } else if (is_sexpr(src, i)) { - push_sexpr(tgt, to_sexpr(src, i)); - } else if (is_format(src, i)) { - push_format(tgt, to_format(src, i)); - } else if (is_context_entry(src, i)) { - push_context_entry(tgt, to_context_entry(src, i)); - } else if (is_local_context(src, i)) { - push_local_context(tgt, to_local_context(src, i)); - } else if (is_local_entry(src, i)) { - push_local_entry(tgt, to_local_entry(src, i)); + if (lua_migrate_fn f = get_migrate_fn(src, i)) { + f(src, i, tgt); } else { throw exception("unsupported value type for inter-State call"); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 9676a7f88..9326ba408 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -238,8 +238,17 @@ static const struct luaL_Reg local_context_m[] = { {0, 0} }; +static void local_entry_migrate(lua_State * src, int i, lua_State * tgt) { + push_local_entry(tgt, to_local_entry(src, i)); +} + +static void local_context_migrate(lua_State * src, int i, lua_State * tgt) { + push_local_context(tgt, to_local_context(src, i)); +} + static void open_local_context(lua_State * L) { luaL_newmetatable(L, local_entry_mt); + set_migrate_fn_field(L, -1, local_entry_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, local_entry_m, 0); @@ -248,6 +257,7 @@ static void open_local_context(lua_State * L) { SET_GLOBAL_FUN(local_entry_pred, "is_local_entry"); luaL_newmetatable(L, local_context_mt); + set_migrate_fn_field(L, -1, local_context_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, local_context_m, 0); @@ -630,8 +640,13 @@ static const struct luaL_Reg expr_m[] = { {0, 0} }; +static void expr_migrate(lua_State * src, int i, lua_State * tgt) { + push_expr(tgt, to_expr(src, i)); +} + static void open_expr(lua_State * L) { luaL_newmetatable(L, expr_mt); + set_migrate_fn_field(L, -1, expr_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, expr_m, 0); @@ -752,8 +767,17 @@ static const struct luaL_Reg context_m[] = { {0, 0} }; +static void context_entry_migrate(lua_State * src, int i, lua_State * tgt) { + push_context_entry(tgt, to_context_entry(src, i)); +} + +static void context_migrate(lua_State * src, int i, lua_State * tgt) { + push_context(tgt, to_context(src, i)); +} + static void open_context(lua_State * L) { luaL_newmetatable(L, context_entry_mt); + set_migrate_fn_field(L, -1, context_entry_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, context_entry_m, 0); @@ -761,6 +785,7 @@ static void open_context(lua_State * L) { SET_GLOBAL_FUN(context_entry_pred, "is_context_entry"); luaL_newmetatable(L, context_mt); + set_migrate_fn_field(L, -1, context_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, context_m, 0); @@ -1105,8 +1130,13 @@ int get_environment(lua_State * L) { return push_environment(L, get_global_environment(L)); } +static void environment_migrate(lua_State * src, int i, lua_State * tgt) { + push_environment(tgt, to_environment(src, i)); +} + static void open_environment(lua_State * L) { luaL_newmetatable(L, environment_mt); + set_migrate_fn_field(L, -1, environment_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, environment_m, 0); diff --git a/src/util/lua.cpp b/src/util/lua.cpp index 6877c61d3..fe13b3192 100644 --- a/src/util/lua.cpp +++ b/src/util/lua.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include #include "util/lua.h" #include "util/lua_exception.h" +#include "util/debug.h" namespace lean { /** @@ -149,4 +150,29 @@ int (*g_safe_function_wrapper)(lua_State * L, lua_CFunction f) = simple_safe_fun set_safe_function_wrapper::set_safe_function_wrapper(int (*f)(lua_State *, lua_CFunction)) { g_safe_function_wrapper = f; } + +void set_migrate_fn_field(lua_State * L, int i, lua_migrate_fn fn) { + lean_assert(lua_istable(L, i)); + lua_pushvalue(L, i); // copy table to the top of the stack + lua_pushlightuserdata(L, reinterpret_cast(fn)); + lua_setfield(L, -2, "___migrate"); + lua_pop(L, 1); // remove table from the stack +} + +/** + \brief Return the value of the ___migrate field from metatable + for the userdata at position \c i. +*/ +lua_migrate_fn get_migrate_fn(lua_State * L, int i) { + if (lua_getmetatable(L, i)) { + lua_getfield(L, -1, "___migrate"); + if (lua_islightuserdata(L, -1)) { + lua_migrate_fn r = reinterpret_cast(lua_touserdata(L, -1)); + lua_pop(L, 2); + return r; + } + lua_pop(L, 2); + } + return nullptr; +} } diff --git a/src/util/lua.h b/src/util/lua.h index f6b3ff702..23c40eb0d 100644 --- a/src/util/lua.h +++ b/src/util/lua.h @@ -117,4 +117,18 @@ int push_ ## T(lua_State * L, T && e); class T; \ UDATA_DEFS_CORE(T) // ======================================= + +// ======================================= +// Goodies for installing code for migrating objects +// between different lua_State objects +typedef void (*lua_migrate_fn)(lua_State * src, int i, lua_State * tgt); +/** + \brief Set the field ___migrate in the metatable at position \c i with \c fn. +*/ +void set_migrate_fn_field(lua_State * src, int i, lua_migrate_fn fn); +/** + \brief Return the value of the ___migrate field from metatable + for the userdata at position \c i. +*/ +lua_migrate_fn get_migrate_fn(lua_State * src, int i); } diff --git a/src/util/name.cpp b/src/util/name.cpp index d428dd0a9..a6b4db67c 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -429,8 +429,13 @@ static const struct luaL_Reg name_m[] = { {0, 0} }; +static void name_migrate(lua_State * src, int i, lua_State * tgt) { + push_name(tgt, to_name(src, i)); +} + void open_name(lua_State * L) { luaL_newmetatable(L, name_mt); + set_migrate_fn_field(L, -1, name_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, name_m, 0); diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp index ffc5c3f22..ed202d1d6 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/numerics/mpq.cpp @@ -222,8 +222,15 @@ static const struct luaL_Reg mpq_m[] = { {0, 0} }; +static void mpq_migrate(lua_State * src, int i, lua_State * tgt) { + push_mpq(tgt, to_mpq(src, i)); +} + void open_mpq(lua_State * L) { luaL_newmetatable(L, mpq_mt); + set_migrate_fn_field(L, -1, mpq_migrate); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); setfuncs(L, mpq_m, 0); SET_GLOBAL_FUN(mk_mpq, "mpq"); diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp index fc07db87e..c37668c32 100644 --- a/src/util/numerics/mpz.cpp +++ b/src/util/numerics/mpz.cpp @@ -170,8 +170,15 @@ static const struct luaL_Reg mpz_m[] = { {0, 0} }; +static void mpz_migrate(lua_State * src, int i, lua_State * tgt) { + push_mpz(tgt, to_mpz(src, i)); +} + void open_mpz(lua_State * L) { luaL_newmetatable(L, mpz_mt); + set_migrate_fn_field(L, -1, mpz_migrate); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); setfuncs(L, mpz_m, 0); SET_GLOBAL_FUN(mk_mpz, "mpz"); diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index bd54ad86e..8dd8b742c 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -529,8 +529,13 @@ static const struct luaL_Reg format_m[] = { {0, 0} }; +static void format_migrate(lua_State * src, int i, lua_State * tgt) { + push_format(tgt, to_format(src, i)); +} + void open_format(lua_State * L) { luaL_newmetatable(L, format_mt); + set_migrate_fn_field(L, -1, format_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, format_m, 0); diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp index efbafb6fb..5ae907210 100644 --- a/src/util/sexpr/options.cpp +++ b/src/util/sexpr/options.cpp @@ -373,8 +373,13 @@ static int _set_global_option(lua_State * L) { return 0; } +static void options_migrate(lua_State * src, int i, lua_State * tgt) { + push_options(tgt, to_options(src, i)); +} + void open_options(lua_State * L) { luaL_newmetatable(L, options_mt); + set_migrate_fn_field(L, -1, options_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, options_m, 0); diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp index 00dde2bb6..b2dfaaac7 100644 --- a/src/util/sexpr/sexpr.cpp +++ b/src/util/sexpr/sexpr.cpp @@ -486,8 +486,13 @@ static const struct luaL_Reg sexpr_m[] = { {0, 0} }; +static void sexpr_migrate(lua_State * src, int i, lua_State * tgt) { + push_sexpr(tgt, to_sexpr(src, i)); +} + void open_sexpr(lua_State * L) { luaL_newmetatable(L, sexpr_mt); + set_migrate_fn_field(L, -1, sexpr_migrate); lua_pushvalue(L, -1); lua_setfield(L, -2, "__index"); setfuncs(L, sexpr_m, 0);