fix(library/kernel_bindings): make sure that when a formatter is invoked and it has a reference to an environment object, we get a read-only lock to the environment object

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

src/frontends/lean/pp.cpp

@@ -1378,6 +1378,8 @@ public:
                       });
         return r;
     }
+
+    virtual optional<environment> get_environment() const { return optional<environment>(env()); }
 };
 
 formatter mk_pp_formatter(environment const & env) {

src/kernel/formatter.h

@@ -8,10 +8,9 @@ Author: Leonardo de Moura
 #include <memory>
 #include "util/sexpr/options.h"
 #include "kernel/context.h"
+#include "kernel/environment.h"
 
 namespace lean {
-class environment;
-class object;
 /**
    \brief API for formatting expressions, contexts and environments.
 */
@@ -34,6 +33,12 @@ public:
     virtual format operator()(object const & obj, options const & opts) = 0;
     /** \brief Format the given environment */
     virtual format operator()(environment const & env, options const & opts) = 0;
+
+    /**
+        \brief Return environment object associated with this formatter.
+        Not every formatter has an associated environment object.
+    */
+    virtual optional<environment> get_environment() { return optional<environment>(); }
 };
 /**
    \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
@@ -47,6 +52,7 @@ public:
     format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) const { return (*m_cell)(c, e, format_ctx, opts); }
     format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); }
     format operator()(environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); }
+    optional<environment> get_environment() { return m_cell->get_environment(); }
 
     template<typename FCell>
     friend formatter mk_formatter(FCell && fcell) {

src/library/kernel_bindings.cpp

@@ -815,7 +815,7 @@ DECL_UDATA(formatter)
     throw exception("invalid formatter invocation, the acceptable arguments are: (expr, options?), (context, options?), (context, expr, bool? options?), (kernel object, options?), (environment, options?)");
 }
 
-static int formatter_call(lua_State * L) {
+static int formatter_call_core(lua_State * L) {
     int nargs = lua_gettop(L);
     formatter & fmt = to_formatter(L, 1);
     options opts = get_global_options(L);
@@ -849,6 +849,17 @@ static int formatter_call(lua_State * L) {
     }
 }
 
+static int formatter_call(lua_State * L) {
+    formatter & fmt = to_formatter(L, 1);
+    optional<environment> env = fmt.get_environment();
+    if (env) {
+        read_only_environment ro_env(*env);
+        return formatter_call_core(L);
+    } else {
+        return formatter_call_core(L);
+    }
+}
+
 static const struct luaL_Reg formatter_m[] = {
     {"__gc",            formatter_gc}, // never throws
     {"__call",          safe_function<formatter_call>},