refactor(library/exception): avoid throw_generic_exception functions

src/api/exception.cpp

@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/unifier.h"
 #include "library/print.h"
-// #include "library/tactic/tactic.h"
 #include "library/error_handling.h"
 #include "api/exception.h"
 #include "api/string.h"

src/api/exception.h

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include "util/exception.h"
-#include "library/parser_nested_exception.h"
+#include "library/exception.h"
 #include "api/lean_macros.h"
 #include "api/lean_bool.h"
 #include "api/lean_exception.h"

src/frontends/lean/old_elaborator_exception.cpp

@@ -9,19 +9,15 @@ Author: Leonardo de Moura
 
 namespace lean {
 [[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m) {
-    throw_generic_exception(msg, m);
+    throw generic_exception(m, msg);
 }
 
 [[ noreturn ]] void throw_elaborator_exception(sstream const & strm, expr const & m) {
-    throw_generic_exception(strm, m);
-}
-
-[[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m, pp_fn const & fn) {
-    throw_generic_exception(msg, m, fn);
+    throw generic_exception(m, strm);
 }
 
 [[ noreturn ]] void throw_elaborator_exception(expr const & m, pp_fn const & fn) {
-    throw_generic_exception(m, fn);
+    throw generic_exception(m, fn);
 }
 
 [[ noreturn ]] void throw_elaborator_exception(expr const & m, format const & msg) {

src/frontends/lean/old_elaborator_exception.h

@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 namespace lean {
 [[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m);
 [[ noreturn ]] void throw_elaborator_exception(sstream const & strm, expr const & m);
-[[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m, pp_fn const & fn);
 [[ noreturn ]] void throw_elaborator_exception(expr const & m, format const & msg);
 [[ noreturn ]] void throw_elaborator_exception(expr const & m, pp_fn const & fn);
 }

src/frontends/lean/parser.cpp

@@ -700,7 +700,7 @@ environment parser::add_local_ref(environment const & env, name const & n, expr
 static void check_no_metavars(name const & n, expr const & e) {
     lean_assert(is_local(e));
     if (has_metavar(e)) {
-        throw_generic_exception(none_expr(), [=](formatter const & fmt) {
+        throw generic_exception(none_expr(), [=](formatter const & fmt) {
                 format r("failed to add declaration '");
                 r += format(n);
                 r += format("' to local context, type has metavariables");

src/frontends/lean/structure_cmd.cpp

@@ -376,7 +376,7 @@ struct structure_cmd_fn {
                     return optional<unsigned>(i);
                 } else {
                     expr prev_ftype = mlocal_type(m_fields[i]);
-                    throw_generic_exception(parent, [=](formatter const & fmt) {
+                    throw generic_exception(parent, [=](formatter const & fmt) {
                             format r = format("invalid 'structure' header, field '");
                             r += format(fname);
                             r += format("' from '");

src/library/class_instance_resolution.cpp

@@ -28,8 +28,8 @@ Author: Leonardo de Moura
 #include "library/scope_pos_info_provider.h"
 
 namespace lean {
-[[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
-[[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); }
+[[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw generic_exception(m, msg); }
+[[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw generic_exception(m, fn); }
 
 static name * g_class_force_new              = nullptr;
 

src/library/equations_compiler/elim_match.cpp

@@ -97,11 +97,11 @@ struct elim_match_fn {
     };
 
     [[ noreturn ]] void throw_error(char const * msg) {
-        throw_generic_exception(msg, m_ref);
+        throw generic_exception(m_ref, msg);
     }
 
     [[ noreturn ]] void throw_error(sstream const & strm) {
-        throw_generic_exception(strm, m_ref);
+        throw generic_exception(m_ref, strm);
     }
 
     local_context get_local_context(expr const & mvar) {

src/library/equations_compiler/old_compiler.cpp

@@ -82,11 +82,11 @@ class equation_compiler_fn {
         return ::lean::to_telescope(m_tc, e, tele, optional<binder_info>());
     }
 
-    [[ noreturn ]] static void throw_error(char const * msg, expr const & src) { throw_generic_exception(msg, src); }
-    [[ noreturn ]] static void throw_error(sstream const & ss, expr const & src) { throw_generic_exception(ss, src); }
-    [[ noreturn ]] static void throw_error(expr const & src, pp_fn const & fn) { throw_generic_exception(src, fn); }
-    [[ noreturn ]] void throw_error(sstream const & ss) const { throw_generic_exception(ss, m_meta); }
-    [[ noreturn ]] void throw_error(expr const & src, sstream const & ss) const { throw_generic_exception(ss, src); }
+    [[ noreturn ]] static void throw_error(char const * msg, expr const & src) { throw generic_exception(src, msg); }
+    [[ noreturn ]] static void throw_error(sstream const & ss, expr const & src) { throw generic_exception(src, ss); }
+    [[ noreturn ]] static void throw_error(expr const & src, pp_fn const & fn) { throw generic_exception(src, fn); }
+    [[ noreturn ]] void throw_error(sstream const & ss) const { throw generic_exception(m_meta, ss); }
+    [[ noreturn ]] void throw_error(expr const & src, sstream const & ss) const { throw generic_exception(src, ss); }
 
     void check_limitations(expr const & eqns) const {
         if (is_wf_equations(eqns) && equations_num_fns(eqns) != 1)

src/library/equations_compiler/structural_rec.cpp

@@ -45,11 +45,11 @@ struct structural_rec_fn {
     }
 
     [[ noreturn ]] void throw_error(char const * msg) {
-        throw_generic_exception(msg, m_ref);
+        throw generic_exception(m_ref, msg);
     }
 
     [[ noreturn ]] void throw_error(sstream const & strm) {
-        throw_generic_exception(strm, m_ref);
+        throw generic_exception(m_ref, strm);
     }
 
     type_context mk_type_context() {

src/library/exception.cpp

@@ -8,37 +8,11 @@ Author: Leonardo de Moura
 #include "library/exception.h"
 
 namespace lean {
-
-[[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m) {
+static pp_fn mk_pp_fn(char const * msg) {
     std::string msg_str = msg;
-    throw generic_exception(msg, m, [=](formatter const &) { return format(msg_str); });
+    return [=](formatter const &) { return format(msg_str); }; // NOLINT
 }
 
-[[ noreturn ]] void throw_generic_exception(sstream const & strm, optional<expr> const & m) {
-    throw_generic_exception(strm.str().c_str(), m);
-}
-
-[[ noreturn ]] void throw_generic_exception(char const * msg, expr const & m) {
-    throw_generic_exception(msg, some_expr(m));
-}
-
-[[ noreturn ]] void throw_generic_exception(sstream const & strm, expr const & m) {
-    throw_generic_exception(strm, some_expr(m));
-}
-
-[[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn) {
-    throw generic_exception(msg, m, fn);
-}
-
-[[ noreturn ]] void throw_generic_exception(char const * msg, expr const & m, pp_fn const & fn) {
-    throw_generic_exception(msg, some_expr(m), fn);
-}
-
-[[ noreturn ]] void throw_generic_exception(optional<expr> const & m, pp_fn const & fn) {
-    throw generic_exception(m, fn);
-}
-
-[[ noreturn ]] void throw_generic_exception(expr const & m, pp_fn const & fn) {
-    throw_generic_exception(some_expr(m), fn);
-}
+generic_exception::generic_exception(optional<expr> const & m, char const * msg):
+    generic_exception(msg, m, mk_pp_fn(msg)) {}
 }

src/library/exception.h

@@ -20,6 +20,14 @@ public:
         ext_exception(msg), m_main_expr(m), m_pp_fn(fn) {}
     generic_exception(optional<expr> const & m, pp_fn const & fn):
         ext_exception(), m_main_expr(m), m_pp_fn(fn) {}
+    generic_exception(optional<expr> const & m, char const * msg);
+    generic_exception(optional<expr> const & m, sstream const & strm):generic_exception(m, strm.str().c_str()) {}
+    explicit generic_exception(char const * msg):generic_exception(none_expr(), msg) {}
+    explicit generic_exception(sstream const & strm):generic_exception(none_expr(), strm) {}
+    generic_exception(expr const & m, char const * msg):generic_exception(some_expr(m), msg) {}
+    generic_exception(expr const & m, sstream const & strm):generic_exception(some_expr(m), strm) {}
+    generic_exception(expr const & m, pp_fn const & fn):generic_exception(some_expr(m), fn) {}
+
     virtual ~generic_exception() noexcept {}
     virtual optional<expr> get_main_expr() const override { return m_main_expr; }
     virtual format pp(formatter const & fmt) const override { return m_pp_fn(fmt); }
@@ -27,15 +35,6 @@ public:
     virtual void rethrow() const override { throw *this; }
 };
 
-[[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m);
-[[ noreturn ]] void throw_generic_exception(sstream const & strm, optional<expr> const & m);
-[[ noreturn ]] void throw_generic_exception(char const * msg, expr const & m);
-[[ noreturn ]] void throw_generic_exception(sstream const & strm, expr const & m);
-[[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn);
-[[ noreturn ]] void throw_generic_exception(char const * msg, expr const & m, pp_fn const & fn);
-[[ noreturn ]] void throw_generic_exception(optional<expr> const & m, pp_fn const & fn);
-[[ noreturn ]] void throw_generic_exception(expr const & m, pp_fn const & fn);
-
 /** \brief Lean exception occurred when parsing file. */
 class parser_nested_exception : public exception {
     std::shared_ptr<throwable>          m_exception;

src/library/old_type_context.cpp

@@ -1534,7 +1534,7 @@ bool old_type_context::update_options(options const & opts) {
     return r;
 }
 
-[[ noreturn ]] static void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
+[[ noreturn ]] static void throw_class_exception(char const * msg, expr const & m) { throw generic_exception(m, msg); }
 
 void old_type_context::trace(unsigned depth, expr const & mvar, expr const & mvar_type, expr const & r) {
     auto out = tout();

src/library/type_context.cpp

@@ -2403,7 +2403,7 @@ optional<name> type_context::is_class(expr const & type) {
     return is_full_class(type);
 }
 
-[[ noreturn ]] static void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
+[[ noreturn ]] static void throw_class_exception(expr const & m, char const * msg) { throw generic_exception(m, msg); }
 
 struct instance_synthesizer {
     struct stack_entry {
@@ -2552,11 +2552,11 @@ struct instance_synthesizer {
     bool mk_choice_point(expr const & mvar) {
         lean_assert(is_metavar(mvar));
         if (m_choices.size() > m_ctx.m_cache->m_ci_max_depth) {
-            throw_class_exception("maximum class-instance resolution depth has been reached "
+            throw_class_exception(m_ctx.infer(m_main_mvar),
+                                  "maximum class-instance resolution depth has been reached "
                                   "(the limit can be increased by setting option 'class.instance_max_depth') "
                                   "(the class-instance resolution trace can be visualized "
-                                  "by setting option 'trace.class_instances')",
-                                  m_ctx.infer(m_main_mvar));
+                                  "by setting option 'trace.class_instances')");
         }
         // Remark: we initially tried to reject branches where mvar_type contained unassigned metavariables.
         // The idea was to make the procedure easier to understand.

src/library/unfold_macros.cpp

@@ -38,7 +38,7 @@ class unfold_untrusted_macros_fn {
             if (optional<expr> new_r = m_tc.expand_macro(r)) {
                 return *new_r;
             } else {
-                throw_generic_exception("failed to expand macro", e);
+                throw generic_exception(e, "failed to expand macro");
             }
         } else {
             return r;