feat(lua): allow Lua scripts to update 'global' options

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

src/bindings/lua/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp
 options.cpp sexpr.cpp format.cpp level.cpp local_context.cpp expr.cpp
-context.cpp object.cpp environment.cpp formatter.cpp leanlua_state.cpp)
+context.cpp object.cpp environment.cpp formatter.cpp state.cpp leanlua_state.cpp)
 
 target_link_libraries(lua ${LEAN_LIBS})

src/bindings/lua/formatter.cpp

@@ -46,7 +46,7 @@ static int formatter_gc(lua_State * L) {
 static int formatter_call(lua_State * L) {
     int nargs = lua_gettop(L);
     formatter & fmt = to_formatter(L, 1);
-    options opts;
+    options opts = get_global_options(L);
     if (nargs <= 3) {
         if (nargs == 3) {
             if (is_options(L, 3))

src/bindings/lua/leanlua_state.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/context.h"
 #include "bindings/lua/object.h"
 #include "bindings/lua/environment.h"
+#include "bindings/lua/state.h"
 #include "bindings/lua/lean.lua"
 
 extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
@@ -168,6 +169,11 @@ struct leanlua_state::imp {
         set_environment set(m_state, env);
         dostring(str);
     }
+
+    void dostring(char const * str, environment & env, state & st) {
+        set_state set(m_state, st);
+        dostring(str, env);
+    }
 };
 
 leanlua_state::leanlua_state():
@@ -189,6 +195,10 @@ void leanlua_state::dostring(char const * str, environment & env) {
     m_ptr->dostring(str, env);
 }
 
+void leanlua_state::dostring(char const * str, environment & env, state & st) {
+    m_ptr->dostring(str, env, st);
+}
+
 static std::mutex g_print_mutex;
 
 /** \brief Thread safe version of print function */
@@ -222,7 +232,7 @@ static void open_patch(lua_State * L) {
     set_global_function<print>(L, "print");
 }
 
-constexpr char const * state_mt = "state.mt";
+constexpr char const * state_mt = "luastate.mt";
 
 bool is_state(lua_State * L, int idx) {
     return testudata(L, idx, state_mt);

src/bindings/lua/leanlua_state.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 class environment;
+class state;
 /**
    \brief Wrapper for lua_State objects which contains all Lean bindings.
 */
@@ -43,5 +44,7 @@ public:
        The script \c str should not store a reference to the environment \c env.
     */
     void dostring(char const * str, environment & env);
+
+    void dostring(char const * str, environment & env, state & st);
 };
 }

src/bindings/lua/options.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/option_declarations.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
+#include "bindings/lua/state.h"
 
 namespace lean {
 constexpr char const * options_mt = "options.mt";
@@ -171,6 +172,54 @@ static int options_pred(lua_State * L) {
     return 1;
 }
 
+static char g_options_key;
+
+options get_global_options(lua_State * L) {
+    state * S = get_state(L);
+    if (S != nullptr) {
+        return S->get_options();
+    } else {
+        lua_pushlightuserdata(L, static_cast<void *>(&g_options_key));
+        lua_gettable(L, LUA_REGISTRYINDEX);
+        options r;
+        if (!is_options(L, -1))
+            r = to_options(L, -1);
+        lua_pop(L, 1);
+        return r;
+    }
+}
+
+void set_global_options(lua_State * L, options const & o) {
+    state * S = get_state(L);
+    if (S != nullptr) {
+        S->set_options(o);
+    } else {
+        lua_pushlightuserdata(L, static_cast<void *>(&g_options_key));
+        push_options(L, o);
+        lua_settable(L, LUA_REGISTRYINDEX);
+    }
+}
+
+static int _get_global_options(lua_State * L) {
+    return push_options(L, get_global_options(L));
+}
+
+static int _set_global_options(lua_State * L) {
+    options o = to_options(L, 1);
+    set_global_options(L, o);
+    return 0;
+}
+
+static int _set_global_option(lua_State * L) {
+    options o = get_global_options(L);
+    push_options(L, o);
+    lua_insert(L, 1);
+    options_update(L);
+    o = to_options(L, -1);
+    set_global_options(L, o);
+    return 0;
+}
+
 static const struct luaL_Reg options_m[] = {
     {"__gc",            options_gc}, // never throws
     {"__tostring",      safe_function<options_tostring>},
@@ -202,5 +251,8 @@ void open_options(lua_State * L) {
 
     set_global_function<mk_options>(L, "options");
     set_global_function<options_pred>(L, "is_options");
+    set_global_function<_get_global_options>(L, "get_options");
+    set_global_function<_set_global_options>(L, "set_options");
+    set_global_function<_set_global_option>(L, "set_option");
 }
 }

src/bindings/lua/options.h

@@ -12,4 +12,17 @@ void open_options(lua_State * L);
 bool is_options(lua_State * L, int idx);
 options & to_options(lua_State * L, int idx);
 int push_options(lua_State * L, options const & o);
+/**
+   \brief Return the set of options associated with the given Lua State.
+   This procedure checks for options at:
+   1- Lean state object associated with \c L
+   2- Lua Registry associated with \c L
+*/
+options get_global_options(lua_State * L);
+/**
+   \brief Update the set of options associated with the given Lua State.
+   If \c L is associated with a Lean state object \c S, then we update the options of \c S.
+   Otherwise, we update the registry of \c L.
+*/
+void set_global_options(lua_State * L, options const & o);
 }

src/bindings/lua/state.cpp

@@ -0,0 +1,39 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <lua.hpp>
+#include "library/state.h"
+#include "bindings/lua/state.h"
+
+namespace lean {
+static char g_set_state_key;
+
+set_state::set_state(lua_State * L, state & st) {
+    m_state = L;
+    lua_pushlightuserdata(m_state, static_cast<void *>(&g_set_state_key));
+    lua_pushlightuserdata(m_state, &st);
+    lua_settable(m_state, LUA_REGISTRYINDEX);
+}
+
+set_state::~set_state() {
+    lua_pushlightuserdata(m_state, static_cast<void *>(&g_set_state_key));
+    lua_pushnil(m_state);
+    lua_settable(m_state, LUA_REGISTRYINDEX);
+}
+
+state * get_state(lua_State * L) {
+    lua_pushlightuserdata(L, static_cast<void *>(&g_set_state_key));
+    lua_gettable(L, LUA_REGISTRYINDEX);
+    if (!lua_islightuserdata(L, -1)) {
+        lua_pop(L, 1);
+        return nullptr;
+    } else {
+        state * r = static_cast<state*>(lua_touserdata(L, -1));
+        lua_pop(L, 1);
+        return r;
+    }
+}
+}

src/bindings/lua/state.h

@@ -0,0 +1,27 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <lua.hpp>
+#include "library/state.h"
+
+namespace lean {
+/**
+   \brief Auxiliary class for temporarily setting the Lua registry of a Lua state
+   with a Lean state object.
+*/
+class set_state {
+    lua_State * m_state;
+public:
+    set_state(lua_State * L, state & st);
+    ~set_state();
+};
+/**
+   \brief Return the Lean state object associated with the given Lua state.
+   Return nullptr is there is none.
+*/
+state * get_state(lua_State * L);
+}

src/frontends/lean/parser.cpp

@@ -1593,7 +1593,7 @@ class parser::imp {
         m_last_script_pos = mk_pair(m_scanner.get_script_block_line(), m_scanner.get_script_block_pos());
         if (!m_leanlua_state)
             throw exception("failed to execute Lua script, parser does not have a Lua interpreter");
-        m_leanlua_state->dostring(m_scanner.get_str_val().c_str(), m_frontend.get_environment());
+        m_leanlua_state->dostring(m_scanner.get_str_val().c_str(), m_frontend.get_environment(), m_frontend.get_state());
         next();
     }
 

tests/lean/lua6.lean

@@ -0,0 +1,19 @@
+Variable x : Int
+Set pp::notation false
+{{
+print(get_options())
+}}
+Check x + 2
+{{
+o = get_options()
+o = o:update(name('lean', 'pp', 'notation'), true)
+set_options(o)
+print(get_options())
+}}
+Check x + 2
+{{
+set_option(name('lean', 'pp', 'notation'), false)
+print(get_options())
+}}
+Variable y : Int
+Check x + y

tests/lean/lua6.lean.expected.out

@@ -0,0 +1,11 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: x
+  Set: lean::pp::notation
+⟨lean::pp::notation ↦ false, pp::unicode ↦ true, pp::colors ↦ false⟩
+Int::add x 2 : ℤ
+⟨lean::pp::notation ↦ true, pp::unicode ↦ true, pp::colors ↦ false⟩
+x + 2 : ℤ
+⟨lean::pp::notation ↦ false, pp::unicode ↦ true, pp::colors ↦ false⟩
+  Assumed: y
+Int::add x y : ℤ