diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index 63b37bc2f..358ed7874 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -28,6 +28,42 @@ Author: Leonardo de Moura extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); } namespace lean { +static void open_state(lua_State * L); + +static void copy_values(lua_State * src, int first, int last, lua_State * tgt) { + for (int i = first; i <= last; i++) { + if (lua_isstring(src, i)) { + lua_pushfstring(tgt, lua_tostring(src, i)); + } else if (lua_isnumber(src, i)) { + lua_pushnumber(tgt, lua_tonumber(src, i)); + } else 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_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)); + } else { + throw exception("unsupported value type for inter-State call"); + } + } +} + struct leanlua_state::imp { lua_State * m_state; std::mutex m_mutex; @@ -52,6 +88,7 @@ struct leanlua_state::imp { lean::open_expr(m_state); lean::open_context(m_state); lean::open_environment(m_state); + lean::open_state(m_state); dostring(g_leanlua_extra); } @@ -73,6 +110,30 @@ struct leanlua_state::imp { set_environment set(m_state, env); dostring(str); } + + int dostring(char const * str, lua_State * src, int first, int last) { + std::lock_guard lock(m_mutex); + + int sz_before = lua_gettop(m_state); + + int result = luaL_loadstring(m_state, str); + if (result) + throw lua_exception(lua_tostring(m_state, -1)); + + copy_values(src, first, last, m_state); + + result = lua_pcall(m_state, first > last ? 0 : last - first + 1, LUA_MULTRET, 0); + if (result) + throw lua_exception(lua_tostring(m_state, -1)); + + int sz_after = lua_gettop(m_state); + + if (sz_after > sz_before) { + copy_values(m_state, sz_before + 1, sz_after, src); + lua_pop(m_state, sz_after - sz_before); + } + return sz_after - sz_before; + } }; leanlua_state::leanlua_state(): @@ -93,4 +154,55 @@ void leanlua_state::dostring(char const * str) { void leanlua_state::dostring(char const * str, environment & env) { m_ptr->dostring(str, env); } + +int leanlua_state::dostring(char const * str, lua_State * src, int first, int last) { + return m_ptr->dostring(str, src, first, last); +} + +constexpr char const * state_mt = "state.mt"; + +bool is_state(lua_State * L, int idx) { + return testudata(L, idx, state_mt); +} + +leanlua_state & to_state(lua_State * L, int idx) { + return *static_cast(luaL_checkudata(L, idx, state_mt)); +} + +int push_state(lua_State * L, leanlua_state const & s) { + void * mem = lua_newuserdata(L, sizeof(leanlua_state)); + new (mem) leanlua_state(s); + luaL_getmetatable(L, state_mt); + lua_setmetatable(L, -2); + return 1; +} + +static int mk_state(lua_State * L) { + leanlua_state r; + return push_state(L, r); +} + +static int state_gc(lua_State * L) { + to_state(L, 1).~leanlua_state(); + return 0; +} + +static int state_dostring(lua_State * L) { + return to_state(L, 1).dostring(luaL_checkstring(L, 2), L, 3, lua_gettop(L)); +} + +static const struct luaL_Reg state_m[] = { + {"__gc", state_gc}, + {"dostring", safe_function}, + {0, 0} +}; + +static void open_state(lua_State * L) { + luaL_newmetatable(L, state_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, state_m, 0); + + set_global_function(L, "State"); +} } diff --git a/src/bindings/lua/leanlua_state.h b/src/bindings/lua/leanlua_state.h index 8a7ab25c3..49b43690d 100644 --- a/src/bindings/lua/leanlua_state.h +++ b/src/bindings/lua/leanlua_state.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include #include "bindings/lua/lua_exception.h" namespace lean { @@ -30,6 +31,20 @@ public: This method throws an exception if an error occurs. */ void dostring(char const * str); + + /** + \brief Execute the given script, but sets the registry with the given environment object. + The registry can be accessed by \str by invoking the function env(). + The script \c str should not store a reference to the environment \c env. + */ void dostring(char const * str, environment & env); + + /** + \brief Execute the given script, but copy the values at positions [first, last] from the stack of \c src. + The values are passed as arguments to the script \c str. + The values returned by the script \c str are copied back to the stack of \c src. + The result is the number of values returned by the script \c str. + */ + int dostring(char const * str, lua_State * src, int first, int last); }; } diff --git a/tests/lua/n3.lua b/tests/lua/n3.lua new file mode 100644 index 000000000..7000cb7ac --- /dev/null +++ b/tests/lua/n3.lua @@ -0,0 +1 @@ +print(2^32) diff --git a/tests/lua/st1.lua b/tests/lua/st1.lua new file mode 100644 index 000000000..987ae0e11 --- /dev/null +++ b/tests/lua/st1.lua @@ -0,0 +1,21 @@ +f = Const("f") +a = Const("a") +t = f(a) +s = State() +s:dostring("x = 10") + +t1, t2, t3 = +s:dostring([[ +a, b = ... +print("x = " .. tostring(x)) +print("a = " .. tostring(a)) +print("b = " .. tostring(b)) +g = Const("g") +return g(b), g(g(b)), g(b, b) +]], 10, t) +print("t1: " .. tostring(t1)) +print("t2: " .. tostring(t2)) +print("t3: " .. tostring(t3)) +print(x) +print(a) +s:dostring([[ print(b) ]])