perf(lua/name): improve to_name_ext performance

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

src/bindings/lua/expr.cpp

@@ -427,7 +427,7 @@ void open_expr(lua_State * L) {
     SET_GLOBAL_FUN(expr_mk_app,      "mk_app");
     SET_GLOBAL_FUN(expr_mk_eq,       "mk_eq");
     SET_GLOBAL_FUN(expr_mk_eq,       "Eq");
-    SET_GLOBAL_FUN(expr_mk_lambda,        "mk_lambda");
+    SET_GLOBAL_FUN(expr_mk_lambda,   "mk_lambda");
     SET_GLOBAL_FUN(expr_mk_pi,       "mk_pi");
     SET_GLOBAL_FUN(expr_mk_arrow,    "mk_arrow");
     SET_GLOBAL_FUN(expr_mk_let,      "mk_let");

src/bindings/lua/name.cpp

@@ -13,31 +13,6 @@ Author: Leonardo de Moura
 namespace lean {
 DECL_UDATA(name)
 
-name to_name_ext(lua_State * L, int idx) {
-    if (lua_isstring(L, idx)) {
-        return luaL_checkstring(L, idx);
-    } else if (lua_istable(L, idx)) {
-        name r;
-        int n = objlen(L, idx);
-        for (int i = 1; i <= n; i++) {
-            lua_rawgeti(L, idx, i);
-            if (lua_isnil(L, -1)) {
-                // skip
-            } else if (lua_isuserdata(L, -1)) {
-                r = r + to_name(L, -1);
-            } else if (lua_isstring(L, -1)) {
-                r = name(r, luaL_checkstring(L, -1));
-            } else {
-                r = name(r, luaL_checkinteger(L, -1));
-            }
-            lua_pop(L, 1);
-        }
-        return r;
-    } else {
-        return to_name(L, idx);
-    }
-}
-
 static int mk_name(lua_State * L) {
     int nargs = lua_gettop(L);
     name r;
@@ -47,13 +22,35 @@ static int mk_name(lua_State * L) {
         case LUA_TNUMBER:   r = name(r, lua_tointeger(L, i)); break;
         case LUA_TSTRING:   r = name(r, lua_tostring(L, i)); break;
         case LUA_TUSERDATA: r = r + to_name(L, i); break;
-        default:
+        default:            throw exception(sstream() << "arg #" << i << " must be a hierarchical name, string, or integer");
-            throw exception(sstream() << "arg #" << i << " must be a hierarchical name, string, or integer");
         }
     }
     return push_name(L, r);
 }
 
+name to_name_ext(lua_State * L, int idx) {
+    if (lua_isstring(L, idx)) {
+        return luaL_checkstring(L, idx);
+    } else if (lua_istable(L, idx)) {
+        name r;
+        int n = objlen(L, idx);
+        for (int i = 1; i <= n; i++) {
+            lua_rawgeti(L, idx, i);
+            switch (lua_type(L, -1)) {
+            case LUA_TNIL:      break; // skip
+            case LUA_TNUMBER:   r = name(r, lua_tointeger(L, -1)); break;
+            case LUA_TSTRING:   r = name(r, lua_tostring(L, -1));  break;
+            case LUA_TUSERDATA: r = r + to_name(L, -1); break;
+            default:            throw exception("invalid array arguments, elements must be a hierarchical name, string, or integer");
+            }
+            lua_pop(L, 1);
+        }
+        return r;
+    } else {
+        return to_name(L, idx);
+    }
+}
+
 static int name_tostring(lua_State * L) {
     lua_pushstring(L, to_name(L, 1).to_string().c_str());
     return 1;

src/tests/kernel/expr.cpp

@@ -376,8 +376,6 @@ int main() {
     std::cout << "sizeof(expr):      " << sizeof(expr) << "\n";
     std::cout << "sizeof(expr_app):  " << sizeof(expr_app) << "\n";
     std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";
-    tst3();
-    return 0;
     tst1();
     tst2();
     tst3();

tests/lua/slow/t1.lua

@@ -0,0 +1,12 @@
+function mk_big(f, depth, val)
+    if depth == 1 then
+       return Const{"foo", val}
+    else
+       return f(mk_big(f, depth - 1, 2 * val), mk_big(f, depth - 1, 2 * val + 1))
+    end
+end
+
+local f  = Const("f")
+local r1 = mk_big(f, 20, 0)
+local r2 = mk_big(f, 20, 0)
+assert(r1 == r2)