From 98aefca014957b059102f22e864f736509b49f6e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Aug 2016 13:49:54 -0700 Subject: [PATCH] fix(library/local_context): depends_on should take into account assigned metavariables --- src/library/local_context.cpp | 47 ++++++++++++++++++-------- src/library/local_context.h | 12 ++++--- src/library/tactic/cases_tactic.cpp | 2 +- src/library/tactic/clear_tactic.cpp | 4 +-- src/library/tactic/revert_tactic.cpp | 3 +- src/library/type_context.cpp | 8 ++--- tests/lean/dep_bug.lean | 16 +++++++++ tests/lean/dep_bug.lean.expected.out | 17 ++++++++++ tests/lean/focus_tac.lean.expected.out | 2 +- 9 files changed, 83 insertions(+), 28 deletions(-) create mode 100644 tests/lean/dep_bug.lean create mode 100644 tests/lean/dep_bug.lean.expected.out diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index 95d6ec9866..d1e1375a9c 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/pp_options.h" #include "library/local_context.h" #include "library/metavar_context.h" +#include "library/trace.h" namespace lean { static name * g_local_prefix; @@ -49,39 +50,58 @@ expr local_decl::mk_ref() const { return mk_local_ref(m_ptr->m_name, m_ptr->m_pp_name, m_ptr->m_bi); } -bool depends_on(expr const & e, unsigned num, expr const * locals) { +static bool depends_on_core(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals, + name_set & visited_mvars) { lean_assert(std::all_of(locals, locals+num, is_local_decl_ref)); - if (!has_local(e)) + if (!has_local(e) && !has_expr_metavar(e)) return false; bool found = false; for_each(e, [&](expr const & e, unsigned) { if (found) return false; - if (!has_local(e)) return false; + if (!has_local(e) && !has_expr_metavar(e)) return false; if (is_local_decl_ref(e) && std::any_of(locals, locals+num, [&](expr const & l) { return mlocal_name(e) == mlocal_name(l); })) { found = true; return false; } + if (is_metavar_decl_ref(e)) { + if (auto v = mctx.get_assignment(e)) { + if (!visited_mvars.contains(mlocal_name(e))) { + visited_mvars.insert(mlocal_name(e)); + if (depends_on_core(*v, mctx, num, locals, visited_mvars)) { + found = true; + return false; + } + } + } + } return true; }); return found; } -bool depends_on(local_decl const & d, unsigned num, expr const * locals) { - if (depends_on(d.get_type(), num, locals)) +bool depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals) { + name_set visited_mvars; + return depends_on_core(e, mctx, num, locals, visited_mvars); +} + +bool depends_on(local_decl const & d, metavar_context const & mctx, unsigned num, expr const * locals) { + name_set visited_mvars; + if (depends_on_core(d.get_type(), mctx, num, locals, visited_mvars)) return true; - if (auto v = d.get_value()) - return depends_on(*v, num, locals); + if (auto v = d.get_value()) { + return depends_on_core(*v, mctx, num, locals, visited_mvars); + } return false; } -bool depends_on(expr const & e, buffer const & locals) { - return depends_on(e, locals.size(), locals.data()); +bool depends_on(expr const & e, metavar_context const & mctx, buffer const & locals) { + return depends_on(e, mctx, locals.size(), locals.data()); } -bool depends_on(local_decl const & d, buffer const & locals) { - return depends_on(d, locals.size(), locals.data()); +bool depends_on(local_decl const & d, metavar_context const & mctx, buffer const & locals) { + return depends_on(d, mctx, locals.size(), locals.data()); } expr local_context::mk_local_decl(name const & n, name const & ppn, expr const & type, optional const & value, binder_info const & bi) { @@ -167,13 +187,13 @@ bool local_context::rename_user_name(name const & from, name const & to) { } } -optional local_context::has_dependencies(local_decl const & d) const { +optional local_context::has_dependencies(local_decl const & d, metavar_context const & mctx) const { lean_assert(get_local_decl(d.get_name())); expr l = d.mk_ref(); optional r; for_each_after(d, [&](local_decl const & d2) { if (r) return; - if (depends_on(d2, 1, &l)) + if (depends_on(d2, mctx, 1, &l)) r = d2; }); return r; @@ -181,7 +201,6 @@ optional local_context::has_dependencies(local_decl const & d) const void local_context::clear(local_decl const & d) { lean_assert(get_local_decl(d.get_name())); - lean_assert(!has_dependencies(d)); m_idx2local_decl.erase(d.get_idx()); m_name2local_decl.erase(d.get_name()); } diff --git a/src/library/local_context.h b/src/library/local_context.h index 4bc3fc4084..6c565b72f1 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -57,10 +57,12 @@ public: bool is_local_decl_ref(expr const & e); -bool depends_on(expr const & e, unsigned num, expr const * locals); -bool depends_on(local_decl const & d, unsigned num, expr const * locals); -bool depends_on(expr const & e, buffer const & locals); -bool depends_on(local_decl const & d, buffer const & locals); +class metavar_context; + +bool depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals); +bool depends_on(local_decl const & d, metavar_context const & mctx, unsigned num, expr const * locals); +bool depends_on(expr const & e, metavar_context const & mctx, buffer const & locals); +bool depends_on(local_decl const & d, metavar_context const & mctx, buffer const & locals); class metavar_context; @@ -106,7 +108,7 @@ public: /** \brief Return a non-none iff other local decls depends on \c d. If the result is not none, then it is the name of the local decl that depends on d. \pre \c d is in this local context. */ - optional has_dependencies(local_decl const & d) const; + optional has_dependencies(local_decl const & d, metavar_context const & mctx) const; /** \brief Return an unused hypothesis "user name" with the given prefix, the suffix is an unsigned >= idx. */ diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 5b82b55945..4efb56b27a 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -138,7 +138,7 @@ struct cases_tactic_fn { lctx.for_each_after(*h_decl, [&](local_decl const & h1) { if (!ok) return; /* h1 must not depend on the indices */ - if (depends_on(h1, m_nindices, args.end() - m_nindices)) + if (depends_on(h1, m_mctx, m_nindices, args.end() - m_nindices)) ok = false; }); return ok; diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index 06ae790004..cc61de545d 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -18,9 +18,9 @@ expr clear(metavar_context & mctx, expr const & mvar, expr const & H) { optional d = lctx.get_local_decl(H); if (!d) throw exception(sstream() << "clear tactic failed, unknown '" << local_pp_name(H) << "' hypothesis"); - if (depends_on(g->get_type(), 1, &H)) + if (depends_on(g->get_type(), mctx, 1, &H)) throw exception(sstream() << "clear tactic failed, target type depends on '" << local_pp_name(H) << "'"); - if (optional d2 = lctx.has_dependencies(*d)) + if (optional d2 = lctx.has_dependencies(*d, mctx)) throw exception(sstream() << "clear tactic failed, hypothesis '" << d2->get_pp_name() << "' depends on '" << local_pp_name(H) << "'"); lctx.clear(*d); expr new_mvar = mctx.mk_metavar_decl(lctx, g->get_type()); diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index 63e412ebc8..0a65c1eefe 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -35,7 +35,8 @@ vm_obj revert(list const & ls, tactic_state const & s) { if (lctx.get_local_decl(l)) { locals.push_back(l); } else { - return mk_tactic_exception(sstream() << "revert tactic failed, unknown '" << local_pp_name(l) << "' hypothesis", s); + return mk_tactic_exception(sstream() << "revert tactic failed, unknown '" + << local_pp_name(l) << "' hypothesis", s); } } tactic_state new_s = revert(locals, s); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 6e0f2c30e9..f03528a0ae 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -267,7 +267,7 @@ pair type_context::revert_core(buffer & to_revert, lo } } /* We may still need to revert d if it depends on locals already in reverted */ - if (depends_on(d, to_revert)) { + if (depends_on(d, m_mctx, to_revert)) { to_revert.push_back(d.mk_ref()); } }); @@ -320,13 +320,13 @@ expr type_context::mk_binding(bool is_pi, unsigned num_locals, expr const * loca for (unsigned i = 0; i < num_locals; i++) { local_decl const & decl = *m_lctx.get_local_decl(locals[i]); decls.push_back(decl); - types.push_back(abstract_locals(decl.get_type(), i, locals)); + types.push_back(abstract_locals(instantiate_mvars(decl.get_type()), i, locals)); if (auto v = decl.get_value()) - values.push_back(some_expr(abstract_locals(*v, i, locals))); + values.push_back(some_expr(abstract_locals(instantiate_mvars(*v), i, locals))); else values.push_back(none_expr()); } - expr new_e = abstract_locals(e, num_locals, locals); + expr new_e = abstract_locals(instantiate_mvars(e), num_locals, locals); lean_assert(types.size() == values.size()); unsigned i = types.size(); while (i > 0) { diff --git a/tests/lean/dep_bug.lean b/tests/lean/dep_bug.lean new file mode 100644 index 0000000000..0d72e222d3 --- /dev/null +++ b/tests/lean/dep_bug.lean @@ -0,0 +1,16 @@ +open tactic + + + +example (a b c : nat) (H : c = b) : a + c = a + b := +by do + N ← to_expr `(nat), + define `v N, + trace_state, + trace "------------", + to_expr `(a + b) >>= exact, + trace_state, + trace "------------", + get_local `H >>= subst, + trace_state, + to_expr `(eq.refl v) >>= exact diff --git a/tests/lean/dep_bug.lean.expected.out b/tests/lean/dep_bug.lean.expected.out new file mode 100644 index 0000000000..ee0131e0dc --- /dev/null +++ b/tests/lean/dep_bug.lean.expected.out @@ -0,0 +1,17 @@ +a b c : ℕ, +H : c = b +⊢ ℕ + +a b c : ℕ, +H : c = b, +v : ℕ := ?m_1 +⊢ a + c = a + b +------------ +a b c : ℕ, +H : c = b, +v : ℕ := a + b +⊢ a + c = a + b +------------ +a c : ℕ, +v : ℕ := a + c +⊢ a + c = a + c diff --git a/tests/lean/focus_tac.lean.expected.out b/tests/lean/focus_tac.lean.expected.out index ed8eda523f..3cdd9294e9 100644 --- a/tests/lean/focus_tac.lean.expected.out +++ b/tests/lean/focus_tac.lean.expected.out @@ -27,5 +27,5 @@ a : ℕ ⊢ ℕ ---- after focus tac ---- a : ℕ, -x : ℕ := ?m_1 +x : ℕ := a ⊢ a = a