@@ -13,6 +13,7 @@ import core.StdNames._
1313import core .NameOps ._
1414import core .Constants ._
1515import reporting .diagnostic .messages ._
16+ import config .Printers .{ exhaustivity => debug }
1617
1718/** Space logic for checking exhaustivity and unreachability of pattern matching
1819 *
@@ -29,7 +30,6 @@ import reporting.diagnostic.messages._
2930 * 4. For a case class Kon(x1: T1, x2: T2, .., xn: Tn), if S1, S2, ..., Sn
3031 * are spaces, then `Kon(S1, S2, ..., Sn)` is a space.
3132 * 5. A constant `Const(value, T)` is a point in space
32- * 6. A stable identifier `Var(sym, T)` is a space
3333 *
3434 * For the problem of exhaustivity check, its formulation in terms of space is as follows:
3535 *
@@ -70,9 +70,6 @@ case class Or(spaces: List[Space]) extends Space
7070/** Point in space */
7171sealed trait Point extends Space
7272
73- /** Point representing variables(stable identifier) in patterns */
74- case class Var (sym : Symbol , tp : Type ) extends Point
75-
7673/** Point representing literal constants in patterns */
7774case class Const (value : Constant , tp : Type ) extends Point
7875
@@ -97,6 +94,9 @@ trait SpaceLogic {
9794 /** Get components of decomposable types */
9895 def decompose (tp : Type ): List [Space ]
9996
97+ /** Display space in string format */
98+ def show (sp : Space ): String
99+
100100 /** Simplify space using the laws, there's no nested union after simplify */
101101 def simplify (space : Space ): Space = space match {
102102 case Kon (tp, spaces) =>
@@ -137,7 +137,7 @@ trait SpaceLogic {
137137 def tryDecompose1 (tp : Type ) = canDecompose(tp) && isSubspace(Or (decompose(tp)), b)
138138 def tryDecompose2 (tp : Type ) = canDecompose(tp) && isSubspace(a, Or (decompose(tp)))
139139
140- (a, b) match {
140+ val res = (a, b) match {
141141 case (Empty , _) => true
142142 case (_, Empty ) => false
143143 case (Or (ss), _) => ss.forall(isSubspace(_, b))
@@ -162,20 +162,19 @@ trait SpaceLogic {
162162 case (Const (_, _), Or (ss)) => ss.exists(isSubspace(a, _))
163163 case (Const (_, _), _) => false
164164 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
170165 }
166+
167+ debug.println(s " ${show(a)} < ${show(b)} = $res" )
168+
169+ res
171170 }
172171
173172 /** Intersection of two spaces */
174173 def intersect (a : Space , b : Space ): Space = {
175174 def tryDecompose1 (tp : Type ) = intersect(Or (decompose(tp)), b)
176175 def tryDecompose2 (tp : Type ) = intersect(a, Or (decompose(tp)))
177176
178- (a, b) match {
177+ val res = (a, b) match {
179178 case (Empty , _) | (_, Empty ) => Empty
180179 case (_, Or (ss)) => Or (ss.map(intersect(a, _)).filterConserve(_ ne Empty ))
181180 case (Or (ss), _) => Or (ss.map(intersect(_, b)).filterConserve(_ ne Empty ))
@@ -211,27 +210,19 @@ trait SpaceLogic {
211210 else if (canDecompose(tp1)) tryDecompose1(tp1)
212211 else Empty
213212 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
226213 }
214+
215+ debug.println(s " ${show(a)} & ${show(b)} = ${show(res)}" )
216+
217+ res
227218 }
228219
229220 /** The space of a not covered by b */
230221 def minus (a : Space , b : Space ): Space = {
231222 def tryDecompose1 (tp : Type ) = minus(Or (decompose(tp)), b)
232223 def tryDecompose2 (tp : Type ) = minus(a, Or (decompose(tp)))
233224
234- (a, b) match {
225+ val res = (a, b) match {
235226 case (Empty , _) => Empty
236227 case (_, Empty ) => a
237228 case (Typ (tp1, _), Typ (tp2, _)) =>
@@ -275,15 +266,11 @@ trait SpaceLogic {
275266 if (canDecompose(tp1)) tryDecompose1(tp1)
276267 else a
277268 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
286269 }
270+
271+ debug.println(s " ${show(a)} - ${show(b)} = ${show(res)}" )
272+
273+ res
287274 }
288275}
289276
@@ -298,16 +285,14 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
298285 */
299286 def project (pat : Tree , roundUp : Boolean = true )(implicit ctx : Context ): Space = pat match {
300287 case Literal (c) => Const (c, c.tpe)
301- case _ : BackquotedIdent => Var (pat.symbol, pat.tpe )
288+ case _ : BackquotedIdent => Typ (pat.tpe, false )
302289 case Ident (_) | Select (_, _) =>
303290 pat.tpe.stripAnnots match {
304291 case tp : TermRef =>
305292 if (pat.symbol.is(Enum ))
306293 Const (Constant (pat.symbol), tp)
307- else if (tp.underlyingIterator.exists(_.classSymbol.is(Module )))
308- Typ (tp.widenTermRefExpr.stripAnnots, false )
309294 else
310- Var (pat.symbol, tp )
295+ Typ (tp, false )
311296 case tp => Typ (tp, false )
312297 }
313298 case Alternative (trees) => Or (trees.map(project(_, roundUp)))
@@ -345,7 +330,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
345330 /** Is `tp1` a subtype of `tp2`? */
346331 def isSubType (tp1 : Type , tp2 : Type ): Boolean = {
347332 // 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
349336 }
350337
351338 def isEqualType (tp1 : Type , tp2 : Type ): Boolean = tp1 =:= tp2
@@ -373,6 +360,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
373360 }
374361 }
375362
363+ debug.println(s " candidates for ${tp.show} : [ ${children.map(_.show).mkString(" , " )}] " )
364+
376365 tp match {
377366 case OrType (tp1, tp2) => List (Typ (tp1, true ), Typ (tp2, true ))
378367 case _ if tp =:= ctx.definitions.BooleanType =>
@@ -385,21 +374,36 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
385374 case _ =>
386375 val parts = children.map { sym =>
387376 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)
389380 else if (sym.info.typeParams.length > 0 || tp.isInstanceOf [TypeRef ])
390381 refine(tp, sym.typeRef)
391382 else
392383 sym.typeRef
393384 } filter { tpe =>
394385 // Child class may not always be subtype of parent:
395386 // 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
397390 }
398391
392+ debug.println(s " ${tp.show} decomposes to [ ${parts.map(_.show).mkString(" , " )}] " )
393+
399394 parts.map(Typ (_, true ))
400395 }
401396 }
402397
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+
403407 /** Refine tp2 based on tp1
404408 *
405409 * E.g. if `tp1` is `Option[Int]`, `tp2` is `Some`, then return
@@ -409,20 +413,26 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
409413 * `path2`, then return `path1.B`.
410414 */
411415 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))
413417 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
416422 case _ => tp2
417423 }
418424
419425 /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
420426 def canDecompose (tp : Type ): Boolean = {
421- tp.classSymbol.is(allOf(Abstract , Sealed )) ||
427+ val res = tp.classSymbol.is(allOf(Abstract , Sealed )) ||
422428 tp.classSymbol.is(allOf(Trait , Sealed )) ||
423429 tp.isInstanceOf [OrType ] ||
424430 tp =:= ctx.definitions.BooleanType ||
425431 tp.classSymbol.is(Enum )
432+
433+ debug.println(s " decomposable: ${tp.show} = $res" )
434+
435+ res
426436 }
427437
428438 /** Show friendly type name with current scope in mind
@@ -475,13 +485,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
475485 def doShow (s : Space , mergeList : Boolean = false ): String = s match {
476486 case Empty => " "
477487 case Const (v, _) => v.show
478- case Var (x , _) => x.show
488+ case Typ ( tp : TermRef , _) => tp.symbol.showName
479489 case Typ (tp, decomposed) =>
480490 val sym = tp.widen.classSymbol
481491
482- if (sym.is(ModuleClass ))
483- showType(tp)
484- else if (ctx.definitions.isTupleType(tp))
492+ if (ctx.definitions.isTupleType(tp))
485493 signature(tp).map(_ => " _" ).mkString(" (" , " , " , " )" )
486494 else if (sym.showFullName == " scala.collection.immutable.::" )
487495 if (mergeList) " _" else " List(_)"
@@ -523,7 +531,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
523531 }
524532
525533 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
527537 }
528538
529539
@@ -584,7 +594,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
584594 val selTyp = sel.tpe.widen.deAnonymize.dealias
585595
586596
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)))
588602 val uncovered = simplify(minus(Typ (selTyp, true ), patternSpace))
589603
590604 if (uncovered != Empty )
0 commit comments