From 9620b00e24809be073e0262f6d6c483e68403bfd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 16:08:32 -0800 Subject: [PATCH] feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones. This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator. For example, suppose we have the constraint ctx |- ?M1[inst:0 ?M2] == a If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions: ?M1 == a or ?M1 == #0 and ?M2 == a On the other hand, if ?M2 is assigned to b, then we can ignore the second case. Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 26 ++++++++++++++-- src/library/elaborator/elaborator.cpp | 44 +++++++++++++++++++-------- tests/lean/bad9.lean | 8 +++++ tests/lean/bad9.lean.expected.out | 8 +++++ 4 files changed, 70 insertions(+), 16 deletions(-) create mode 100644 tests/lean/bad9.lean create mode 100644 tests/lean/bad9.lean.expected.out diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 71b2e2356..4581849f4 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -303,9 +303,17 @@ bool metavar_env_cell::has_assigned_metavar(expr const & e) const { return false; if (!has_metavar(n)) return false; - if (is_metavar(n) && is_assigned(n)) { - result = true; - return false; + if (is_metavar(n)) { + if (is_assigned(n)) { + result = true; + return false; + } + for (auto const & entry : metavar_lctx(n)) { + if (entry.is_inst() && has_assigned_metavar(entry.v())) { + result = true; + return false; + } + } } return true; }); @@ -339,6 +347,7 @@ protected: } virtual expr visit_metavar(expr const & m, context const & ctx) { + local_context const & lctx = metavar_lctx(m); if (is_metavar(m) && m_menv->is_assigned(m)) { auto p = m_menv->get_subst_jst(m); lean_assert(p); @@ -349,6 +358,17 @@ protected: } else { return r; } + } else if (std::find_if(lctx.begin(), lctx.end(), [&](local_entry const & e) { return e.is_inst() && m_menv->has_assigned_metavar(e.v()); }) + != lctx.end()) { + // local context has assigned metavariables + buffer new_lctx; + for (auto const & e : lctx) { + if (e.is_inst()) + new_lctx.push_back(mk_inst(e.s(), visit(e.v(), ctx))); + else + new_lctx.push_back(e); + } + return mk_metavar(metavar_name(m), to_list(new_lctx.begin(), new_lctx.end())); } else { return m; } diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index f285c1d59..c9de25fad 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -183,15 +183,23 @@ class elaborator::imp { push_active(c); } + void collect_mvars(expr const & e, name_set & r) { + for_each(e, [&](expr const & m, unsigned) { + if (is_metavar(m) && !r.contains(metavar_name(m))) { + r.insert(metavar_name(m)); + for (auto const & entry : metavar_lctx(m)) { + if (entry.is_inst()) + collect_mvars(entry.v(), r); + } + } + return true; + }); + } + /** \brief Collect metavars in \c c */ name_list collect_mvars(unification_constraint const & c) { - buffer r; - auto f = [&](expr const & m, unsigned) { - if (is_metavar(m)) - r.push_back(metavar_name(m)); - return true; - }; - for_each_fn proc(f); + name_set s; + auto proc = [&](expr const & e) { return collect_mvars(e, s); }; switch (c.kind()) { case unification_constraint_kind::Eq: proc(eq_lhs(c)); proc(eq_rhs(c)); break; @@ -203,10 +211,7 @@ class elaborator::imp { lean_unreachable(); // we never delay Choice break; } - std::sort(r.begin(), r.end(), name_quick_cmp()); - auto new_end = std::unique(r.begin(), r.end()); - r.resize(r.size() + r.end() - new_end); - return to_list(r.begin(), r.end()); + return s.fold([](name const & n, name_list const & l) { return cons(n, l); }, name_list()); } /** \brief Add given constraint to the delayed list */ @@ -1074,10 +1079,23 @@ class elaborator::imp { /** \brief Process a constraint ctx |- a == b where \c a is of the form ?m[(inst:i t), ...]. We perform a "case split", - Case 1) ?m[...] == #i and t == b + Case 1) ?m[...] == #i and t == b (for constants, variables, values and Type) Case 2) imitate b */ bool process_metavar_inst(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { + // This method is miss some cases. In particular the local context of \c a contains metavariables. + // + // (f#2 #1) == ?M2[i:1 ?M1] + // + // A possible solution for this constraint is: + // ?M2 == #1 + // ?M1 == f#2 #1 + // + // TODO(Leo): consider the following alternative design: We do NOT use approximations, since it is quite + // hard to understand what happened when they do not work. Instead, we rely on user provided plugins + // for handling the nasty cases. + // + // TODO(Leo): another possible design is to inform the user where approximation was used. if (is_metavar_inst(a) && (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) { lean_assert(!is_assigned(a)); if (is_constant(b) || is_type(b) || is_value(b) || is_var(b)) { @@ -1085,7 +1103,7 @@ class elaborator::imp { buffer solutions; collect_metavar_solutions(lctx, b, solutions); lean_assert(solutions.size() >= 1); - bool keep_c = local_context_has_metavar(lctx); + bool keep_c = local_context_has_metavar(metavar_lctx(a)); expr m = mk_metavar(metavar_name(a)); context ctx_m = m_state.m_menv->get_context(m); if (solutions.size() == 1) { diff --git a/tests/lean/bad9.lean b/tests/lean/bad9.lean new file mode 100644 index 000000000..2b8eab1c8 --- /dev/null +++ b/tests/lean/bad9.lean @@ -0,0 +1,8 @@ +SetOption pp::implicit true. +SetOption pp::colors false. +Variable N : Type. + +Check +fun (a : N) (f : N -> N) (H : f a == a), +let calc1 : f a == a := SubstP (fun x : N, f a == _) (Refl (f a)) H +in calc1. \ No newline at end of file diff --git a/tests/lean/bad9.lean.expected.out b/tests/lean/bad9.lean.expected.out new file mode 100644 index 000000000..079e9bcd4 --- /dev/null +++ b/tests/lean/bad9.lean.expected.out @@ -0,0 +1,8 @@ + Set: pp::colors + Set: pp::unicode + Set: lean::pp::implicit + Set: pp::colors + Assumed: N +λ (a : N) (f : N → N) (H : f a == a), + let calc1 : f a == a := @SubstP N (f a) a (λ x : N, f a == x) (@Refl N (f a)) H in calc1 : + Π (a : N) (f : N → N), f a == a → f a == a