From df5a17cdce1cd5cc1bd3a00923655b02a4e0aa49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Nov 2014 12:06:16 -0800 Subject: [PATCH] feat(frontends/lean/placeholder_elaborator): include type in class-instance resolution trace --- src/frontends/lean/placeholder_elaborator.cpp | 6 +++--- tests/lean/run/class8.lean | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 6c6bb6615..d431f562e 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -164,7 +164,7 @@ struct placeholder_elaborator : public choice_iterator { return cons(c, to_list(cs.begin(), cs.end())); } - void trace(expr const & r) { + void trace(expr const & t, expr const & r) { if (!m_C->trace_instances()) return; auto out = diagnostic(m_C->env(), m_C->ios()); @@ -181,7 +181,7 @@ struct placeholder_elaborator : public choice_iterator { out << " "; if (m_depth > 0) out << "[" << m_depth << "] "; - out << m_meta << " := " << r << endl; + out << m_meta << " : " << t << " := " << r << endl; } optional try_instance(expr const & inst, expr const & inst_type) { @@ -216,7 +216,7 @@ struct placeholder_elaborator : public choice_iterator { type = instantiate(binding_body(type), arg); } r = Fun(locals, r); - trace(r); + trace(meta_type, r); bool relax = m_C->m_relax; constraint c = mk_eq_cnstr(m_meta, r, m_jst, relax); return optional(mk_constraints(c, cs)); diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean index aa7db0f1c..c37b209ff 100644 --- a/tests/lean/run/class8.lean +++ b/tests/lean/run/class8.lean @@ -25,6 +25,7 @@ definition assump := eassumption tactic_hint assump theorem tst {A B : Type} (H : inh B) : inh (A → B → B) +set_option elaborator.trace_instances true theorem T1 {A B C D : Type} {P : C → Prop} (a : A) (H1 : inh B) (H2 : ∃x, P x) : inh ((A → A) × B × (D → C) × Prop) := have h1 [visible] : inh A, from inh.intro a,