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

refactor(library/unifier): add is_def_eq alias

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-03 18:01:48 -07:00
parent b5f63e78ca
commit c854ad3d65
1 changed files with 12 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/library/unifier.cpp
View file

@ -479,6 +479,15 @@ struct unifier_fn {
add_cnstr(c, mlvl_occs, mvar_occs, g_first_very_delayed); add_cnstr(c, mlvl_occs, mvar_occs, g_first_very_delayed);
} }
bool is_def_eq(expr const & t1, expr const & t2, justification const & j) {
if (m_tc.is_def_eq(t1, t2, j)) {
return true;
} else {
set_conflict(j);
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.
@ -491,10 +500,8 @@ struct unifier_fn {
expr v_type = m_tc.infer(v); expr v_type = m_tc.infer(v);
if (in_conflict()) if (in_conflict())
return false; return false;
if (!m_tc.is_def_eq(m_type, v_type, j)) { if (!is_def_eq(m_type, v_type, j))
set_conflict(j);
return false; return false;
}
auto it = m_mvar_occs.find(mlocal_name(m)); auto it = m_mvar_occs.find(mlocal_name(m));
if (it) { if (it) {
cnstr_idx_set s = *it; cnstr_idx_set s = *it;
@ -575,12 +582,7 @@ struct unifier_fn {
// Update justification using the justification of the instantiated metavariables // Update justification using the justification of the instantiated metavariables
justification new_jst = mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second); justification new_jst = mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second);
if (!has_metavar(lhs) && !has_metavar(rhs)) { if (!has_metavar(lhs) && !has_metavar(rhs)) {
if (!m_tc.is_def_eq(lhs, rhs, new_jst)) { return is_def_eq(lhs, rhs, new_jst);
set_conflict(new_jst);
return false; // trivial failure
} else {
return true;
}
} }
// Handle higher-order pattern matching. // Handle higher-order pattern matching.
@ -596,12 +598,7 @@ struct unifier_fn {
// If lhs or rhs were updated, then invoke is_def_eq again. // If lhs or rhs were updated, then invoke is_def_eq again.
if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) { if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) {
// some metavariables were instantiated, try is_def_eq again // some metavariables were instantiated, try is_def_eq again
if (m_tc.is_def_eq(lhs, rhs, new_jst)) { return is_def_eq(lhs, rhs, new_jst);
return true;
} else {
set_conflict(new_jst);
return false;
}
} }
if (is_meta(lhs) && is_meta(rhs)) { if (is_meta(lhs) && is_meta(rhs)) {