chore(*): remove Lua 'migrate'

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

src/library/kernel_bindings.cpp

@@ -817,13 +817,8 @@ static const struct luaL_Reg expr_m[] = {
 
 static int enable_expr_caching(lua_State * L) { return push_boolean(L, enable_expr_caching(lua_toboolean(L, 1))); }
 
-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);
@@ -1128,13 +1123,8 @@ static const struct luaL_Reg certified_declaration_m[] = {
     {0, 0}
 };
 
-static void certified_declaration_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_certified_declaration(tgt, to_certified_declaration(src, i));
-}
-
 static void open_certified_declaration(lua_State * L) {
     luaL_newmetatable(L, certified_declaration_mt);
-    set_migrate_fn_field(L, -1, certified_declaration_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, certified_declaration_m, 0);
@@ -1328,13 +1318,8 @@ int set_environment(lua_State * L) {
     return 0;
 }
 
-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);

src/library/tactic/cex_builder.cpp

@@ -73,13 +73,8 @@ static const struct luaL_Reg cex_builder_m[] = {
     {0, 0}
 };
 
-static void cex_builder_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_cex_builder(tgt, to_cex_builder(src, i));
-}
-
 void open_cex_builder(lua_State * L) {
     luaL_newmetatable(L, cex_builder_mt);
-    set_migrate_fn_field(L, -1, cex_builder_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, cex_builder_m, 0);

src/library/tactic/goal.cpp

@@ -302,17 +302,8 @@ static const struct luaL_Reg goal_m[] = {
     {0, 0}
 };
 
-static void hypotheses_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_hypotheses(tgt, to_hypotheses(src, i));
-}
-
-static void goal_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_goal(tgt, to_goal(src, i));
-}
-
 void open_goal(lua_State * L) {
     luaL_newmetatable(L, hypotheses_mt);
-    set_migrate_fn_field(L, -1, hypotheses_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, hypotheses_m, 0);
@@ -321,7 +312,6 @@ void open_goal(lua_State * L) {
     SET_GLOBAL_FUN(mk_hypotheses, "hypotheses");
 
     luaL_newmetatable(L, goal_mt);
-    set_migrate_fn_field(L, -1, goal_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, goal_m, 0);

src/library/tactic/proof_builder.cpp

@@ -129,21 +129,8 @@ static const struct luaL_Reg proof_builder_m[] = {
     {0, 0}
 };
 
-static void proof_map_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_proof_map(tgt, to_proof_map(src, i));
-}
-
-static void assignment_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_assignment(tgt, to_assignment(src, i));
-}
-
-static void proof_builder_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_proof_builder(tgt, to_proof_builder(src, i));
-}
-
 void open_proof_builder(lua_State * L) {
     luaL_newmetatable(L, proof_map_mt);
-    set_migrate_fn_field(L, -1, proof_map_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, proof_map_m, 0);
@@ -152,7 +139,6 @@ void open_proof_builder(lua_State * L) {
     SET_GLOBAL_FUN(mk_proof_map, "proof_map");
 
     luaL_newmetatable(L, assignment_mt);
-    set_migrate_fn_field(L, -1, assignment_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, assignment_m, 0);
@@ -161,7 +147,6 @@ void open_proof_builder(lua_State * L) {
     SET_GLOBAL_FUN(mk_assignment, "assignment");
 
     luaL_newmetatable(L, proof_builder_mt);
-    set_migrate_fn_field(L, -1, proof_builder_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, proof_builder_m, 0);

src/library/tactic/proof_state.cpp

@@ -316,17 +316,8 @@ static const struct luaL_Reg proof_state_m[] = {
     {0, 0}
 };
 
-static void goals_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_goals(tgt, to_goals(src, i));
-}
-
-static void proof_state_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_proof_state(tgt, to_proof_state(src, i));
-}
-
 void open_proof_state(lua_State * L) {
     luaL_newmetatable(L, goals_mt);
-    set_migrate_fn_field(L, -1, goals_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, goals_m, 0);
@@ -335,7 +326,6 @@ void open_proof_state(lua_State * L) {
     SET_GLOBAL_FUN(mk_goals, "goals");
 
     luaL_newmetatable(L, proof_state_mt);
-    set_migrate_fn_field(L, -1, proof_state_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, proof_state_m, 0);

src/library/tactic/tactic.cpp

@@ -795,10 +795,6 @@ static const struct luaL_Reg tactic_m[] = {
     {0, 0}
 };
 
-static void tactic_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_tactic(tgt, to_tactic(src, i));
-}
-
 void open_tactic(lua_State * L) {
     luaL_newmetatable(L, proof_state_seq_mt);
     lua_pushvalue(L, -1);
@@ -807,7 +803,6 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(proof_state_seq_pred, "is_proof_state_seq");
 
     luaL_newmetatable(L, tactic_mt);
-    set_migrate_fn_field(L, -1, tactic_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, tactic_m, 0);

src/util/exception.cpp

@@ -89,13 +89,8 @@ static const struct luaL_Reg exception_m[] = {
     {0, 0}
 };
 
-static void exception_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_exception(tgt, to_exception(src, i));
-}
-
 void open_exception(lua_State * L) {
     luaL_newmetatable(L, exception_mt);
-    set_migrate_fn_field(L, -1, exception_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, exception_m, 0);

src/util/lua.cpp

@@ -171,31 +171,6 @@ int safe_function_wrapper(lua_State * L, lua_CFunction f) {
     return lua_error(L);
 }
 
-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<void*>(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_migrate_fn>(lua_touserdata(L, -1));
-            lua_pop(L, 2);
-            return r;
-        }
-        lua_pop(L, 2);
-    }
-    return nullptr;
-}
-
 void check_num_args(lua_State * L, int num) {
     if (lua_gettop(L) != num) throw exception("incorrect number of arguments to function");
 }

src/util/lua.h

@@ -112,21 +112,6 @@ 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);
-// =======================================
-
 // =======================================
 // Useful macros
 inline int push_boolean(lua_State * L, bool b) { lua_pushboolean(L, b); return 1; }

src/util/lua_list.h

@@ -68,12 +68,8 @@ list<T> to_list_ ## T ## _ext(lua_State * L, int idx) {                 \
     else                                                                \
         return table_to_list<T>(L, idx, ToVal);                         \
 }                                                                       \
-static void list_ ## T ## _migrate(lua_State * src, int i, lua_State * tgt) { \
-    push_list_ ## T(tgt, to_list_ ## T(src, i));                        \
-}                                                                       \
 static void open_list_ ## T(lua_State * L) {                            \
     luaL_newmetatable(L, list_ ## T ## _mt);                            \
-    set_migrate_fn_field(L, -1, list_ ## T ## _migrate);                \
     lua_pushvalue(L, -1);                                               \
     lua_setfield(L, -2, "__index");                                     \
     setfuncs(L, list_ ## T ## _m, 0);                                   \

src/util/name.cpp

@@ -583,15 +583,10 @@ 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));
-}
-
 DEFINE_LUA_LIST(name, push_name, to_name_ext)
 
 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);

src/util/name_generator.cpp

@@ -37,11 +37,9 @@ static const struct luaL_Reg name_generator_m[] = {
     {"mk_child", safe_function<name_generator_mk_child>},
     {0, 0}
 };
-static void name_generator_migrate(lua_State * src, int i, lua_State * tgt) { push_name_generator(tgt, to_name_generator(src, i)); }
 
 void open_name_generator(lua_State * L) {
     luaL_newmetatable(L, name_generator_mt);
-    set_migrate_fn_field(L, -1, name_generator_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, name_generator_m, 0);

src/util/name_set.cpp

@@ -37,11 +37,9 @@ static const struct luaL_Reg name_set_m[] = {
     {"erase",    safe_function<name_set_erase>},
     {0, 0}
 };
-static void name_set_migrate(lua_State * src, int i, lua_State * tgt) { push_name_set(tgt, to_name_set(src, i)); }
 
 void open_name_set(lua_State * L) {
     luaL_newmetatable(L, name_set_mt);
-    set_migrate_fn_field(L, -1, name_set_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, name_set_m, 0);

src/util/numerics/mpq.cpp

@@ -234,13 +234,8 @@ 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);

src/util/numerics/mpz.cpp

@@ -181,13 +181,8 @@ 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);

src/util/sexpr/format.cpp

@@ -481,13 +481,8 @@ 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);

src/util/sexpr/options.cpp

@@ -394,13 +394,8 @@ 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);

src/util/sexpr/sexpr.cpp

@@ -545,13 +545,8 @@ 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);