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

Remove cleanup_subst. The residue may still reference auxiliary variable. So, it is not safe to remove then from the resultant partial substitution.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-19 13:42:50 -07:00
parent d7cc5d2404
commit b3aa8b37f3
1 changed files with 4 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/library/ho_unifier.cpp
View file

@ -83,24 +83,8 @@ class ho_unifier::imp {
add_constraint(ctx, l, r); add_constraint(ctx, l, r);
} }
metavar_env cleanup_subst(metavar_env const & s, unsigned num_input_metavars) { list<result> save_result(list<result> const & r, metavar_env const & s, residue const & rs) {
// eliminate auxiliary metavariables return cons(result(s, rs), r);
if (!m_ho) {
return s;
} else {
metavar_env new_s;
for (unsigned i = 0; i < num_input_metavars; i++) {
new_s.mk_metavar(s.get_type(i), s.get_context(i));
expr subst = s.get_subst(i);
if (subst)
new_s.assign(i, subst);
}
return new_s;
}
}
list<result> save_result(list<result> const & r, metavar_env const & s, residue const & rs, unsigned num_input_metavars) {
return cons(result(cleanup_subst(s, num_input_metavars), rs), r);
} }
/** /**
@ -419,7 +403,6 @@ public:
} }
list<result> unify(context const & ctx, expr const & a, expr const & b, metavar_env const & menv) { list<result> unify(context const & ctx, expr const & a, expr const & b, metavar_env const & menv) {
unsigned num_metavars = menv.size();
init(ctx, a, b, menv); init(ctx, a, b, menv);
list<result> r; list<result> r;
while (!m_state_stack.empty()) { while (!m_state_stack.empty()) {
@ -429,7 +412,7 @@ public:
unsigned cq_size = cq.size(); unsigned cq_size = cq.size();
if (cq.empty()) { if (cq.empty()) {
// no constraints left to be solved // no constraints left to be solved
r = save_result(r, subst_of(top_state), residue(), num_metavars); r = save_result(r, subst_of(top_state), residue());
m_state_stack.pop_back(); m_state_stack.pop_back();
} else { } else {
// try cq_sz times to find a constraint that can be processed // try cq_sz times to find a constraint that can be processed
@ -447,7 +430,7 @@ public:
residue rs; residue rs;
for (auto c : cq) for (auto c : cq)
rs = cons(c, rs); rs = cons(c, rs);
r = save_result(r, subst_of(top_state), rs, num_metavars); r = save_result(r, subst_of(top_state), rs);
reset_delayed(); reset_delayed();
m_state_stack.pop_back(); m_state_stack.pop_back();
} }