From e90585737fcfbf307effa7b6d76159423b8ed5bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Jun 2018 14:57:32 -0700 Subject: [PATCH] refactor(*): use C++11 `std::current_exception` and `std::rethrow_exception` With these new C++11 APIs, we can delete the `clone` and `rethrow` methods from our exception classes. --- src/frontends/lean/definition_cmds.cpp | 2 +- src/frontends/lean/elaborator.cpp | 26 +++++----- src/frontends/lean/info_manager.cpp | 2 +- src/frontends/lean/match_expr.cpp | 2 +- src/kernel/ext_exception.h | 2 - src/kernel/kernel_exception.cpp | 2 - src/kernel/kernel_exception.h | 4 -- src/library/abstract_parser.h | 2 - src/library/constructions/injective.cpp | 2 +- src/library/equations_compiler/elim_match.cpp | 2 +- .../equations_compiler/unbounded_rec.cpp | 2 +- src/library/equations_compiler/util.cpp | 10 ++-- src/library/equations_compiler/wf_rec.cpp | 6 +-- src/library/exception.cpp | 26 +++++----- src/library/exception.h | 50 +++++++++---------- src/library/inductive_compiler/mutual.cpp | 2 +- src/library/inductive_compiler/nested.cpp | 4 +- src/library/io_state.h | 2 - src/library/tactic/app_builder_tactics.cpp | 6 +-- src/library/tactic/apply_tactic.cpp | 2 +- src/library/tactic/cases_tactic.cpp | 6 +-- src/library/tactic/change_tactic.cpp | 2 +- src/library/tactic/clear_tactic.cpp | 2 +- src/library/tactic/destruct_tactic.cpp | 2 +- src/library/tactic/dsimplify.cpp | 4 +- src/library/tactic/elaborate.cpp | 4 +- src/library/tactic/elaborator_exception.cpp | 28 ++++++----- src/library/tactic/elaborator_exception.h | 27 +++++----- src/library/tactic/eval.cpp | 4 +- src/library/tactic/exact_tactic.cpp | 2 +- src/library/tactic/generalize_tactic.cpp | 2 +- src/library/tactic/induction_tactic.cpp | 4 +- src/library/tactic/kabstract.cpp | 4 +- src/library/tactic/revert_tactic.cpp | 2 +- src/library/tactic/rewrite_tactic.cpp | 2 +- src/library/tactic/simplify.cpp | 4 +- src/library/tactic/subst_tactic.cpp | 2 +- src/library/tactic/tactic_state.cpp | 38 +++++++------- src/library/tactic/tactic_state.h | 2 +- src/library/tactic/unfold_tactic.cpp | 6 +-- src/library/vm/interaction_state.h | 2 +- src/library/vm/interaction_state_imp.h | 10 ++-- src/library/vm/vm_environment.cpp | 6 +-- src/library/vm/vm_exceptional.cpp | 36 +++++++------ src/library/vm/vm_exceptional.h | 4 +- src/library/vm/vm_parser.cpp | 4 +- src/runtime/debug.h | 2 - src/runtime/exception.h | 10 ---- src/util/parser_exception.h | 2 - src/util/worker_queue.h | 12 ++--- 50 files changed, 185 insertions(+), 206 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 48f9a7df65..10f6972db4 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -192,7 +192,7 @@ static certified_declaration check(parser & p, environment const & env, name con msg += line() + format("elaborated value:"); msg += nest(i, line() + pp_fn(d.get_value())); } - throw nested_exception(msg, ex); + throw nested_exception(msg, std::current_exception()); } } diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 50962395cd..88c5941cb4 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1164,7 +1164,8 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< return r; } catch (elaborator_exception & ex) { // TODO(gabriel): the additional information is not added in error-recovery mode - throw nested_elaborator_exception(ref, ex, format("the inferred motive for the eliminator-like application is") + + throw nested_elaborator_exception(ref, std::current_exception(), + format("the inferred motive for the eliminator-like application is") + pp_indent(motive)); } } @@ -1669,7 +1670,7 @@ expr elaborator::visit_base_app_core(expr const & fn, arg_mask amask, buffer const & fns, bu msg += pp_indent(pp_fn, expected_type); msg += line() + format("this can happen because, for example, coercions were not considered in the process"); msg += line() + mk_no_overload_applicable_msg(fns, error_msgs); - throw nested_elaborator_exception(ref, ex, msg); + throw nested_elaborator_exception(ref, std::current_exception(), msg); } } @@ -1820,7 +1821,7 @@ expr elaborator::visit_overloaded_app_with_expected(buffer const & fns, bu msg += line() + error_msg.pp(); } - throw nested_elaborator_exception(ref, ex, msg); + throw nested_elaborator_exception(ref, std::current_exception(), msg); } } @@ -1837,7 +1838,7 @@ expr elaborator::visit_overloaded_app_with_expected(buffer const & fns, bu msg += line() + format("the following overloaded terms were applicable"); for (auto const & c : candidates) msg += pp_indent(pp_fn, std::get<0>(c)); - throw nested_elaborator_exception(ref, ex, msg); + throw nested_elaborator_exception(ref, std::current_exception(), msg); } } @@ -1854,7 +1855,7 @@ expr elaborator::visit_overloaded_app(buffer const & fns, buffer con } catch (elaborator_exception & ex) { format msg = format("switched to basic overload resolution where arguments are elaborated without " "any information about the expected type because expected type was not available"); - throw nested_elaborator_exception(ref, ex, msg); + throw nested_elaborator_exception(ref, std::current_exception(), msg); } } } @@ -1990,7 +1991,7 @@ expr elaborator::visit_app_core(expr fn, buffer const & args, optionalm_nexplicit) + format(" explicit arguments expected")); @@ -2003,7 +2004,7 @@ expr elaborator::visit_app_core(expr fn, buffer const & args, optional const & expected_ty throw nested_exception("invalid match/convoy expression, " "user did not provide type for the expression, " "lean tried to infer one using expected type information, " - "but result is not type correct", ex); + "but result is not type correct", std::current_exception()); } } else { // User provided some typing information for the match @@ -2836,10 +2837,11 @@ elaborator::field_resolution elaborator::find_field_fn(expr const & e, expr cons new_s_type = m_ctx.whnf_head_pred(new_s_type, [](expr const &) { return false; }); if (new_s_type == s_type) throw; + std::exception_ptr ex1_ptr = std::current_exception(); try { return find_field_fn(e, s, new_s_type); } catch (elaborator_exception & ex2) { - throw nested_elaborator_exception(ex2.get_pos(), ex1, ex2.pp()); + throw nested_elaborator_exception(ex2.get_pos(), ex1_ptr, ex2.pp()); } } } @@ -4214,7 +4216,7 @@ vm_obj tactic_resolve_local_name(vm_obj const & vm_id, vm_obj const & vm_s) { bool ignore_aliases = false; return tactic::mk_success(to_obj(resolve_local_name(s.env(), g->get_context(), id, src, ignore_aliases, names())), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -4320,7 +4322,7 @@ static vm_obj tactic_save_type_info(vm_obj const &, vm_obj const & _e, vm_obj co else if (is_local(e)) get_global_info_manager()->add_identifier_info(*pos, mlocal_pp_name(e)); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } return tactic::mk_success(s); } diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 7440a50038..278b8e4708 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -203,7 +203,7 @@ vm_obj tactic_save_info_thunk(vm_obj const & pos, vm_obj const & thunk, vm_obj c } return tactic::mk_success(tactic::to_state(s)); } catch (exception & ex) { - return tactic::mk_exception(ex, tactic::to_state(s)); + return tactic::mk_exception(std::current_exception(), tactic::to_state(s)); } } diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp index 201176a3c2..72c6b2de28 100644 --- a/src/frontends/lean/match_expr.cpp +++ b/src/frontends/lean/match_expr.cpp @@ -79,7 +79,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) { } } catch (exception & ex) { consume_until_end_or_command(p); - ex.rethrow(); + throw; } expr f = p.save_pos(mk_equations(header, eqns.size(), eqns.data()), pos); return p.mk_app(f, ts, pos); diff --git a/src/kernel/ext_exception.h b/src/kernel/ext_exception.h index eac4fb4284..235b0fefdb 100644 --- a/src/kernel/ext_exception.h +++ b/src/kernel/ext_exception.h @@ -21,7 +21,5 @@ public: virtual ~ext_exception() noexcept {} virtual optional get_pos() const override { return {}; } virtual format pp(formatter const &) const { return format(what()); } - virtual throwable * clone() const override { return new ext_exception(m_msg.c_str()); } - virtual void rethrow() const override { throw *this; } }; } diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp index 3b2ffd1e7c..304c9eeeb7 100644 --- a/src/kernel/kernel_exception.cpp +++ b/src/kernel/kernel_exception.cpp @@ -30,8 +30,6 @@ public: virtual ~generic_kernel_exception() noexcept {} virtual optional get_pos() const override { return m_pos; } virtual format pp(formatter const & fmt) const override { return m_pp_fn(fmt); } - virtual throwable * clone() const override { return new generic_kernel_exception(m_env, m_msg.c_str(), m_pos, m_pp_fn); } - virtual void rethrow() const override { throw *this; } }; [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional const & m) { diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 9d1379004b..1abefdfa2f 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -21,8 +21,6 @@ public: kernel_exception(environment const & env, sstream const & strm):ext_exception(strm), m_env(env) {} environment const & get_environment() const { return m_env; } virtual format pp(formatter const & fmt) const override; - virtual throwable * clone() const override { return new kernel_exception(m_env, m_msg.c_str()); } - virtual void rethrow() const override { throw *this; } }; class definition_type_mismatch_exception : public kernel_exception { @@ -34,8 +32,6 @@ public: expr const & get_given_type() const { return m_given_type; } virtual optional get_pos() const override { return get_pos_info(m_decl.get_value()); } virtual format pp(formatter const & fmt) const override; - virtual throwable * clone() const override { return new definition_type_mismatch_exception(m_env, m_decl, m_given_type); } - virtual void rethrow() const override { throw *this; } }; [[ noreturn ]] void throw_kernel_exception(environment const & env, char const * msg, optional const & m = none_expr()); diff --git a/src/library/abstract_parser.h b/src/library/abstract_parser.h index 93d301f48a..2d764445be 100644 --- a/src/library/abstract_parser.h +++ b/src/library/abstract_parser.h @@ -18,8 +18,6 @@ struct parser_error : public exception_with_pos { parser_error(sstream const & msg, pos_info const & p):exception_with_pos(msg), m_pos(p) {} virtual optional get_pos() const override { return some(m_pos); } std::string const & get_msg() const { return m_msg; } - virtual throwable * clone() const override { return new parser_error(m_msg.c_str(), m_pos); } - virtual void rethrow() const override { throw *this; } }; /** \brief Base class for frontend parsers with basic functions */ diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp index f67c269692..9f85d5f586 100644 --- a/src/library/constructions/injective.cpp +++ b/src/library/constructions/injective.cpp @@ -258,7 +258,7 @@ expr prove_injective_eq(environment const & env, expr const & inj_eq_type, name return mctx.instantiate_mvars(new_s->main()); } } catch (exception & ex) { - throw nested_exception(sstream() << "failed to generate auxiliary lemma '" << inj_eq_name << "'", ex); + throw nested_exception(sstream() << "failed to generate auxiliary lemma '" << inj_eq_name << "'", std::current_exception()); } throw exception(sstream() << "failed to generate auxiliary lemma '" << inj_eq_name << "'"); } diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 433615e3d3..7a4e6cb122 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -779,7 +779,7 @@ struct elim_match_fn { lean_assert(length(new_goals) == length(slist)); } catch (exception & ex) { throw nested_exception("equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' " - "for additional details)", ex); + "for additional details)", std::current_exception()); } if (empty(new_goals)) { return some(list()); diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp index 069989a528..9e9f25d898 100644 --- a/src/library/equations_compiler/unbounded_rec.cpp +++ b/src/library/equations_compiler/unbounded_rec.cpp @@ -196,7 +196,7 @@ eqn_compiler_result unbounded_rec(environment & env, elaborator & elab, ss << "equation compiler failed to generate bytecode for"; for (name const & n : header.m_fn_names) ss << " '" << n << "'"; - throw nested_exception(ss, ex); + throw nested_exception(ss, std::current_exception()); } return { to_list(result_fns), to_list(counter_examples) }; diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 69b258c430..7a2a1af830 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -261,7 +261,7 @@ local_context erase_inaccessible_annotations(local_context const & lctx) { return r; } -static void throw_mk_aux_definition_error(local_context const & lctx, name const & c, expr const & type, expr const & value, exception & ex) { +static void throw_mk_aux_definition_error(local_context const & lctx, name const & c, expr const & type, expr const & value, std::exception_ptr const & ex) { sstream strm; strm << "equation compiler failed to create auxiliary declaration '" << c << "'"; if (contains_let_local_decl(lctx, type) || contains_let_local_decl(lctx, value)) { @@ -277,7 +277,7 @@ void compile_aux_definition(environment & env, equations_header const & header, } catch (exception & ex) { if (!header.m_prev_errors) { throw nested_exception(sstream() << "equation compiler failed to generate bytecode for " - << "auxiliary declaration '" << user_name << "'", ex); + << "auxiliary declaration '" << user_name << "'", std::current_exception()); } } } @@ -305,7 +305,7 @@ pair mk_aux_definition(environment const & env, options const mk_aux_lemma(new_env, mctx, lctx, new_c, new_type, new_value) : mk_aux_definition(new_env, mctx, lctx, new_c, new_type, new_value); } catch (exception & ex) { - throw_mk_aux_definition_error(lctx, c, new_type, new_value, ex); + throw_mk_aux_definition_error(lctx, c, new_type, new_value, std::current_exception()); } compile_aux_definition(new_env, header, c, new_c); return mk_pair(new_env, r); @@ -362,7 +362,7 @@ static environment add_equation_lemma(environment const & env, options const & o new_env = mark_rfl_lemma(new_env, new_eqn_name); new_env = add_eqn_lemma(new_env, new_eqn_name); } catch (exception & ex) { - throw_mk_aux_definition_error(lctx, eqn_name, new_type, new_value, ex); + throw_mk_aux_definition_error(lctx, eqn_name, new_type, new_value, std::current_exception()); } return new_env; } @@ -1069,7 +1069,7 @@ environment mk_smart_unfolding_definition(environment const & env, options const auto cdef = check(env, def); return module::add(env, cdef); } catch (exception & ex) { - throw nested_exception("failed to generate helper declaration for smart unfolding, type error", ex); + throw nested_exception("failed to generate helper declaration for smart unfolding, type error", std::current_exception()); } } diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp index 1df09e61ce..df21570e6e 100644 --- a/src/library/equations_compiler/wf_rec.cpp +++ b/src/library/equations_compiler/wf_rec.cpp @@ -127,7 +127,7 @@ struct wf_rec_fn { } catch (exception & ex) { throw nested_exception(some_expr(m_ref), "failed to create well founded relation using tactic", - ex); + std::current_exception()); } } } @@ -186,7 +186,7 @@ struct wf_rec_fn { return mk_app(m_ctx, get_wf_term_hack_name(), *m_parent.m_has_well_founded_inst, y, m_x); } catch (exception & ex) { throw nested_exception("failed to use wf_term_hack axiom", - ex); + std::current_exception()); } } else { expr y_R_x = mk_app(m_parent.m_R, y, m_x); @@ -229,7 +229,7 @@ struct wf_rec_fn { r += line() + format("The nested exception contains the failure state for the decreasing tactic."); return r; }, - ex); + std::current_exception()); if (!m_parent.m_elab.try_report(ex2)) throw ex2; } return m_parent.m_elab.mk_sorry(y_R_x); diff --git a/src/library/exception.cpp b/src/library/exception.cpp index c737391b21..9b048bd58e 100644 --- a/src/library/exception.cpp +++ b/src/library/exception.cpp @@ -19,24 +19,26 @@ generic_exception::generic_exception(optional const & m, char const * msg) optional nested_exception::get_pos() const { if (m_pos) return m_pos; - else if (ext_exception * ex = dynamic_cast(m_exception.get())) - return ex->get_pos(); - else - return {}; + try { + std::rethrow_exception(m_exception); + } catch (ext_exception & ex) { + return ex.get_pos(); + } catch (...) { + return optional(); + } } format nested_exception::pp(formatter const & fmt) const { format r = m_pp_fn(fmt); r += line() + format("nested exception message:") + line(); - if (ext_exception * ex = dynamic_cast(m_exception.get())) { - r += ex->pp(fmt); - } else { - r += format(m_exception->what()); + try { + std::rethrow_exception(m_exception); + } catch (ext_exception & ex) { + r += ex.pp(fmt); + } catch (std::exception & ex) { + r += format(ex.what()); + } catch (...) { } return r; } - -throwable * nested_exception::clone() const { - return new nested_exception(m_pos, m_pp_fn, *m_exception); -} } diff --git a/src/library/exception.h b/src/library/exception.h index d0afd803bc..5c918c4dac 100644 --- a/src/library/exception.h +++ b/src/library/exception.h @@ -34,58 +34,56 @@ public: virtual optional get_pos() const override { return m_pos; } virtual format pp(formatter const & fmt) const override { return m_pp_fn(fmt); } - virtual throwable * clone() const override { return new generic_exception(m_msg.c_str(), m_pos, m_pp_fn); } - virtual void rethrow() const override { throw *this; } }; class nested_exception : public generic_exception { protected: - std::shared_ptr m_exception; + std::exception_ptr m_exception; public: - nested_exception(optional const & p, pp_fn const & fn, throwable const & ex): - generic_exception(p, fn), m_exception(std::shared_ptr(ex.clone())) {} - nested_exception(optional const & m, pp_fn const & fn, throwable const & ex): - generic_exception(m, fn), m_exception(std::shared_ptr(ex.clone())) {} - nested_exception(optional const & m, char const * msg, throwable const & ex): - generic_exception(m, msg), m_exception(std::shared_ptr(ex.clone())) {} - nested_exception(optional const & m, sstream const & strm, throwable const & ex): - generic_exception(m, strm), m_exception(std::shared_ptr(ex.clone())) {} - explicit nested_exception(char const * msg, throwable const & ex): + nested_exception(optional const & p, pp_fn const & fn, std::exception_ptr const & ex): + generic_exception(p, fn), m_exception(ex) {} + nested_exception(optional const & m, pp_fn const & fn, std::exception_ptr const & ex): + generic_exception(m, fn), m_exception(ex) {} + nested_exception(optional const & m, char const * msg, std::exception_ptr const & ex): + generic_exception(m, msg), m_exception(ex) {} + nested_exception(optional const & m, sstream const & strm, std::exception_ptr const & ex): + generic_exception(m, strm), m_exception(ex) {} + explicit nested_exception(char const * msg, std::exception_ptr const & ex): nested_exception(none_expr(), msg, ex) {} - explicit nested_exception(format const & fmt, throwable const & ex): + explicit nested_exception(format const & fmt, std::exception_ptr const & ex): nested_exception(none_expr(), [=](formatter const &) { return fmt; }, ex) {} - explicit nested_exception(sstream const & strm, throwable const & ex): + explicit nested_exception(sstream const & strm, std::exception_ptr const & ex): nested_exception(none_expr(), strm, ex) {} virtual ~nested_exception() noexcept {} virtual optional get_pos() const override; virtual format pp(formatter const & fmt) const override; - virtual throwable * clone() const override; - virtual void rethrow() const override { throw *this; } }; /* Similar to nested_exception but get_pos returns none even if nested exception has position information. */ class nested_exception_without_pos : public nested_exception { - nested_exception_without_pos(pp_fn const & fn, throwable const & ex): + nested_exception_without_pos(pp_fn const & fn, std::exception_ptr const & ex): nested_exception(none_expr(), fn, ex) {} public: - nested_exception_without_pos(char const * msg, throwable const & ex): + nested_exception_without_pos(char const * msg, std::exception_ptr const & ex): nested_exception(msg, ex) {} virtual optional get_pos() const override { return optional(); } - virtual throwable * clone() const override { return new nested_exception_without_pos(m_pp_fn, *m_exception); } - virtual void rethrow() const override { throw *this; } }; /** \brief Lean exception occurred when parsing file. */ class parser_nested_exception : public exception { - std::shared_ptr m_exception; + std::exception_ptr m_exception; public: - parser_nested_exception(std::shared_ptr const & ex): exception("parser exception"), m_exception(ex) {} + parser_nested_exception(std::exception_ptr const & ex): exception("parser exception"), m_exception(ex) {} virtual ~parser_nested_exception() {} - virtual throwable * clone() const override { return new parser_nested_exception(m_exception); } - virtual void rethrow() const override { throw *this; } - virtual char const * what() const noexcept override { return m_exception->what(); } - throwable const & get_exception() const { return *(m_exception.get()); } + virtual char const * what() const noexcept override { + try { + std::rethrow_exception(m_exception); + } catch (std::exception & ex) { + return ex.what(); + } + } + std::exception_ptr const & get_exception() const { return m_exception; } }; } diff --git a/src/library/inductive_compiler/mutual.cpp b/src/library/inductive_compiler/mutual.cpp index 8e2e1ae586..80f585667b 100644 --- a/src/library/inductive_compiler/mutual.cpp +++ b/src/library/inductive_compiler/mutual.cpp @@ -897,7 +897,7 @@ public: try { m_env = add_inner_inductive_declaration(m_env, m_ngen, m_opts, m_implicit_infer_map, m_basic_decl, m_is_meta); } catch (exception & ex) { - throw nested_exception(sstream() << "mutually inductive types compiled to invalid basic inductive type", ex); + throw nested_exception(sstream() << "mutually inductive types compiled to invalid basic inductive type", std::current_exception()); } define_ind_types(); diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 1440836959..992350fcd7 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -279,7 +279,7 @@ class add_nested_inductive_decl_fn { try { m_env = add_inner_inductive_declaration(m_env, m_ngen, m_opts, m_implicit_infer_map, m_inner_decl, m_is_meta); } catch (exception & ex) { - throw nested_exception(sstream() << "nested inductive type compiled to invalid inductive type", ex); + throw nested_exception(sstream() << "nested inductive type compiled to invalid inductive type", std::current_exception()); } m_tctx.set_env(m_env); } @@ -394,7 +394,7 @@ class add_nested_inductive_decl_fn { lean_trace(name({"inductive_compiler", "nested", "define", "success"}), tout() << n << " : " << ty << " :=\n " << val << "\n";); } catch (exception & ex) { lean_trace(name({"inductive_compiler", "nested", "define", "failure"}), tout() << n << " : " << ty << " :=\n " << val << "\n";); - throw nested_exception(sstream() << "error when adding '" << n << "' to the environment", ex); + throw nested_exception(sstream() << "error when adding '" << n << "' to the environment", std::current_exception()); } m_tctx.set_env(m_env); } diff --git a/src/library/io_state.h b/src/library/io_state.h index 211cb13215..fad93b3355 100644 --- a/src/library/io_state.h +++ b/src/library/io_state.h @@ -70,8 +70,6 @@ public: formatted_exception(optional const & e, format const & fmt):formatted_exception(get_pos_info(e), fmt) {} formatted_exception(expr const & e, format const & fmt):formatted_exception(some(e), fmt) {} virtual char const * what() const noexcept override; - virtual throwable * clone() const override { return new formatted_exception(m_pos, m_fmt); } - virtual void rethrow() const override { throw *this; } virtual optional get_pos() const override { return m_pos; } virtual format pp() const { return m_fmt; } }; diff --git a/src/library/tactic/app_builder_tactics.cpp b/src/library/tactic/app_builder_tactics.cpp index c4f3e6ee0b..cd2e40d7e0 100644 --- a/src/library/tactic/app_builder_tactics.cpp +++ b/src/library/tactic/app_builder_tactics.cpp @@ -22,7 +22,7 @@ vm_obj tactic_mk_app(vm_obj const & c, vm_obj const & as, vm_obj const & tmode, expr r = mk_app(ctx, to_name(c), args.size(), args.data()); return tactic::mk_success(to_obj(r), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -33,7 +33,7 @@ vm_obj tactic_mk_app(vm_obj const & c, vm_obj const & as, vm_obj const & tmode, expr r = CODE; \ return tactic::mk_success(to_obj(r), s); \ } catch (exception & ex) { \ - return tactic::mk_exception(ex, s); \ + return tactic::mk_exception(std::current_exception(), s); \ } \ } @@ -89,7 +89,7 @@ vm_obj tactic_mk_mapp(vm_obj const & c, vm_obj const & as, vm_obj const & tmode, expr r = mk_app(ctx, to_name(c), mask.size(), mask.data(), args.data()); return tactic::mk_success(to_obj(r), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index b93b8bf7f0..7565e7aa72 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -270,7 +270,7 @@ vm_obj tactic_apply_core(vm_obj const & e, vm_obj const & cfg0, vm_obj const & s return error_obj; return tactic::mk_success(new_metas, *new_s); } catch(exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 4c2eabbe9d..915b6cdf74 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -33,8 +33,6 @@ struct cases_tactic_exception : public ext_exception { m_s(s), m_msg(msg) {} virtual format pp(formatter const &) const override { return m_msg(); } - virtual throwable * clone() const override { return new cases_tactic_exception(m_s, m_msg); } - virtual void rethrow() const override { throw cases_tactic_exception(m_s, m_msg); } }; struct cases_tactic_fn { @@ -671,9 +669,9 @@ vm_obj tactic_cases_core(vm_obj const & H, vm_obj const & ns, vm_obj const & m, } return tactic::mk_success(to_obj(info_objs), set_mctx_goals(s, mctx, append(info.first, tail(s.goals())))); } catch (cases_tactic_exception & ex) { - return tactic::mk_exception(ex, ex.m_s); + return tactic::mk_exception(std::current_exception(), ex.m_s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/change_tactic.cpp b/src/library/tactic/change_tactic.cpp index 756a53d0e8..81af561ff7 100644 --- a/src/library/tactic/change_tactic.cpp +++ b/src/library/tactic/change_tactic.cpp @@ -43,7 +43,7 @@ vm_obj change_core(expr const & e, bool check, tactic_state const & s) { return tactic::mk_exception(thunk, s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index e56bb4f38f..801565a9ea 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -59,7 +59,7 @@ vm_obj clear(expr const & H, tactic_state const & s) { expr new_mvar = clear(mctx, *mvar, H); return tactic::mk_success(set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())))); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/destruct_tactic.cpp b/src/library/tactic/destruct_tactic.cpp index b8b21a48c5..20c84dbfbe 100644 --- a/src/library/tactic/destruct_tactic.cpp +++ b/src/library/tactic/destruct_tactic.cpp @@ -166,7 +166,7 @@ vm_obj tactic_destruct(vm_obj const & e, vm_obj const & md, vm_obj const & _s) { tactic_state new_s = destruct(to_transparency_mode(md), to_expr(e), s); return tactic::mk_success(new_s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp index 8eb80e78ab..f801142b19 100644 --- a/src/library/tactic/dsimplify.cpp +++ b/src/library/tactic/dsimplify.cpp @@ -441,7 +441,7 @@ vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a, return tactic::mk_success(mk_vm_pair(F.get_a(), to_obj(new_e)), new_s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -465,7 +465,7 @@ vm_obj simp_lemmas_dsimplify(vm_obj const & lemmas, vm_obj const & u, vm_obj con return tactic::mk_success(to_obj(new_e), new_s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 387bfa2308..5997771146 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -54,9 +54,9 @@ vm_obj tactic_to_expr(vm_obj const & qe, vm_obj const & allow_mvars, vm_obj cons return tactic::mk_success(to_obj(r), set_env_mctx(s, env, mctx)); } } catch (elaborator_exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/elaborator_exception.cpp b/src/library/tactic/elaborator_exception.cpp index de4f0d99e7..2ce6efeec6 100644 --- a/src/library/tactic/elaborator_exception.cpp +++ b/src/library/tactic/elaborator_exception.cpp @@ -9,27 +9,31 @@ Author: Leonardo de Moura #include "library/tactic/elaborator_exception.h" namespace lean { -throwable * elaborator_exception::clone() const { - return new elaborator_exception(m_pos, m_fmt); -} - format failed_to_synthesize_placeholder_exception::pp() const { return m_fmt + line() + format("context:") + line() + m_state.pp(); } -throwable * nested_elaborator_exception::clone() const { - return new nested_elaborator_exception(m_pos, m_fmt, m_exception); -} - optional nested_elaborator_exception::get_pos() const { - if (auto r = m_exception->get_pos()) return r; - else return m_pos; + try { + std::rethrow_exception(m_exception); + } catch (elaborator_exception & ex) { + if (auto r = ex.get_pos()) + return r; + } catch (...) { + } + return m_pos; } format nested_elaborator_exception::pp() const { - format r = m_exception->pp(); - if (dynamic_cast(m_exception.get()) == nullptr) { + format r; + try { + std::rethrow_exception(m_exception); + } catch (nested_elaborator_exception & ex) { + r = ex.pp(); + } catch (elaborator_exception & ex) { + r = ex.pp(); r += line() + format("Additional information:"); + } catch (...) { } pos_info_provider * pip = get_pos_info_provider(); r += line(); diff --git a/src/library/tactic/elaborator_exception.h b/src/library/tactic/elaborator_exception.h index 82a0cf7e8c..92a07bd307 100644 --- a/src/library/tactic/elaborator_exception.h +++ b/src/library/tactic/elaborator_exception.h @@ -22,9 +22,6 @@ public: elaborator_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); } bool is_ignored() const { return m_ignore; } - - virtual throwable * clone() const override; - virtual void rethrow() const override { throw *this; } }; class failed_to_synthesize_placeholder_exception : public elaborator_exception { @@ -34,32 +31,32 @@ public: failed_to_synthesize_placeholder_exception(expr const & e, tactic_state const & s): elaborator_exception(e, "don't know how to synthesize placeholder"), m_mvar(e), m_state(s) {} - virtual throwable * clone() const override { - return new failed_to_synthesize_placeholder_exception(m_mvar, m_state); - } failed_to_synthesize_placeholder_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); } - virtual void rethrow() const override { throw *this; } expr const & get_mvar() const { return m_mvar; } tactic_state const & get_tactic_state() const { return m_state; } virtual format pp() const override; }; class nested_elaborator_exception : public elaborator_exception { - std::shared_ptr m_exception; + std::exception_ptr m_exception; nested_elaborator_exception(optional const & p, format const & fmt, - std::shared_ptr const & ex): + std::exception_ptr const & ex): elaborator_exception(p, fmt), m_exception(ex) {} public: - nested_elaborator_exception(optional const & p, elaborator_exception const & ex, format const & fmt): + nested_elaborator_exception(optional const & p, std::exception_ptr const & ex, format const & fmt): elaborator_exception(p, fmt), - m_exception(static_cast(ex.clone())) { - m_ignore = ex.is_ignored(); + m_exception(ex) { + try { + std::rethrow_exception(ex); + } catch (elaborator_exception & ex) { + m_ignore = ex.is_ignored(); + } catch (...) { + m_ignore = false; + } } - nested_elaborator_exception(expr const & ref, elaborator_exception const & ex, format const & fmt): + nested_elaborator_exception(expr const & ref, std::exception_ptr const & ex, format const & fmt): nested_elaborator_exception(get_pos_info(ref), ex, fmt) {} nested_elaborator_exception && ignore_if(bool b) { m_ignore = b; return std::move(*this); } - virtual void rethrow() const override { throw *this; } - virtual throwable * clone() const override; virtual optional get_pos() const override; virtual format pp() const override; }; diff --git a/src/library/tactic/eval.cpp b/src/library/tactic/eval.cpp index 90ec5a07f0..ee71893e91 100644 --- a/src/library/tactic/eval.cpp +++ b/src/library/tactic/eval.cpp @@ -44,12 +44,12 @@ static vm_obj eval(expr const & A, expr a, tactic_state const & s) { } catch (kernel_exception & ex) { /* We use nested_exception_without_pos to make sure old position information nested in 'a' is not used in type error messages. */ - return tactic::mk_exception(nested_exception_without_pos("eval_expr failed", ex), s); + return tactic::mk_exception(std::make_exception_ptr(nested_exception_without_pos("eval_expr failed", std::current_exception())), s); } try { aux_env = vm_compile(aux_env, aux_env.get(eval_aux_name)); } catch (exception & ex) { - return tactic::mk_exception(nested_exception_without_pos("eval_expr failed to compile given expression into bytecode", ex), s); + return tactic::mk_exception(std::make_exception_ptr(nested_exception_without_pos("eval_expr failed to compile given expression into bytecode", std::current_exception())), s); } S.update_env(aux_env); /* diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 342e8d146e..7b37c0dce4 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -50,7 +50,7 @@ static vm_obj exact(expr const & e, transparency_mode const & m, tactic_state s) auto mctx = ctx.mctx(); return tactic::mk_success(set_mctx_goals(s, mctx, tail(s.goals()))); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index 5d8b369a0e..7ed9d802f4 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -26,7 +26,7 @@ static vm_obj generalize(transparency_mode m, expr const & e, name const & id, t try { check(ctx, new_type); } catch (exception & ex) { - return tactic::mk_exception(nested_exception("generalize tactic failed, result is not type correct", ex), s); + return tactic::mk_exception(std::make_exception_ptr(nested_exception("generalize tactic failed, result is not type correct", std::current_exception())), s); } expr mvar = ctx.mk_metavar_decl(g->get_context(), new_type); ctx.assign(head(s.goals()), mk_app(mvar, e)); diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index f937f6a4cf..cee721fa90 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -413,7 +413,7 @@ vm_obj induction_tactic_core(transparency_mode const & m, expr const & H, name c } return tactic::mk_success(to_obj(info), new_s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -431,7 +431,7 @@ vm_obj tactic_induction(vm_obj const & H, vm_obj const & ns, vm_obj const & rec, tactic::to_state(s)); } } catch (exception & ex) { - return tactic::mk_exception(ex, tactic::to_state(s)); + return tactic::mk_exception(std::current_exception(), tactic::to_state(s)); } } else { return induction_tactic_core(to_transparency_mode(m), to_expr(H), diff --git a/src/library/tactic/kabstract.cpp b/src/library/tactic/kabstract.cpp index e35f617c55..503a9fc4b1 100644 --- a/src/library/tactic/kabstract.cpp +++ b/src/library/tactic/kabstract.cpp @@ -70,7 +70,7 @@ vm_obj tactic_kdepends_on(vm_obj const & e, vm_obj const & t, vm_obj const & md, type_context_old ctx = mk_type_context_for(s, md); return tactic::mk_success(mk_vm_bool(kdepends_on(ctx, to_expr(e), to_expr(t))), tactic::to_state(s)); } catch (exception & ex) { - return tactic::mk_exception(ex, tactic::to_state(s)); + return tactic::mk_exception(std::current_exception(), tactic::to_state(s)); } } @@ -81,7 +81,7 @@ vm_obj tactic_kabstract(vm_obj const & e, vm_obj const & t, vm_obj const & md, v auto a = kabstract(ctx, to_expr(e), to_expr(t), occurrences(), to_bool(u)); return tactic::mk_success(to_obj(a), set_mctx(s, ctx.mctx())); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index 13af37afbf..f043c6bafd 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -44,7 +44,7 @@ vm_obj revert(list const & ls, tactic_state const & s, bool preserve_local tactic_state new_s = revert(locals, s, preserve_locals_order); return tactic::mk_success(mk_vm_nat(locals.size()), new_s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 4b1a9b4bba..2d693381e3 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -93,7 +93,7 @@ static vm_obj rewrite_core(expr h, expr e, rewrite_cfg const & cfg, tactic_state type_context_old::transparency_scope scope(ctx, ensure_semireducible_mode(ctx.mode())); check(ctx, motive); } catch (exception & ex) { - throw nested_exception("rewrite tactic failed, motive is not type correct", ex); + throw nested_exception("rewrite tactic failed, motive is not type correct", std::current_exception()); } expr prf = mk_eq_rec(ctx, motive, mk_eq_refl(ctx, e), h); tactic_state new_s = set_mctx_goals(s, ctx.mctx(), append(cons(head(s.goals()), to_list(new_goals)), tail(s.goals()))); diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 5eeb312254..e6e6a3fb2a 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -1251,7 +1251,7 @@ vm_obj tactic_simplify(vm_obj const & slss, vm_obj const & u, vm_obj const & e, return tactic::mk_exception("simplify tactic failed to simplify", s); } } catch (exception & e) { - return tactic::mk_exception(e, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -1274,7 +1274,7 @@ static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas return tactic::mk_exception("simplify tactic failed to simplify", s); } } catch (exception & e) { - return tactic::mk_exception(e, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index 3e9e925522..6abfb8e2b3 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -129,7 +129,7 @@ vm_obj tactic_subst_core(name const & n, bool symm, tactic_state const & s) { expr new_mvar = subst(s.env(), s.get_options(), transparency_mode::Semireducible, mctx, mvar, H, symm, nullptr); return tactic::mk_success(set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())))); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index a371fe6a40..20287f7de6 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -387,7 +387,7 @@ vm_obj tactic_infer_type(vm_obj const & e, vm_obj const & s0) { check_closed("infer_type", to_expr(e)); return tactic::mk_success(to_obj(ctx.infer(to_expr(e))), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -403,7 +403,7 @@ vm_obj tactic_whnf(vm_obj const & e, vm_obj const & t, vm_obj const & unfold_gin return tactic::mk_success(to_obj(whnf_ginductive_gintro_rule(ctx, to_expr(e))), s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -415,7 +415,7 @@ vm_obj tactic_head_eta_expand(vm_obj const & e, vm_obj const & s0) { check_closed("head_eta_expand", to_expr(e)); return tactic::mk_success(to_obj(ctx.eta_expand(to_expr(e))), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -424,7 +424,7 @@ vm_obj tactic_head_eta(vm_obj const & e, vm_obj const & s0) { try { return tactic::mk_success(to_obj(try_eta(to_expr(e))), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -433,7 +433,7 @@ vm_obj tactic_head_beta(vm_obj const & e, vm_obj const & s0) { try { return tactic::mk_success(to_obj(annotated_head_beta_reduce(to_expr(e))), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -450,7 +450,7 @@ vm_obj tactic_head_zeta(vm_obj const & e0, vm_obj const & s0) { if (!ldecl || !ldecl->get_value()) return tactic::mk_success(e0, s); return tactic::mk_success(to_obj(*ldecl->get_value()), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -464,7 +464,7 @@ vm_obj tactic_zeta(vm_obj const & e0, vm_obj const & s0) { local_context lctx = mdecl->get_context(); return tactic::mk_success(to_obj(zeta_expand(lctx, e)), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -476,7 +476,7 @@ vm_obj tactic_is_class(vm_obj const & e, vm_obj const & s0) { check_closed("is_class", to_expr(e)); return tactic::mk_success(mk_vm_bool(static_cast(ctx.is_class(to_expr(e)))), s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -498,7 +498,7 @@ vm_obj tactic_mk_instance(vm_obj const & e, vm_obj const & s0) { return tactic::mk_exception(thunk, s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -539,7 +539,7 @@ vm_obj tactic_unify(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_o to_expr(e1), to_expr(e2), s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -560,7 +560,7 @@ vm_obj tactic_is_def_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, to_expr(e1), to_expr(e2), s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -717,7 +717,7 @@ vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) { new_env = vm_compile(new_env, d); return tactic::mk_success(set_env(s, new_env)); } catch (throwable & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -753,7 +753,7 @@ vm_obj tactic_add_doc_string(vm_obj const & n, vm_obj const & doc, vm_obj const environment new_env = add_doc_string(s.env(), to_name(n), to_string(doc)); return tactic::mk_success(set_env(s, new_env)); } catch (throwable & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -821,7 +821,7 @@ vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const & : mk_aux_definition(s.env(), s.mctx(), g->get_context(), to_name(n), to_expr(type), to_expr(val)); return tactic::mk_success(to_obj(r.second), set_env(s, r.first)); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -832,7 +832,7 @@ vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const & s) } else { optional e = is_io_error(r); lean_assert(e); - return tactic::mk_exception(io_error_to_string(*e), tactic::to_state(s)); + return tactic::mk_exception(format(io_error_to_string(*e)), tactic::to_state(s)); } } @@ -906,7 +906,7 @@ vm_obj tactic_using_new_ref(vm_obj const &, vm_obj const &, vm_obj const & a, vm return r; } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -920,7 +920,7 @@ vm_obj tactic_read_ref(vm_obj const &, vm_obj const & ref, vm_obj const & s0) { vm_obj r = us.read(cidx(ref)); return tactic::mk_success(r, s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -935,7 +935,7 @@ vm_obj tactic_write_ref(vm_obj const &, vm_obj const & ref, vm_obj const & v, vm s = set_user_state(s, us); return tactic::mk_success(s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -958,7 +958,7 @@ vm_obj tactic_type_check(vm_obj const & e, vm_obj const & m, vm_obj const & s0) check(ctx, to_expr(e)); return tactic::mk_success(s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 51804f68a7..0dcd56beb4 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -215,7 +215,7 @@ type_context_old mk_cacheless_type_context_for(tactic_state const & s, transpare }) #define LEAN_TACTIC_TRY try { -#define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return tactic::mk_exception(ex, S); } +#define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return tactic::mk_exception(std::current_exception(), S); } void initialize_tactic_state(); void finalize_tactic_state(); diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp index 05e00b3a42..438a79e785 100644 --- a/src/library/tactic/unfold_tactic.cpp +++ b/src/library/tactic/unfold_tactic.cpp @@ -30,7 +30,7 @@ vm_obj tactic_unfold_projection(vm_obj const & _e, vm_obj const & m, vm_obj cons return tactic::mk_success(to_obj(*new_e), s); return tactic::mk_exception("unfold projection failed, failed to unfold", s); } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -130,7 +130,7 @@ vm_obj tactic_dunfold(vm_obj const & cs, vm_obj const & _e, vm_obj const & _cfg, return tactic::mk_success(to_obj(new_e), new_s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } @@ -160,7 +160,7 @@ vm_obj tactic_dunfold_head(vm_obj const & _e, vm_obj const & m, vm_obj const & _ return tactic::mk_exception("dunfold_expr failed, failed to unfold", s); } } catch (exception & ex) { - return tactic::mk_exception(ex, s); + return tactic::mk_exception(std::current_exception(), s); } } diff --git a/src/library/vm/interaction_state.h b/src/library/vm/interaction_state.h index 33a2dcb6f3..d07924f9d4 100644 --- a/src/library/vm/interaction_state.h +++ b/src/library/vm/interaction_state.h @@ -50,7 +50,7 @@ struct interaction_monad { static vm_obj mk_exception(vm_obj const & fn, State const & s); static vm_obj mk_silent_exception(State const & s); static vm_obj mk_exception(vm_obj const & fn, vm_obj const & pos, State const & s); - static vm_obj mk_exception(throwable const & ex, State const & s); + static vm_obj mk_exception(std::exception_ptr const & ex, State const & s); static vm_obj mk_exception(format const & fmt, State const & s); static vm_obj mk_exception(char const * msg, State const & s); static vm_obj mk_exception(sstream const & strm, State const & s); diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h index df0eefa36e..442520e3eb 100644 --- a/src/library/vm/interaction_state_imp.h +++ b/src/library/vm/interaction_state_imp.h @@ -156,12 +156,16 @@ vm_obj interaction_monad::update_exception_state(vm_obj const & ex, State } template -vm_obj interaction_monad::mk_exception(throwable const & ex, State const & s) { +vm_obj interaction_monad::mk_exception(std::exception_ptr const & ex, State const & s) { vm_obj _ex = lean::to_obj(ex); vm_obj fn = mk_vm_closure(get_throwable_to_format_fun_idx(), 1, &_ex); optional pos; - if (auto kex = dynamic_cast(&ex)) - pos = kex->get_pos(); + try { + std::rethrow_exception(ex); + } catch (exception_with_pos & ex) { + pos = ex.get_pos(); + } catch (...) { + } vm_obj _pos = pos ? mk_vm_some(mk_vm_pair(mk_vm_nat(pos->first), mk_vm_nat(pos->second))) : mk_vm_none(); return mk_exception(fn, _pos, s); } diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index e040880d69..3ebb279507 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -64,7 +64,7 @@ vm_obj environment_add(vm_obj const & env, vm_obj const & decl) { try { return mk_vm_exceptional_success(to_obj(module::add(to_env(env), check(to_env(env), to_declaration(decl))))); } catch (throwable & ex) { - return mk_vm_exceptional_exception(ex); + return mk_vm_exceptional_exception(std::current_exception()); } } @@ -72,7 +72,7 @@ vm_obj environment_get(vm_obj const & env, vm_obj const & n) { try { return mk_vm_exceptional_success(to_obj(to_env(env).get(to_name(n)))); } catch (throwable & ex) { - return mk_vm_exceptional_exception(ex); + return mk_vm_exceptional_exception(std::current_exception()); } } @@ -97,7 +97,7 @@ vm_obj environment_add_inductive(vm_obj const & env, vm_obj const & n, vm_obj co !to_bool(is_meta)); return mk_vm_exceptional_success(to_obj(new_env)); } catch (throwable & ex) { - return mk_vm_exceptional_exception(ex); + return mk_vm_exceptional_exception(std::current_exception()); } } diff --git a/src/library/vm/vm_exceptional.cpp b/src/library/vm/vm_exceptional.cpp index b7890a130f..4debb75532 100644 --- a/src/library/vm/vm_exceptional.cpp +++ b/src/library/vm/vm_exceptional.cpp @@ -12,20 +12,20 @@ Author: Leonardo de Moura namespace lean { struct vm_throwable : public vm_external { - throwable * m_val; - vm_throwable(throwable const & ex):m_val(ex.clone()) {} - virtual ~vm_throwable() { delete m_val; } + std::exception_ptr m_val; + vm_throwable(std::exception_ptr const & ex):m_val(ex) {} + virtual ~vm_throwable() {} virtual void dealloc() override { delete this; } - virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_throwable(*m_val); } - virtual vm_external * clone(vm_clone_fn const &) override { return new vm_throwable(*m_val); } + virtual vm_external * ts_clone(vm_clone_fn const &) override { return new vm_throwable(m_val); } + virtual vm_external * clone(vm_clone_fn const &) override { return new vm_throwable(m_val); } }; -throwable * to_throwable(vm_obj const & o) { +std::exception_ptr const & to_throwable(vm_obj const & o) { lean_vm_check(dynamic_cast(to_external(o))); return static_cast(to_external(o))->m_val; } -vm_obj to_obj(throwable const & ex) { +vm_obj to_obj(std::exception_ptr const & ex) { return mk_vm_external(new vm_throwable(ex)); } @@ -33,26 +33,30 @@ vm_obj to_obj(throwable const & ex) { 1) throwable -> options -> format 2) throwable -> unit -> format */ vm_obj throwable_to_format(vm_obj const & _ex, vm_obj const & _opts) { - throwable * ex = to_throwable(_ex); + std::exception_ptr const & ex = to_throwable(_ex); if (!ex) return to_obj(format("null-exception")); - if (auto kex = dynamic_cast(ex)) { + try { + std::rethrow_exception(ex); + } catch (ext_exception & ex) { if (is_simple(_opts)) { io_state_stream ios = tout(); formatter fmt = ios.get_formatter(); - return to_obj(kex->pp(fmt)); + return to_obj(ex.pp(fmt)); } else { options opts = to_options(_opts); scope_trace_env scope1(opts); io_state_stream ios = tout(); formatter fmt = ios.get_formatter(); - return to_obj(kex->pp(fmt)); + return to_obj(ex.pp(fmt)); } - } else if (auto fex = dynamic_cast(ex)) { - return to_obj(fex->pp()); - } else { - return to_obj(format(ex->what())); + } catch (formatted_exception & ex) { + return to_obj(ex.pp()); + } catch (std::exception & ex) { + return to_obj(format(ex.what())); + } catch (...) { + return to_obj(format("unknown-exception")); } } @@ -66,7 +70,7 @@ vm_obj mk_vm_exceptional_success(vm_obj const & a) { return mk_vm_constructor(0, a); } -vm_obj mk_vm_exceptional_exception(throwable const & ex) { +vm_obj mk_vm_exceptional_exception(std::exception_ptr const & ex) { vm_obj _ex = to_obj(ex); return mk_vm_constructor(1, mk_vm_closure(g_throwable_to_format_fun_idx, 1, &_ex)); } diff --git a/src/library/vm/vm_exceptional.h b/src/library/vm/vm_exceptional.h index d048e64809..7c7036bdd3 100644 --- a/src/library/vm/vm_exceptional.h +++ b/src/library/vm/vm_exceptional.h @@ -10,11 +10,11 @@ Author: Leonardo de Moura namespace lean { /* Convert exception into vm_exception */ -vm_obj to_obj(throwable const & ex); +vm_obj to_obj(std::exception_ptr const & ex); /* Return fun_idx for vm_exception -> options -> format */ unsigned get_throwable_to_format_fun_idx(); vm_obj mk_vm_exceptional_success(vm_obj const & a); -vm_obj mk_vm_exceptional_exception(throwable const & ex); +vm_obj mk_vm_exceptional_exception(std::exception_ptr const & ex); void initialize_vm_exceptional(); void finalize_vm_exceptional(); void initialize_vm_exceptional_builtin_idxs(); diff --git a/src/library/vm/vm_parser.cpp b/src/library/vm/vm_parser.cpp index a81840884e..a8f6e73a40 100644 --- a/src/library/vm/vm_parser.cpp +++ b/src/library/vm/vm_parser.cpp @@ -41,7 +41,7 @@ typedef interaction_monad lean_parser; #define TRY try { #define CATCH } catch (break_at_pos_exception const & ex) { throw; }\ - catch (exception const & ex) { return lean_parser::mk_exception(ex, s); } + catch (exception const & ex) { return lean_parser::mk_exception(std::current_exception(), s); } vm_obj run_parser(parser & p, expr const & spec, buffer const & args) { type_context_old ctx(p.env(), p.get_options()); @@ -314,7 +314,7 @@ static vm_obj vm_parser_of_tactic(vm_obj const &, vm_obj const & tac, vm_obj con return lean_parser::update_exception_state(r, s); } } catch (exception & ex) { - return lean_parser::mk_exception(ex, s); + return lean_parser::mk_exception(std::current_exception(), s); } } diff --git a/src/runtime/debug.h b/src/runtime/debug.h index bf9c120f74..f9ded2e1fd 100644 --- a/src/runtime/debug.h +++ b/src/runtime/debug.h @@ -118,8 +118,6 @@ public: unreachable_reached() {} virtual ~unreachable_reached() noexcept {} virtual char const * what() const noexcept { return "'unreachable' code was reached"; } - virtual throwable * clone() const { return new unreachable_reached(); } - virtual void rethrow() const { throw *this; } }; namespace debug { template void display_var(char const * name, T const & value) { diff --git a/src/runtime/exception.h b/src/runtime/exception.h index 937f2a33cc..ed4fb4fa3f 100644 --- a/src/runtime/exception.h +++ b/src/runtime/exception.h @@ -22,8 +22,6 @@ public: throwable(sstream const & strm); virtual ~throwable() noexcept; virtual char const * what() const noexcept; - virtual throwable * clone() const { return new throwable(m_msg); } - virtual void rethrow() const { throw *this; } }; /** \brief Base class for all Lean "logical" exceptions, that is, exceptions not related @@ -35,8 +33,6 @@ public: exception(char const * msg):throwable(msg) {} exception(std::string const & msg):throwable(msg) {} exception(sstream const & strm):throwable(strm) {} - virtual throwable * clone() const { return new exception(m_msg); } - virtual void rethrow() const { throw *this; } }; /** \brief Exception used to sign that a computation was interrupted */ @@ -53,8 +49,6 @@ class stack_space_exception : public throwable { public: stack_space_exception(char const * component_name); virtual char const * what() const noexcept { return m_msg.c_str(); } - virtual throwable * clone() const { return new stack_space_exception(m_msg); } - virtual void rethrow() const { throw *this; } }; class memory_exception : public throwable { @@ -63,15 +57,11 @@ class memory_exception : public throwable { public: memory_exception(char const * component_name); virtual char const * what() const noexcept { return m_msg.c_str(); } - virtual throwable * clone() const { return new memory_exception(m_msg); } - virtual void rethrow() const { throw *this; } }; class heartbeat_exception : public throwable { public: heartbeat_exception() {} virtual char const * what() const noexcept; - virtual throwable * clone() const { return new heartbeat_exception(); } - virtual void rethrow() const { throw *this; } }; } diff --git a/src/util/parser_exception.h b/src/util/parser_exception.h index f48d48fb83..b2fa14089c 100644 --- a/src/util/parser_exception.h +++ b/src/util/parser_exception.h @@ -26,7 +26,5 @@ public: virtual optional get_pos() const override { return some(m_pos); } std::string const & get_file_name() const { return m_fname; } std::string const & get_msg() const { return m_msg; } - virtual throwable * clone() const override { return new parser_exception(m_msg, m_fname.c_str(), m_pos); } - virtual void rethrow() const override { throw *this; } }; } diff --git a/src/util/worker_queue.h b/src/util/worker_queue.h index bac50d2b92..d23764cbbd 100644 --- a/src/util/worker_queue.h +++ b/src/util/worker_queue.h @@ -19,9 +19,8 @@ template class worker_queue { typedef std::function task; typedef std::unique_ptr thread_ptr; - typedef std::unique_ptr exception_ptr; std::vector m_threads; - std::vector m_thread_exceptions; + std::vector m_thread_exceptions; std::vector m_todo; std::vector m_result; mutex m_result_mutex; @@ -60,7 +59,7 @@ public: num_threads = 0; #endif for (unsigned i = 0; i < num_threads; i++) - m_thread_exceptions.push_back(exception_ptr(nullptr)); + m_thread_exceptions.push_back(std::exception_ptr()); for (unsigned i = 0; i < num_threads; i++) { m_threads.push_back(std::unique_ptr(new interruptible_thread([=]() { f(); @@ -70,11 +69,8 @@ public: } m_todo_cv.notify_all(); } catch (interrupted &) { - } catch (throwable & ex) { - m_thread_exceptions[i].reset(ex.clone()); - m_failed_thread = i; } catch (...) { - m_thread_exceptions[i].reset(new exception("thread failed for unknown reasons")); + m_thread_exceptions[i] = std::current_exception(); m_failed_thread = i; } }))); @@ -116,7 +112,7 @@ public: throw; } if (m_failed_thread >= 0) - m_thread_exceptions[m_failed_thread]->rethrow(); + std::rethrow_exception(m_thread_exceptions[m_failed_thread]); if (m_interrupted) throw interrupted(); }