From 10b5ca02e2b5135bf79d23e86af8a3c3a8358ccf Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 7 May 2021 11:08:49 +0200 Subject: [PATCH 1/4] Fix #12358: Avoid spurious unions in simplification And be more lazier in product subtraction --- .../tools/dotc/transform/patmat/Space.scala | 18 +++++++++++------- tests/patmat/i12358.scala | 5 +++++ 2 files changed, 16 insertions(+), 7 deletions(-) create mode 100644 tests/patmat/i12358.scala diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala index bcb021af7b76..b1bb464f359a 100644 --- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala +++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala @@ -113,16 +113,17 @@ trait SpaceLogic { /** Display space in string format */ def show(sp: Space): String - /** Simplify space using the laws, there's no nested union after simplify */ + /** Simplify space such that a space equal to `Empty` becomes `Empty` */ def simplify(space: Space)(using Context): Space = trace(s"simplify ${show(space)} --> ", debug, x => show(x.asInstanceOf[Space]))(space match { case Prod(tp, fun, spaces) => - val sp = Prod(tp, fun, spaces.map(simplify(_))) - if (sp.params.contains(Empty)) Empty + val sps = spaces.map(simplify(_)) + if (sps.contains(Empty)) Empty else if (canDecompose(tp) && decompose(tp).isEmpty) Empty - else sp + else Prod(tp, fun, sps) case Or(spaces) => val spaces2 = spaces.map(simplify(_)).filter(_ != Empty) if spaces2.isEmpty then Empty + else if spaces2.lengthCompare(1) == 0 then spaces2.head else Or(spaces2) case Typ(tp, _) => if (canDecompose(tp) && decompose(tp).isEmpty) Empty @@ -243,10 +244,10 @@ trait SpaceLogic { tryDecompose1(tp1) else a - case (_, Or(ss)) => - ss.foldLeft(a)(minus) case (Or(ss), _) => Or(ss.map(minus(_, b))) + case (_, Or(ss)) => + ss.foldLeft(a)(minus) case (Prod(tp1, fun, ss), Typ(tp2, _)) => // uncovered corner case: tp2 :< tp1, may happen when inheriting case class if (isSubType(tp1, tp2)) @@ -272,7 +273,10 @@ trait SpaceLogic { else if cache.forall(sub => isSubspace(sub, Empty)) then Empty else // `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)` - Or(LazyList(range: _*).map { i => Prod(tp1, fun1, ss1.updated(i, sub(i))) }) + val spaces = LazyList(range: _*).flatMap { i => + flatten(sub(i)).map(s => Prod(tp1, fun1, ss1.updated(i, s))) + } + Or(spaces) } } } diff --git a/tests/patmat/i12358.scala b/tests/patmat/i12358.scala new file mode 100644 index 000000000000..b58d312838ce --- /dev/null +++ b/tests/patmat/i12358.scala @@ -0,0 +1,5 @@ + +def foo(x: List[Int]): Unit = + x match + // case x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: x11 :: x12 :: x13 :: x14 :: Nil => + case x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: x11 :: x12 :: x13 :: x14 :: x15 :: x16 :: x17 :: x18 :: x19 :: x20 :: x21 :: x22 :: Nil => \ No newline at end of file From 2433be6f197b405e5634b1639ccb2c97a9a0bc06 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 7 May 2021 14:56:14 +0200 Subject: [PATCH 2/4] Update check files: order of counter examples changed --- tests/patmat/i12241.check | 2 +- tests/patmat/i12358.check | 1 + tests/patmat/i8922c.check | 2 +- tests/patmat/t10019.check | 2 +- 4 files changed, 4 insertions(+), 3 deletions(-) create mode 100644 tests/patmat/i12358.check diff --git a/tests/patmat/i12241.check b/tests/patmat/i12241.check index 2b3f2416f40a..1ad41cfa2ac1 100644 --- a/tests/patmat/i12241.check +++ b/tests/patmat/i12241.check @@ -1 +1 @@ -54: Pattern Match Exhaustivity: (EndpointInput.Empty(), _), (EndpointInput.Pair(), EndpointInput.MappedPair()), (EndpointInput.Pair(), EndpointInput.Pair2()), (EndpointInput.Pair(), EndpointInput.MappedPair2()), (EndpointInput.Pair(), EndpointInput.FixedMethod()), (EndpointInput.Pair(), EndpointInput.FixedPath()) +54: Pattern Match Exhaustivity: (EndpointInput.Pair(), EndpointInput.MappedPair()), (EndpointInput.Pair(), EndpointInput.Pair2()), (EndpointInput.Pair(), EndpointInput.MappedPair2()), (EndpointInput.Pair(), EndpointInput.FixedMethod()), (EndpointInput.Pair(), EndpointInput.FixedPath()), (EndpointInput.Pair(), EndpointInput.PathCapture()) diff --git a/tests/patmat/i12358.check b/tests/patmat/i12358.check new file mode 100644 index 000000000000..d1979b049b29 --- /dev/null +++ b/tests/patmat/i12358.check @@ -0,0 +1 @@ +3: Pattern Match Exhaustivity: List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _*), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ) diff --git a/tests/patmat/i8922c.check b/tests/patmat/i8922c.check index 608e48c4b67c..acd56ccd2986 100644 --- a/tests/patmat/i8922c.check +++ b/tests/patmat/i8922c.check @@ -1 +1 @@ -26: Pattern Match Exhaustivity: (true, _, _), (false, _, _), ((), _, _), (true, _: Double, _), (true, true, _) +26: Pattern Match Exhaustivity: (_: Int, _: String, _), (_: Int, _: Int, BANG), (_: Int, _: Int, BANG_EQUAL), (_: Int, _: Int, EQUAL), (_: Int, _: Int, EQUAL_EQUAL), (_: Int, true, _) diff --git a/tests/patmat/t10019.check b/tests/patmat/t10019.check index 885aba2381e4..4eb648ea2ae4 100644 --- a/tests/patmat/t10019.check +++ b/tests/patmat/t10019.check @@ -1,2 +1,2 @@ -2: Pattern Match Exhaustivity: (List(_, _, _*), List(_, _*)), (Nil, List(_, _*)), (List(_, _*), List(_, _, _*)), (List(_, _*), Nil), (_: List, List(_, _, _*)) +2: Pattern Match Exhaustivity: (List(_, _, _*), _: List), (Nil, List(_, _*)), (_: List, List(_, _, _*)), (List(_, _*), Nil) 11: Pattern Match Exhaustivity: (Foo(None), Foo(_)) From 1f13d1989256b506a3f70c787ab7a449ae099bbc Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 7 May 2021 15:04:03 +0200 Subject: [PATCH 3/4] Fix printing of counter-examples for List --- compiler/src/dotty/tools/dotc/transform/patmat/Space.scala | 2 +- tests/patmat/i12358.check | 2 +- tests/patmat/i12358.scala | 1 - 3 files changed, 2 insertions(+), 3 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala index b1bb464f359a..0707587b5b99 100644 --- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala +++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala @@ -775,7 +775,7 @@ class SpaceEngine(using Context) extends SpaceLogic { if (ctx.definitions.isTupleType(tp)) "(" + params.map(doShow(_)).mkString(", ") + ")" else if (tp.isRef(scalaConsType.symbol)) - if (flattenList) params.map(doShow(_, flattenList)).mkString(", ") + if (flattenList) params.map(doShow(_, flattenList)).filter(_.nonEmpty).mkString(", ") else params.map(doShow(_, flattenList = true)).filter(!_.isEmpty).mkString("List(", ", ", ")") else { val sym = fun.symbol diff --git a/tests/patmat/i12358.check b/tests/patmat/i12358.check index d1979b049b29..0ffca060173b 100644 --- a/tests/patmat/i12358.check +++ b/tests/patmat/i12358.check @@ -1 +1 @@ -3: Pattern Match Exhaustivity: List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _*), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, ) +3: Pattern Match Exhaustivity: List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _*), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _), List(_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _) diff --git a/tests/patmat/i12358.scala b/tests/patmat/i12358.scala index b58d312838ce..9b8a865ae000 100644 --- a/tests/patmat/i12358.scala +++ b/tests/patmat/i12358.scala @@ -1,5 +1,4 @@ def foo(x: List[Int]): Unit = x match - // case x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: x11 :: x12 :: x13 :: x14 :: Nil => case x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: x8 :: x9 :: x10 :: x11 :: x12 :: x13 :: x14 :: x15 :: x16 :: x17 :: x18 :: x19 :: x20 :: x21 :: x22 :: Nil => \ No newline at end of file From b3ed6f51c2f040da725244fe09119ba3b04cccfe Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 7 May 2021 15:06:03 +0200 Subject: [PATCH 4/4] Add example as bench test --- bench/profiles/exhaustivity.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/bench/profiles/exhaustivity.yml b/bench/profiles/exhaustivity.yml index 0e765bb592d9..d8295a27060e 100644 --- a/bench/profiles/exhaustivity.yml +++ b/bench/profiles/exhaustivity.yml @@ -41,6 +41,12 @@ charts: - key: exhaustivity-i12241 label: bootstrapped + - name: "exhaustivity i12358" + url: https://github.com/lampepfl/dotty/blob/master/tests/patmat/i12358.scala + lines: + - key: exhaustivity-i12358 + label: bootstrapped + scripts: patmatexhaust: @@ -64,5 +70,8 @@ scripts: exhaustivity-i12241: - measure 20 40 3 $PROG_HOME/dotty/tests/patmat/i12241.scala + exhaustivity-i12358: + - measure 20 40 3 $PROG_HOME/dotty/tests/patmat/i12358.scala + config: pr_base_url: "https://github.com/lampepfl/dotty/pull/"