From b94ce412aec00bee2fca56ad9baf86016a490aa0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Jul 2014 10:32:01 -0700 Subject: [PATCH] fix(library/unifier): non-termination Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 11 ++++------- tests/lean/run/tactic23.lean | 8 +++++++- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 2f66a37cc5..496fb3e297 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -596,19 +596,16 @@ struct unifier_fn { rhs = m_tc.whnf(rhs); lhs = m_tc.whnf(lhs); - // We delay constraints where lhs or rhs are of the form (elim ... (?m ...)) - if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs)) { - add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs); - return true; - } - // If lhs or rhs were updated, then invoke is_def_eq again. if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) { // some metavariables were instantiated, try is_def_eq again return is_def_eq(lhs, rhs, new_jst); } - if (is_meta(lhs) && is_meta(rhs)) { + // We delay constraints where lhs or rhs are of the form (elim ... (?m ...)) + if (is_elim_meta_app(lhs) || is_elim_meta_app(rhs)) { + add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs); + } else if (is_meta(lhs) && is_meta(rhs)) { // flex-flex constraints are delayed the most. add_very_delayed_cnstr(c, &unassigned_lvls, &unassigned_exprs); } else if (is_meta(lhs) || is_meta(rhs)) { diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index ceda003c4e..b61029e682 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -26,5 +26,11 @@ check 2 + 3 -- Define an assump as an alias for the eassumption tactic definition assump : tactic := eassumption -theorem T {p : nat → Bool} {a : nat } (H : p (a+1)) : ∃ x, p (succ x) +theorem T1 {p : nat → Bool} {a : nat } (H : p (a+2)) : ∃ x, p (succ x) := by apply exists_intro; assump + +definition is_zero [inline] (n : nat) +:= nat_rec true (λ n r, false) n + +theorem T2 : ∃ a, (is_zero a) = true +:= by apply exists_intro; apply refl \ No newline at end of file