diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index cc3cbb6b41..abe1f5b2e0 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -254,7 +254,6 @@ bool local_context::well_formed(expr const & e) const { if (!ok) return false; if (is_local_decl_ref(e) && !get_local_decl(e)) { ok = false; - lean_unreachable(); } return true; }); diff --git a/src/library/local_context.h b/src/library/local_context.h index f01d4ff4c0..4bc3fc4084 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -132,9 +132,7 @@ public: bool well_formed() const; /** \brief Return true iff \c e is well-formed with respect to this local context. - That is, all local_decl references in \c e are defined in this context. - - \remark This method is for debugging purposes. */ + That is, all local_decl references in \c e are defined in this context. */ bool well_formed(expr const & e) const; format pp(formatter const & fmt) const; diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index aa95f1b047..80f02014a3 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1178,8 +1178,6 @@ Now, we consider some workarounds/approximations. (approximated) solution: restrict the context of `?M'` If `?M'` is assigned, the workaround is precise, and we just unfold `?M'`. - Remark: we only implement the ?M' assigned case. - A5) If some `a_i` is not a local constant, then we use first-order unification (if approximate() is true) @@ -1325,69 +1323,10 @@ bool type_context::process_assignment(expr const & m, expr const & v) { return true; } - while (true) { - /* We use a loop here to implement workaround A1. - If new_v has a "bad" let local decl, we expand it and try again. */ - bool ok = true; - bool bad_let_refs = false; - for_each(new_v, [&](expr const & e, unsigned) { - if (!ok) - return false; // stop search - if (is_mvar(e)) { - if (mvar == e) { - /* mvar occurs in v */ - ok = false; - return false; - } - if (!in_tmp_mode()) { - /* Recall that in tmp_mode all metavariables have the same local context. - So, we don't need to check anything. - In regular mode, we need to check condition 4 - - For every metavariable `?M'@C'` occurring in `t`, `C'` is a subset of `C` - */ - optional e_decl = m_mctx.get_metavar_decl(e); - if (!e_decl || !e_decl->get_context().is_subset_of(mvar_decl->get_context())) { - ok = false; - return false; - } - } - return false; - } else if (is_local_decl_ref(e)) { - bool in_ctx; - if (in_tmp_mode()) { - in_ctx = static_cast(m_tmp_mvar_lctx.get_local_decl(e)); - } else { - in_ctx = static_cast(mvar_decl->get_context().get_local_decl(e)); - } - if (!in_ctx) { - if (auto decl = m_lctx.get_local_decl(e)) { - if (decl->get_value()) { - /* let-decl that is not in the metavar context - workaround A1 */ - ok = false; - bad_let_refs = true; - return false; - } - } - if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) { - return mlocal_name(a) != mlocal_name(e); })) { - ok = false; - return false; - } - } - return false; - } - return true; - }); - if (ok) { - break; - } else if (bad_let_refs) { - new_v = instantiate_mvars(expand_let_decls(new_v)); - } else { - return false; - } - } + if (optional new_new_v = check_assignment(locals, mvar, new_v)) + new_v = *new_new_v; + else + return false; if (args.empty()) { /* easy case */ @@ -1436,6 +1375,111 @@ bool type_context::process_assignment(expr const & m, expr const & v) { return true; } +/* Auxiliary method for process_assignment */ +optional type_context::check_assignment(buffer const & locals, expr const & mvar, expr v) { + optional mvar_decl; + if (!in_tmp_mode()) { + mvar_decl = m_mctx.get_metavar_decl(mvar); + lean_assert(mvar_decl); + } + while (true) { + /* We use a loop here to implement workaround A1. + If new_v has a "bad" let local decl, we expand it and try again. */ + bool ok = true; + bool bad_let_refs = false; + bool inst_mvars = false; + for_each(v, [&](expr const & e, unsigned) { + if (!ok) return false; // stop search + if (is_mvar(e)) { + if (is_assigned(e)) { + inst_mvars = true; + return false; + } + if (mvar == e) { + /* mvar occurs in v */ + ok = false; + return false; + } + if (!in_tmp_mode()) { + /* Recall that in tmp_mode all metavariables have the same local context. + So, we don't need to check anything. + In regular mode, we need to check condition 4 + + For every metavariable `?M'@C'` occurring in `t`, `C'` is a subset of `C` + */ + optional e_decl = m_mctx.get_metavar_decl(e); + if (!e_decl) { + ok = false; + return false; + } + local_context mvar_lctx = mvar_decl->get_context(); + local_context e_lctx = e_decl->get_context(); + if (!e_lctx.is_subset_of(mvar_lctx)) { + if (approximate() && mvar_lctx.is_subset_of(e_lctx)) { + expr e_type = e_decl->get_type(); + if (mvar_lctx.well_formed(e_type)) { + /* Restrict context of the ?M' */ + expr aux_mvar = m_mctx.mk_metavar_decl(mvar_lctx, e_type); + if (process_assignment(e, aux_mvar)) { + inst_mvars = true; + } else { + /* Local context restriction failed */ + ok = false; + return false; + } + } else { + /* e_type uses local_decl's that are not in mvar_lctx */ + ok = false; + return false; + } + } else { + /* The two local contexts are incomparable OR + approximate mode is not enabled. */ + ok = false; + return false; + } + } + } + return false; + } else if (is_local_decl_ref(e)) { + bool in_ctx; + if (in_tmp_mode()) { + in_ctx = static_cast(m_tmp_mvar_lctx.get_local_decl(e)); + } else { + in_ctx = static_cast(mvar_decl->get_context().get_local_decl(e)); + } + if (!in_ctx) { + if (auto decl = m_lctx.get_local_decl(e)) { + if (decl->get_value()) { + /* let-decl that is not in the metavar context + workaround A1 */ + ok = false; + bad_let_refs = true; + return false; + } + } + if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) { + return mlocal_name(a) != mlocal_name(e); })) { + ok = false; + return false; + } + } + return false; + } + return true; + }); + if (inst_mvars) { + v = instantiate_mvars(v); + } else if (ok) { + return some_expr(v); + } else if (bad_let_refs) { + v = instantiate_mvars(expand_let_decls(v)); + } else { + return none_expr(); + } + } +} + bool type_context::is_def_eq_binding(expr e1, expr e2) { lean_assert(e1.kind() == e2.kind()); lean_assert(is_binding(e1)); diff --git a/src/library/type_context.h b/src/library/type_context.h index c7e036118d..1e04f75ff2 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -417,6 +417,7 @@ private: bool approximate(); expr try_zeta(expr const & e); expr expand_let_decls(expr const & e); + optional check_assignment(buffer const & locals, expr const & mvar, expr v); bool process_assignment(expr const & m, expr const & v); optional is_delta(expr const & e); diff --git a/tests/lean/restrict_bug.lean b/tests/lean/restrict_bug.lean new file mode 100644 index 0000000000..252a109db2 --- /dev/null +++ b/tests/lean/restrict_bug.lean @@ -0,0 +1,5 @@ +axiom all {A : Type}: list A → (A → Prop) → Prop +variable {A : Type} +variable {R : A → A → Prop} +set_option pp.all true +check ∀ a l, all l (R a) diff --git a/tests/lean/restrict_bug.lean.expected.out b/tests/lean/restrict_bug.lean.expected.out new file mode 100644 index 0000000000..ca680a254a --- /dev/null +++ b/tests/lean/restrict_bug.lean.expected.out @@ -0,0 +1 @@ +∀ (a : A) (l : list.{l_1} A), @all.{l_1} A l (R a) : Prop