@@ -13,6 +13,7 @@ import core.StdNames._
13
13
import core .NameOps ._
14
14
import core .Constants ._
15
15
import reporting .diagnostic .messages ._
16
+ import config .Printers .{ exhaustivity => debug }
16
17
17
18
/** Space logic for checking exhaustivity and unreachability of pattern matching
18
19
*
@@ -29,7 +30,6 @@ import reporting.diagnostic.messages._
29
30
* 4. For a case class Kon(x1: T1, x2: T2, .., xn: Tn), if S1, S2, ..., Sn
30
31
* are spaces, then `Kon(S1, S2, ..., Sn)` is a space.
31
32
* 5. A constant `Const(value, T)` is a point in space
32
- * 6. A stable identifier `Var(sym, T)` is a space
33
33
*
34
34
* For the problem of exhaustivity check, its formulation in terms of space is as follows:
35
35
*
@@ -70,9 +70,6 @@ case class Or(spaces: List[Space]) extends Space
70
70
/** Point in space */
71
71
sealed trait Point extends Space
72
72
73
- /** Point representing variables(stable identifier) in patterns */
74
- case class Var (sym : Symbol , tp : Type ) extends Point
75
-
76
73
/** Point representing literal constants in patterns */
77
74
case class Const (value : Constant , tp : Type ) extends Point
78
75
@@ -97,6 +94,9 @@ trait SpaceLogic {
97
94
/** Get components of decomposable types */
98
95
def decompose (tp : Type ): List [Space ]
99
96
97
+ /** Display space in string format */
98
+ def show (sp : Space ): String
99
+
100
100
/** Simplify space using the laws, there's no nested union after simplify */
101
101
def simplify (space : Space ): Space = space match {
102
102
case Kon (tp, spaces) =>
@@ -137,7 +137,7 @@ trait SpaceLogic {
137
137
def tryDecompose1 (tp : Type ) = canDecompose(tp) && isSubspace(Or (decompose(tp)), b)
138
138
def tryDecompose2 (tp : Type ) = canDecompose(tp) && isSubspace(a, Or (decompose(tp)))
139
139
140
- (a, b) match {
140
+ val res = (a, b) match {
141
141
case (Empty , _) => true
142
142
case (_, Empty ) => false
143
143
case (Or (ss), _) => ss.forall(isSubspace(_, b))
@@ -162,20 +162,19 @@ trait SpaceLogic {
162
162
case (Const (_, _), Or (ss)) => ss.exists(isSubspace(a, _))
163
163
case (Const (_, _), _) => false
164
164
case (_, Const (_, _)) => false
165
- case (Var (x, _), Var (y, _)) => x == y
166
- case (Var (_, tp1), Typ (tp2, _)) => isSubType(tp1, tp2) || tryDecompose2(tp2)
167
- case (Var (_, _), Or (ss)) => ss.exists(isSubspace(a, _))
168
- case (Var (_, _), _) => false
169
- case (_, Var (_, _)) => false
170
165
}
166
+
167
+ debug.println(s " ${show(a)} < ${show(b)} = $res" )
168
+
169
+ res
171
170
}
172
171
173
172
/** Intersection of two spaces */
174
173
def intersect (a : Space , b : Space ): Space = {
175
174
def tryDecompose1 (tp : Type ) = intersect(Or (decompose(tp)), b)
176
175
def tryDecompose2 (tp : Type ) = intersect(a, Or (decompose(tp)))
177
176
178
- (a, b) match {
177
+ val res = (a, b) match {
179
178
case (Empty , _) | (_, Empty ) => Empty
180
179
case (_, Or (ss)) => Or (ss.map(intersect(a, _)).filterConserve(_ ne Empty ))
181
180
case (Or (ss), _) => Or (ss.map(intersect(_, b)).filterConserve(_ ne Empty ))
@@ -211,27 +210,19 @@ trait SpaceLogic {
211
210
else if (canDecompose(tp1)) tryDecompose1(tp1)
212
211
else Empty
213
212
case (_, Const (_, _)) => Empty
214
- case (Var (x, _), Var (y, _)) =>
215
- if (x == y) a else Empty
216
- case (Var (_, tp1), Typ (tp2, _)) =>
217
- if (isSubType(tp1, tp2)) a
218
- else if (canDecompose(tp2)) tryDecompose2(tp2)
219
- else Empty
220
- case (Var (_, _), _) => Empty
221
- case (Typ (tp1, _), Var (_, tp2)) =>
222
- if (isSubType(tp2, tp1)) b
223
- else if (canDecompose(tp1)) tryDecompose1(tp1)
224
- else Empty
225
- case (_, Var (_, _)) => Empty
226
213
}
214
+
215
+ debug.println(s " ${show(a)} & ${show(b)} = ${show(res)}" )
216
+
217
+ res
227
218
}
228
219
229
220
/** The space of a not covered by b */
230
221
def minus (a : Space , b : Space ): Space = {
231
222
def tryDecompose1 (tp : Type ) = minus(Or (decompose(tp)), b)
232
223
def tryDecompose2 (tp : Type ) = minus(a, Or (decompose(tp)))
233
224
234
- (a, b) match {
225
+ val res = (a, b) match {
235
226
case (Empty , _) => Empty
236
227
case (_, Empty ) => a
237
228
case (Typ (tp1, _), Typ (tp2, _)) =>
@@ -275,15 +266,11 @@ trait SpaceLogic {
275
266
if (canDecompose(tp1)) tryDecompose1(tp1)
276
267
else a
277
268
case (_, Const (_, _)) => a
278
- case (Var (x, _), Var (y, _)) =>
279
- if (x == y) Empty else a
280
- case (Var (_, tp1), Typ (tp2, _)) =>
281
- if (isSubType(tp1, tp2)) Empty
282
- else if (canDecompose(tp2)) tryDecompose2(tp2)
283
- else a
284
- case (Var (_, _), _) => a
285
- case (_, Var (_, _)) => a
286
269
}
270
+
271
+ debug.println(s " ${show(a)} - ${show(b)} = ${show(res)}" )
272
+
273
+ res
287
274
}
288
275
}
289
276
@@ -298,16 +285,14 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
298
285
*/
299
286
def project (pat : Tree , roundUp : Boolean = true )(implicit ctx : Context ): Space = pat match {
300
287
case Literal (c) => Const (c, c.tpe)
301
- case _ : BackquotedIdent => Var (pat.symbol, pat.tpe )
288
+ case _ : BackquotedIdent => Typ (pat.tpe, false )
302
289
case Ident (_) | Select (_, _) =>
303
290
pat.tpe.stripAnnots match {
304
291
case tp : TermRef =>
305
292
if (pat.symbol.is(Enum ))
306
293
Const (Constant (pat.symbol), tp)
307
- else if (tp.underlyingIterator.exists(_.classSymbol.is(Module )))
308
- Typ (tp.widenTermRefExpr.stripAnnots, false )
309
294
else
310
- Var (pat.symbol, tp )
295
+ Typ (tp, false )
311
296
case tp => Typ (tp, false )
312
297
}
313
298
case Alternative (trees) => Or (trees.map(project(_, roundUp)))
@@ -345,7 +330,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
345
330
/** Is `tp1` a subtype of `tp2`? */
346
331
def isSubType (tp1 : Type , tp2 : Type ): Boolean = {
347
332
// check SI-9657 and tests/patmat/gadt.scala
348
- erase(tp1) <:< erase(tp2)
333
+ val res = erase(tp1) <:< erase(tp2)
334
+ debug.println(s " ${tp1.show} <:< ${tp2.show} = $res" )
335
+ res
349
336
}
350
337
351
338
def isEqualType (tp1 : Type , tp2 : Type ): Boolean = tp1 =:= tp2
@@ -373,6 +360,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
373
360
}
374
361
}
375
362
363
+ debug.println(s " candidates for ${tp.show} : [ ${children.map(_.show).mkString(" , " )}] " )
364
+
376
365
tp match {
377
366
case OrType (tp1, tp2) => List (Typ (tp1, true ), Typ (tp2, true ))
378
367
case _ if tp =:= ctx.definitions.BooleanType =>
@@ -385,21 +374,36 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
385
374
case _ =>
386
375
val parts = children.map { sym =>
387
376
if (sym.is(ModuleClass ))
388
- sym.asClass.classInfo.selfType
377
+ refine(tp, sym.sourceModule.termRef)
378
+ else if (sym.isTerm)
379
+ refine(tp, sym.termRef)
389
380
else if (sym.info.typeParams.length > 0 || tp.isInstanceOf [TypeRef ])
390
381
refine(tp, sym.typeRef)
391
382
else
392
383
sym.typeRef
393
384
} filter { tpe =>
394
385
// Child class may not always be subtype of parent:
395
386
// GADT & path-dependent types
396
- tpe <:< expose(tp)
387
+ val res = tpe <:< expose(tp)
388
+ if (! res) debug.println(s " unqualified child ousted: ${tpe.show} !< ${tp.show}" )
389
+ res
397
390
}
398
391
392
+ debug.println(s " ${tp.show} decomposes to [ ${parts.map(_.show).mkString(" , " )}] " )
393
+
399
394
parts.map(Typ (_, true ))
400
395
}
401
396
}
402
397
398
+ // simplify p.Case$.This.m => p.Case.m
399
+ def simplifyPrefix (tp : Type ): Type = tp match {
400
+ case tp @ ThisType (mcls : TypeRef ) if mcls.symbol.sourceModule.exists =>
401
+ TermRef (simplifyPrefix(mcls.prefix), mcls.symbol.sourceModule.asTerm)
402
+ case tp @ TypeRef (prefix, _) => tp.derivedSelect(simplifyPrefix(prefix))
403
+ case tp @ TermRef (prefix, _) => tp.derivedSelect(simplifyPrefix(prefix))
404
+ case _ => tp
405
+ }
406
+
403
407
/** Refine tp2 based on tp1
404
408
*
405
409
* E.g. if `tp1` is `Option[Int]`, `tp2` is `Some`, then return
@@ -409,20 +413,26 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
409
413
* `path2`, then return `path1.B`.
410
414
*/
411
415
def refine (tp1 : Type , tp2 : Type ): Type = (tp1, tp2) match {
412
- case (tp1 : RefinedType , _) => tp1.wrapIfMember(refine(tp1.parent, tp2))
416
+ case (tp1 : RefinedType , _ : TypeRef ) => tp1.wrapIfMember(refine(tp1.parent, tp2))
413
417
case (tp1 : HKApply , _) => refine(tp1.superType, tp2)
414
- case (TypeRef (ref1 : TypeProxy , _), tp2 @ TypeRef (ref2 : TypeProxy , name)) =>
415
- if (ref1.underlying <:< ref2.underlying) TypeRef (ref1, name) else tp2
418
+ case (TypeRef (ref1 : TypeProxy , _), tp2 @ TypeRef (ref2 : TypeProxy , _)) =>
419
+ if (ref1.underlying <:< ref2.underlying) tp2.derivedSelect(ref1) else tp2
420
+ case (TypeRef (ref1 : TypeProxy , _), tp2 @ TermRef (ref2 : TypeProxy , _)) =>
421
+ if (ref1.underlying <:< ref2.underlying) tp2.derivedSelect(ref1) else tp2
416
422
case _ => tp2
417
423
}
418
424
419
425
/** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
420
426
def canDecompose (tp : Type ): Boolean = {
421
- tp.classSymbol.is(allOf(Abstract , Sealed )) ||
427
+ val res = tp.classSymbol.is(allOf(Abstract , Sealed )) ||
422
428
tp.classSymbol.is(allOf(Trait , Sealed )) ||
423
429
tp.isInstanceOf [OrType ] ||
424
430
tp =:= ctx.definitions.BooleanType ||
425
431
tp.classSymbol.is(Enum )
432
+
433
+ debug.println(s " decomposable: ${tp.show} = $res" )
434
+
435
+ res
426
436
}
427
437
428
438
/** Show friendly type name with current scope in mind
@@ -475,13 +485,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
475
485
def doShow (s : Space , mergeList : Boolean = false ): String = s match {
476
486
case Empty => " "
477
487
case Const (v, _) => v.show
478
- case Var (x , _) => x.show
488
+ case Typ ( tp : TermRef , _) => tp.symbol.showName
479
489
case Typ (tp, decomposed) =>
480
490
val sym = tp.widen.classSymbol
481
491
482
- if (sym.is(ModuleClass ))
483
- showType(tp)
484
- else if (ctx.definitions.isTupleType(tp))
492
+ if (ctx.definitions.isTupleType(tp))
485
493
signature(tp).map(_ => " _" ).mkString(" (" , " , " , " )" )
486
494
else if (sym.showFullName == " scala.collection.immutable.::" )
487
495
if (mergeList) " _" else " List(_)"
@@ -523,7 +531,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
523
531
}
524
532
525
533
val Match (sel, cases) = tree
526
- isCheckable(sel.tpe.widen.deAnonymize.dealiasKeepAnnots)
534
+ val res = isCheckable(sel.tpe.widen.deAnonymize.dealiasKeepAnnots)
535
+ debug.println(s " checkable: ${sel.show} = $res" )
536
+ res
527
537
}
528
538
529
539
@@ -584,7 +594,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
584
594
val selTyp = sel.tpe.widen.deAnonymize.dealias
585
595
586
596
587
- val patternSpace = cases.map(x => project(x.pat)).reduce((a, b) => Or (List (a, b)))
597
+ val patternSpace = cases.map({ x =>
598
+ val space = project(x.pat)
599
+ debug.println(s " ${x.pat.show} projects to ${show(space)}" )
600
+ space
601
+ }).reduce((a, b) => Or (List (a, b)))
588
602
val uncovered = simplify(minus(Typ (selTyp, true ), patternSpace))
589
603
590
604
if (uncovered != Empty )
0 commit comments