From d5bb7d45ec8f08a989fe8627174a3658f78a9c87 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Aug 2014 13:30:28 -0700 Subject: [PATCH] fix(library/unifier): constraint priority in the unifier, and remove hack from if.lean Signed-off-by: Leonardo de Moura --- library/standard/logic/connectives/if.lean | 6 +----- src/frontends/lean/elaborator.cpp | 4 ++-- src/library/unifier.cpp | 6 +++--- src/library/unifier.h | 14 +++++++------- 4 files changed, 13 insertions(+), 17 deletions(-) diff --git a/library/standard/logic/connectives/if.lean b/library/standard/logic/connectives/if.lean index ad4c278bc..765d4cb3d 100644 --- a/library/standard/logic/connectives/if.lean +++ b/library/standard/logic/connectives/if.lean @@ -49,11 +49,7 @@ rec_on H₁ theorem if_congr_aux {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : (if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) := --- TODO(Leo): We can't write (Ht ▸ He ▸ if_cond_congr Hc t₁ e₁) because the class instance --- mechanism is not applicable to the auxiliary metavariables created by the unifier. --- We should fix that in the future. -have e : (@ite c₁ H₁ A t₁ e₁) = (@ite c₂ H₂ A t₁ e₁), from if_cond_congr Hc t₁ e₁, -Ht ▸ He ▸ e +Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁) theorem if_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : (if c₁ then t₁ else e₁) = (@ite c₂ (decidable_iff_equiv H₁ Hc) A t₂ e₂) := diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index be597a0d0..dc15db5ae 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -630,7 +630,7 @@ public: ignore_failure, m_relax_main_opaque)); } }; - add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), false, j, m_relax_main_opaque)); + add_cnstr(mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::DelayedChoice2), false, j, m_relax_main_opaque)); return m; } @@ -740,7 +740,7 @@ public: 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)) { + if (is_meta(new_d_type) && delay_factor < to_delay_factor(cnstr_group::DelayedChoice1)) { // 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 { diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 1a9400ca7..a609cdf57 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -205,8 +205,8 @@ 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; -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}; +constexpr unsigned g_num_groups = 7; +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, 6*g_group_size}; static unsigned get_group_first_index(cnstr_group g) { return g_cnstr_group_first_index[static_cast(g)]; } @@ -1647,7 +1647,7 @@ struct unifier_fn { lean_assert(!m_tc[1]->next_cnstr()); auto const * p = m_cnstrs.min(); unsigned cidx = p->second; - if (!m_expensive && cidx > get_group_first_index(cnstr_group::MaxDelayed)) + if (!m_expensive && cidx >= get_group_first_index(cnstr_group::DelayedChoice2)) m_pattern = true; // use only higher-order (pattern) matching after we start processing MaxDelayed (aka class-instance constraints) constraint c = p->first; m_cnstrs.erase_min(); diff --git a/src/library/unifier.h b/src/library/unifier.h index 5dca5b99c..1be5466f8 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -50,7 +50,7 @@ lazy_list unify(environment const & env, expr const & lhs, expr co bool relax_main_opaque, substitution const & s, options const & o); /** - The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed + The unifier divides the constraints in 6 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice1, DelayedChoice2, 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. @@ -64,17 +64,17 @@ lazy_list unify(environment const & env, expr const & lhs, expr co 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. + 5) DelayedChoice1: for delayed choice constraints (we use this group for the maximally delayed coercions constraints). - 6) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other + 6) DelayedChoice2: for delayed choice constraints (we use this group for class-instance). + + 7) 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 + 8) MaxDelayed: maximally delayed constraint group */ -enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, PreFlexFlex, FlexFlex, MaxDelayed }; +enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice1, DelayedChoice2, FlexFlex, MaxDelayed }; inline unsigned to_delay_factor(cnstr_group g) { return static_cast(g); } class unifier_exception : public exception {