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

refactor(kernel/default_converter): move delay_check code to postpone_is_def_eq method

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-22 13:59:32 -07:00
parent cfafc90cc0
commit a2389fb664
2 changed files with 16 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/kernel/default_converter.cpp
View file

@ -575,6 +575,18 @@ lbool default_converter::reduce_def_eq(expr & t_n, expr & s_n, constraint_seq &
}
}
bool default_converter::postpone_is_def_eq(expr const & t, expr const & s) {
if (has_expr_metavar(t) || has_expr_metavar(s)) {
optional<declaration> d_t = is_delta(t);
optional<declaration> d_s = is_delta(s);
if (d_t && d_s && is_eqp(*d_t, *d_s))
return true;
else if (is_stuck(t) && is_stuck(s))
return true;
}
return false;
}
pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, expr const & s) {
check_system("is_definitionally_equal");
constraint_seq cs;
@ -601,19 +613,10 @@ pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, exp
if (is_local(t_n) && is_local(s_n) && mlocal_name(t_n) == mlocal_name(s_n))
return to_bcs(true, cs);
optional<declaration> d_t, d_s;
bool delay_check = false;
if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) {
d_t = is_delta(t_n);
d_s = is_delta(s_n);
if (d_t && d_s && is_eqp(*d_t, *d_s))
delay_check = true;
else if (is_stuck(t_n) && is_stuck(s_n))
delay_check = true;
}
bool postpone = postpone_is_def_eq(t_n, s_n);
// At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance)
if (!delay_check && is_def_eq_app(t_n, s_n, cs))
if (!postpone && is_def_eq_app(t_n, s_n, cs))
return to_bcs(true, cs);
if (try_eta_expansion(t_n, s_n, cs))
@ -623,7 +626,7 @@ pair<bool, constraint_seq> default_converter::is_def_eq_core(expr const & t, exp
if (is_def_eq_proof_irrel(t, s, pi_cs))
return to_bcs(true, pi_cs);
if (is_stuck(t_n) || is_stuck(s_n) || delay_check) {
if (is_stuck(t_n) || is_stuck(s_n) || postpone) {
cs += constraint_seq(mk_eq_cnstr(t_n, s_n, m_jst->get()));
return to_bcs(true, cs);
}

1
src/kernel/default_converter.h
View file

@ -84,6 +84,7 @@ protected:
reduction_status ext_reduction_step(expr & t_n, expr & s_n, constraint_seq & cs);
virtual lbool reduce_def_eq(expr & t_n, expr & s_n, constraint_seq & cs);
virtual bool postpone_is_def_eq(expr const & t, expr const & s);
public:
default_converter(environment const & env, bool memoize = true);