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 <leonardo@microsoft.com>

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");
             }

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);

src/util/lua.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include <memory>
 #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<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;
+}
 }

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);
 }

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);

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");

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");

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);

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);

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);