From d31cde473eedc4a10c5e118ed22d27852a0d967d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Jul 2014 11:13:17 -0700
Subject: [PATCH] fix(util/sexpr): nested Lua objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/pp.cpp |  1 +
 src/util/lua.cpp          | 24 +++++++++++++++++++++++-
 src/util/lua.h            |  1 +
 src/util/sexpr/sexpr.cpp  |  2 +-
 4 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 444a6e15d..2434e9956 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -310,6 +310,7 @@ pretty_fn::pretty_fn(environment const & env, options const & o):
 }
 
 format pretty_fn::operator()(expr const & e) {
+    m_depth = 0; m_num_steps = 0;
     return pp_child(purify(e), 0).first;
 }
 
diff --git a/src/util/lua.cpp b/src/util/lua.cpp
index 5e16306c9..7cf05e0a4 100644
--- a/src/util/lua.cpp
+++ b/src/util/lua.cpp
@@ -81,6 +81,29 @@ int equal(lua_State * L, int idx1, int idx2) {
     #endif
 }
 
+char const * tostring(lua_State * L, int idx) {
+    if (!luaL_callmeta(L, idx, "__tostring")) {  /* no metafield? */
+        switch (lua_type(L, idx)) {
+        case LUA_TNUMBER:
+        case LUA_TSTRING:
+            lua_pushvalue(L, idx);
+            break;
+        case LUA_TBOOLEAN:
+            lua_pushstring(L, (lua_toboolean(L, idx) ? "true" : "false"));
+            break;
+        case LUA_TNIL:
+            lua_pushliteral(L, "nil");
+            break;
+        default: {
+            std::ostringstream strm;
+            strm << lua_typename(L, idx) << ": " << lua_topointer(L, idx);
+            lua_pushstring(L, strm.str().c_str());
+            break;
+        }}
+    }
+    return lua_tostring(L, -1);
+}
+
 int get_nonnil_top(lua_State * L) {
     int top = lua_gettop(L);
     while (top > 0 && lua_isnil(L, top))
@@ -181,4 +204,3 @@ void check_atleast_num_args(lua_State * L, int low) {
     if (lua_gettop(L) < low) throw exception("too few arguments to function");
 }
 }
-
diff --git a/src/util/lua.h b/src/util/lua.h
index ea23beb88..eecda7e8d 100644
--- a/src/util/lua.h
+++ b/src/util/lua.h
@@ -20,6 +20,7 @@ size_t objlen(lua_State * L, int idx);
 void dofile(lua_State * L, char const * fname);
 void dostring(lua_State * L, char const * str);
 void pcall(lua_State * L, int nargs, int nresults, int errorfun);
+char const * tostring (lua_State * L, int idx);
 /**
     \brief Return true iff coroutine is done, false if it has yielded,
     and throws an exception if error.
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index dc3ccf7db..5f150b5b3 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -441,7 +441,7 @@ public:
     virtual void display(std::ostream & out) const {
         lua_State * L = m_ref.get_state();
         m_ref.push();
-        out << lua_tostring(L, -1);
+        out << tostring(L, -1);
         lua_pop(L, 1);
     }
 };