@@ -69,7 +69,7 @@ case object Empty extends Space
69
69
case class Typ (tp : Type , decomposed : Boolean = true ) extends Space
70
70
71
71
/** Space representing an extractor pattern */
72
- case class Prod (tp : Type , unappTp : Type , unappSym : Symbol , params : List [Space ], full : Boolean ) extends Space
72
+ case class Prod (tp : Type , unappTp : TermRef , params : List [Space ], full : Boolean ) extends Space
73
73
74
74
/** Union of spaces */
75
75
case class Or (spaces : List [Space ]) extends Space
@@ -97,7 +97,7 @@ trait SpaceLogic {
97
97
def canDecompose (tp : Type ): Boolean
98
98
99
99
/** Return term parameter types of the extractor `unapp` */
100
- def signature (unapp : Type , unappSym : Symbol , argLen : Int ): List [Type ]
100
+ def signature (unapp : TermRef , scrutineeTp : Type , argLen : Int ): List [Type ]
101
101
102
102
/** Get components of decomposable types */
103
103
def decompose (tp : Type ): List [Space ]
@@ -113,8 +113,8 @@ trait SpaceLogic {
113
113
* This reduces noise in counterexamples.
114
114
*/
115
115
def simplify (space : Space , aggressive : Boolean = false )(implicit ctx : Context ): Space = trace(s " simplify ${show(space)}, aggressive = $aggressive --> " , debug, x => show(x.asInstanceOf [Space ]))(space match {
116
- case Prod (tp, fun, sym, spaces, full) =>
117
- val sp = Prod (tp, fun, sym, spaces.map(simplify(_)), full)
116
+ case Prod (tp, fun, spaces, full) =>
117
+ val sp = Prod (tp, fun, spaces.map(simplify(_)), full)
118
118
if (sp.params.contains(Empty )) Empty
119
119
else if (canDecompose(tp) && decompose(tp).isEmpty) Empty
120
120
else sp
@@ -143,13 +143,13 @@ trait SpaceLogic {
143
143
144
144
/** Flatten space to get rid of `Or` for pretty print */
145
145
def flatten (space : Space )(implicit ctx : Context ): List [Space ] = space match {
146
- case Prod (tp, fun, sym, spaces, full) =>
146
+ case Prod (tp, fun, spaces, full) =>
147
147
spaces.map(flatten) match {
148
- case Nil => Prod (tp, fun, sym, Nil , full) :: Nil
148
+ case Nil => Prod (tp, fun, Nil , full) :: Nil
149
149
case ss =>
150
150
ss.foldLeft(List [Prod ]()) { (acc, flat) =>
151
- if (acc.isEmpty) flat.map(s => Prod (tp, fun, sym, s :: Nil , full))
152
- else for (Prod (tp, fun, sym, ss, full) <- acc; s <- flat) yield Prod (tp, fun, sym , ss :+ s, full)
151
+ if (acc.isEmpty) flat.map(s => Prod (tp, fun, s :: Nil , full))
152
+ else for (Prod (tp, fun, ss, full) <- acc; s <- flat) yield Prod (tp, fun, ss :+ s, full)
153
153
}
154
154
}
155
155
case Or (spaces) =>
@@ -173,13 +173,13 @@ trait SpaceLogic {
173
173
ss.exists(isSubspace(a, _)) || tryDecompose1(tp1)
174
174
case (_, Or (_)) =>
175
175
simplify(minus(a, b)) == Empty
176
- case (Prod (tp1, _, _, _, _ ), Typ (tp2, _)) =>
176
+ case (Prod (tp1, _, _, _), Typ (tp2, _)) =>
177
177
isSubType(tp1, tp2)
178
- case (Typ (tp1, _), Prod (tp2, fun, sym, ss, full)) =>
178
+ case (Typ (tp1, _), Prod (tp2, fun, ss, full)) =>
179
179
// approximation: a type can never be fully matched by a partial extractor
180
- full && isSubType(tp1, tp2) && isSubspace(Prod (tp2, fun, sym, signature(fun, sym , ss.length).map(Typ (_, false )), full), b)
181
- case (Prod (_, fun1, sym1, ss1, _), Prod (_, fun2, sym2 , ss2, _)) =>
182
- sym1 == sym2 && isEqualType(fun1, fun2) && ss1.zip(ss2).forall((isSubspace _).tupled)
180
+ full && isSubType(tp1, tp2) && isSubspace(Prod (tp2, fun, signature(fun, tp2 , ss.length).map(Typ (_, false )), full), b)
181
+ case (Prod (_, fun1, ss1, _), Prod (_, fun2, ss2, _)) =>
182
+ isEqualType(fun1, fun2) && ss1.zip(ss2).forall((isSubspace _).tupled)
183
183
}
184
184
}
185
185
@@ -198,28 +198,28 @@ trait SpaceLogic {
198
198
else if (canDecompose(tp1)) tryDecompose1(tp1)
199
199
else if (canDecompose(tp2)) tryDecompose2(tp2)
200
200
else intersectUnrelatedAtomicTypes(tp1, tp2)
201
- case (Typ (tp1, _), Prod (tp2, fun, _, ss, true )) =>
201
+ case (Typ (tp1, _), Prod (tp2, fun, ss, true )) =>
202
202
if (isSubType(tp2, tp1)) b
203
203
else if (isSubType(tp1, tp2)) a // problematic corner case: inheriting a case class
204
204
else if (canDecompose(tp1)) tryDecompose1(tp1)
205
205
else Empty
206
- case (Typ (tp1, _), Prod (tp2, _, _, _, false )) =>
206
+ case (Typ (tp1, _), Prod (tp2, _, _, false )) =>
207
207
if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) b // prefer extractor space for better approximation
208
208
else if (canDecompose(tp1)) tryDecompose1(tp1)
209
209
else Empty
210
- case (Prod (tp1, fun, _, ss, true ), Typ (tp2, _)) =>
210
+ case (Prod (tp1, fun, ss, true ), Typ (tp2, _)) =>
211
211
if (isSubType(tp1, tp2)) a
212
212
else if (isSubType(tp2, tp1)) a // problematic corner case: inheriting a case class
213
213
else if (canDecompose(tp2)) tryDecompose2(tp2)
214
214
else Empty
215
- case (Prod (tp1, _, _, _, false ), Typ (tp2, _)) =>
215
+ case (Prod (tp1, _, _, false ), Typ (tp2, _)) =>
216
216
if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) a
217
217
else if (canDecompose(tp2)) tryDecompose2(tp2)
218
218
else Empty
219
- case (Prod (tp1, fun1, sym1, ss1, full), Prod (tp2, fun2, sym2 , ss2, _)) =>
220
- if (sym1 != sym2 || ! isEqualType(fun1, fun2)) Empty
219
+ case (Prod (tp1, fun1, ss1, full), Prod (tp2, fun2, ss2, _)) =>
220
+ if (! isEqualType(fun1, fun2)) Empty
221
221
else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty )) Empty
222
- else Prod (tp1, fun1, sym1, ss1.zip(ss2).map((intersect _).tupled), full)
222
+ else Prod (tp1, fun1, ss1.zip(ss2).map((intersect _).tupled), full)
223
223
}
224
224
}
225
225
@@ -236,34 +236,34 @@ trait SpaceLogic {
236
236
else if (canDecompose(tp1)) tryDecompose1(tp1)
237
237
else if (canDecompose(tp2)) tryDecompose2(tp2)
238
238
else a
239
- case (Typ (tp1, _), Prod (tp2, fun, sym, ss, true )) =>
239
+ case (Typ (tp1, _), Prod (tp2, fun, ss, true )) =>
240
240
// rationale: every instance of `tp1` is covered by `tp2(_)`
241
- if (isSubType(tp1, tp2)) minus(Prod (tp1, fun, sym, signature(fun, sym , ss.length).map(Typ (_, false )), true ), b)
241
+ if (isSubType(tp1, tp2)) minus(Prod (tp1, fun, signature(fun, tp1 , ss.length).map(Typ (_, false )), true ), b)
242
242
else if (canDecompose(tp1)) tryDecompose1(tp1)
243
243
else a
244
244
case (_, Or (ss)) =>
245
245
ss.foldLeft(a)(minus)
246
246
case (Or (ss), _) =>
247
247
Or (ss.map(minus(_, b)))
248
- case (Prod (tp1, fun, _, ss, true ), Typ (tp2, _)) =>
248
+ case (Prod (tp1, fun, ss, true ), Typ (tp2, _)) =>
249
249
// uncovered corner case: tp2 :< tp1
250
250
if (isSubType(tp1, tp2)) Empty
251
251
else if (simplify(a) == Empty ) Empty
252
252
else if (canDecompose(tp2)) tryDecompose2(tp2)
253
253
else a
254
- case (Prod (tp1, _, _, _, false ), Typ (tp2, _)) =>
254
+ case (Prod (tp1, _, _, false ), Typ (tp2, _)) =>
255
255
if (isSubType(tp1, tp2)) Empty
256
256
else a
257
- case (Typ (tp1, _), Prod (tp2, _, _, _, false )) =>
257
+ case (Typ (tp1, _), Prod (tp2, _, _, false )) =>
258
258
a // approximation
259
- case (Prod (tp1, fun1, sym1, ss1, full), Prod (tp2, fun2, sym2 , ss2, _)) =>
260
- if (sym1 != sym2 || ! isEqualType(fun1, fun2)) a
259
+ case (Prod (tp1, fun1, ss1, full), Prod (tp2, fun2, ss2, _)) =>
260
+ if (! isEqualType(fun1, fun2)) a
261
261
else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty )) a
262
262
else if (ss1.zip(ss2).forall((isSubspace _).tupled)) Empty
263
263
else
264
264
// `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
265
265
Or (ss1.zip(ss2).map((minus _).tupled).zip(0 to ss2.length - 1 ).map {
266
- case (ri, i) => Prod (tp1, fun1, sym1, ss1.updated(i, ri), full)
266
+ case (ri, i) => Prod (tp1, fun1, ss1.updated(i, ri), full)
267
267
})
268
268
269
269
}
@@ -360,18 +360,20 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
360
360
case Bind (_, pat) => project(pat)
361
361
case SeqLiteral (pats, _) => projectSeq(pats)
362
362
case UnApply (fun, _, pats) =>
363
+ val (fun1, _, _) = decomposeCall(fun)
364
+ val funRef = fun1.tpe.asInstanceOf [TermRef ]
363
365
if (fun.symbol.name == nme.unapplySeq)
364
366
if (fun.symbol.owner == scalaSeqFactoryClass)
365
367
projectSeq(pats)
366
368
else {
367
369
val (arity, elemTp, resultTp) = unapplySeqInfo(fun.tpe.widen.finalResultType, fun.sourcePos)
368
370
if (elemTp.exists)
369
- Prod (erase(pat.tpe.stripAnnots), fun.tpe, fun.symbol , projectSeq(pats) :: Nil , isIrrefutableUnapplySeq(fun, pats.size))
371
+ Prod (erase(pat.tpe.stripAnnots), funRef , projectSeq(pats) :: Nil , isIrrefutableUnapplySeq(fun, pats.size))
370
372
else
371
- Prod (erase(pat.tpe.stripAnnots), fun.tpe, fun.symbol , pats.take(arity - 1 ).map(project) :+ projectSeq(pats.drop(arity - 1 )), isIrrefutableUnapplySeq(fun, pats.size))
373
+ Prod (erase(pat.tpe.stripAnnots), funRef , pats.take(arity - 1 ).map(project) :+ projectSeq(pats.drop(arity - 1 )), isIrrefutableUnapplySeq(fun, pats.size))
372
374
}
373
375
else
374
- Prod (erase(pat.tpe.stripAnnots), erase(fun.tpe), fun.symbol , pats.map(project), isIrrefutableUnapply(fun, pats.length))
376
+ Prod (erase(pat.tpe.stripAnnots), funRef , pats.map(project), isIrrefutableUnapply(fun, pats.length))
375
377
case Typed (pat @ UnApply (_, _, _), _) => project(pat)
376
378
case Typed (expr, _) =>
377
379
Typ (erase(expr.tpe.stripAnnots), true )
@@ -386,6 +388,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
386
388
Typ (pat.tpe.narrow, false )
387
389
}
388
390
391
+ private def project (tp : Type ): Space = tp match {
392
+ case OrType (tp1, tp2) => Or (project(tp1) :: project(tp2) :: Nil )
393
+ case tp => Typ (tp, decomposed = true )
394
+ }
395
+
389
396
private def unapplySeqInfo (resTp : Type , pos : SourcePosition )(implicit ctx : Context ): (Int , Type , Type ) = {
390
397
var resultTp = resTp
391
398
var elemTp = unapplySeqTypeElemTp(resultTp)
@@ -458,11 +465,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
458
465
else
459
466
(pats, Typ (scalaNilType, false ))
460
467
468
+ val unapplyTp = scalaConsType.classSymbol.companionModule.termRef.select(nme.unapply)
461
469
items.foldRight[Space ](zero) { (pat, acc) =>
462
470
val consTp = scalaConsType.appliedTo(pats.head.tpe.widen)
463
- val unapplySym = consTp.classSymbol.linkedClass.info.member(nme.unapply).symbol
464
- val unapplyTp = unapplySym.info.appliedTo(pats.head.tpe.widen)
465
- Prod (consTp, unapplyTp, unapplySym, project(pat) :: acc :: Nil , true )
471
+ Prod (consTp, unapplyTp, project(pat) :: acc :: Nil , true )
466
472
}
467
473
}
468
474
@@ -480,15 +486,26 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
480
486
def isEqualType (tp1 : Type , tp2 : Type ): Boolean = tp1 =:= tp2
481
487
482
488
/** Parameter types of the case class type `tp`. Adapted from `unapplyPlan` in patternMatcher */
483
- def signature (unapp : Type , unappSym : Symbol , argLen : Int ): List [Type ] = {
489
+ def signature (unapp : TermRef , scrutineeTp : Type , argLen : Int ): List [Type ] = {
490
+ val unappSym = unapp.symbol
484
491
def caseClass = unappSym.owner.linkedClass
485
492
486
493
lazy val caseAccessors = caseClass.caseAccessors.filter(_.is(Method ))
487
494
488
495
def isSyntheticScala2Unapply (sym : Symbol ) =
489
496
sym.isAllOf(SyntheticCase ) && sym.owner.is(Scala2x )
490
497
491
- val mt @ MethodType (_) = unapp.widen
498
+ val mt : MethodType = unapp.widen match {
499
+ case mt : MethodType => mt
500
+ case pt : PolyType =>
501
+ inContext(ctx.fresh.setNewTyperState()) {
502
+ val tvars = pt.paramInfos.map(newTypeVar)
503
+ val mt = pt.instantiate(tvars).asInstanceOf [MethodType ]
504
+ scrutineeTp <:< mt.paramInfos(0 )
505
+ instantiateSelected(mt, tvars)
506
+ mt
507
+ }
508
+ }
492
509
493
510
// Case unapply:
494
511
// 1. return types of constructor fields if the extractor is synthesized for Scala2 case classes & length match
@@ -657,8 +674,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
657
674
def impossible : Nothing = throw new AssertionError (" `satisfiable` only accepts flattened space." )
658
675
659
676
def genConstraint (space : Space ): List [(Type , Type )] = space match {
660
- case Prod (tp, unappTp, unappSym, ss, _) =>
661
- val tps = signature(unappTp, unappSym , ss.length)
677
+ case Prod (tp, unappTp, ss, _) =>
678
+ val tps = signature(unappTp, tp , ss.length)
662
679
ss.zip(tps).flatMap {
663
680
case (sp : Prod , tp) => sp.tp -> tp :: genConstraint(sp)
664
681
case (Typ (tp1, _), tp2) => tp1 -> tp2 :: Nil
@@ -717,13 +734,14 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
717
734
showType(tp) + params(tp).map(_ => " _" ).mkString(" (" , " , " , " )" )
718
735
else if (decomposed) " _: " + showType(tp, showTypeArgs = true )
719
736
else " _"
720
- case Prod (tp, fun, sym, params, _) =>
737
+ case Prod (tp, fun, params, _) =>
721
738
if (ctx.definitions.isTupleType(tp))
722
739
" (" + params.map(doShow(_)).mkString(" , " ) + " )"
723
740
else if (tp.isRef(scalaConsType.symbol))
724
741
if (flattenList) params.map(doShow(_, flattenList)).mkString(" , " )
725
742
else params.map(doShow(_, flattenList = true )).filter(! _.isEmpty).mkString(" List(" , " , " , " )" )
726
743
else {
744
+ val sym = fun.symbol
727
745
val isUnapplySeq = sym.name.eq(nme.unapplySeq)
728
746
val paramsStr = params.map(doShow(_, flattenList = isUnapplySeq)).mkString(" (" , " , " , " )" )
729
747
showType(sym.owner.typeRef) + paramsStr
@@ -781,7 +799,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
781
799
val checkGADTSAT = shouldCheckExamples(selTyp)
782
800
783
801
val uncovered =
784
- flatten(simplify(minus(Typ (selTyp, true ), patternSpace), aggressive = true )).filter { s =>
802
+ flatten(simplify(minus(project (selTyp), patternSpace), aggressive = true )).filter { s =>
785
803
s != Empty && (! checkGADTSAT || satisfiable(s))
786
804
}
787
805
@@ -805,9 +823,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
805
823
806
824
val targetSpace =
807
825
if (ctx.explicitNulls || selTyp.classSymbol.isPrimitiveValueClass)
808
- Typ (selTyp, true )
826
+ project (selTyp)
809
827
else
810
- Or ( Typ (selTyp, true ) :: constantNullSpace :: Nil )
828
+ project( OrType (selTyp, constantNullType) )
811
829
812
830
// in redundancy check, take guard as false in order to soundly approximate
813
831
def projectPrevCases (cases : List [CaseDef ]): Space =
0 commit comments