From 9df10a4048acbb1022fb9377137881ae8827a563 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Dec 2015 13:36:11 -0800 Subject: [PATCH] feat(library): add tracing messages to app_builder and congr_lemma_manager --- src/library/app_builder.cpp | 125 +++++++++++++++++++++++----- src/library/app_builder.h | 2 + src/library/congr_lemma_manager.cpp | 23 +++++ src/library/congr_lemma_manager.h | 3 + src/library/init_module.cpp | 6 ++ 5 files changed, 139 insertions(+), 20 deletions(-) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index b61bea7e9..796a01ccf 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/name_map.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" +#include "library/trace.h" #include "library/match.h" #include "library/constants.h" #include "library/app_builder.h" @@ -159,6 +160,20 @@ struct app_builder::imp { } } + void trace_fun(name const & n) { + tout() << "failed to create an '" << n << "'-application"; + } + + void trace_failure(name const & n, unsigned nargs, char const * msg) { + lean_trace("app_builder", + trace_fun(n); tout() << " with " << nargs << ", " << msg << "\n";); + } + + void trace_failure(name const & n, char const * msg) { + lean_trace("app_builder", + trace_fun(n); tout() << ", " << msg << "\n";); + } + levels mk_metavars(declaration const & d, unsigned arity, buffer & mvars, buffer> & inst_args) { m_ctx->clear(); unsigned num_univ = d.get_num_univ_params(); @@ -170,8 +185,10 @@ struct app_builder::imp { expr type = instantiate_type_univ_params(d, lvls); for (unsigned i = 0; i < arity; i++) { type = m_ctx->relaxed_whnf(type); - if (!is_pi(type)) + if (!is_pi(type)) { + trace_failure(d.get_name(), arity, "too many arguments"); throw app_builder_exception(); + } expr mvar = m_ctx->mk_mvar(binding_domain(type)); if (binding_info(type).is_inst_implicit()) inst_args.push_back(some_expr(mvar)); @@ -247,22 +264,36 @@ struct app_builder::imp { m_ctx->set_next_mvar_idx(e.m_num_emeta); } + void trace_unify_failure(name const & n, unsigned i, expr const & m, expr const & v) { + lean_trace("app_builder", + trace_fun(n); + tout () << ", failed to solve unification constraint for #" << (i+1) + << "argument (" << m_ctx->infer(m) << " =?= " << m_ctx->infer(v) << ")\n";); + } + expr mk_app(name const & c, unsigned nargs, expr const * args) { optional e = get_entry(c, nargs); - if (!e) + if (!e) { + trace_failure(c, "failed to retrieve declaration"); throw app_builder_exception(); + } init_ctx_for(*e); unsigned i = nargs; for (auto m : e->m_expl_args) { - if (i == 0) + if (i == 0) { + trace_failure(c, "too many explicit arguments"); throw app_builder_exception(); + } --i; if (!m_ctx->relaxed_assign(m, args[i])) { + trace_unify_failure(c, i, m, args[i]); throw app_builder_exception(); } } - if (!check_all_assigned(*e)) + if (!check_all_assigned(*e)) { + trace_failure(c, "there are missing implicit arguments"); throw app_builder_exception(); + } return m_ctx->instantiate_uvars_mvars(e->m_app); } @@ -282,8 +313,10 @@ struct app_builder::imp { expr mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) { unsigned nargs = get_nargs(mask_sz, mask); optional e = get_entry(c, mask_sz, mask); - if (!e) + if (!e) { + trace_failure(c, "failed to retrieve declaration"); throw app_builder_exception(); + } init_ctx_for(*e); unsigned i = mask_sz; unsigned j = nargs; @@ -293,13 +326,17 @@ struct app_builder::imp { if (mask[i]) { --j; expr const & m = head(it); - if (!m_ctx->relaxed_assign(m, args[j])) + if (!m_ctx->relaxed_assign(m, args[j])) { + trace_unify_failure(c, j, m, args[j]); throw app_builder_exception(); + } it = tail(it); } } - if (!check_all_assigned(*e)) + if (!check_all_assigned(*e)) { + trace_failure(c, "there are missing implicit arguments"); throw app_builder_exception(); + } return m_ctx->instantiate_uvars_mvars(e->m_app); } @@ -317,8 +354,10 @@ struct app_builder::imp { level get_level(expr const & A) { expr Type = m_ctx->relaxed_whnf(m_ctx->infer(A)); - if (!is_sort(Type)) + if (!is_sort(Type)) { + lean_trace("app_builder", tout() << "failed to infer universe level for type " << A << "\n";); throw app_builder_exception(); + } return sort_level(Type); } @@ -345,8 +384,10 @@ struct app_builder::imp { expr mk_eq_symm(expr const & H) { expr p = m_ctx->relaxed_whnf(m_ctx->infer(H)); expr lhs, rhs; - if (!is_eq(p, lhs, rhs)) + if (!is_eq(p, lhs, rhs)) { + lean_trace("app_builder", tout() << "failed to build eq.symm, equality expected:\n" << H << "\n";); throw app_builder_exception(); + } expr A = m_ctx->infer(lhs); level lvl = get_level(A); return ::lean::mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H); @@ -366,8 +407,11 @@ struct app_builder::imp { expr p1 = m_ctx->relaxed_whnf(m_ctx->infer(H1)); expr p2 = m_ctx->relaxed_whnf(m_ctx->infer(H2)); expr lhs1, rhs1, lhs2, rhs2; - if (!is_eq(p1, lhs1, rhs1) || !is_eq(p2, lhs2, rhs2)) + if (!is_eq(p1, lhs1, rhs1) || !is_eq(p2, lhs2, rhs2)) { + lean_trace("app_builder", tout() << "failed to build eq.trans, equality expected:\n" + << H1 << "\n" << H2 << "\n";); throw app_builder_exception(); + } expr A = m_ctx->infer(lhs1); level lvl = get_level(A); return ::lean::mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, lhs1, rhs1, rhs2, H1, H2}); @@ -411,6 +455,8 @@ struct app_builder::imp { } else if (auto info = m_refl_getter(relname)) { return mk_app(info->m_name, 1, &a); } else { + lean_trace("app_builder", tout() << "failed to build reflexivity proof, '" << relname + << "' is not registered as a reflexive relation\n";); throw app_builder_exception(); } } @@ -423,6 +469,8 @@ struct app_builder::imp { } else if (auto info = m_symm_getter(relname)) { return mk_app(info->m_name, 1, &H); } else { + lean_trace("app_builder", tout() << "failed to build symmetry proof, '" << relname + << "' is not registered as a symmetric relation\n";); throw app_builder_exception(); } } @@ -436,6 +484,8 @@ struct app_builder::imp { expr args[2] = {H1, H2}; return mk_app(info->m_name, 2, args); } else { + lean_trace("app_builder", tout() << "failed to build symmetry proof, '" << relname + << "' is not registered as a transitive relation\n";); throw app_builder_exception(); } } @@ -460,13 +510,17 @@ struct app_builder::imp { return H1; expr p = m_ctx->relaxed_whnf(m_ctx->infer(H2)); expr lhs, rhs; - if (!is_eq(p, lhs, rhs)) + if (!is_eq(p, lhs, rhs)) { + lean_trace("app_builder", tout() << "failed to build eq.rec, equality proof expected:\n" << H2 << "\n";); throw app_builder_exception(); + } expr A = m_ctx->infer(lhs); level A_lvl = get_level(A); expr mtype = m_ctx->relaxed_whnf(m_ctx->infer(motive)); - if (!is_pi(mtype) || !is_sort(binding_body(mtype))) + if (!is_pi(mtype) || !is_sort(binding_body(mtype))) { + lean_trace("app_builder", tout() << "failed to build eq.rec, invalid motive:\n" << motive << "\n";); throw app_builder_exception(); + } level l_1 = sort_level(binding_body(mtype)); name const & eqrec = is_standard(m_ctx->env()) ? get_eq_rec_name() : get_eq_nrec_name(); return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2}); @@ -477,13 +531,17 @@ struct app_builder::imp { return H1; expr p = m_ctx->relaxed_whnf(m_ctx->infer(H2)); expr lhs, rhs; - if (!is_eq(p, lhs, rhs)) + if (!is_eq(p, lhs, rhs)) { + lean_trace("app_builder", tout() << "failed to build eq.drec, equality proof expected:\n" << H2 << "\n";); throw app_builder_exception(); + } expr A = m_ctx->infer(lhs); level A_lvl = get_level(A); expr mtype = m_ctx->relaxed_whnf(m_ctx->infer(motive)); - if (!is_pi(mtype) || !is_pi(binding_body(mtype)) || !is_sort(binding_body(binding_body(mtype)))) + if (!is_pi(mtype) || !is_pi(binding_body(mtype)) || !is_sort(binding_body(binding_body(mtype)))) { + lean_trace("app_builder", tout() << "failed to build eq.drec, invalid motive:\n" << motive << "\n";); throw app_builder_exception(); + } level l_1 = sort_level(binding_body(binding_body(mtype))); name const & eqrec = is_standard(m_ctx->env()) ? get_eq_drec_name() : get_eq_rec_name(); return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2}); @@ -542,45 +600,68 @@ struct app_builder::imp { return mk_app(get_not_name(), {H}); } + void trace_inst_failure(expr const & A, char const * n) { + lean_trace("app_builder", + tout() << "failed to build instance of '" << n << "' for:\n" << A << "\n";); + } + expr mk_partial_add(expr const & A) { level lvl = get_level(A); auto A_has_add = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_add_name(), {lvl}), A)); - if (!A_has_add) throw app_builder_exception(); + if (!A_has_add) { + trace_inst_failure(A, "has_add"); + throw app_builder_exception(); + } return ::lean::mk_app(mk_constant(get_add_name(), {lvl}), A, *A_has_add); } expr mk_partial_mul(expr const & A) { level lvl = get_level(A); auto A_has_mul = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_mul_name(), {lvl}), A)); - if (!A_has_mul) throw app_builder_exception(); + if (!A_has_mul) { + trace_inst_failure(A, "has_mul"); + throw app_builder_exception(); + } return ::lean::mk_app(mk_constant(get_mul_name(), {lvl}), A, *A_has_mul); } expr mk_zero(expr const & A) { level lvl = get_level(A); auto A_has_zero = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_zero_name(), {lvl}), A)); - if (!A_has_zero) throw app_builder_exception(); + if (!A_has_zero) { + trace_inst_failure(A, "has_zero"); + throw app_builder_exception(); + } return ::lean::mk_app(mk_constant(get_zero_name(), {lvl}), A, *A_has_zero); } expr mk_one(expr const & A) { level lvl = get_level(A); auto A_has_one = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_one_name(), {lvl}), A)); - if (!A_has_one) throw app_builder_exception(); + if (!A_has_one) { + trace_inst_failure(A, "has_one"); + throw app_builder_exception(); + } return ::lean::mk_app(mk_constant(get_one_name(), {lvl}), A, *A_has_one); } expr mk_partial_left_distrib(expr const & A) { level lvl = get_level(A); auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_distrib_name(), {lvl}), A)); - if (!A_distrib) throw app_builder_exception(); + if (!A_distrib) { + trace_inst_failure(A, "distrib"); + throw app_builder_exception(); + } return ::lean::mk_app(mk_constant(get_left_distrib_name(), {lvl}), A, *A_distrib); } expr mk_partial_right_distrib(expr const & A) { level lvl = get_level(A); auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_distrib_name(), {lvl}), A)); - if (!A_distrib) throw app_builder_exception(); + if (!A_distrib) { + trace_inst_failure(A, "distrib"); + throw app_builder_exception(); + } return ::lean::mk_app(mk_constant(get_right_distrib_name(), {lvl}), A, *A_distrib); } @@ -751,4 +832,8 @@ expr app_builder::mk_false_rec(expr const & c, expr const & H) { void app_builder::set_local_instances(list const & insts) { m_ptr->m_ctx->set_local_instances(insts); } +void initialize_app_builder() { + register_trace_class("app_builder"); +} +void finalize_app_builder() {} } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index d17c35f60..9e3ccd430 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -173,4 +173,6 @@ public: the initialization can be performed outside. */ void set_local_instances(list const & insts); }; +void initialize_app_builder(); +void finalize_app_builder(); } diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp index 15cc52913..d228713f0 100644 --- a/src/library/congr_lemma_manager.cpp +++ b/src/library/congr_lemma_manager.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "library/util.h" +#include "library/trace.h" #include "library/locals.h" #include "library/constants.h" #include "library/replace_visitor.h" @@ -145,6 +146,16 @@ struct congr_lemma_manager::imp { } } + void trace_too_many_arguments(expr const & fn, unsigned nargs) { + lean_trace("congruence_manager", tout() << "failed to generate lemma for (" << fn << ") with " << nargs + << " arguments, too many arguments\n";); + } + + void trace_app_builder_failure(expr const & fn) { + lean_trace("congruence_manager", tout() << "failed to generate lemma for (" << fn << "), " + << " failed to build proof (enable 'trace.app_builder' for details\n";); + } + optional mk_congr_simp(expr const & fn, buffer const & pinfos, buffer const & kinds) { try { expr fn_type = relaxed_whnf(infer(fn)); @@ -155,6 +166,7 @@ struct congr_lemma_manager::imp { buffer hyps; // contains lhss + rhss + eqs for (unsigned i = 0; i < pinfos.size(); i++) { if (!is_pi(fn_type)) { + trace_too_many_arguments(fn, pinfos.size()); return optional(); } expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type)); @@ -198,6 +210,7 @@ struct congr_lemma_manager::imp { congr_proof = Fun(hyps, congr_proof); return optional(congr_type, congr_proof, to_list(kinds)); } catch (app_builder_exception &) { + trace_app_builder_failure(fn); return optional(); } } @@ -215,6 +228,7 @@ struct congr_lemma_manager::imp { buffer simp_lemma_args; for (unsigned i = 0; i < pinfos.size(); i++) { if (!is_pi(fn_type1)) { + trace_too_many_arguments(fn, pinfos.size()); return optional(); } expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type1), binding_domain(fn_type1)); @@ -292,6 +306,7 @@ struct congr_lemma_manager::imp { expr congr_proof = Fun(hyps, m_builder.mk_eq_trans(pr1, pr2)); return optional(congr_type, congr_proof, to_list(kinds)); } catch (app_builder_exception &) { + trace_app_builder_failure(fn); return optional(); } } @@ -475,6 +490,7 @@ public: m_rel_cache[is_iff].insert(mk_pair(k, res)); return optional(res); } catch (app_builder_exception &) { + trace_app_builder_failure(R); return optional(); } } @@ -517,4 +533,11 @@ auto congr_lemma_manager::mk_rel_iff_congr(expr const & R) -> optional { auto congr_lemma_manager::mk_rel_eq_congr(expr const & R) -> optional { return m_ptr->mk_rel_eq_congr(R); } + +void initialize_congr_lemma_manager() { + register_trace_class("congruence_manager"); +} + +void finalize_congr_lemma_manager() { +} } diff --git a/src/library/congr_lemma_manager.h b/src/library/congr_lemma_manager.h index e912a0df3..6ea1581b7 100644 --- a/src/library/congr_lemma_manager.h +++ b/src/library/congr_lemma_manager.h @@ -52,4 +52,7 @@ public: R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) */ optional mk_rel_eq_congr(expr const & R); }; + +void initialize_congr_lemma_manager(); +void finalize_congr_lemma_manager(); } diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index a6de6a786..46b687f86 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -47,6 +47,8 @@ Author: Leonardo de Moura #include "library/norm_num.h" #include "library/class_instance_resolution.h" #include "library/type_context.h" +#include "library/congr_lemma_manager.h" +#include "library/app_builder.h" namespace lean { void initialize_library_module() { @@ -93,9 +95,13 @@ void initialize_library_module() { initialize_class_instance_resolution(); initialize_type_context(); initialize_light_rule_set(); + initialize_congr_lemma_manager(); + initialize_app_builder(); } void finalize_library_module() { + finalize_app_builder(); + finalize_congr_lemma_manager(); finalize_light_rule_set(); finalize_type_context(); finalize_class_instance_resolution();