From fdc30e3097ce811ddf7bf8d4e672842476b8e030 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 11 Sep 2019 19:27:15 +0200 Subject: [PATCH] chore(library/type_context): revert "simple instance pre-filtering" This reverts commit ab2e66e4a3df09f761cbfdd56852f8bb3ff160ee. This hack is not immediately needed anymore and will hopefully be replaced with a much better design in the future --- src/library/type_context.cpp | 22 ---------------------- 1 file changed, 22 deletions(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 7e61226d50..190d5f5a62 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -3445,28 +3445,6 @@ struct instance_synthesizer { r = mk_app(r, new_arg); type = instantiate(binding_body(type), new_arg); } - - /* simple pre-filter: Discard applications of the same class where the last argument's heads are different - * and both nonreducible. - * Furthermore, we don't even list these "trivially non-applicable instances" in the class_instances trace, - * which can drastically reduce the noise in it. */ - if (is_app(mvar_type)) { - expr const & mvar_type_fn = get_app_fn(mvar_type); - expr const & type_fn = get_app_fn(type); - if (is_const(mvar_type_fn) && is_const(type_fn) && const_name(mvar_type_fn) == const_name(type_fn)) { - auto const & m_head = beta_reduce(get_app_fn(m_ctx.instantiate_mvars(app_arg(mvar_type)))); - auto const & t_head = get_app_fn(app_arg(type)); - if (is_const(m_head) && is_const(t_head) && const_name(m_head) != const_name(t_head) && - !m_ctx.is_delta(m_head) && !m_ctx.is_projection(m_head) && - !m_ctx.is_delta(t_head) && !m_ctx.is_projection(t_head)) { - // lean_trace_plain("class_instances", - // scope_trace_env scope(m_ctx.env(), m_ctx); - // tout() << "PRE-FILTER: " << const_name(m_head) << " " << const_name(t_head) << "\n";); - return false; - } - } - } - lean_trace_plain("class_instances", scope_trace_env scope(m_ctx.env(), m_ctx); trace(e.m_depth, mk_app(mvar, locals.as_buffer()), mvar_type, r););