From b11e1a5f34eef1e76c56e3f003f202dacc12f565 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2014 18:38:09 -0700 Subject: [PATCH] feat(kernel/type_checker): add mk_app_justification auxiliary function Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 22 +++++++++++----------- src/kernel/type_checker.h | 6 ++++++ 2 files changed, 17 insertions(+), 11 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 38fe26e6d..2ae1129d0 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -200,21 +200,21 @@ void type_checker::check_level(level const & l, expr const & s) { app_delayed_justification::app_delayed_justification(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) {} +justification mk_app_justification(environment const & env, expr const & e, expr const & d_type, expr const & a_type) { + auto pp_fn = [=](formatter const & fmt, options const & o, substitution const & subst) { + return pp_app_type_mismatch(fmt, env, o, + subst.instantiate_metavars_wo_jst(e), + subst.instantiate_metavars_wo_jst(d_type), + subst.instantiate_metavars_wo_jst(a_type)); + }; + return mk_justification(e, pp_fn); +} + justification app_delayed_justification::get() { if (!m_jst) { // We should not have a reference to this object inside the closure. // So, we create the following locals that will be captured by the closure instead of 'this'. - environment env = m_env; - expr e = m_e; - expr fn_type = m_fn_type; - expr arg_type = m_arg_type; - m_jst = mk_justification(e, - [=](formatter const & fmt, options const & o, substitution const & subst) { - return pp_app_type_mismatch(fmt, env, o, - subst.instantiate_metavars_wo_jst(e), - subst.instantiate_metavars_wo_jst(binding_domain(fn_type)), - subst.instantiate_metavars_wo_jst(arg_type)); - }); + m_jst = mk_app_justification(m_env, m_e, binding_domain(m_fn_type), m_arg_type); } return *m_jst; } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 8452cdfc5..cc90a1b6c 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -151,6 +151,12 @@ certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque = name_set(), bool memoize = true); certified_declaration check(environment const & env, declaration const & d, name_set const & extra_opaque = name_set(), bool memoize = true); +/** + \brief Create a justification for an application \c e where the expected type must be \c d_type and + the argument type is \c a_type. +*/ +justification mk_app_justification(environment const & env, expr const & e, expr const & d_type, expr const & a_type); + /** \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.