From 150d285b397ea667afdf716ece4ee813ac596301 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2014 14:00:20 -0700 Subject: [PATCH] fix (library/unifier): occurs_context_check Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 86 ++++++++++++++++++++++++++++------------- tests/lean/run/e16.lean | 28 ++++++++++++++ 2 files changed, 88 insertions(+), 26 deletions(-) create mode 100644 tests/lean/run/e16.lean diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 90be060472..08ae19db01 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -11,10 +11,12 @@ Author: Leonardo de Moura #include "util/luaref.h" #include "util/lazy_list_fn.h" #include "util/sstream.h" +#include "util/lbool.h" #include "kernel/for_each_fn.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/type_checker.h" +#include "library/occurs.h" #include "library/unifier.h" #include "library/kernel_bindings.h" @@ -44,31 +46,54 @@ optional is_simple_meta(expr const & e, buffer & args) { return some_expr(m); } -// Return true if \c e does not contain the metavariable \c m, and all local -// constants are in \c e are in \c locals -bool occurs_context_check(expr const & e, expr const & m, buffer const & locals) { +// Return true if all local constants in \c e are in locals +bool context_check(expr const & e, buffer const & locals) { bool failed = false; for_each(e, [&](expr const & e, unsigned) { if (failed) return false; if (is_local(e) && std::find(locals.begin(), locals.end(), e) == locals.end()) { - // right-hand-side contains variable that is not in the scope - // of metavariable. failed = true; return false; } - if (is_metavar(e) && e == m) { - // occurs-check failed - failed = true; - return false; - } - // we only need to continue exploring e if it contains - // metavariables and/or local constants. - return has_metavar(e) || has_local(e); + return true; }); return !failed; } +// Return +// - l_undef if \c e contains a metavariable application that contains +// a local constant not in locals +// - l_true if \c e does not contain the metavariable \c m, and all local +// 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 +// not in locals that is not in a metavariable application. +lbool occurs_context_check(expr const & e, expr const & m, buffer const & locals) { + expr root = e; + lbool r = l_true; + for_each(e, [&](expr const & e, unsigned) { + if (r == l_false) { + return false; + } else if (is_local(e) && std::find(locals.begin(), locals.end(), e) == locals.end()) { + // right-hand-side contains variable that is not in the scope + // of metavariable. + r = l_false; + 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; + return false; // do not visit children + } else { + // we only need to continue exploring e if it contains + // metavariables and/or local constants. + return has_metavar(e) || has_local(e); + } + }); + return r; +} + // Create a lambda abstraction by abstracting the local constants \c locals in \c e expr lambda_abstract_locals(expr const & e, buffer const & locals) { expr v = abstract_locals(e, locals.size(), locals.data()); @@ -86,14 +111,18 @@ static std::pair unify_simple_core(substitution cons lean_assert(is_meta(lhs)); buffer args; auto m = is_simple_meta(lhs, args); - if (!m || (is_meta(rhs) && get_app_fn(rhs) == *m)) { + if (!m || is_meta(rhs)) { return mk_pair(unify_status::Unsupported, s); - } else if (!occurs_context_check(rhs, *m, args)) { - return mk_pair(unify_status::Failed, s); } else { - expr v = lambda_abstract_locals(rhs, args); - return mk_pair(unify_status::Solved, s.assign(mlocal_name(*m), v, j)); + switch (occurs_context_check(rhs, *m, args)) { + case l_false: return mk_pair(unify_status::Failed, s); + case l_undef: mk_pair(unify_status::Unsupported, s); + case l_true: { + expr v = lambda_abstract_locals(rhs, args); + return mk_pair(unify_status::Solved, s.assign(mlocal_name(*m), v, j)); + }} } + lean_unreachable(); // LCOV_EXCL_LINE } std::pair unify_simple(substitution const & s, expr const & lhs, expr const & rhs, justification const & j) { @@ -509,18 +538,23 @@ struct unifier_fn { return Continue; buffer locals; auto m = is_simple_meta(lhs, locals); - if (!m || (is_meta(rhs) && get_app_fn(rhs) == *m)) + if (!m || is_meta(rhs)) return Continue; - if (!occurs_context_check(rhs, *m, locals)) { + switch (occurs_context_check(rhs, *m, locals)) { + case l_false: set_conflict(j); return Failed; + case l_undef: + return Continue; + case l_true: + lean_assert(!m_subst.is_assigned(*m)); + if (assign(*m, lambda_abstract_locals(rhs, locals), j)) { + return Assigned; + } else { + return Failed; + } } - lean_assert(!m_subst.is_assigned(*m)); - if (assign(*m, lambda_abstract_locals(rhs, locals), j)) { - return Assigned; - } else { - return Failed; - } + lean_unreachable(); // LCOV_EXCL_LINE } /** \brief Process an equality constraints. */ diff --git a/tests/lean/run/e16.lean b/tests/lean/run/e16.lean new file mode 100644 index 0000000000..81fa79c6ee --- /dev/null +++ b/tests/lean/run/e16.lean @@ -0,0 +1,28 @@ +inductive nat : Type := +| zero : nat +| succ : nat → nat + +inductive list (A : Type) : Type := +| nil : list A +| cons : A → list A → list A + +check nil +check nil.{1} +check @nil.{1} nat +check @nil nat + +check cons zero nil + +inductive vector (A : Type) : nat → Type := +| vnil : vector A zero +| vcons : forall {n : nat}, A → vector A n → vector A (succ n) + +check vcons zero vnil +variable n : nat +check vcons n vnil + +check vector_rec + +definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A +:= vector_rec nil (fun n a v l, cons a l) v +