From c46edcf370c8bf874cce5c93fb50284201ef4b6c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 Nov 2013 11:19:15 -0800
Subject: [PATCH] feat(lua): expose formatter in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/bindings/lua/CMakeLists.txt |  2 +-
 src/bindings/lua/formatter.cpp  | 99 +++++++++++++++++++++++++++++++++
 src/bindings/lua/formatter.h    | 15 +++++
 3 files changed, 115 insertions(+), 1 deletion(-)
 create mode 100644 src/bindings/lua/formatter.cpp
 create mode 100644 src/bindings/lua/formatter.h

diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt
index 1b8e99a46..301534d74 100644
--- a/src/bindings/lua/CMakeLists.txt
+++ b/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 leanlua_state.cpp)
+context.cpp object.cpp environment.cpp formatter.cpp leanlua_state.cpp)
 
 target_link_libraries(lua ${LEAN_LIBS})
diff --git a/src/bindings/lua/formatter.cpp b/src/bindings/lua/formatter.cpp
new file mode 100644
index 000000000..b3a6e6058
--- /dev/null
+++ b/src/bindings/lua/formatter.cpp
@@ -0,0 +1,99 @@
+/*
+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 <sstream>
+#include <lua.hpp>
+#include "kernel/formatter.h"
+#include "bindings/lua/util.h"
+#include "bindings/lua/options.h"
+#include "bindings/lua/format.h"
+#include "bindings/lua/expr.h"
+#include "bindings/lua/context.h"
+#include "bindings/lua/environment.h"
+#include "bindings/lua/object.h"
+
+namespace lean {
+constexpr char const * formatter_mt = "formatter.mt";
+
+bool is_formatter(lua_State * L, int idx) {
+    return testudata(L, idx, formatter_mt);
+}
+
+formatter & to_formatter(lua_State * L, int idx) {
+    return *static_cast<formatter*>(luaL_checkudata(L, idx, formatter_mt));
+}
+
+int push_formatter(lua_State * L, formatter const & o) {
+    void * mem = lua_newuserdata(L, sizeof(formatter));
+    new (mem) formatter(o);
+    luaL_getmetatable(L, formatter_mt);
+    lua_setmetatable(L, -2);
+    return 1;
+}
+
+static int formatter_gc(lua_State * L) {
+    to_formatter(L, 1).~formatter();
+    return 0;
+}
+
+[[ noreturn ]] void throw_invalid_formatter_call() {
+    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) {
+    int nargs = lua_gettop(L);
+    formatter & fmt = to_formatter(L, 1);
+    options opts;
+    if (nargs <= 3) {
+        if (nargs == 3) {
+            if (is_options(L, 3))
+                opts = to_options(L, 3);
+            else if (is_context(L, 2) && is_expr(L, 3))
+                return push_format(L, fmt(to_context(L, 2), to_expr(L, 3)));
+            else
+                throw_invalid_formatter_call();
+        }
+        if (is_expr(L, 2))  {
+            return push_format(L, fmt(to_expr(L, 2), opts));
+        } else if (is_context(L, 2)) {
+            return push_format(L, fmt(to_context(L, 2), opts));
+        } else if (is_environment(L, 2)) {
+            ro_environment env(L, 2);
+            return push_format(L, fmt(env, opts));
+        } else if (is_object(L, 2)) {
+            return push_format(L, fmt(to_object(L, 2), opts));
+        } else {
+            throw_invalid_formatter_call();
+        }
+    } else if (nargs <= 5) {
+        if (nargs == 5)
+            opts = to_options(L, 5);
+        return push_format(L, fmt(to_context(L, 2), to_expr(L, 3), lua_toboolean(L, 4), opts));
+    } else {
+        throw_invalid_formatter_call();
+    }
+}
+
+static int formatter_pred(lua_State * L) {
+    lua_pushboolean(L, is_formatter(L, 1));
+    return 1;
+}
+
+static const struct luaL_Reg formatter_m[] = {
+    {"__gc",            formatter_gc}, // never throws
+    {"__call",          safe_function<formatter_call>},
+    {0, 0}
+};
+
+void open_formatter(lua_State * L) {
+    luaL_newmetatable(L, formatter_mt);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, formatter_m, 0);
+
+    set_global_function<formatter_pred>(L, "is_formatter");
+}
+}
diff --git a/src/bindings/lua/formatter.h b/src/bindings/lua/formatter.h
new file mode 100644
index 000000000..e8b587949
--- /dev/null
+++ b/src/bindings/lua/formatter.h
@@ -0,0 +1,15 @@
+/*
+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>
+namespace lean {
+class formatter;
+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);
+}