From 38c2c7dae81c148ba7a68908c765fb54297003bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Jul 2017 22:03:52 -0700 Subject: [PATCH] feat(library/equations_compiler/elim_match): extend is_value_transition trick to other infinite types --- src/library/equations_compiler/elim_match.cpp | 20 ++++++++++++------- tests/lean/eqn_hole.lean.expected.out | 2 +- tests/lean/non_exhaustive_error.lean | 18 +++++++++++++++-- .../non_exhaustive_error.lean.expected.out | 16 ++++++++++++--- 4 files changed, 43 insertions(+), 13 deletions(-) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index 5ef3fa93b1..64980dd50f 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -326,6 +326,11 @@ struct elim_match_fn { } } + bool is_finite_value(type_context & ctx, expr const & e) { + lean_assert(is_value(ctx, e)); + return is_char_value(ctx, e); + } + bool is_transport_app(expr const & e) { if (!is_app(e)) return false; expr const & fn = get_app_fn(e); @@ -549,9 +554,9 @@ struct elim_match_fn { string literal. */ bool is_value_transition(problem const & P) { - bool has_value = false; - bool has_variable = false; - bool has_string = false; + bool has_value = false; + bool has_variable = false; + bool has_finite_value = false; bool r = all_equations(P, [&](equation const & eqn) { expr const & p = head(eqn.m_patterns); if (is_local(p)) { @@ -560,16 +565,17 @@ struct elim_match_fn { type_context ctx = mk_type_context(eqn.m_lctx); if (is_value(ctx, p)) { has_value = true; - if (is_string_value(p)) { - has_string = true; - } + if (is_finite_value(ctx, p)) + has_finite_value = true; return true; } else { return false; } } }); - if (!has_string && (!r || !has_value || !has_variable)) + if (!r || !has_value) + return false; + if (!has_variable && has_finite_value) return false; type_context ctx = mk_type_context(P); /* Check whether other variables on the variable stack depend on the head. */ diff --git a/tests/lean/eqn_hole.lean.expected.out b/tests/lean/eqn_hole.lean.expected.out index 72ea9168fd..e0ffc31be7 100644 --- a/tests/lean/eqn_hole.lean.expected.out +++ b/tests/lean/eqn_hole.lean.expected.out @@ -3,7 +3,7 @@ context: f : ℕ → ℕ ⊢ ℕ eqn_hole.lean:2:11: error: non-exhaustive match, the following cases are missing: -f (nat.succ _) +f _ eqn_hole.lean:8:13: error: don't know how to synthesize placeholder context: g : ℕ → ℕ, diff --git a/tests/lean/non_exhaustive_error.lean b/tests/lean/non_exhaustive_error.lean index 1c8591351a..6a0622b786 100644 --- a/tests/lean/non_exhaustive_error.lean +++ b/tests/lean/non_exhaustive_error.lean @@ -1,4 +1,4 @@ - +-- def g : ℕ × ℕ → ℕ | (0, n) := n | (m+2, 0) := m @@ -25,4 +25,18 @@ end other inductive term | mk : ℕ → list term → term def const_name : term → ℕ -| (term.mk n []) := n \ No newline at end of file +| (term.mk n []) := n + +namespace other2 +def f : nat → nat +| 1000 := 1 + +def g : string → nat +| "hello" := 0 + +meta def h : name → nat +| `eq := 0 + +def r : int → nat +| -1000 := 0 +end other2 diff --git a/tests/lean/non_exhaustive_error.lean.expected.out b/tests/lean/non_exhaustive_error.lean.expected.out index 2ea4db1dcd..3a12360c43 100644 --- a/tests/lean/non_exhaustive_error.lean.expected.out +++ b/tests/lean/non_exhaustive_error.lean.expected.out @@ -1,10 +1,9 @@ non_exhaustive_error.lean:2:4: error: non-exhaustive match, the following cases are missing: g (1, _) -g (nat.succ (nat.succ _), nat.succ _) +g (nat.succ (nat.succ _), _) non_exhaustive_error.lean:2:0: warning: declaration 'g' uses sorry non_exhaustive_error.lean:6:11: error: non-exhaustive match, the following cases are missing: -f "hello world" 0 -f "hello world" (nat.succ (nat.succ _)) +f "hello world" _ f _ _ non_exhaustive_error.lean:6:0: warning: declaration 'f' uses sorry non_exhaustive_error.lean:10:4: error: non-exhaustive match, the following cases are missing: @@ -19,3 +18,14 @@ non_exhaustive_error.lean:17:0: warning: declaration '_mutual.f.g' uses sorry non_exhaustive_error.lean:27:4: error: non-exhaustive match, the following cases are missing: const_name (term.mk _ (term.mk _ _ :: _)) non_exhaustive_error.lean:27:0: warning: declaration 'const_name' uses sorry +non_exhaustive_error.lean:31:4: error: non-exhaustive match, the following cases are missing: +f _ +non_exhaustive_error.lean:31:0: warning: declaration 'other2.f' uses sorry +non_exhaustive_error.lean:34:4: error: non-exhaustive match, the following cases are missing: +g _ +non_exhaustive_error.lean:34:0: warning: declaration 'other2.g' uses sorry +non_exhaustive_error.lean:37:9: error: non-exhaustive match, the following cases are missing: +h _ +non_exhaustive_error.lean:40:4: error: non-exhaustive match, the following cases are missing: +r _ +non_exhaustive_error.lean:40:0: warning: declaration 'other2.r' uses sorry