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

fix(library/unifier): bug in process_delta

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-16 04:55:09 +01:00
parent c8849d42e9
commit 6ddba9c276
1 changed files with 25 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/library/unifier.cpp
View file

@ -387,6 +387,7 @@ struct unifier_fn {
return cidx; return cidx;
} }
/** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j */
bool is_def_eq(expr const & t1, expr const & t2, justification const & j) { bool is_def_eq(expr const & t1, expr const & t2, justification const & j) {
if (m_tc->is_def_eq(t1, t2, j)) { if (m_tc->is_def_eq(t1, t2, j)) {
return true; return true;
@ -396,6 +397,22 @@ struct unifier_fn {
} }
} }
/** \brief Check if \c t1 and \c t2 are definitionally, and accumulate constraints in \c new_cs
\pre m_tc must not have pending constraints
*/
bool is_def_eq(expr const & t1, expr const & t2, justification const & j, buffer<constraint> & new_cs) {
type_checker::scope s(*m_tc);
lean_assert(!m_tc->next_cnstr());
if (m_tc->is_def_eq(t1, t2, j)) {
while (auto c = m_tc->next_cnstr())
new_cs.push_back(*c);
return true;
} else {
return false;
}
}
/** /**
\brief Assign \c v to metavariable \c m with justification \c j. \brief Assign \c v to metavariable \c m with justification \c j.
The type of v and m are inferred, and is_def_eq is invoked. The type of v and m are inferred, and is_def_eq is invoked.
@ -859,15 +876,18 @@ struct unifier_fn {
return false; return false;
} }
justification a = mk_assumption_justification(m_next_assumption_idx); justification a;
// add case_split for t =?= s // add case_split for t =?= s
expr lhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), const_levels(lhs_fn)); expr lhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), const_levels(lhs_fn));
expr rhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), const_levels(rhs_fn)); expr rhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), const_levels(rhs_fn));
expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data()); expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data());
expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data()); expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data());
constraints cs2(mk_eq_cnstr(t, s, j)); buffer<constraint> cs2;
add_case_split(std::unique_ptr<case_split>(new simple_case_split(*this, j, list<constraints>(cs2)))); if (is_def_eq(t, s, j, cs2)) {
// create a case split
a = mk_assumption_justification(m_next_assumption_idx);
add_case_split(std::unique_ptr<case_split>(new simple_case_split(*this, j, to_list(cs2.begin(), cs2.end()))));
}
// process first case // process first case
justification new_j = mk_composite1(j, a); justification new_j = mk_composite1(j, a);
@ -1252,6 +1272,7 @@ struct unifier_fn {
} else { } else {
auto r = instantiate_metavars(c); auto r = instantiate_metavars(c);
c = r.first; c = r.first;
lean_assert(!m_tc->next_cnstr());
bool modified = r.second; bool modified = r.second;
if (is_level_eq_cnstr(c)) { if (is_level_eq_cnstr(c)) {
if (modified) if (modified)