feat(api): add API (lean_exception_to_pp_string) for pretty printing exceptions

src/api/exception.cpp

@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/kernel_exception.h"
+#include "library/unifier.h"
+#include "library/tactic/tactic.h"
 #include "api/exception.h"
 #include "api/string.h"
 
@@ -49,5 +51,11 @@ lean_exception_kind lean_exception_get_kind(lean_exception e) {
         return LEAN_KERNEL_EXCEPTION;
     if (dynamic_cast<lean::interrupted*>(ex))
         return LEAN_INTERRUPTED;
+    if (dynamic_cast<lean::unifier_exception*>(ex))
+        return LEAN_UNIFIER_EXCEPTION;
+    if (dynamic_cast<lean::tactic_exception*>(ex))
+        return LEAN_TACTIC_EXCEPTION;
+    if (dynamic_cast<lean::parser_exception*>(ex))
+        return LEAN_PARSER_EXCEPTION;
     return LEAN_OTHER_EXCEPTION;
 }

src/api/exception.h

@@ -6,11 +6,12 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
+#include "util/exception.h"
+#include "library/parser_nested_exception.h"
 #include "api/lean_macros.h"
 #include "api/lean_bool.h"
 #include "api/lean_exception.h"
 #include "api/exception.h"
-#include "util/exception.h"
 
 namespace lean {
 inline throwable * to_exception(lean_exception e) { return reinterpret_cast<throwable *>(e); }
@@ -41,6 +42,9 @@ void check_nonnull(void const *);
 
 #define LEAN_TRY try {
 #define LEAN_CATCH                                      \
+} catch (lean::parser_nested_exception & e) {           \
+    *ex = of_exception(e.get_exception().clone());      \
+    return lean_false;                                  \
 } catch (lean::exception & e) {                         \
     *ex = of_exception(e.clone());                      \
     return lean_false;                                  \

src/api/ios.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/error_handling/error_handling.h"
 #include "frontends/lean/pp.h"
 #include "api/string.h"
 #include "api/exception.h"
@@ -101,3 +102,19 @@ lean_bool lean_expr_to_pp_string(lean_env env, lean_ios ios, lean_expr e, char c
     *r = mk_string(out.str());
     LEAN_CATCH;
 }
+
+lean_bool lean_exception_to_pp_string(lean_env env, lean_ios ios, lean_exception e, char const ** r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(env);
+    check_nonnull(ios);
+    check_nonnull(e);
+    io_state new_ios(to_io_state_ref(ios));
+    std::shared_ptr<output_channel> aux(new string_output_channel());
+    new_ios.set_regular_channel(aux);
+    new_ios.set_diagnostic_channel(aux);
+    io_state_stream ioss(to_env_ref(env), new_ios);
+    throwable * _e = to_exception(e);
+    display_error(ioss, nullptr, *_e);
+    *r = mk_string(static_cast<string_output_channel const *>(aux.get())->str());
+    LEAN_CATCH;
+}

src/api/lean_exception.h

@@ -29,12 +29,15 @@ void lean_exception_del(lean_exception e);
 char const * lean_exception_get_message(lean_exception e);
 
 typedef enum {
-    LEAN_NULL_EXCEPTION,   // null (aka there is no exception)
-    LEAN_SYSTEM_EXCEPTION, // exception generated by the C++ runtime
-    LEAN_OUT_OF_MEMORY,    // out of memory exception
-    LEAN_INTERRUPTED,      // execution was interrupted by user request
-    LEAN_KERNEL_EXCEPTION, // type checking error
-    LEAN_OTHER_EXCEPTION   // other (TODO) lean exceptions
+    LEAN_NULL_EXCEPTION,    // null (aka there is no exception)
+    LEAN_SYSTEM_EXCEPTION,  // exception generated by the C++ runtime
+    LEAN_OUT_OF_MEMORY,     // out of memory exception
+    LEAN_INTERRUPTED,       // execution was interrupted by user request
+    LEAN_KERNEL_EXCEPTION,  // type checking error
+    LEAN_UNIFIER_EXCEPTION, // unification exception
+    LEAN_TACTIC_EXCEPTION,  // tactic exception
+    LEAN_PARSER_EXCEPTION,  // parser exception
+    LEAN_OTHER_EXCEPTION    // other (TODO) lean exceptions
 } lean_exception_kind;
 
 /** \brief Return the kind of the given exception. */

src/api/lean_ios.h

@@ -60,6 +60,9 @@ lean_bool lean_ios_reset_diagnostic(lean_ios ios, lean_exception * ex);
 /** \brief Store in \c r a pretty printed representation of \c e */
 lean_bool lean_expr_to_pp_string(lean_env env, lean_ios ios, lean_expr e, char const ** r, lean_exception * ex);
 
+/** \brief Store in \c r a pretty printed representation of the exception \c e */
+lean_bool lean_exception_to_pp_string(lean_env env, lean_ios ios, lean_exception e, char const ** r, lean_exception * ex);
+
 /*@}*/
 /*@}*/
 

src/tests/shared/env.c

@@ -511,6 +511,31 @@ void test_parser() {
     lean_ios_del(new_ios);
 }
 
+void test_parser_error() {
+    lean_exception ex = 0;
+    lean_env env      = mk_env();
+    lean_ios ios;
+    lean_env new_env;
+    lean_ios new_ios;
+    lean_options o;
+    check(lean_options_mk_empty(&o, &ex));
+    check(lean_ios_mk_std(o, &ios, &ex));
+    check(!lean_parse_commands(env, ios, "import data.nat open nat definition double (a : nat) := a + true",
+                               &new_env, &new_ios, &ex));
+    {
+        lean_exception ex2 = 0;
+        char const * s;
+        printf("\nexception kind: %d\n", lean_exception_get_kind(ex));
+        check(lean_exception_to_pp_string(env, ios, ex, &s, &ex2));
+        printf("exception\n%s", s);
+        lean_string_del(s);
+    }
+    lean_exception_del(ex);
+    lean_env_del(env);
+    lean_ios_del(ios);
+}
+
+
 int main() {
     test_add_univ();
     test_id();
@@ -518,5 +543,6 @@ int main() {
     test_import();
     test_inductive();
     test_parser();
+    test_parser_error();
     return 0;
 }