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

feat(library/unifier): eagerly apply substitution to improve quick failure

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-03 12:58:30 -07:00
parent db0ef64c04
commit 079592c446
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/unifier.cpp
View file

@ -1193,7 +1193,9 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
unifier_plugin const & p, unsigned max_steps) {
name_generator new_ngen(ngen);
type_checker tc(env, new_ngen.mk_child());
if (!tc.is_def_eq(lhs, rhs))
expr _lhs = s.instantiate(lhs);
expr _rhs = s.instantiate(rhs);
if (!tc.is_def_eq(_lhs, _rhs))
return lazy_list<substitution>();
buffer<constraint> cs;
while (auto c = tc.next_cnstr()) {