From 590b14570f0300a0663425d818f03ac5446a142f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 16 Nov 2013 18:21:42 -0800
Subject: [PATCH] feat(lua): improve error handling in Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/bindings/lua/justification.cpp            |  2 +-
 src/bindings/lua/util.cpp                     | 16 ++++++++++++++++
 src/library/elaborator/elaborator_exception.h |  2 --
 tests/lean/lua15.lean                         | 14 ++++++++++++++
 tests/lean/lua15.lean.expected.out            |  7 +++++++
 5 files changed, 38 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/lua15.lean
 create mode 100644 tests/lean/lua15.lean.expected.out

diff --git a/src/bindings/lua/justification.cpp b/src/bindings/lua/justification.cpp
index 14a16e222..341a2ef2a 100644
--- a/src/bindings/lua/justification.cpp
+++ b/src/bindings/lua/justification.cpp
@@ -22,7 +22,7 @@ static int justification_tostring(lua_State * L) {
     if (jst) {
         formatter fmt  = get_global_formatter(L);
         options   opts = get_global_options(L);
-        out << mk_pair(jst.pp(fmt, opts, nullptr, false), opts);
+        out << mk_pair(jst.pp(fmt, opts), opts);
     } else {
         out << "<null-justification>";
     }
diff --git a/src/bindings/lua/util.cpp b/src/bindings/lua/util.cpp
index 065675c57..0ca49e87c 100644
--- a/src/bindings/lua/util.cpp
+++ b/src/bindings/lua/util.cpp
@@ -6,8 +6,15 @@ Author: Leonardo de Moura
 */
 #include <lua.hpp>
 #include <string>
+#include <sstream>
+#include "kernel/kernel_exception.h"
+#include "library/elaborator/elaborator_exception.h"
 #include "bindings/lua/util.h"
 #include "bindings/lua/lua_exception.h"
+#include "bindings/lua/options.h"
+#include "bindings/lua/format.h"
+#include "bindings/lua/formatter.h"
+#include "bindings/lua/justification.h"
 
 namespace lean {
 /**
@@ -103,6 +110,15 @@ int safe_function_wrapper(lua_State * L, lua_CFunction f){
     char const * error_msg;
     try {
         return f(L);
+    } catch (kernel_exception & e) {
+        std::ostringstream out;
+        options o = get_global_options(L);
+        out << mk_pair(e.pp(get_global_formatter(L), o), o);
+        _error_msg = out.str();
+        error_msg  = _error_msg.c_str();
+    } catch (elaborator_exception & e) {
+        push_justification(L, e.get_justification());
+        lua_error(L);
     } catch (exception & e) {
         _error_msg = e.what();
         error_msg  = _error_msg.c_str();
diff --git a/src/library/elaborator/elaborator_exception.h b/src/library/elaborator/elaborator_exception.h
index 7c4bce966..1a8f244a4 100644
--- a/src/library/elaborator/elaborator_exception.h
+++ b/src/library/elaborator/elaborator_exception.h
@@ -21,6 +21,4 @@ public:
     virtual char const * what() const noexcept { return "elaborator exception"; }
     justification const & get_justification() const { return m_justification; }
 };
-
-
 }
diff --git a/tests/lean/lua15.lean b/tests/lean/lua15.lean
new file mode 100644
index 000000000..92f7b5d12
--- /dev/null
+++ b/tests/lean/lua15.lean
@@ -0,0 +1,14 @@
+Variables i j : Int
+Variable p : Bool
+
+(**
+ local env = get_environment()
+ ok, jst = pcall(
+    function()
+       print(parse_lean("i + p"))
+ end)
+ assert(not ok)
+ assert(is_justification(jst))
+ assert(not jst:is_null())
+ print(jst:pp{display_children = false})
+**)
diff --git a/tests/lean/lua15.lean.expected.out b/tests/lean/lua15.lean.expected.out
new file mode 100644
index 000000000..3b5aff40d
--- /dev/null
+++ b/tests/lean/lua15.lean.expected.out
@@ -0,0 +1,7 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: i
+  Assumed: j
+  Assumed: p
+Failed to solve
+ ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) ⊕ (?M::0 ≈ Real::add)