Spread list tests can never touch exact-sized bounds tests

When compiling a pattern match like

```
[] -> ..
[_] -> ..
[_, ..] -> ..
```

to a decision tree, we must make sure that the last test (len >= 1)
does not touch the branch reached by the second test (len == 1). It is
enough to ban (len >=) tests from ever touching exact-sized list
patterns, because a spread test (len >=) can never reach an exact-sized
test.

On the other hand, an exact-sized test can reach a spread pattern,
because in

```
[_, _] -> ..
[..] -> ..
```

the last branch generates tests for patterns `[]` and `[_]`, and we would
like those patterns to be covered by the spread test (len >= 0)!

Closes #4685
This commit is contained in:
Ayaz Hafiz 2022-12-05 13:45:35 -06:00
parent b6a96ebb85
commit 759127660d
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
3 changed files with 62 additions and 62 deletions

View file

@ -425,6 +425,7 @@ fn flatten<'a>(
/// variables to "how to get their value". So a pattern like (Just (x,_)) will give
/// us something like ("x" => value.0.0)
#[derive(Debug)]
enum Match {
Exact(Label),
GuardOnly,
@ -795,7 +796,22 @@ fn to_relevant_branch_help<'a>(
elements,
element_layout: _,
} => match test {
IsListLen { bound: _, len } if my_arity.covers_length(*len as _) => {
IsListLen {
bound: test_bound,
len,
} if my_arity.covers_length(*len as _)
// Spread tests [_, ..] can only match spread tests, not exact-sized bounds [_].
//
// On the other hand, exact-sized tests [_] can match spread bounds [_, ..],
// because each spread bound generates 0 or more exact-sized tests.
//
// See exhaustiveness checking of lists for more details on the tests generated
// for spread bounds.
&& !matches!(
(test_bound, my_arity),
(ListLenBound::AtLeast, ListArity::Exact(..))
) =>
{
let sub_positions = elements.into_iter().enumerate().map(|(index, elem_pat)| {
let mut new_path = path.to_vec();

View file

@ -1,24 +1,18 @@
procedure Test.0 ():
let Test.8 : Str = "";
let Test.1 : List Str = Array [Test.8];
joinpoint Test.6:
let Test.4 : Str = "C";
ret Test.4;
in
joinpoint Test.5:
let Test.3 : Str = "B";
ret Test.3;
in
let Test.7 : U64 = lowlevel ListLen Test.1;
let Test.6 : Str = "";
let Test.1 : List Str = Array [Test.6];
let Test.5 : U64 = lowlevel ListLen Test.1;
dec Test.1;
switch Test.7:
switch Test.5:
case 0:
let Test.2 : Str = "A";
ret Test.2;
case 1:
jump Test.5;
let Test.3 : Str = "B";
ret Test.3;
default:
jump Test.5;
let Test.4 : Str = "C";
ret Test.4;

View file

@ -1,52 +1,49 @@
procedure Test.0 ():
let Test.36 : Int1 = false;
let Test.37 : Int1 = true;
let Test.1 : List Int1 = Array [Test.36, Test.37];
joinpoint Test.10:
let Test.31 : Int1 = false;
let Test.32 : Int1 = true;
let Test.1 : List Int1 = Array [Test.31, Test.32];
joinpoint Test.9:
let Test.8 : Str = "E";
ret Test.8;
in
joinpoint Test.9:
let Test.5 : Str = "B";
ret Test.5;
in
let Test.33 : U64 = lowlevel ListLen Test.1;
let Test.34 : U64 = 0i64;
let Test.35 : Int1 = lowlevel Eq Test.33 Test.34;
if Test.35 then
let Test.28 : U64 = lowlevel ListLen Test.1;
let Test.29 : U64 = 0i64;
let Test.30 : Int1 = lowlevel Eq Test.28 Test.29;
if Test.30 then
dec Test.1;
let Test.4 : Str = "A";
ret Test.4;
else
let Test.30 : U64 = lowlevel ListLen Test.1;
let Test.31 : U64 = 1i64;
let Test.32 : Int1 = lowlevel Eq Test.30 Test.31;
if Test.32 then
let Test.11 : U64 = 0i64;
let Test.12 : Int1 = lowlevel ListGetUnsafe Test.1 Test.11;
let Test.25 : U64 = lowlevel ListLen Test.1;
let Test.26 : U64 = 1i64;
let Test.27 : Int1 = lowlevel Eq Test.25 Test.26;
if Test.27 then
let Test.10 : U64 = 0i64;
let Test.11 : Int1 = lowlevel ListGetUnsafe Test.1 Test.10;
dec Test.1;
let Test.13 : Int1 = false;
let Test.14 : Int1 = lowlevel Eq Test.13 Test.12;
if Test.14 then
jump Test.9;
let Test.12 : Int1 = false;
let Test.13 : Int1 = lowlevel Eq Test.12 Test.11;
if Test.13 then
let Test.5 : Str = "B";
ret Test.5;
else
jump Test.10;
jump Test.9;
else
let Test.27 : U64 = lowlevel ListLen Test.1;
let Test.28 : U64 = 2i64;
let Test.29 : Int1 = lowlevel NumGte Test.27 Test.28;
if Test.29 then
let Test.19 : U64 = 0i64;
let Test.20 : Int1 = lowlevel ListGetUnsafe Test.1 Test.19;
let Test.21 : Int1 = false;
let Test.22 : Int1 = lowlevel Eq Test.21 Test.20;
if Test.22 then
let Test.15 : U64 = 1i64;
let Test.16 : Int1 = lowlevel ListGetUnsafe Test.1 Test.15;
let Test.22 : U64 = lowlevel ListLen Test.1;
let Test.23 : U64 = 2i64;
let Test.24 : Int1 = lowlevel NumGte Test.22 Test.23;
if Test.24 then
let Test.18 : U64 = 0i64;
let Test.19 : Int1 = lowlevel ListGetUnsafe Test.1 Test.18;
let Test.20 : Int1 = false;
let Test.21 : Int1 = lowlevel Eq Test.20 Test.19;
if Test.21 then
let Test.14 : U64 = 1i64;
let Test.15 : Int1 = lowlevel ListGetUnsafe Test.1 Test.14;
dec Test.1;
let Test.17 : Int1 = false;
let Test.18 : Int1 = lowlevel Eq Test.17 Test.16;
if Test.18 then
let Test.16 : Int1 = false;
let Test.17 : Int1 = lowlevel Eq Test.16 Test.15;
if Test.17 then
let Test.6 : Str = "C";
ret Test.6;
else
@ -54,14 +51,7 @@ procedure Test.0 ():
ret Test.7;
else
dec Test.1;
jump Test.10;
else
let Test.23 : U64 = 0i64;
let Test.24 : Int1 = lowlevel ListGetUnsafe Test.1 Test.23;
dec Test.1;
let Test.25 : Int1 = false;
let Test.26 : Int1 = lowlevel Eq Test.25 Test.24;
if Test.26 then
jump Test.9;
else
jump Test.10;
else
dec Test.1;
jump Test.9;