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

fix(library/type_context): methods assign and force_assign were not processing postponed constraints

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-12 18:52:31 -08:00
parent 1e436b8b3e
commit 15cd92f89f
2 changed files with 18 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/library/type_context.cpp
View file

@ -685,7 +685,7 @@ bool type_context::is_def_eq_proof_irrel(expr const & e1, expr const & e2) {
/** \brief Given \c ma of the form <tt>?m t_1 ... t_n</tt>, (try to) assign
?m to (an abstraction of) v. Return true if success and false otherwise. */
bool type_context::process_assignment(expr const & ma, expr const & v) {
bool type_context::process_assignment_core(expr const & ma, expr const & v) {
buffer<expr> args;
expr const & m = get_app_args(ma, args);
buffer<expr> locals;
@ -754,6 +754,20 @@ bool type_context::process_assignment(expr const & ma, expr const & v) {
}
}
bool type_context::process_assignment(expr const & ma, expr const & v) {
scope s(*this);
unsigned psz = m_postponed.size();
if (!process_assignment_core(ma, v)) {
return false;
}
if (process_postponed(psz)) {
m_postponed.resize(psz);
s.commit();
return true;
}
return false;
}
bool type_context::assign(expr const & ma, expr const & v) {
expr const & f = get_app_fn(ma);
if (is_assigned(f)) {
@ -777,7 +791,7 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
if (is_assigned(f1)) {
return to_lbool(is_def_eq_core(subst_mvar(e1), e2));
} else {
return to_lbool(process_assignment(e1, e2));
return to_lbool(process_assignment_core(e1, e2));
}
}
@ -786,7 +800,7 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
if (is_assigned(f2)) {
return to_lbool(is_def_eq_core(e1, subst_mvar(e2)));
} else {
return to_lbool(process_assignment(e2, e1));
return to_lbool(process_assignment_core(e2, e1));
}
}

1
src/library/type_context.h
View file

@ -188,6 +188,7 @@ class type_context {
bool is_def_eq_proof_irrel(expr const & e1, expr const & e2);
expr subst_mvar(expr const & e);
bool process_assignment_core(expr const & ma, expr const & v);
bool process_assignment(expr const & ma, expr const & v);
enum class reduction_status { Continue, DefUnknown, DefEqual, DefDiff };
reduction_status lazy_delta_reduction_step(expr & t_n, expr & s_n);