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

fix(library/unifier): catch type error when checking is_def_eq of type incorrect expressions

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-09 08:43:16 -07:00
parent fd85d4702e
commit a5698a55ec
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/unifier.cpp
View file

@ -485,6 +485,7 @@ struct unifier_fn {
\remark If relax is true then opaque definitions from the main module are treated as transparent. \remark If relax is true then opaque definitions from the main module are treated as transparent.
*/ */
bool is_def_eq(expr const & t1, expr const & t2, justification const & j, bool relax) { bool is_def_eq(expr const & t1, expr const & t2, justification const & j, bool relax) {
try {
auto dcs = m_tc[relax]->is_def_eq(t1, t2, j); auto dcs = m_tc[relax]->is_def_eq(t1, t2, j);
if (!dcs.first) { if (!dcs.first) {
// std::cout << "conflict: " << t1 << " =?= " << t2 << "\n"; // std::cout << "conflict: " << t1 << " =?= " << t2 << "\n";
@ -493,6 +494,10 @@ struct unifier_fn {
} else { } else {
return process_constraints(dcs.second); return process_constraints(dcs.second);
} }
} catch (exception&) {
set_conflict(j);
return false;
}
} }
/** \brief Process the given constraints. Return true iff no conflict was detected. */ /** \brief Process the given constraints. Return true iff no conflict was detected. */