@@ -105,7 +105,7 @@ trait SpaceLogic {
105
105
def signature (unapp : TermRef , scrutineeTp : Type , argLen : Int ): List [Type ]
106
106
107
107
/** Get components of decomposable types */
108
- def decompose (tp : Type ): List [Space ]
108
+ def decompose (tp : Type ): List [Typ ]
109
109
110
110
/** Whether the extractor covers the given type */
111
111
def covers (unapp : TermRef , scrutineeTp : Type ): Boolean
@@ -176,6 +176,8 @@ trait SpaceLogic {
176
176
ss.forall(isSubspace(_, b))
177
177
case (Typ (tp1, _), Typ (tp2, _)) =>
178
178
isSubType(tp1, tp2)
179
+ || canDecompose(tp1) && tryDecompose1(tp1)
180
+ || canDecompose(tp2) && tryDecompose2(tp2)
179
181
case (Typ (tp1, _), Or (ss)) => // optimization: don't go to subtraction too early
180
182
ss.exists(isSubspace(a, _)) || tryDecompose1(tp1)
181
183
case (_, Or (_)) =>
@@ -337,9 +339,7 @@ class SpaceEngine(using Context) extends SpaceLogic {
337
339
val res = TypeComparer .provablyDisjoint(tp1, tp2)
338
340
339
341
if (res) Empty
340
- else if (tp1.isSingleton) Typ (tp1, true )
341
- else if (tp2.isSingleton) Typ (tp2, true )
342
- else Typ (AndType (tp1, tp2), true )
342
+ else Typ (AndType (tp1, tp2), decomposed = true )
343
343
}
344
344
}
345
345
@@ -591,14 +591,27 @@ class SpaceEngine(using Context) extends SpaceLogic {
591
591
}
592
592
593
593
/** Decompose a type into subspaces -- assume the type can be decomposed */
594
- def decompose (tp : Type ): List [Space ] =
594
+ def decompose (tp : Type ): List [Typ ] =
595
595
tp.dealias match {
596
596
case AndType (tp1, tp2) =>
597
- intersect(Typ (tp1, false ), Typ (tp2, false )) match {
598
- case Or (spaces) => spaces.toList
599
- case Empty => Nil
600
- case space => List (space)
601
- }
597
+ def decomposeComponent (tpA : Type , tpB : Type ): List [Typ ] =
598
+ decompose(tpA).flatMap {
599
+ case Typ (tp, _) =>
600
+ if tp <:< tpB then
601
+ Typ (tp, decomposed = true ) :: Nil
602
+ else if tpB <:< tp then
603
+ Typ (tpB, decomposed = true ) :: Nil
604
+ else if TypeComparer .provablyDisjoint(tp, tpB) then
605
+ Nil
606
+ else
607
+ Typ (AndType (tp, tpB), decomposed = true ) :: Nil
608
+ }
609
+
610
+ if canDecompose(tp1) then
611
+ decomposeComponent(tp1, tp2)
612
+ else
613
+ decomposeComponent(tp2, tp1)
614
+
602
615
case OrType (tp1, tp2) => List (Typ (tp1, true ), Typ (tp2, true ))
603
616
case tp if tp.isRef(defn.BooleanClass ) =>
604
617
List (
@@ -833,6 +846,9 @@ class SpaceEngine(using Context) extends SpaceLogic {
833
846
834
847
if (! exhaustivityCheckable(sel)) return
835
848
849
+ debug.println(" checking " + _match.show)
850
+ debug.println(" selTyp = " + selTyp.show)
851
+
836
852
val patternSpace = Or (cases.foldLeft(List .empty[Space ]) { (acc, x) =>
837
853
val space = if (x.guard.isEmpty) project(x.pat) else Empty
838
854
debug.println(s " ${x.pat.show} ====> ${show(space)}" )
0 commit comments