Skip to content

Commit 123e538

Browse files
liufengyunliufengyun
authored
Merge pull request #12271 from dotty-staging/fix-12241
Fix #12241: Make space computation lazy
2 parents 3633d62 + 16a622f commit 123e538

File tree

7 files changed

+132
-43
lines changed

7 files changed

+132
-43
lines changed

‎bench/profiles/exhaustivity.yml

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,12 @@ charts:
3535
- key: exhaustivity-mips
3636
label: bootstrapped
3737

38+
- name: "exhaustivity i12241"
39+
url: https://github.com/lampepfl/dotty/blob/master/tests/patmat/i12241.scala
40+
lines:
41+
- key: exhaustivity-i12241
42+
label: bootstrapped
43+
3844
scripts:
3945

4046
patmatexhaust:
@@ -55,5 +61,8 @@ scripts:
5561
exhaustivity-mips:
5662
- measure 20 40 3 $PROG_HOME/dotty/tests/patmat/i7186.scala
5763

64+
exhaustivity-i12241:
65+
- measure 20 40 3 $PROG_HOME/dotty/tests/patmat/i12241.scala
66+
5867
config:
5968
pr_base_url: "https://github.com/lampepfl/dotty/pull/"

‎compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

Lines changed: 34 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ case class Typ(tp: Type, decomposed: Boolean = true) extends Space
7272
case class Prod(tp: Type, unappTp: TermRef, params: List[Space]) extends Space
7373

7474
/** Union of spaces */
75-
case class Or(spaces: List[Space]) extends Space
75+
case class Or(spaces: Seq[Space]) extends Space
7676

7777
/** abstract space logic */
7878
trait SpaceLogic {
@@ -113,45 +113,37 @@ trait SpaceLogic {
113113
/** Display space in string format */
114114
def show(sp: Space): String
115115

116-
/** Simplify space using the laws, there's no nested union after simplify
117-
*
118-
* @param aggressive if true and OR space has less than 5 components, `simplify` will
119-
* collapse `sp1 | sp2` to `sp1` if `sp2` is a subspace of `sp1`.
120-
*
121-
* This reduces noise in counterexamples.
122-
*/
123-
def simplify(space: Space, aggressive: Boolean = false)(using Context): Space = trace(s"simplify ${show(space)}, aggressive = $aggressive --> ", debug, x => show(x.asInstanceOf[Space]))(space match {
116+
/** Simplify space using the laws, there's no nested union after simplify */
117+
def simplify(space: Space)(using Context): Space = trace(s"simplify ${show(space)} --> ", debug, x => show(x.asInstanceOf[Space]))(space match {
124118
case Prod(tp, fun, spaces) =>
125119
val sp = Prod(tp, fun, spaces.map(simplify(_)))
126120
if (sp.params.contains(Empty)) Empty
127121
else if (canDecompose(tp) && decompose(tp).isEmpty) Empty
128122
else sp
129123
case Or(spaces) =>
130-
val buf = new mutable.ListBuffer[Space]
131-
def include(s: Space) = if s != Empty then buf += s
132-
for space <- spaces do
133-
simplify(space) match
134-
case Or(ss) => ss.foreach(include)
135-
case s => include(s)
136-
val set = buf.toList
137-
138-
if (set.isEmpty) Empty
139-
else if (set.size == 1) set.toList(0)
140-
else if (aggressive && spaces.size < 5) {
141-
val res = set.map(sp => (sp, set.filter(_ ne sp))).find {
142-
case (sp, sps) =>
143-
isSubspace(sp, Or(sps))
144-
}
145-
if (res.isEmpty) Or(set)
146-
else simplify(Or(res.get._2), aggressive)
147-
}
148-
else Or(set)
124+
val spaces2 = spaces.map(simplify(_)).filter(_ != Empty)
125+
if spaces2.isEmpty then Empty
126+
else Or(spaces2)
149127
case Typ(tp, _) =>
150128
if (canDecompose(tp) && decompose(tp).isEmpty) Empty
151129
else space
152130
case _ => space
153131
})
154132

133+
/** Remove a space if it's a subspace of remaining spaces
134+
*
135+
* Note: `dedup` will return the same result if the sequence >= 10
136+
*/
137+
def dedup(spaces: Seq[Space])(using Context): Seq[Space] =
138+
if (spaces.lengthCompare(1) <= 0 || spaces.lengthCompare(10) >= 0) spaces
139+
else {
140+
val res = spaces.map(sp => (sp, spaces.filter(_ ne sp))).find {
141+
case (sp, sps) => isSubspace(sp, Or(LazyList(sps: _*)))
142+
}
143+
if (res.isEmpty) spaces
144+
else res.get._2
145+
}
146+
155147
/** Flatten space to get rid of `Or` for pretty print */
156148
def flatten(space: Space)(using Context): Seq[Space] = space match {
157149
case Prod(tp, fun, spaces) =>
@@ -205,8 +197,8 @@ trait SpaceLogic {
205197

206198
(a, b) match {
207199
case (Empty, _) | (_, Empty) => Empty
208-
case (_, Or(ss)) => Or(ss.map(intersect(a, _)).filterConserve(_ ne Empty))
209-
case (Or(ss), _) => Or(ss.map(intersect(_, b)).filterConserve(_ ne Empty))
200+
case (_, Or(ss)) => Or(ss.map(intersect(a, _)).filter(_ ne Empty))
201+
case (Or(ss), _) => Or(ss.map(intersect(_, b)).filter(_ ne Empty))
210202
case (Typ(tp1, _), Typ(tp2, _)) =>
211203
if (isSubType(tp1, tp2)) a
212204
else if (isSubType(tp2, tp1)) b
@@ -263,8 +255,6 @@ trait SpaceLogic {
263255
Empty
264256
else if (canDecompose(tp2))
265257
tryDecompose2(tp2)
266-
else if (isSubType(tp2, tp1) &&covers(fun, tp2))
267-
minus(a, Prod(tp1, fun, signature(fun, tp1, ss.length).map(Typ(_, false))))
268258
else
269259
a
270260
case (Prod(tp1, fun1, ss1), Prod(tp2, fun2, ss2)) =>
@@ -282,7 +272,7 @@ trait SpaceLogic {
282272
else if cache.forall(sub => isSubspace(sub, Empty)) then Empty
283273
else
284274
// `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
285-
Or(range.map { i => Prod(tp1, fun1, ss1.updated(i, sub(i))) })
275+
Or(LazyList(range: _*).map { i => Prod(tp1, fun1, ss1.updated(i, sub(i))) })
286276
}
287277
}
288278
}
@@ -601,7 +591,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
601591
tp.dealias match {
602592
case AndType(tp1, tp2) =>
603593
intersect(Typ(tp1, false), Typ(tp2, false)) match {
604-
case Or(spaces) => spaces
594+
case Or(spaces) => spaces.toList
605595
case Empty => Nil
606596
case space => List(space)
607597
}
@@ -842,14 +832,15 @@ class SpaceEngine(using Context) extends SpaceLogic {
842832
val checkGADTSAT = shouldCheckExamples(selTyp)
843833

844834
val uncovered =
845-
flatten(simplify(minus(project(selTyp), patternSpace), aggressive = true)).filter { s =>
835+
flatten(simplify(minus(project(selTyp), patternSpace))).filter({ s =>
846836
s != Empty && (!checkGADTSAT || satisfiable(s))
847-
}
837+
})
848838

849839

850840
if uncovered.nonEmpty then
851841
val hasMore = uncovered.lengthCompare(6) > 0
852-
report.warning(PatternMatchExhaustivity(show(uncovered.take(6)), hasMore), sel.srcPos)
842+
val deduped = dedup(uncovered.take(6))
843+
report.warning(PatternMatchExhaustivity(show(deduped), hasMore), sel.srcPos)
853844
}
854845

855846
private def redundancyCheckable(sel: Tree): Boolean =
@@ -908,11 +899,13 @@ class SpaceEngine(using Context) extends SpaceLogic {
908899
// If explicit nulls are enabled, this check isn't needed because most of the cases
909900
// that would trigger it would also trigger unreachability warnings.
910901
if (!ctx.explicitNulls && i == cases.length - 1 && !isNullLit(pat) ) {
911-
simplify(minus(covered, prevs)) match {
912-
case Typ(`constantNullType`, _) =>
902+
val spaces = flatten(simplify(minus(covered, prevs)))
903+
if spaces.lengthCompare(10) < 0 then
904+
dedup(spaces).toList match
905+
case Typ(`constantNullType`, _) :: Nil =>
913906
report.warning(MatchCaseOnlyNullWarning(), pat.srcPos)
914-
case _ =>
915-
}
907+
case s =>
908+
debug.println("`_` matches = " + s)
916909
}
917910
}
918911
}

‎tests/patmat/dotty-trees.scala

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
abstract class Tree[-T >: Null]
2+
3+
case class TypeTree[-T >: Null]() extends Tree[T]
4+
5+
abstract class DerivedTypeTree() extends TypeTree[Null]
6+
7+
def foo(tree: Tree[Null]): Unit =
8+
tree match
9+
case _: DerivedTypeTree =>
10+
case TypeTree() =>
11+
case _ =>

‎tests/patmat/i12241.check

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +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())

‎tests/patmat/i12241.scala

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
sealed trait EndpointInput[T]
2+
3+
object EndpointInput {
4+
case class Pair[T]() extends EndpointInput[T]
5+
case class MappedPair[T]() extends EndpointInput[T]
6+
case class Pair2[T]() extends EndpointInput[T]
7+
case class MappedPair2[T]() extends EndpointInput[T]
8+
case class FixedMethod[T]() extends EndpointInput[T]
9+
case class FixedPath[T]() extends EndpointInput[T]
10+
case class PathCapture[T]() extends EndpointInput[T]
11+
case class PathsCapture[T]() extends EndpointInput[T]
12+
case class Query[T]() extends EndpointInput[T]
13+
case class QueryParams[T]() extends EndpointInput[T]
14+
case class Cookie[T]() extends EndpointInput[T]
15+
case class ExtractFromRequest[T]() extends EndpointInput[T]
16+
case class ApiKey[T]() extends EndpointInput[T]
17+
case class Http[T]() extends EndpointInput[T]
18+
case class Body[R, T]() extends EndpointInput[T]
19+
case class FixedHeader[T]() extends EndpointInput[T]
20+
case class Header[T]() extends EndpointInput[T]
21+
case class Headers[T]() extends EndpointInput[T]
22+
case class StatusCode[T]() extends EndpointInput[T]
23+
case class Empty[T]() extends EndpointInput[T]
24+
}
25+
26+
object Test extends App {
27+
import EndpointInput._
28+
29+
def compare(left: EndpointInput[_], right: EndpointInput[_]): Boolean =
30+
(left, right) match {
31+
case (Pair(), Pair()) => true
32+
case (MappedPair(), MappedPair()) => true
33+
case (Pair2(), Pair2()) => true
34+
case (MappedPair2(), MappedPair2()) => true
35+
case (FixedMethod(), FixedMethod()) => true
36+
case (FixedPath(), FixedPath()) => true
37+
case (PathCapture(), PathCapture()) => true
38+
case (PathsCapture(), PathsCapture()) => true
39+
case (Query(), Query()) => true
40+
case (QueryParams(), QueryParams()) => true
41+
case (Cookie(), Cookie()) => true
42+
case (ExtractFromRequest(), ExtractFromRequest()) => true
43+
case (ApiKey(), ApiKey()) => true
44+
case (Http(), Http()) => true
45+
case (Body(), Body()) => true
46+
case (FixedHeader(), FixedHeader()) => true
47+
case (Header(), Header()) => true
48+
case (Headers(), Headers()) => true
49+
case (StatusCode(), StatusCode()) => true
50+
case (_, _) => false
51+
}
52+
53+
def compare2(left: EndpointInput[_], right: EndpointInput[_]): Boolean =
54+
(left, right) match {
55+
case (Pair(), Pair()) => true
56+
case (MappedPair(), MappedPair()) => true
57+
case (Pair2(), Pair2()) => true
58+
case (MappedPair2(), MappedPair2()) => true
59+
case (FixedMethod(), FixedMethod()) => true
60+
case (FixedPath(), FixedPath()) => true
61+
case (PathCapture(), PathCapture()) => true
62+
case (PathsCapture(), PathsCapture()) => true
63+
case (Query(), Query()) => true
64+
case (QueryParams(), QueryParams()) => true
65+
case (Cookie(), Cookie()) => true
66+
case (ExtractFromRequest(), ExtractFromRequest()) => true
67+
case (ApiKey(), ApiKey()) => true
68+
case (Http(), Http()) => true
69+
case (Body(), Body()) => true
70+
case (FixedHeader(), FixedHeader()) => true
71+
case (Header(), Header()) => true
72+
case (Headers(), Headers()) => true
73+
case (StatusCode(), StatusCode()) => true
74+
}
75+
}

‎tests/patmat/i8922c.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
26: Pattern Match Exhaustivity: (true, _: String, _), (true, _: Double, _), (true, true, _), (true, false, _), (true, (), _), (false, _: String, _)
1+
26: Pattern Match Exhaustivity: (true, _, _), (false, _, _), ((), _, _), (true, _: Double, _), (true, true, _)

‎tests/patmat/t10019.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
2: Pattern Match Exhaustivity: (List(_, _, _*), List(_, _*)), (Nil, List(_, _*)), (List(_, _*), List(_, _, _*)), (List(_, _*), Nil)
1+
2: Pattern Match Exhaustivity: (List(_, _, _*), List(_, _*)), (Nil, List(_, _*)), (List(_, _*), List(_, _, _*)), (List(_, _*), Nil), (_: List, List(_, _, _*))
22
11: Pattern Match Exhaustivity: (Foo(None), Foo(_))

0 commit comments

Comments
 (0)