From b956ce68d20038c6fabd3301fa0a3dce085b0dde Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Jul 2014 12:40:00 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): keep postponing delayed coercions until the type can be inferred Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 25 +++++++++++----- src/kernel/constraint.cpp | 18 ++++++------ src/kernel/constraint.h | 8 +++--- src/library/kernel_bindings.cpp | 14 ++++----- src/library/unifier.cpp | 45 +++++++++-------------------- src/library/unifier.h | 28 ++++++++++++++++++ tests/lean/run/alias1.lean | 47 +++++++++++++++++++++++++++++++ tests/lean/run/alias2.lean | 23 +++++++++++++++ 8 files changed, 150 insertions(+), 58 deletions(-) create mode 100644 tests/lean/run/alias1.lean create mode 100644 tests/lean/run/alias2.lean diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7fa3abba1..a4b41183b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -502,7 +502,7 @@ public: else return choose(std::make_shared(*this, mvar, mvar_type, local_insts, insts, ctx, s, j)); }; - add_cnstr(mk_choice_cnstr(m, choice_fn, true, j)); + add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), j)); } return m; } @@ -544,7 +544,7 @@ public: return choose(std::make_shared(*this, mvar, e, ctx, s)); }; justification j = mk_justification("none of the overloads is applicable", some_expr(e)); - add_cnstr(mk_choice_cnstr(m, fn, false, j)); + add_cnstr(mk_choice_cnstr(m, fn, to_delay_factor(cnstr_group::Basic), j)); return m; } @@ -609,6 +609,21 @@ public: return a; } + constraint mk_delayed_coercion_cnstr(expr const & m, expr const & a, expr const & a_type, justification const & j, unsigned delay_factor) { + auto choice_fn = [=](expr const & mvar, expr const & new_d_type, substitution const & /* s */, name_generator const & /* ngen */) { + // Remark: we want the coercions solved before we start discarding FlexFlex constraints. So, we use PreFlexFlex as a max cap + // for delaying coercions. + if (is_meta(new_d_type) && delay_factor < to_delay_factor(cnstr_group::PreFlexFlex)) { + // The type is still unknown, delay the constraint even more. + return lazy_list(constraints(mk_delayed_coercion_cnstr(m, a, a_type, justification(), delay_factor+1))); + } else { + expr r = apply_coercion(a, a_type, new_d_type); + return lazy_list(constraints(mk_eq_cnstr(mvar, r, justification()))); + } + }; + return mk_choice_cnstr(m, choice_fn, delay_factor, j); + } + /** \brief Given an application \c e, where the expected type is d_type, and the argument type is a_type, create a "delayed coercion". The idea is to create a choice constraint and postpone the coercion search. We do that whenever d_type or a_type is a metavar application, and d_type or a_type is a coercion source/target. @@ -616,12 +631,8 @@ public: expr mk_delayed_coercion(expr const & e, expr const & d_type, expr const & a_type) { expr a = app_arg(e); expr m = mk_meta(some_expr(d_type), a.get_tag()); - auto choice_fn = [=](expr const & mvar, expr const & new_d_type, substitution const & /* s */, name_generator const & /* ngen */) { - expr r = apply_coercion(a, a_type, new_d_type); - return lazy_list(constraints(mk_eq_cnstr(mvar, r, justification()))); - }; justification j = mk_app_justification(m_env, e, d_type, a_type); - add_cnstr(mk_choice_cnstr(m, choice_fn, false, j)); + add_cnstr(mk_delayed_coercion_cnstr(m, a, a_type, j, to_delay_factor(cnstr_group::Basic))); return update_app(e, app_fn(e), m); } diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp index e0b53e33c..eb1b1034f 100644 --- a/src/kernel/constraint.cpp +++ b/src/kernel/constraint.cpp @@ -31,10 +31,10 @@ struct level_constraint_cell : public constraint_cell { struct choice_constraint_cell : public constraint_cell { expr m_expr; choice_fn m_fn; - bool m_delayed; - choice_constraint_cell(expr const & e, choice_fn const & fn, bool delayed, justification const & j): + unsigned m_delay_factor; + choice_constraint_cell(expr const & e, choice_fn const & fn, unsigned delay_factor, justification const & j): constraint_cell(constraint_kind::Choice, j), - m_expr(e), m_fn(fn), m_delayed(delayed) {} + m_expr(e), m_fn(fn), m_delay_factor(delay_factor) {} }; void constraint_cell::dealloc() { @@ -63,9 +63,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, bool delayed, justification const & j) { +constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j) { lean_assert(is_meta(m)); - return constraint(new choice_constraint_cell(m, fn, delayed, j)); + return constraint(new choice_constraint_cell(m, fn, delay_factor, j)); } expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eq_cnstr(c)); return static_cast(c.raw())->m_lhs; } @@ -82,8 +82,8 @@ expr const & cnstr_expr(constraint const & c) { lean_assert(is_choice_cnstr(c)); choice_fn const & cnstr_choice_fn(constraint const & c) { lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_fn; } -bool cnstr_delayed(constraint const & c) { - lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_delayed; +unsigned cnstr_delay_factor(constraint const & c) { + lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_delay_factor; } constraint update_justification(constraint const & c, justification const & j) { @@ -93,7 +93,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_delayed(c), j); + return mk_choice_cnstr(cnstr_expr(c), cnstr_choice_fn(c), cnstr_delay_factor(c), j); } lean_unreachable(); // LCOV_EXCL_LINE } @@ -108,7 +108,7 @@ std::ostream & operator<<(std::ostream & out, constraint const & c) { break; case constraint_kind::Choice: out << "choice "; - if (cnstr_delayed(c)) out << "[delayed] "; + if (cnstr_delay_factor(c) != 0) out << "[delayed:" << cnstr_delay_factor(c) << "] "; out << cnstr_expr(c); break; } diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h index 1e103bf71..7adc7ff12 100644 --- a/src/kernel/constraint.h +++ b/src/kernel/constraint.h @@ -67,7 +67,7 @@ public: friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j); 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, bool delayed, justification const & j); + friend constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j); constraint_cell * raw() const { return m_ptr; } }; @@ -77,7 +77,7 @@ inline bool operator!=(constraint const & c1, constraint const & c2) { return !( constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j); 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, bool delayed, justification const & j); +constraint mk_choice_cnstr(expr const & m, choice_fn const & fn, unsigned delay_factor, justification const & j); 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; } @@ -97,8 +97,8 @@ level const & cnstr_rhs_level(constraint const & c); expr const & cnstr_expr(constraint const & c); /** \brief Return the choice_fn associated with a choice constraint. */ choice_fn const & cnstr_choice_fn(constraint const & c); -/** \brief Return true iff choice constraint must be delayed. */ -bool cnstr_delayed(constraint const & c); +/** \brief Return the choice constraint delay factor */ +unsigned cnstr_delay_factor(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 b1b0194b8..33385c0b6 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1513,13 +1513,13 @@ 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, false, justification())); + return push_constraint(L, mk_choice_cnstr(m, fn, 0, justification())); else if (nargs == 3 && is_justification(L, 3)) - return push_constraint(L, mk_choice_cnstr(m, fn, false, to_justification(L, 3))); + return push_constraint(L, mk_choice_cnstr(m, fn, 0, to_justification(L, 3))); else if (nargs == 3) - return push_constraint(L, mk_choice_cnstr(m, fn, lua_toboolean(L, 3), justification())); + return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), justification())); else - return push_constraint(L, mk_choice_cnstr(m, fn, lua_toboolean(L, 3), to_justification(L, 4))); + return push_constraint(L, mk_choice_cnstr(m, fn, lua_tonumber(L, 3), to_justification(L, 4))); } static int constraint_expr(lua_State * L) { @@ -1530,10 +1530,10 @@ static int constraint_expr(lua_State * L) { throw exception("arg #1 must be a choice constraint"); } -static int constraint_delayed(lua_State * L) { +static int constraint_delay_factor(lua_State * L) { constraint const & c = to_constraint(L, 1); if (is_choice_cnstr(c)) - return push_boolean(L, cnstr_delayed(c)); + return push_integer(L, cnstr_delay_factor(c)); else throw exception("arg #1 must be a choice constraint"); } @@ -1550,7 +1550,7 @@ static const struct luaL_Reg constraint_m[] = { {"rhs", safe_function}, {"justification", safe_function}, {"expr", safe_function}, - {"delayed", safe_function}, + {"delay_factor", safe_function}, {0, 0} }; diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 34c474cdb..9d71bbd35 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -191,37 +191,23 @@ std::pair unify_simple(substitution const & s, const } static constraint g_dont_care_cnstr = mk_eq_cnstr(expr(), expr(), justification()); - -/** - The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, Reduction, FlexFlex, DelayedChoice - - 1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t. - The are not even inserted in the constraint priority queue. - - 2) Basic: contains user choice constraints used to model coercions and overloaded constraints, and constraints - that cannot be solved, and the unification plugin must be invoked. - - 3) FlexRigid constraints (?M t_1 ... t_n) =?= t, where t_n is not an introduction application - - 4) PluginDelayed: contraints delayed by the unifier_plugin. Examples: (elim ... (?m ...)) and (?m ... (intro ...)), - where elim is an eliminator/recursor and intro is an introduction/constructor. - This constraints are delayed because after ?m is assigned we may be able to reduce them. - - 5) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other - ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then - we simply discard it. - - 6) DelayedChoice: delayed choice constraints, they are used to model features such as class-instance - They are really term synthesizers. We use the unifier just to exploit the non-chronological backtracking - infrastructure -*/ -enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, FlexFlex, DelayedChoice }; -static unsigned g_group_size = 1u << 28; -static unsigned g_cnstr_group_first_index[5] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size}; +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}; static unsigned get_group_first_index(cnstr_group g) { return g_cnstr_group_first_index[static_cast(g)]; } +/** \brief Convert choice constraint delay factor to cnstr_group */ +cnstr_group get_choice_cnstr_group(constraint const & c) { + lean_assert(is_choice_cnstr(c)); + unsigned f = cnstr_delay_factor(c); + if (f > static_cast(cnstr_group::MaxDelayed)) { + return cnstr_group::MaxDelayed; + } else { + return static_cast(f); + } +} + /** \brief Auxiliary functional object for implementing simultaneous higher-order unification */ struct unifier_fn { typedef std::pair cnstr; // constraint + idx @@ -638,10 +624,7 @@ struct unifier_fn { switch (c.kind()) { case constraint_kind::Choice: // Choice constraints are never considered easy. - if (cnstr_delayed(c)) - add_cnstr(c, nullptr, nullptr, cnstr_group::DelayedChoice); - else - add_cnstr(c, nullptr, nullptr, cnstr_group::Basic); + add_cnstr(c, nullptr, nullptr, get_choice_cnstr_group(c)); return true; case constraint_kind::Eq: return process_eq_constraint(c); diff --git a/src/library/unifier.h b/src/library/unifier.h index 2b4a1f7bd..935e0b4ea 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -45,6 +45,34 @@ lazy_list unify(environment const & env, expr const & lhs, expr co lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, options const & o); +/** + The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed + + 1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t. + The are not even inserted in the constraint priority queue. + + 2) Basic: contains user choice constraints used to model coercions and overloaded constraints, and constraints + that cannot be solved, and the unification plugin must be invoked. + + 3) FlexRigid constraints (?M t_1 ... t_n) =?= t, where t_n is not an introduction application + + 4) PluginDelayed: contraints delayed by the unifier_plugin. Examples: (elim ... (?m ...)) and (?m ... (intro ...)), + where elim is an eliminator/recursor and intro is an introduction/constructor. + This constraints are delayed because after ?m is assigned we may be able to reduce them. + + 5) PreFlexFlex: this group is for constraints we want solved before we start discarding FlexFlex constraints. + + 6) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other + ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then + we simply discard it. + + 7) MaxDelayed: for delayed choice constraints, they are used to model features such as class-instance + They are really term synthesizers. We use the unifier just to exploit the non-chronological backtracking + infrastructure +*/ +enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed }; +inline unsigned to_delay_factor(cnstr_group g) { return static_cast(g); } + class unifier_exception : public exception { justification m_jst; substitution m_subst; diff --git a/tests/lean/run/alias1.lean b/tests/lean/run/alias1.lean new file mode 100644 index 000000000..9838e7ed2 --- /dev/null +++ b/tests/lean/run/alias1.lean @@ -0,0 +1,47 @@ +import logic + +namespace N1 + variable num : Type.{1} + variable foo : num → num → num +end + +namespace N2 + variable val : Type.{1} + variable foo : val → val → val +end + +using N1 +using N2 +variables a b : num +variables x y : val + + +check foo a b +check foo x y + +variable f : num → val +coercion f + +check foo a x +check foo x y +check foo x a + +check foo a b +theorem T1 : foo a b = N1.foo a b +:= refl _ + +definition aux1 := foo a b -- System elaborated it to N2.foo (f a) (f b) +theorem T2 : aux1 = N2.foo (f a) (f b) +:= refl _ + +using N1 +definition aux2 := foo a b -- Now N1 is in the beginning of the queue again, and this is elaborated to N1.foo a b +check aux2 + +theorem T3 : aux2 = N1.foo a b +:= refl aux2 + + +check foo a b +theorem T4 : foo a b = N1.foo a b +:= refl _ diff --git a/tests/lean/run/alias2.lean b/tests/lean/run/alias2.lean new file mode 100644 index 000000000..777903d88 --- /dev/null +++ b/tests/lean/run/alias2.lean @@ -0,0 +1,23 @@ +import logic + +namespace N1 + variable num : Type.{1} + variable foo : num → num → num +end + +namespace N2 + variable val : Type.{1} + variable foo : val → val → val +end + +using N2 +using N1 +variables a b : num +variable f : num → val +coercion f + +definition aux2 := foo a b +check aux2 +theorem T3 : aux2 = N1.foo a b +:= refl _ +