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

refactor(library/unifier): improve occurs_context_check

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-15 02:08:16 +01:00
parent 46005b4ffe
commit 29c7eeaa99
1 changed files with 14 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/library/unifier.cpp
View file

@ -68,22 +68,24 @@ bool context_check(expr const & e, buffer<expr> const & locals) {
// constants are in \c e are in \c locals. // constants are in \c e are in \c locals.
// - l_false if \c e contains \c m or it contains a local constant \c l // - l_false if \c e contains \c m or it contains a local constant \c l
// not in locals that is not in a metavariable application. // not in locals that is not in a metavariable application.
lbool occurs_context_check(expr const & e, expr const & m, buffer<expr> const & locals) { lbool occurs_context_check(substitution const & s, expr const & e, expr const & m, buffer<expr> const & locals) {
if (s.occurs(m, e))
return l_false;
expr root = e; expr root = e;
lbool r = l_true; lbool r = l_true;
for_each(e, [&](expr const & e, unsigned) { for_each(e, [&](expr const & e, unsigned) {
if (r == l_false) { if (r == l_false) {
return false; return false;
} else if (is_local(e) && std::find(locals.begin(), locals.end(), e) == locals.end()) { } else if (is_local(e)) {
// right-hand-side contains variable that is not in the scope if (std::find(locals.begin(), locals.end(), e) == locals.end()) {
// of metavariable. // right-hand-side contains variable that is not in the scope
r = l_false; // of metavariable.
return false;
} else if (is_meta(e)) {
if (!context_check(e, locals) || occurs(m, e))
r = l_undef;
if (get_app_fn(e) == m)
r = l_false; r = l_false;
}
return false; // do not visit type
} else if (is_meta(e)) {
if (!context_check(e, locals))
r = l_undef;
return false; // do not visit children return false; // do not visit children
} else { } else {
// we only need to continue exploring e if it contains // we only need to continue exploring e if it contains
@ -114,7 +116,7 @@ static std::pair<unify_status, substitution> unify_simple_core(substitution cons
if (!m || is_meta(rhs)) { if (!m || is_meta(rhs)) {
return mk_pair(unify_status::Unsupported, s); return mk_pair(unify_status::Unsupported, s);
} else { } else {
switch (occurs_context_check(rhs, *m, args)) { switch (occurs_context_check(s, rhs, *m, args)) {
case l_false: return mk_pair(unify_status::Failed, s); case l_false: return mk_pair(unify_status::Failed, s);
case l_undef: mk_pair(unify_status::Unsupported, s); case l_undef: mk_pair(unify_status::Unsupported, s);
case l_true: { case l_true: {
@ -444,7 +446,7 @@ struct unifier_fn {
auto m = is_simple_meta(lhs, locals); auto m = is_simple_meta(lhs, locals);
if (!m || is_meta(rhs)) if (!m || is_meta(rhs))
return Continue; return Continue;
switch (occurs_context_check(rhs, *m, locals)) { switch (occurs_context_check(m_subst, rhs, *m, locals)) {
case l_false: case l_false:
set_conflict(j); set_conflict(j);
return Failed; return Failed;