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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-27 23:16:49 -07:00
parent 1b4c9f63ce
commit e206fcc1af
5 changed files with 48 additions and 25 deletions

View file

@ -12,9 +12,9 @@ Author: Leonardo de Moura
#include "kernel/free_vars.h" #include "kernel/free_vars.h"
namespace lean { namespace lean {
static no_delayed_justification g_no_delayed_jst;
bool converter::is_def_eq(expr const & t, expr const & s, context & c) { 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, g_no_delayed_jst);
return is_def_eq(t, s, c, j);
} }
/** \brief Do nothing converter */ /** \brief Do nothing converter */

View file

@ -758,7 +758,7 @@ optional<expr> inductive_normalizer_extension::operator()(expr const & e, extens
// std::cout << "Candidate: " << e << "\n"; // std::cout << "Candidate: " << e << "\n";
if (it1->m_num_params > 0) { if (it1->m_num_params > 0) {
// Global parameters of elim and intro be definitionally equal // 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++) { for (unsigned i = 0; i < it1->m_num_params; i++) {
if (!ctx.is_def_eq(elim_args[i], intro_args[i], jst)) if (!ctx.is_def_eq(elim_args[i], intro_args[i], jst))
return none_expr(); return none_expr();

View file

@ -144,10 +144,21 @@ std::ostream & operator<<(std::ostream & out, justification const & j);
/** \brief Object to simulate delayed justification creation. */ /** \brief Object to simulate delayed justification creation. */
class delayed_justification { 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<justification> m_jst; optional<justification> m_jst;
std::function<justification()> m_mk; std::function<justification()> m_mk;
public: public:
template<typename Mk> delayed_justification(Mk && mk):m_mk(mk) {} template<typename Mk> simple_delayed_justification(Mk && mk):m_mk(mk) {}
justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; } virtual justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; }
}; };
} }

View file

@ -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, \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. \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); 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<justification> 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. \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) if (!m)
throw_kernel_exception(m_env, "failed to expand macro", e); throw_kernel_exception(m_env, "failed to expand macro", e);
expr t = infer_type_core(*m, infer_only); 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)) if (!is_def_eq(r, t, jst))
throw_kernel_exception(m_env, g_macro_error_msg, e); 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)); expr f_type = ensure_pi(infer_type_core(app_fn(e), infer_only), app_fn(e));
if (!infer_only) { if (!infer_only) {
expr a_type = infer_type_core(app_arg(e), 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)) { if (!is_def_eq(a_type, binding_domain(f_type), jst)) {
environment env = m_env; environment env = m_env;
throw_kernel_exception(m_env, e, throw_kernel_exception(m_env, e,
@ -363,7 +375,7 @@ struct type_checker::imp {
if (!infer_only) { if (!infer_only) {
ensure_sort(infer_type_core(let_type(e), infer_only), let_type(e)); ensure_sort(infer_type_core(let_type(e), infer_only), let_type(e));
expr val_type = infer_type_core(let_value(e), infer_only); 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)) { if (!is_def_eq(val_type, let_type(e), jst)) {
environment env = m_env; environment env = m_env;
throw_kernel_exception(env, e, throw_kernel_exception(env, e,

View file

@ -65,14 +65,14 @@ static expr g_var_0(mk_var(0));
It may be used also by users to avoid tedious steps. It may be used also by users to avoid tedious steps.
*/ */
class resolve_macro_definition_cell : public macro_definition_cell { class resolve_macro_definition_cell : public macro_definition_cell {
delayed_justification m_dummy_jst; simple_delayed_justification m_dummy_jst;
public: public:
resolve_macro_definition_cell():m_dummy_jst([] { return mk_justification("resolve macro"); }) { 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. 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. // The following const cast is say because we already initialized the delayed justification in the constructor.
delayed_justification & jst() const { return const_cast<delayed_justification&>(m_dummy_jst); } delayed_justification & jst() const { return const_cast<simple_delayed_justification&>(m_dummy_jst); }
static void check_num_args(environment const & env, expr const & m) { static void check_num_args(environment const & env, expr const & m) {
lean_assert(is_macro(m)); lean_assert(is_macro(m));