From de587f938c8e7a0dbcdd9d0961455bc86ab9fe05 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 6 Jul 2017 15:10:52 +0200 Subject: [PATCH] fix(library/equations_compiler): always use ite for string literals --- src/library/equations_compiler/elim_match.cpp | 17 +- .../non_exhaustive_error.lean.expected.out | 177 ++---------------- 2 files changed, 26 insertions(+), 168 deletions(-) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index b3a5a42fe5..e72f22ec80 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -541,12 +541,17 @@ struct elim_match_fn { return r && has_variable && has_constructor; } - /* Return true iff the next pattern of every equation is a value or variable, + /* Return true if the next pattern of every equation is a value or variable, and there are at least one equation where it is a variable and another where it is a - value. */ + value. + + We also perform a value transition if one of the next patterns is a + string literal. + */ bool is_value_transition(problem const & P) { bool has_value = false; bool has_variable = false; + bool has_string = false; bool r = all_equations(P, [&](equation const & eqn) { expr const & p = head(eqn.m_patterns); if (is_local(p)) { @@ -554,12 +559,18 @@ struct elim_match_fn { } else { type_context ctx = mk_type_context(eqn.m_lctx); if (is_value(ctx, p)) { - has_value = true; return true; + has_value = true; + if (is_string_value(p)) { + has_string = true; + } + return true; } else { return false; } } }); + if (has_string) + return true; if (!r || !has_value || !has_variable) return false; type_context ctx = mk_type_context(P); diff --git a/tests/lean/non_exhaustive_error.lean.expected.out b/tests/lean/non_exhaustive_error.lean.expected.out index 58288b2c72..a8481d8fc0 100644 --- a/tests/lean/non_exhaustive_error.lean.expected.out +++ b/tests/lean/non_exhaustive_error.lean.expected.out @@ -3,169 +3,16 @@ g (1, _) g (nat.succ (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 {data := list.nil char} _ -f {data := ⟨0, _⟩ :: _} _ -f {data := ⟨1, _⟩ :: _} _ -f {data := ⟨2, _⟩ :: _} _ -f {data := ⟨3, _⟩ :: _} _ -f {data := ⟨4, _⟩ :: _} _ -f {data := ⟨5, _⟩ :: _} _ -f {data := ⟨6, _⟩ :: _} _ -f {data := ⟨7, _⟩ :: _} _ -f {data := ⟨8, _⟩ :: _} _ -f {data := ⟨9, _⟩ :: _} _ -f {data := ⟨10, _⟩ :: _} _ -f {data := ⟨11, _⟩ :: _} _ -f {data := ⟨12, _⟩ :: _} _ -f {data := ⟨13, _⟩ :: _} _ -f {data := ⟨14, _⟩ :: _} _ -f {data := ⟨15, _⟩ :: _} _ -f {data := ⟨16, _⟩ :: _} _ -f {data := ⟨17, _⟩ :: _} _ -f {data := ⟨18, _⟩ :: _} _ -f {data := ⟨19, _⟩ :: _} _ -f {data := ⟨20, _⟩ :: _} _ -f {data := ⟨21, _⟩ :: _} _ -f {data := ⟨22, _⟩ :: _} _ -f {data := ⟨23, _⟩ :: _} _ -f {data := ⟨24, _⟩ :: _} _ -f {data := ⟨25, _⟩ :: _} _ -f {data := ⟨26, _⟩ :: _} _ -f {data := ⟨27, _⟩ :: _} _ -f {data := ⟨28, _⟩ :: _} _ -f {data := ⟨29, _⟩ :: _} _ -f {data := ⟨30, _⟩ :: _} _ -f {data := ⟨31, _⟩ :: _} _ -f {data := ⟨32, _⟩ :: _} _ -f {data := ⟨33, _⟩ :: _} _ -f {data := ⟨34, _⟩ :: _} _ -f {data := ⟨35, _⟩ :: _} _ -f {data := ⟨36, _⟩ :: _} _ -f {data := ⟨37, _⟩ :: _} _ -f {data := ⟨38, _⟩ :: _} _ -f {data := ⟨39, _⟩ :: _} _ -f {data := ⟨40, _⟩ :: _} _ -f {data := ⟨41, _⟩ :: _} _ -f {data := ⟨42, _⟩ :: _} _ -f {data := ⟨43, _⟩ :: _} _ -f {data := ⟨44, _⟩ :: _} _ -f {data := ⟨45, _⟩ :: _} _ -f {data := ⟨46, _⟩ :: _} _ -f {data := ⟨47, _⟩ :: _} _ -f {data := ⟨48, _⟩ :: _} _ -f {data := ⟨49, _⟩ :: _} _ -f {data := ⟨50, _⟩ :: _} _ -f {data := ⟨51, _⟩ :: _} _ -f {data := ⟨52, _⟩ :: _} _ -f {data := ⟨53, _⟩ :: _} _ -f {data := ⟨54, _⟩ :: _} _ -f {data := ⟨55, _⟩ :: _} _ -f {data := ⟨56, _⟩ :: _} _ -f {data := ⟨57, _⟩ :: _} _ -f {data := ⟨58, _⟩ :: _} _ -f {data := ⟨59, _⟩ :: _} _ -f {data := ⟨60, _⟩ :: _} _ -f {data := ⟨61, _⟩ :: _} _ -f {data := ⟨62, _⟩ :: _} _ -f {data := ⟨63, _⟩ :: _} _ -f {data := ⟨64, _⟩ :: _} _ -f {data := ⟨65, _⟩ :: _} _ -f {data := ⟨66, _⟩ :: _} _ -f {data := ⟨67, _⟩ :: _} _ -f {data := ⟨68, _⟩ :: _} _ -f {data := ⟨69, _⟩ :: _} _ -f {data := ⟨70, _⟩ :: _} _ -f {data := ⟨71, _⟩ :: _} _ -f {data := ⟨72, _⟩ :: _} _ -f {data := ⟨73, _⟩ :: _} _ -f {data := ⟨74, _⟩ :: _} _ -f {data := ⟨75, _⟩ :: _} _ -f {data := ⟨76, _⟩ :: _} _ -f {data := ⟨77, _⟩ :: _} _ -f {data := ⟨78, _⟩ :: _} _ -f {data := ⟨79, _⟩ :: _} _ -f {data := ⟨80, _⟩ :: _} _ -f {data := ⟨81, _⟩ :: _} _ -f {data := ⟨82, _⟩ :: _} _ -f {data := ⟨83, _⟩ :: _} _ -f {data := ⟨84, _⟩ :: _} _ -f {data := ⟨85, _⟩ :: _} _ -f {data := ⟨86, _⟩ :: _} _ -f {data := ⟨87, _⟩ :: _} _ -f {data := ⟨88, _⟩ :: _} _ -f {data := ⟨89, _⟩ :: _} _ -f {data := ⟨90, _⟩ :: _} _ -f {data := ⟨91, _⟩ :: _} _ -f {data := ⟨92, _⟩ :: _} _ -f {data := ⟨93, _⟩ :: _} _ -f {data := ⟨94, _⟩ :: _} _ -f {data := ⟨95, _⟩ :: _} _ -f {data := ⟨96, _⟩ :: _} _ -f {data := ⟨97, _⟩ :: _} _ -f {data := ⟨98, _⟩ :: _} _ -f {data := ⟨99, _⟩ :: _} _ -f - {data := ⟨nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - (nat.succ - …)))))))))))))))))))))))))))))))))))))))))))))))))))))))))), - _⟩ :: - _} - _ +f "hello world" 0 +f "hello world" (nat.succ (nat.succ _)) +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: +foo (nat.succ _) 1 +non_exhaustive_error.lean:10:0: warning: declaration 'foo' uses sorry +non_exhaustive_error.lean:17:11: error: non-exhaustive match, the following cases are missing: +f 0 (nat.succ _) +f (nat.succ _) _ +g 0 (nat.succ _) +g (nat.succ _) _ +non_exhaustive_error.lean:17:0: warning: declaration '_mutual.f.g' uses sorry