@@ -72,7 +72,7 @@ case class Typ(tp: Type, decomposed: Boolean = true) extends Space
72
72
case class Prod (tp : Type , unappTp : TermRef , params : List [Space ]) extends Space
73
73
74
74
/** Union of spaces */
75
- case class Or (spaces : List [Space ]) extends Space
75
+ case class Or (spaces : Seq [Space ]) extends Space
76
76
77
77
/** abstract space logic */
78
78
trait SpaceLogic {
@@ -113,45 +113,40 @@ trait SpaceLogic {
113
113
/** Display space in string format */
114
114
def show (sp : Space ): String
115
115
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 {
124
118
case Prod (tp, fun, spaces) =>
125
119
val sp = Prod (tp, fun, spaces.map(simplify(_)))
126
120
if (sp.params.contains(Empty )) Empty
127
121
else if (canDecompose(tp) && decompose(tp).isEmpty) Empty
128
122
else sp
129
123
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)
149
127
case Typ (tp, _) =>
150
128
if (canDecompose(tp) && decompose(tp).isEmpty) Empty
151
129
else space
152
130
case _ => space
153
131
})
154
132
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
+ val total = spaces.take(10 )
139
+
140
+ if (total.size < 1 || total.size >= 10 ) total
141
+ else {
142
+ val res = spaces.map(sp => (sp, spaces.filter(_ ne sp))).find {
143
+ case (sp, sps) => isSubspace(sp, Or (LazyList (sps : _* )))
144
+ }
145
+ if (res.isEmpty) spaces
146
+ else res.get._2
147
+ }
148
+ }
149
+
155
150
/** Flatten space to get rid of `Or` for pretty print */
156
151
def flatten (space : Space )(using Context ): Seq [Space ] = space match {
157
152
case Prod (tp, fun, spaces) =>
@@ -205,8 +200,8 @@ trait SpaceLogic {
205
200
206
201
(a, b) match {
207
202
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 ))
203
+ case (_, Or (ss)) => Or (ss.map(intersect(a, _)).filter (_ ne Empty ))
204
+ case (Or (ss), _) => Or (ss.map(intersect(_, b)).filter (_ ne Empty ))
210
205
case (Typ (tp1, _), Typ (tp2, _)) =>
211
206
if (isSubType(tp1, tp2)) a
212
207
else if (isSubType(tp2, tp1)) b
@@ -282,7 +277,7 @@ trait SpaceLogic {
282
277
else if cache.forall(sub => isSubspace(sub, Empty )) then Empty
283
278
else
284
279
// `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
285
- Or (range.map { i => Prod (tp1, fun1, ss1.updated(i, sub(i))) })
280
+ Or (LazyList ( range : _* ) .map { i => Prod (tp1, fun1, ss1.updated(i, sub(i))) })
286
281
}
287
282
}
288
283
}
@@ -601,7 +596,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
601
596
tp.dealias match {
602
597
case AndType (tp1, tp2) =>
603
598
intersect(Typ (tp1, false ), Typ (tp2, false )) match {
604
- case Or (spaces) => spaces
599
+ case Or (spaces) => spaces.toList
605
600
case Empty => Nil
606
601
case space => List (space)
607
602
}
@@ -842,14 +837,15 @@ class SpaceEngine(using Context) extends SpaceLogic {
842
837
val checkGADTSAT = shouldCheckExamples(selTyp)
843
838
844
839
val uncovered =
845
- flatten(simplify(minus(project(selTyp), patternSpace), aggressive = true )).filter { s =>
840
+ flatten(simplify(minus(project(selTyp), patternSpace))).filter( { s =>
846
841
s != Empty && (! checkGADTSAT || satisfiable(s))
847
- }
842
+ })
848
843
849
844
850
845
if uncovered.nonEmpty then
851
846
val hasMore = uncovered.lengthCompare(6 ) > 0
852
- report.warning(PatternMatchExhaustivity (show(uncovered.take(6 )), hasMore), sel.srcPos)
847
+ val deduped = dedup(uncovered.take(6 ))
848
+ report.warning(PatternMatchExhaustivity (show(deduped), hasMore), sel.srcPos)
853
849
}
854
850
855
851
private def redundancyCheckable (sel : Tree ): Boolean =
@@ -908,10 +904,11 @@ class SpaceEngine(using Context) extends SpaceLogic {
908
904
// If explicit nulls are enabled, this check isn't needed because most of the cases
909
905
// that would trigger it would also trigger unreachability warnings.
910
906
if (! ctx.explicitNulls && i == cases.length - 1 && ! isNullLit(pat) ) {
911
- simplify(minus(covered, prevs)) match {
912
- case Typ (`constantNullType`, _) =>
907
+ dedup(flatten( simplify(minus(covered, prevs)))).toList match {
908
+ case Typ (`constantNullType`, _) :: Nil =>
913
909
report.warning(MatchCaseOnlyNullWarning (), pat.srcPos)
914
- case _ =>
910
+ case s =>
911
+ debug.println(" `_` matches = " + s)
915
912
}
916
913
}
917
914
}
0 commit comments