From e206fcc1af31c4fed503cd96e3a1e1bba05db83d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 May 2014 23:16:49 -0700 Subject: [PATCH] perf(kernel/type_checker): reduce the overhead of creating delayed_justification objects, a huge number of them is created when type checking applications We reduce the cost by avoiding the allocation of std::functional objects, and the unnecessary increment/decrement of reference counters. Signed-off-by: Leonardo de Moura --- src/kernel/converter.cpp | 4 +-- src/kernel/inductive/inductive.cpp | 2 +- src/kernel/justification.h | 15 ++++++++-- src/kernel/type_checker.cpp | 48 +++++++++++++++++++----------- src/library/resolve_macro.cpp | 4 +-- 5 files changed, 48 insertions(+), 25 deletions(-) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 7ddaeb5cf..589648807 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -12,9 +12,9 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" namespace lean { +static no_delayed_justification g_no_delayed_jst; bool converter::is_def_eq(expr const & t, expr const & s, context & c) { - delayed_justification j([]() { return justification(); }); - return is_def_eq(t, s, c, j); + return is_def_eq(t, s, c, g_no_delayed_jst); } /** \brief Do nothing converter */ diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 44184094b..88e34f63b 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -758,7 +758,7 @@ optional inductive_normalizer_extension::operator()(expr const & e, extens // std::cout << "Candidate: " << e << "\n"; if (it1->m_num_params > 0) { // Global parameters of elim and intro be definitionally equal - delayed_justification jst([=]() { return mk_justification("elim/intro global parameters must match", some_expr(e)); }); + simple_delayed_justification jst([=]() { return mk_justification("elim/intro global parameters must match", some_expr(e)); }); for (unsigned i = 0; i < it1->m_num_params; i++) { if (!ctx.is_def_eq(elim_args[i], intro_args[i], jst)) return none_expr(); diff --git a/src/kernel/justification.h b/src/kernel/justification.h index ddedbbfba..608ce38f1 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -144,10 +144,21 @@ std::ostream & operator<<(std::ostream & out, justification const & j); /** \brief Object to simulate delayed justification creation. */ class delayed_justification { +public: + virtual ~delayed_justification() {} + virtual justification get() = 0; +}; + +class no_delayed_justification : public delayed_justification { +public: + virtual justification get() { return justification(); } +}; + +class simple_delayed_justification : public delayed_justification { optional m_jst; std::function m_mk; public: - template delayed_justification(Mk && mk):m_mk(mk) {} - justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; } + template simple_delayed_justification(Mk && mk):m_mk(mk) {} + virtual justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; } }; } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index f984c65fc..29cf9ebec 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -219,21 +219,6 @@ struct type_checker::imp { } } - /** - \brief Create a justification for a application type mismatch, - \c e is the application, \c fn_type and \c arg_type are the function and argument type. - */ - justification mk_app_mismatch_jst(expr const & e, expr const & fn_type, expr const & arg_type) { - lean_assert(is_app(e)); - return mk_justification(e, - [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_app_type_mismatch(fmt, m_env, o, - subst.instantiate_metavars_wo_jst(e), - subst.instantiate_metavars_wo_jst(binding_domain(fn_type)), - subst.instantiate_metavars_wo_jst(arg_type)); - }); - } - /** \brief Create a justification for a let definition type mismatch, \c e is the let expression, and \c val_type is the type inferred for the let value. @@ -264,6 +249,33 @@ struct type_checker::imp { throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '" << *n2 << "'", s); } + /** + \brief Create a justification for a application type mismatch, + \c e is the application, \c fn_type and \c arg_type are the function and argument type. + */ + struct app_delayed_jst : public delayed_justification { + environment const & m_env; + expr const & m_e; + expr const & m_fn_type; + expr const & m_arg_type; + optional m_jst; + app_delayed_jst(environment const & env, expr const & e, expr const & f_type, expr const & a_type): + m_env(env), m_e(e), m_fn_type(f_type), m_arg_type(a_type) {} + + virtual justification get() { + if (!m_jst) { + m_jst = mk_justification(m_e, + [=](formatter const & fmt, options const & o, substitution const & subst) { + return pp_app_type_mismatch(fmt, m_env, o, + subst.instantiate_metavars_wo_jst(m_e), + subst.instantiate_metavars_wo_jst(binding_domain(m_fn_type)), + subst.instantiate_metavars_wo_jst(m_arg_type)); + }); + } + return *m_jst; + } + }; + /** \brief Return type of expression \c e, if \c infer_only is false, then it also check whether \c e is type correct or not. @@ -318,7 +330,7 @@ struct type_checker::imp { if (!m) throw_kernel_exception(m_env, "failed to expand macro", e); expr t = infer_type_core(*m, infer_only); - delayed_justification jst([=]() { return mk_macro_jst(e); }); + simple_delayed_justification jst([=]() { return mk_macro_jst(e); }); if (!is_def_eq(r, t, jst)) throw_kernel_exception(m_env, g_macro_error_msg, e); } @@ -347,7 +359,7 @@ struct type_checker::imp { expr f_type = ensure_pi(infer_type_core(app_fn(e), infer_only), app_fn(e)); if (!infer_only) { expr a_type = infer_type_core(app_arg(e), infer_only); - delayed_justification jst([=]() { return mk_app_mismatch_jst(e, f_type, a_type); }); + app_delayed_jst jst(m_env, e, f_type, a_type); if (!is_def_eq(a_type, binding_domain(f_type), jst)) { environment env = m_env; throw_kernel_exception(m_env, e, @@ -363,7 +375,7 @@ struct type_checker::imp { if (!infer_only) { ensure_sort(infer_type_core(let_type(e), infer_only), let_type(e)); expr val_type = infer_type_core(let_value(e), infer_only); - delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); }); + simple_delayed_justification jst([=]() { return mk_let_mismatch_jst(e, val_type); }); if (!is_def_eq(val_type, let_type(e), jst)) { environment env = m_env; throw_kernel_exception(env, e, diff --git a/src/library/resolve_macro.cpp b/src/library/resolve_macro.cpp index f1ec6c7dc..06a3ac888 100644 --- a/src/library/resolve_macro.cpp +++ b/src/library/resolve_macro.cpp @@ -65,14 +65,14 @@ static expr g_var_0(mk_var(0)); It may be used also by users to avoid tedious steps. */ class resolve_macro_definition_cell : public macro_definition_cell { - delayed_justification m_dummy_jst; + simple_delayed_justification m_dummy_jst; public: resolve_macro_definition_cell():m_dummy_jst([] { return mk_justification("resolve macro"); }) { m_dummy_jst.get(); // the delayed_justification may be accessed by different threads, thus we force its initialization. } // The following const cast is say because we already initialized the delayed justification in the constructor. - delayed_justification & jst() const { return const_cast(m_dummy_jst); } + delayed_justification & jst() const { return const_cast(m_dummy_jst); } static void check_num_args(environment const & env, expr const & m) { lean_assert(is_macro(m));