@@ -101,7 +101,13 @@ trait SpaceLogic {
101
101
/** Display space in string format */
102
102
def show (sp : Space ): String
103
103
104
- /** Simplify space using the laws, there's no nested union after simplify */
104
+ /** Simplify space using the laws, there's no nested union after simplify
105
+ *
106
+ * @param aggressive if true and OR space has less than 5 components, `simplify` will
107
+ * collapse `sp1 | sp2` to `sp1` if `sp2` is a subspace of `sp1`.
108
+ *
109
+ * This reduces noise in counterexamples.
110
+ */
105
111
def simplify (space : Space , aggressive : Boolean = false ): Space = space match {
106
112
case Kon (tp, spaces) =>
107
113
val sp = Kon (tp, spaces.map(simplify(_)))
@@ -160,7 +166,7 @@ trait SpaceLogic {
160
166
ss.forall(isSubspace(_, b))
161
167
case (Typ (tp1, _), Typ (tp2, _)) =>
162
168
isSubType(tp1, tp2)
163
- case (Typ (tp1, _), Or (ss)) => // optimization
169
+ case (Typ (tp1, _), Or (ss)) => // optimization: don't go to subtraction too early
164
170
ss.exists(isSubspace(a, _)) || tryDecompose1(tp1)
165
171
case (_, Or (_)) =>
166
172
simplify(minus(a, b)) == Empty
@@ -323,11 +329,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
323
329
import SpaceEngine ._
324
330
import tpd ._
325
331
326
- private val scalaSomeClass = ctx.requiredClassRef (" scala.Some" .toTypeName).symbol.asClass
332
+ private val scalaSomeClass = ctx.requiredClass (" scala.Some" .toTypeName)
327
333
private val scalaSeqFactoryClass = ctx.requiredClass(" scala.collection.generic.SeqFactory" .toTypeName)
328
334
private val scalaListType = ctx.requiredClassRef(" scala.collection.immutable.List" .toTypeName)
329
335
private val scalaNilType = ctx.requiredModuleRef(" scala.collection.immutable.Nil" .toTermName)
330
- private val scalaConType = ctx.requiredClassRef(" scala.collection.immutable.::" .toTypeName)
336
+ private val scalaConsType = ctx.requiredClassRef(" scala.collection.immutable.::" .toTypeName)
331
337
332
338
/** Checks if it's possible to create a trait/class which is a subtype of `tp`.
333
339
*
@@ -442,7 +448,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
442
448
(pats, Typ (scalaNilType, false ))
443
449
444
450
items.foldRight[Space ](zero) { (pat, acc) =>
445
- Kon (scalaConType .appliedTo(pats.head.tpe.widen), project(pat) :: acc :: Nil )
451
+ Kon (scalaConsType .appliedTo(pats.head.tpe.widen), project(pat) :: acc :: Nil )
446
452
}
447
453
}
448
454
@@ -469,6 +475,19 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
469
475
/** Is `tp1` a subtype of `tp2`? */
470
476
def isSubType (tp1 : Type , tp2 : Type ): Boolean = {
471
477
// check SI-9657 and tests/patmat/gadt.scala
478
+ //
479
+ // `erase` is a walkaround to make the following code pass the check:
480
+ //
481
+ // def f(e: Either[Int, String]) = e match {
482
+ // case Left(i) => i
483
+ // case Right(s) => 0
484
+ // }
485
+ //
486
+ // The problem is that when decompose `Either[Int, String]`, `Type.wrapIfMember`
487
+ // only refines the type member inherited from `Either` -- it's complex to refine
488
+ // the type members in `Left` and `Right`.
489
+ //
490
+ // FIXME: remove this hack
472
491
val res = tp1 <:< erase(tp2)
473
492
debug.println(s " ${tp1.show} <:< ${tp2.show} = $res" )
474
493
res
@@ -509,7 +528,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
509
528
case space => List (space)
510
529
}
511
530
case OrType (tp1, tp2) => List (Typ (tp1, true ), Typ (tp2, true ))
512
- case tp if tp =:= ctx.definitions. BooleanType =>
531
+ case tp if tp.isRef(defn. BooleanClass ) =>
513
532
List (
514
533
Typ (ConstantType (Constant (true )), true ),
515
534
Typ (ConstantType (Constant (false )), true )
@@ -568,7 +587,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
568
587
val and = dealiasedTp.asInstanceOf [AndType ]
569
588
canDecompose(and.tp1) || canDecompose(and.tp2)
570
589
}) ||
571
- tp =:= ctx.definitions. BooleanType ||
590
+ tp.isRef(defn. BooleanClass ) ||
572
591
tp.classSymbol.is(allOf(Enum , Sealed )) // Enum value doesn't have Sealed flag
573
592
574
593
debug.println(s " decomposable: ${tp.show} = $res" )
@@ -632,9 +651,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
632
651
633
652
if (ctx.definitions.isTupleType(tp))
634
653
signature(tp).map(_ => " _" ).mkString(" (" , " , " , " )" )
635
- else if (sym.showFullName == " scala.collection.immutable.List " )
654
+ else if (scalaListType.isRef(sym) )
636
655
if (mergeList) " _*" else " _: List"
637
- else if (sym.showFullName == " scala.collection.immutable.:: " )
656
+ else if (scalaConsType.isRef(sym) )
638
657
if (mergeList) " _" else " List(_)"
639
658
else if (tp.classSymbol.is(CaseClass ))
640
659
// use constructor syntax for case class
@@ -646,7 +665,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
646
665
case Kon (tp, params) =>
647
666
if (ctx.definitions.isTupleType(tp))
648
667
" (" + params.map(doShow(_)).mkString(" , " ) + " )"
649
- else if (tp.widen.classSymbol.showFullName == " scala.collection.immutable.:: " )
668
+ else if (tp.isRef(scalaConsType.symbol) )
650
669
if (mergeList) params.map(doShow(_, mergeList)).mkString(" , " )
651
670
else params.map(doShow(_, true )).filter(_ != " Nil" ).mkString(" List(" , " , " , " )" )
652
671
else
@@ -673,7 +692,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
673
692
val and = tp.asInstanceOf [AndType ]
674
693
isCheckable(and.tp1) || isCheckable(and.tp2)
675
694
}) ||
676
- tp.typeSymbol == ctx.definitions. BooleanType .typeSymbol ||
695
+ tp.isRef(defn. BooleanClass ) ||
677
696
tp.typeSymbol.is(Enum ) ||
678
697
canDecompose(tp) ||
679
698
(defn.isTupleType(tp) && tp.dealias.argInfos.exists(isCheckable(_)))
0 commit comments