feat(library/equations_compiler/elim_match): extend is_value_transition trick to other infinite types

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. */

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 : ℕ → ℕ,

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
+| (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

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