diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp index 6c3e0daf5..daf5e7e51 100644 --- a/src/bindings/lua/expr.cpp +++ b/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"); diff --git a/src/bindings/lua/name.cpp b/src/bindings/lua/name.cpp index 7bc980ede..a54a9ef77 100644 --- a/src/bindings/lua/name.cpp +++ b/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: - throw exception(sstream() << "arg #" << i << " must be a hierarchical name, string, or integer"); + default: 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; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 07b736296..597917417 100644 --- a/src/tests/kernel/expr.cpp +++ b/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(); diff --git a/tests/lua/slow/t1.lua b/tests/lua/slow/t1.lua new file mode 100644 index 000000000..d8f33c28c --- /dev/null +++ b/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)