From 91f4ced83b9b9ec69391bde03365d51c26297f0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Dec 2013 16:41:20 -0800 Subject: [PATCH] feat(library/elaborator): do not create trivial constraints of the form 'ctx |- t =:= t' Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 43 +++++++++++---------------- 1 file changed, 18 insertions(+), 25 deletions(-) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 724bc3121..50a7ef23d 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -316,6 +316,8 @@ class elaborator::imp { */ void push_new_constraint(cnstr_list & active_cnstrs, bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) { + if (new_a == new_b) + return; // trivial constraint if (is_eq) push_front(active_cnstrs, mk_eq_constraint(new_ctx, new_a, new_b, new_jst)); else @@ -349,12 +351,7 @@ class elaborator::imp { The update is justified by \c new_jst. */ void push_updated_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b, justification const & new_jst) { - lean_assert(is_eq(c) || is_convertible(c)); - context const & ctx = get_context(c); - if (is_eq(c)) - push_active(mk_eq_constraint(ctx, new_a, new_b, new_jst)); - else - push_active(mk_convertible_constraint(ctx, new_a, new_b, new_jst)); + push_new_constraint(m_state.m_active_cnstrs, is_eq(c), get_context(c), new_a, new_b, new_jst); } /** @@ -365,17 +362,16 @@ class elaborator::imp { */ void push_updated_constraint(unification_constraint const & c, bool is_lhs, expr const & new_a, justification const & new_jst) { lean_assert(is_eq(c) || is_convertible(c)); - context const & ctx = get_context(c); if (is_eq(c)) { if (is_lhs) - push_active(mk_eq_constraint(ctx, new_a, eq_rhs(c), new_jst)); + push_updated_constraint(c, new_a, eq_rhs(c), new_jst); else - push_active(mk_eq_constraint(ctx, eq_lhs(c), new_a, new_jst)); + push_updated_constraint(c, eq_lhs(c), new_a, new_jst); } else { if (is_lhs) - push_active(mk_convertible_constraint(ctx, new_a, convertible_to(c), new_jst)); + push_updated_constraint(c, new_a, convertible_to(c), new_jst); else - push_active(mk_convertible_constraint(ctx, convertible_from(c), new_a, new_jst)); + push_updated_constraint(c, convertible_from(c), new_a, new_jst); } } @@ -779,7 +775,7 @@ class elaborator::imp { expr s = mk_lambda(types, b); if (!is_lhs) swap(m, s); - push_active(mk_eq_constraint(ctx, m, s, new_jst)); + push_new_eq_constraint(ctx, m, s, new_jst); return true; } else { return false; @@ -1165,7 +1161,7 @@ class elaborator::imp { // ctx |- a2 == b2 justification new_jst(new destruct_justification(c)); for (unsigned i = 1; i < num_args(a); i++) - push_active(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst)); + push_new_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst); return true; } @@ -1220,25 +1216,22 @@ class elaborator::imp { } case expr_kind::Eq: { justification new_jst(new destruct_justification(c)); - push_active(mk_eq_constraint(ctx, eq_lhs(a), eq_lhs(b), new_jst)); - push_active(mk_eq_constraint(ctx, eq_rhs(a), eq_rhs(b), new_jst)); + push_new_eq_constraint(ctx, eq_lhs(a), eq_lhs(b), new_jst); + push_new_eq_constraint(ctx, eq_rhs(a), eq_rhs(b), new_jst); return true; } case expr_kind::Pi: { justification new_jst(new destruct_justification(c)); - push_active(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst)); + push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst); context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); - if (eq) - push_active(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst)); - else - push_active(mk_convertible_constraint(new_ctx, abst_body(a), abst_body(b), new_jst)); + push_new_constraint(eq, new_ctx, abst_body(a), abst_body(b), new_jst); return true; } case expr_kind::Lambda: { justification new_jst(new destruct_justification(c)); - push_active(mk_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst)); + push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst); context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); - push_active(mk_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst)); + push_new_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst); return true; } case expr_kind::App: @@ -1246,7 +1239,7 @@ class elaborator::imp { if (num_args(a) == num_args(b)) { justification new_jst(new destruct_justification(c)); for (unsigned i = 0; i < num_args(a); i++) - push_active(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst)); + push_new_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst); return true; } else { m_conflict = justification(new unification_failure_justification(c)); @@ -1336,7 +1329,7 @@ class elaborator::imp { if (is_type(lhs1) && is_type(lhs2)) { justification new_jst(new normalize_justification(c)); expr new_lhs = mk_type(max(ty_level(lhs1), ty_level(lhs2))); - push_active(mk_eq_constraint(get_context(c), new_lhs, rhs, new_jst)); + push_new_eq_constraint(get_context(c), new_lhs, rhs, new_jst); return true; } if (lhs1 == rhs) { @@ -1402,7 +1395,7 @@ class elaborator::imp { s.m_idx++; s.m_curr_assumption = mk_assumption(); m_state = s.m_prev_state; - push_active(mk_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption)); + push_new_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption); return true; } else { m_conflict = justification(new unification_failure_by_cases_justification(choice, s.m_failed_justifications.size(),