max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/type_context): revert "simple instance pre-filtering"

Browse source 
This reverts commit ab2e66e4a3.

This hack is not immediately needed anymore and will hopefully be
replaced with a much better design in the future
This commit is contained in:
Sebastian Ullrich 2019-09-11 19:27:15 +02:00
parent 2901195790
commit fdc30e3097
1 changed files with 0 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/library/type_context.cpp
View file

@ -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););