michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/default_converter): add "eager" proof irrelevance optimization

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-29 19:10:39 -07:00
parent b5444c1314
commit acc0832928
1 changed files with 23 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/kernel/default_converter.cpp
View file

@ -587,6 +587,21 @@ bool default_converter::postpone_is_def_eq(expr const & t, expr const & s) {
return false;
}
/** \brief Return true if we should try proof irrelevance eagerly.
\remark: We do it whenever t and s do not contain metavariables and one of them is a theorem application.
*/
static bool try_eager_proof_irrel(environment const & env, expr const & t, expr const & s) {
if (!env.prop_proof_irrel())
return false;
if (has_expr_metavar(t) || has_expr_metavar(s))
return false;
expr const & f_t = get_app_fn(t);
if (is_constant(f_t) && env.get(const_name(f_t)).is_theorem())
return true;
expr const & f_s = get_app_fn(s);
return is_constant(f_s) && env.get(const_name(f_s)).is_theorem();
}
pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, expr const & s) {
check_system("is_definitionally_equal");
constraint_seq cs;
@ -598,6 +613,11 @@ pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, exp
expr t_n = whnf_core(t);
expr s_n = whnf_core(s);
constraint_seq pi_cs_1;
bool eager_proof_irrel = try_eager_proof_irrel(m_env, t, s);
if (eager_proof_irrel && is_def_eq_proof_irrel(t, s, pi_cs_1))
return to_bcs(true, pi_cs_1);
if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) {
r = quick_is_def_eq(t_n, s_n, cs);
if (r != l_undef) return to_bcs(r == l_true, cs);
@ -622,9 +642,9 @@ pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, exp
if (try_eta_expansion(t_n, s_n, cs))
return to_bcs(true, cs);
constraint_seq pi_cs;
if (is_def_eq_proof_irrel(t, s, pi_cs))
return to_bcs(true, pi_cs);
constraint_seq pi_cs_2;
if (!eager_proof_irrel && is_def_eq_proof_irrel(t, s, pi_cs_2))
return to_bcs(true, pi_cs_2);
if (is_stuck(t_n) || is_stuck(s_n) || postpone) {
cs += constraint_seq(mk_eq_cnstr(t_n, s_n, m_jst->get()));