From 936bb2744b89e3deed64cbdb0bc0cb0b9511ff54 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Jul 2014 17:32:55 -0700 Subject: [PATCH] fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 6 +-- src/kernel/constraint.cpp | 14 ++++--- src/kernel/constraint.h | 22 ++++++++--- src/library/kernel_bindings.cpp | 14 ++++--- src/library/unifier.cpp | 63 ++++++++++++++++++++++++++++--- tests/lean/run/coercion_bug2.lean | 11 ++++++ 6 files changed, 106 insertions(+), 24 deletions(-) create mode 100644 tests/lean/run/coercion_bug2.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index f688f29279..2f3d7e76ea 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -615,7 +615,7 @@ public: ignore_failure, m_relax_main_opaque)); } }; - add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j, m_relax_main_opaque)); + add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), false, j, m_relax_main_opaque)); return m; } @@ -657,7 +657,7 @@ public: return choose(std::make_shared(*this, mvar, e, ctx, s, relax)); }; justification j = mk_justification("none of the overloads is applicable", some_expr(e)); - add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j, m_relax_main_opaque)); + add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), true, j, m_relax_main_opaque)); return m; } @@ -733,7 +733,7 @@ public: return lazy_list(constraints(mk_eq_cnstr(mvar, r, justification(), relax))); } }; - return mk_choice_cnstr(m, choice_fn, delay_factor, j, m_relax_main_opaque); + return mk_choice_cnstr(m, choice_fn, delay_factor, true, j, m_relax_main_opaque); } /** \brief Given a term a : a_type, and an expected type generate a metavariable with a delayed coercion. */ diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp index d02fbf025b..bf8adf691c 100644 --- a/src/kernel/constraint.cpp +++ b/src/kernel/constraint.cpp @@ -33,9 +33,10 @@ struct choice_constraint_cell : public constraint_cell { expr m_expr; choice_fn m_fn; unsigned m_delay_factor; - choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax): + bool m_owner; + choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax): constraint_cell(constraint_kind::Choice, j, relax), - m_expr(e), m_fn(fn), m_delay_factor(delay_factor) {} + m_expr(e), m_fn(fn), m_delay_factor(delay_factor), m_owner(owner) {} }; void constraint_cell::dealloc() { @@ -64,9 +65,9 @@ constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j) { return constraint(new level_constraint_cell(lhs, rhs, j)); } -constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque) { +constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax_main_opaque) { lean_assert(is_meta(m)); - return constraint(new choice_constraint_cell(m, fn, delay_factor, j, relax_main_opaque)); + return constraint(new choice_constraint_cell(m, fn, delay_factor, owner, j, relax_main_opaque)); } expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast(c.raw())->m_lhs; } @@ -87,6 +88,9 @@ choice_fn const & cnstr_choice_fn(constraint const & c) { unsigned cnstr_delay_factor(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_delay_factor; } +bool cnstr_is_owner(constraint const & c) { + lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_owner; +} constraint update_justification(constraint const & c, justification const & j) { switch (c.kind()) { @@ -95,7 +99,7 @@ constraint update_justification(constraint const & c, justification const & j) { case constraint_kind::LevelEq: return mk_level_eq_cnstr(cnstr_lhs_level(c), cnstr_rhs_level(c), j); case constraint_kind::Choice: - return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j, relax_main_opaque(c)); + return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), cnstr_is_owner(c), j, relax_main_opaque(c)); } lean_unreachable(); // LCOV_EXCL_LINE } diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index 7cbfb67015..f88b089741 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -67,8 +67,8 @@ public: friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque); friend constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j); - friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, - bool relax_main_opaque); + friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner, + justification const & j, bool relax_main_opaque); constraint_cell * raw() const { return m_ptr; } }; @@ -76,13 +76,21 @@ public: inline bool operator==(constraint const & c1, constraint const & c2) { return c1.raw() == c2.raw(); } inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); } -/** - \brief Create a unification constraint lhs =?= rhs - If \c relax_main_opaque is true, then opaque definitions from the main module are treated as transparent. +/** \brief Create a unification constraint lhs =?= rhs + If \c relax_main_opaque is true, then opaque definitions from the main module are treated as transparent. */ constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j, bool relax_main_opaque); constraint mk_level_eq_cnstr(level const & lhs, level const & rhs, justification const & j); -constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j, bool relax_main_opaque); +/** \brief Create a "choice" constraint m in fn(...), where fn produces a stream of possible solutions. + \c delay_factor allows to control when the constraint is processed by the elaborator, bigger == later. + If \c owner is true, then the elaborator should not assign the metavariable get_app_fn(m). + The variable will be assigned by the choice constraint, and the elaborator should just check whether a solution + produced by fn satisfies the other constraints or not. + \c j is a justification for the constraint. + If \c relax_main_opaque is true, then it signs that constraint was created in a context where + opaque constants of the main module can be treated as transparent. +*/ +constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, bool owner, justification const & j, bool relax_main_opaque); inline bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; } inline bool is_level_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::LevelEq; } @@ -106,6 +114,8 @@ expr const & cnstr_expr(constraint const & c); choice_fn const & cnstr_choice_fn(constraint const & c); /** \brief Return the choice constraint delay factor */ unsigned cnstr_delay_factor(constraint const & c); +/** \brief Return true iff the given choice constraints owns the right to assign the metavariable in \c c. */ +bool cnstr_is_owner(constraint const & c); /** \brief Printer for debugging purposes */ std::ostream & operator<<(std::ostream & out, constraint const & c); diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 571a1a1dfb..18b86478fb 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1528,15 +1528,19 @@ static int mk_choice_cnstr(lua_State * L) { expr m = to_expr(L, 1); choice_fn fn = to_choice_fn(L, 2); if (nargs == 2) - return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification(), false)); + return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, justification(), false)); else if (nargs == 3 && is_justification(L, 3)) - return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3), false)); + return push_constraint(L, mk_choice_cnstr(m, fn, 0, false, to_justification(L, 3), false)); else if (nargs == 3) - return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification(), false)); + return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), false, justification(), false)); else if (nargs == 4) - return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), false)); + return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4), justification(), false)); + else if (nargs == 5) + return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4), + to_justification(L, 5), false)); else - return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4), lua_toboolean(L, 5))); + return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), lua_toboolean(L, 4), + to_justification(L, 5), lua_toboolean(L, 6))); } static int constraint_expr(lua_State * L) { diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 763c297904..5f783b2bc4 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -211,10 +211,16 @@ unify_status unify_simple(substitution & s, constraint const & c) { static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification(), false); static unsigned g_group_size = 1u << 29; -static unsigned g_cnstr_group_first_index[6] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size}; +constexpr unsigned g_num_groups = 6; +static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size}; static unsigned get_group_first_index(cnstr_group g) { return g_cnstr_group_first_index[static_cast(g)]; } +static cnstr_group to_cnstr_group(unsigned d) { + if (d >= g_num_groups) + d = g_num_groups-1; + return static_cast(d); +} /** \brief Convert choice constraint delay factor to cnstr_group */ cnstr_group get_choice_cnstr_group(constraint const & c) { @@ -236,10 +242,12 @@ struct unifier_fn { typedef rb_tree cnstr_set; typedef rb_tree cnstr_idx_set; typedef rb_map name_to_cnstrs; + typedef rb_map owned_map; typedef std::unique_ptr type_checker_ptr; environment m_env; name_generator m_ngen; substitution m_subst; + owned_map m_owned_map; // mapping from metavariable name m to delay factor of the choice constraint that owns m unifier_plugin m_plugin; type_checker_ptr m_tc[2]; bool m_use_exception; //!< True if we should throw an exception when there are no more solutions. @@ -286,11 +294,12 @@ struct unifier_fn { substitution m_subst; cnstr_set m_cnstrs; name_to_cnstrs m_mvar_occs; + owned_map m_owned_map; /** \brief Save unifier's state */ case_split(unifier_fn & u, justification const & j): m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst), m_cnstrs(u.m_cnstrs), - m_mvar_occs(u.m_mvar_occs) { + m_mvar_occs(u.m_mvar_occs), m_owned_map(u.m_owned_map) { u.m_next_assumption_idx++; u.m_tc[0]->push(); u.m_tc[1]->push(); @@ -306,6 +315,7 @@ struct unifier_fn { u.m_subst = m_subst; u.m_cnstrs = m_cnstrs; u.m_mvar_occs = m_mvar_occs; + u.m_owned_map = m_owned_map; m_assumption_idx = u.m_next_assumption_idx; m_failed_justifications = mk_composite1(m_failed_justifications, *u.m_conflict); u.m_next_assumption_idx++; @@ -608,12 +618,41 @@ struct unifier_fn { return Continue; } + /** \brief Return a delay factor if e is of the form (?m ...) and ?m is a metavariable owned by + a choice constraint. The delay factor is the delay of the choice constraint. + Return none otherwise. */ + optional is_owned(expr const & e) { + expr const & m = get_app_fn(e); + if (!is_metavar(m)) + return optional(); + if (auto it = m_owned_map.find(mlocal_name(m))) + return optional(*it); + else + return optional(); + } + + /** \brief Applies previous method to the left and right hand sides of the equality constraint */ + optional is_owned(constraint const & c) { + if (auto d = is_owned(cnstr_lhs_expr(c))) + return d; + else + return is_owned(cnstr_rhs_expr(c)); + } + /** \brief Process an equality constraints. */ bool process_eq_constraint(constraint const & c) { lean_assert(is_eq_cnstr(c)); // instantiate assigned metavariables status st = instantiate_eq_cnstr(c); if (st != Continue) return st == Solved; + + if (auto d = is_owned(c)) { + // Metavariable in the constraint is owned by choice constraint. + // So, we postpone this constraint. + add_cnstr(c, to_cnstr_group(*d+1)); + return true; + } + st = process_eq_constraint_core(c); if (st != Continue) return st == Solved; @@ -707,6 +746,17 @@ struct unifier_fn { return true; } + bool preprocess_choice_constraint(constraint const & c) { + if (cnstr_is_owner(c)) { + expr m = get_app_fn(cnstr_expr(c)); + lean_assert(is_metavar(m)); + m_owned_map.insert(mlocal_name(m), cnstr_delay_factor(c)); + } + // Choice constraints are never considered easy. + add_cnstr(c, get_choice_cnstr_group(c)); + return true; + } + /** \brief Process the given constraint \c c. "Easy" constraints are solved, and the remaining ones are added to the constraint queue m_cnstrs. By "easy", see the methods @@ -718,9 +768,7 @@ struct unifier_fn { check_system(); switch (c.kind()) { case constraint_kind::Choice: - // Choice constraints are never considered easy. - add_cnstr(c, get_choice_cnstr_group(c)); - return true; + return preprocess_choice_constraint(c); case constraint_kind::Eq: return process_eq_constraint(c); case constraint_kind::LevelEq: @@ -878,6 +926,11 @@ struct unifier_fn { lean_assert(is_choice_cnstr(c)); expr const & m = cnstr_expr(c); choice_fn const & fn = cnstr_choice_fn(c); + if (cnstr_is_owner(c)) { + // choice will have a chance to assign m, so + // we remove the "barrier" that was preventing m from being assigned. + m_owned_map.erase(mlocal_name(get_app_fn(m))); + } expr m_type; bool relax = relax_main_opaque(c); try { diff --git a/tests/lean/run/coercion_bug2.lean b/tests/lean/run/coercion_bug2.lean new file mode 100644 index 0000000000..c26615e649 --- /dev/null +++ b/tests/lean/run/coercion_bug2.lean @@ -0,0 +1,11 @@ +import nat +using nat + +inductive list (T : Type) : Type := +| nil {} : list T +| cons : T → list T → list T + +definition length {T : Type} : list T → nat := list_rec 0 (fun x l m, succ m) +theorem length_nil {T : Type} : length (@nil T) = 0 +:= refl _ +