feat(lua): use formatter available in the state object to convert Lean objects into strings in the Lua API

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

src/bindings/lua/context.cpp

@@ -6,11 +6,15 @@ Author: Leonardo de Moura
 */
 #include <sstream>
 #include <lua.hpp>
+#include "util/sexpr/options.h"
 #include "kernel/context.h"
+#include "kernel/formatter.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
+#include "bindings/lua/options.h"
 #include "bindings/lua/expr.h"
 #include "bindings/lua/context.h"
+#include "bindings/lua/formatter.h"
 
 namespace lean {
 constexpr char const * context_entry_mt = "context_entry.mt";
@@ -86,8 +90,9 @@ static int context_gc(lua_State * L) {
 
 static int context_tostring(lua_State * L) {
     std::ostringstream out;
-    // TODO(Leo): use pretty printer
-    out << to_context(L, 1);
+    formatter fmt = get_global_formatter(L);
+    options opts  = get_global_options(L);
+    out << mk_pair(fmt(to_context(L, 1), opts), opts);
     lua_pushfstring(L, out.str().c_str());
     return 1;
 }

src/bindings/lua/environment.cpp

@@ -10,11 +10,13 @@ Author: Leonardo de Moura
 #include "kernel/formatter.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
+#include "bindings/lua/options.h"
 #include "bindings/lua/level.h"
 #include "bindings/lua/expr.h"
 #include "bindings/lua/object.h"
 #include "bindings/lua/context.h"
 #include "bindings/lua/environment.h"
+#include "bindings/lua/formatter.h"
 
 namespace lean {
 constexpr char const * environment_mt = "environment.mt";
@@ -187,9 +189,9 @@ static int environment_pred(lua_State * L) {
 static int environment_tostring(lua_State * L) {
     ro_environment env(L, 1);
     std::ostringstream out;
-    // TODO(Leo): get formatter from registry
-    formatter fmt = mk_simple_formatter();
-    out << fmt(env);
+    formatter fmt = get_global_formatter(L);
+    options opts  = get_global_options(L);
+    out << mk_pair(fmt(env, opts), opts);
     lua_pushfstring(L, out.str().c_str());
     return 1;
 }

src/bindings/lua/expr.cpp

@@ -10,13 +10,17 @@ Author: Leonardo de Moura
 #include "util/debug.h"
 #include "util/name.h"
 #include "util/buffer.h"
+#include "util/sexpr/options.h"
 #include "kernel/expr.h"
 #include "kernel/abstract.h"
+#include "kernel/formatter.h"
 #include "library/expr_lt.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
+#include "bindings/lua/options.h"
 #include "bindings/lua/level.h"
 #include "bindings/lua/local_context.h"
+#include "bindings/lua/formatter.h"
 
 namespace lean {
 constexpr char const * expr_mt = "expr.mt";
@@ -53,8 +57,9 @@ static int expr_tostring(lua_State * L) {
     std::ostringstream out;
     expr & e = to_expr(L, 1);
     if (e) {
-        // TODO(Leo): use pretty printer
-        out << to_expr(L, 1);
+        formatter fmt = get_global_formatter(L);
+        options opts  = get_global_options(L);
+        out << mk_pair(fmt(to_expr(L, 1), opts), opts);
     } else {
         out << "<null-expr>";
     }

src/bindings/lua/format.cpp

@@ -9,10 +9,12 @@ Author: Leonardo de Moura
 #include <cstring>
 #include "util/debug.h"
 #include "util/sstream.h"
+#include "util/sexpr/options.h"
 #include "util/sexpr/format.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
 #include "bindings/lua/numerics.h"
+#include "bindings/lua/options.h"
 
 namespace lean {
 constexpr char const * format_mt = "format.mt";
@@ -55,7 +57,7 @@ static int format_gc(lua_State * L) {
 
 static int format_tostring(lua_State * L) {
     std::ostringstream out;
-    out << to_format(L, 1);
+    out << mk_pair(to_format(L, 1), get_global_options(L));
     lua_pushfstring(L, out.str().c_str());
     return 1;
 }

src/bindings/lua/formatter.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/context.h"
 #include "bindings/lua/environment.h"
 #include "bindings/lua/object.h"
+#include "bindings/lua/state.h"
 
 namespace lean {
 constexpr char const * formatter_mt = "formatter.mt";
@@ -88,6 +89,38 @@ static const struct luaL_Reg formatter_m[] = {
     {0, 0}
 };
 
+static char g_formatter_key;
+static formatter g_simple_formatter = mk_simple_formatter();
+
+formatter get_global_formatter(lua_State * L) {
+    state * S = get_state(L);
+    if (S != nullptr) {
+        return S->get_formatter();
+    } else {
+        lua_pushlightuserdata(L, static_cast<void *>(&g_formatter_key));
+        lua_gettable(L, LUA_REGISTRYINDEX);
+        if (is_formatter(L, -1)) {
+            formatter r = to_formatter(L, -1);
+            lua_pop(L, 1);
+            return r;
+        } else {
+            lua_pop(L, 1);
+            return g_simple_formatter;
+        }
+    }
+}
+
+void set_global_formatter(lua_State * L, formatter const & fmt) {
+    state * S = get_state(L);
+    if (S != nullptr) {
+        S->set_formatter(fmt);
+    } else {
+        lua_pushlightuserdata(L, static_cast<void *>(&g_formatter_key));
+        push_formatter(L, fmt);
+        lua_settable(L, LUA_REGISTRYINDEX);
+    }
+}
+
 void open_formatter(lua_State * L) {
     luaL_newmetatable(L, formatter_mt);
     lua_pushvalue(L, -1);

src/bindings/lua/formatter.h

@@ -12,4 +12,17 @@ void open_formatter(lua_State * L);
 bool is_formatter(lua_State * L, int idx);
 formatter & to_formatter(lua_State * L, int idx);
 int push_formatter(lua_State * L, formatter const & o);
+/**
+   \brief Return the formatter object 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
+*/
+formatter get_global_formatter(lua_State * L);
+/**
+   \brief Update the formatter object associated with the given Lua State.
+   If \c L is associated with a Lean state object \c S, then we update the formatter of \c S.
+   Otherwise, we update the registry of \c L.
+*/
+void set_global_formatter(lua_State * L, formatter const & fmt);
 }

src/bindings/lua/leanlua_state.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "util/memory.h"
 #include "util/buffer.h"
+#include "library/state.h"
 #include "bindings/lua/leanlua_state.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
@@ -203,7 +204,7 @@ static std::mutex g_print_mutex;
 
 /** \brief Thread safe version of print function */
 static int print(lua_State * L) {
-    // TODO(Leo): use output channels (if available) instead of std::cout
+    state * S = get_state(L);
     int n = lua_gettop(L);
     int i;
     lua_getglobal(L, "tostring");
@@ -218,11 +219,20 @@ static int print(lua_State * L) {
         if (s == NULL)
             throw exception("'to_string' must return a string to 'print'");
         if (i > 1) {
+            if (S)
+                regular(*S) << "\t";
+            else
                 std::cout << "\t";
         }
+        if (S)
+            regular(*S) << s;
+        else
             std::cout << s;
         lua_pop(L, 1);
     }
+    if (S)
+        regular(*S) << endl;
+    else
         std::cout << std::endl;
     return 0;
 }

src/bindings/lua/level.cpp

@@ -7,9 +7,11 @@ Author: Leonardo de Moura
 #include <sstream>
 #include <lua.hpp>
 #include "util/buffer.h"
+#include "util/sexpr/options.h"
 #include "kernel/level.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
+#include "bindings/lua/options.h"
 
 namespace lean {
 constexpr char const * level_mt = "level.mt";
@@ -37,8 +39,8 @@ static int level_gc(lua_State * L) {
 
 static int level_tostring(lua_State * L) {
     std::ostringstream out;
-    // TODO(Leo): use pretty printer
-    out << to_level(L, 1);
+    options opts  = get_global_options(L);
+    out << mk_pair(pp(to_level(L, 1), opts), opts);
     lua_pushfstring(L, out.str().c_str());
     return 1;
 }

src/bindings/lua/object.cpp

@@ -6,11 +6,15 @@ Author: Leonardo de Moura
 */
 #include <sstream>
 #include <lua.hpp>
+#include "util/sexpr/options.h"
 #include "kernel/object.h"
+#include "kernel/formatter.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
+#include "bindings/lua/options.h"
 #include "bindings/lua/level.h"
 #include "bindings/lua/expr.h"
+#include "bindings/lua/formatter.h"
 
 namespace lean {
 constexpr char const * object_mt = "object.mt";
@@ -144,8 +148,22 @@ static int object_pred(lua_State * L) {
     return 1;
 }
 
+static int object_tostring(lua_State * L) {
+    std::ostringstream out;
+    formatter fmt = get_global_formatter(L);
+    options opts  = get_global_options(L);
+    object & obj  = to_object(L, 1);
+    if (obj)
+        out << mk_pair(fmt(to_object(L, 1), opts), opts);
+    else
+        out << "<null-kernel-object>";
+    lua_pushfstring(L, out.str().c_str());
+    return 1;
+}
+
 static const struct luaL_Reg object_m[] = {
     {"__gc",            object_gc}, // never throws
+    {"__tostring",      safe_function<object_tostring>},
     {"is_null",         safe_function<object_is_null>},
     {"keyword",         safe_function<object_keyword>},
     {"has_name",        safe_function<object_has_name>},

src/bindings/lua/options.cpp

@@ -182,7 +182,7 @@ options get_global_options(lua_State * L) {
         lua_pushlightuserdata(L, static_cast<void *>(&g_options_key));
         lua_gettable(L, LUA_REGISTRYINDEX);
         options r;
-        if (!is_options(L, -1))
+        if (is_options(L, -1))
             r = to_options(L, -1);
         lua_pop(L, 1);
         return r;

tests/lean/lua4.lean.expected.out

@@ -1,5 +1,5 @@
   Set: pp::colors
   Set: pp::unicode
   Assumed: x
-type of x is Int
+type of x is ℤ
 x + y : ℤ

tests/lean/lua7.lean

@@ -0,0 +1,6 @@
+(**
+x = Const("x")
+y = Const("y")
+N = Const("N")
+print(fun({{x, N}, {y, N}}, x))
+**)

tests/lean/lua7.lean.expected.out

@@ -0,0 +1,3 @@
+  Set: pp::colors
+  Set: pp::unicode
+λ x y : N, x

tests/lean/lua8.lean

@@ -0,0 +1,13 @@
+Variable x : Int
+
+(**
+ty_x = env():check_type(Const("x"))
+c = context()
+c = context(c, "x", ty_x)
+c = context(c, "y", ty_x)
+print(c)
+o = env():find_object("x")
+print(o)
+o = env():find_object("y")
+print(o)
+**)

tests/lean/lua8.lean.expected.out

@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: x
+x : ℤ,
+y : ℤ
+Variable x : ℤ
+<null-kernel-object>

tests/lua/env3.lua

@@ -0,0 +1,4 @@
+env = environment()
+env:add_var("N", Type())
+env:add_var("x", Const("N"))
+print(env)