Skip to content

Commit f909b8e

Browse files
committed
WIP add test for different refinement approach
1 parent a8a1ebf commit f909b8e

File tree

8 files changed

+56
-64
lines changed

8 files changed

+56
-64
lines changed

compiler/src/dotty/tools/dotc/core/Definitions.scala

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -689,6 +689,9 @@ class Definitions {
689689
lazy val TastyTopLevelSpliceModule = ctx.requiredModule("scala.tasty.TopLevelSplice")
690690
lazy val TastyTopLevelSplice_tastyContext = TastyTopLevelSpliceModule.requiredMethod("tastyContext")
691691

692+
lazy val RefinedScrutineeType: TypeRef = ctx.requiredClassRef("scala.RefinedScrutinee")
693+
def RefinedScrutineeClass(implicit ctx: Context) = RefinedScrutineeType.symbol.asClass
694+
692695
lazy val EqType = ctx.requiredClassRef("scala.Eq")
693696
def EqClass(implicit ctx: Context) = EqType.symbol.asClass
694697
def EqModule(implicit ctx: Context) = EqClass.companionModule

compiler/src/dotty/tools/dotc/core/StdNames.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,8 @@ object StdNames {
216216
final val Type : N = "Type"
217217
final val TypeTree: N = "TypeTree"
218218

219+
final val RefinedScrutinee: N = "RefinedScrutinee"
220+
219221
// Annotation simple names, used in Namer
220222
final val BeanPropertyAnnot: N = "BeanProperty"
221223
final val BooleanBeanPropertyAnnot: N = "BooleanBeanProperty"

compiler/src/dotty/tools/dotc/transform/FirstTransform.scala

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -113,16 +113,20 @@ class FirstTransform extends MiniPhase with InfoTransformer { thisPhase =>
113113
ddef.tpe.widen match {
114114
case mt: MethodType if !mt.resType.widen.isInstanceOf[MethodicType] =>
115115
val resultType = mt.resType.substParam(mt.paramRefs.head, mt.paramRefs.head)
116-
val refinedType = resultType.select(nme.refinedScrutinee).widen.resultType
117-
if (refinedType.exists && !(refinedType <:< mt.paramRefs.head)) {
118-
val paramName = mt.paramNames.head
119-
val paramTpe = mt.paramRefs.head
120-
val paramInfo = mt.paramInfos.head
121-
ctx.error(
122-
i"""Extractor with ${nme.refinedScrutinee} should refine the result type of that member.
123-
|The result type of ${nme.refinedScrutinee} should be a subtype of $paramTpe:
124-
| def unapply($paramName: $paramInfo): ${resultType.widenDealias.classSymbol.name} { def ${nme.refinedScrutinee}: $refinedType & $paramTpe }
116+
resultType match {
117+
case resultType: AppliedType if resultType.derivesFrom(defn.RefinedScrutineeClass) =>
118+
val refinedType :: resultType2 :: Nil = resultType.args
119+
if (refinedType.exists && !(refinedType <:< mt.paramRefs.head)) {
120+
val paramName = mt.paramNames.head
121+
val paramTpe = mt.paramRefs.head
122+
val paramInfo = mt.paramInfos.head
123+
ctx.error(
124+
i"""Extractor with ${tpnme.RefinedScrutinee} should refine the result type of that member.
125+
|The scrutinee type of ${tpnme.RefinedScrutinee} should be a subtype of $paramTpe:
126+
| def unapply($paramName: $paramInfo): ${tpnme.RefinedScrutinee}[$paramTpe & $refinedType, $resultType2]
125127
""".stripMargin, ddef.tpt.pos)
128+
}
129+
case _ =>
126130
}
127131
case _ =>
128132
}

compiler/src/dotty/tools/dotc/typer/Typer.scala

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1352,9 +1352,11 @@ class Typer extends Namer
13521352
fun.tpe.widen match {
13531353
case mt: MethodType if !mt.resType.isInstanceOf[MethodType] =>
13541354
val resultType = mt.resType.substParam(mt.paramRefs.head, symTp0)
1355-
val refinedType = resultType.select(nme.refinedScrutinee).widen.resultType
1356-
if (refinedType.exists) refinedType
1357-
else symTp0
1355+
resultType match {
1356+
case resultType: AppliedType if resultType.derivesFrom(defn.RefinedScrutineeClass) =>
1357+
resultType.args.head
1358+
case _ => symTp0
1359+
}
13581360
case _ =>
13591361
symTp0
13601362
}
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package scala
2+
3+
class RefinedScrutinee[+Scrutinee /*<: Singleton*/, +Result] private (val result: Option[Result]) extends AnyVal {
4+
// Scrutinee in not a singleton to provide a better error message
5+
6+
/** There is no result */
7+
def isEmpty: Boolean = result.isEmpty
8+
9+
/** Get the result */
10+
def get: Result = result.get
11+
}
12+
13+
object RefinedScrutinee {
14+
// TODO when bootstrapped: erase scrutinee as it is just an evidence for that existance of a term of type Scrutinee
15+
def matchOf[Scrutinee <: Singleton, Result](/*erased*/ scrutinee: Scrutinee)(result: Result): RefinedScrutinee[Scrutinee, Result] = new RefinedScrutinee(Some(result))
16+
def noMatch[Scrutinee <: Singleton, Result]: RefinedScrutinee[Scrutinee, Result] = new RefinedScrutinee(None)
17+
}

tests/neg/refined-binding-nat.scala

Lines changed: 7 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,7 @@ trait Peano {
99
val Succ: SuccExtractor
1010
trait SuccExtractor {
1111
def apply(nat: Nat): Succ
12-
def unapply(nat: Nat): SuccOpt // error: missing { def refinedScrutinee: Succ & nat.type }
13-
}
14-
trait SuccOpt {
15-
def isEmpty: Boolean
16-
def refinedScrutinee: Succ
17-
def get: Nat
12+
def unapply(nat: Nat): RefinedScrutinee[Succ, Nat] // error
1813
}
1914
}
2015

@@ -27,11 +22,9 @@ object IntNums extends Peano {
2722

2823
object Succ extends SuccExtractor {
2924
def apply(nat: Nat): Succ = nat + 1
30-
def unapply(nat: Nat) = new SuccOpt { // error: missing { def refinedScrutinee: Succ & nat.type }
31-
def isEmpty: Boolean = nat == 0
32-
def refinedScrutinee: Succ & nat.type = nat
33-
def get: Int = nat - 1
34-
}
25+
def unapply(nat: Nat) = // error
26+
if (nat == 0) RefinedScrutinee.noMatch
27+
else RefinedScrutinee.matchOf(nat)(nat - 1)
3528
}
3629

3730
}
@@ -45,11 +38,9 @@ object IntNums2 extends Peano {
4538

4639
object Succ extends SuccExtractor {
4740
def apply(nat: Nat): Succ = nat + 1
48-
def unapply(nat: Nat): SuccOpt { def refinedScrutinee: Succ & nat.type } = new SuccOpt {
49-
def isEmpty: Boolean = nat == 0
50-
def refinedScrutinee: Succ & nat.type = nat
51-
def get: Int = nat - 1
52-
}
41+
def unapply(nat: Nat): RefinedScrutinee[nat.type & Succ, Nat] =
42+
if (nat == 0) RefinedScrutinee.noMatch
43+
else RefinedScrutinee.matchOf(nat)(nat - 1)
5344
}
5445

5546
}

tests/run/refined-binding-nat.scala

Lines changed: 7 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -38,12 +38,7 @@ trait Peano {
3838
val Succ: SuccExtractor
3939
trait SuccExtractor {
4040
def apply(nat: Nat): Succ
41-
def unapply(nat: Nat): SuccOpt { def refinedScrutinee: Succ & nat.type }
42-
}
43-
trait SuccOpt {
44-
def isEmpty: Boolean
45-
def refinedScrutinee: Succ
46-
def get: Nat
41+
def unapply(nat: Nat): RefinedScrutinee[nat.type & Succ, Nat]
4742
}
4843
}
4944

@@ -58,13 +53,10 @@ object IntNums extends Peano {
5853

5954
object Succ extends SuccExtractor {
6055
def apply(nat: Nat): Succ = nat + 1
61-
def unapply(nat: Nat) = new SuccOpt {
62-
def isEmpty: Boolean = nat == 0
63-
def refinedScrutinee: Succ & nat.type = nat
64-
def get: Int = nat - 1
65-
}
56+
def unapply(nat: Nat) =
57+
if (nat == 0) RefinedScrutinee.noMatch
58+
else RefinedScrutinee.matchOf(nat)(nat - 1)
6659
}
67-
6860
def succDeco(succ: Succ): SuccAPI = new SuccAPI {
6961
def pred: Nat = succ - 1
7062
}
@@ -75,17 +67,7 @@ object ClassNums extends Peano {
7567
object ZeroObject extends NatTrait {
7668
override def toString: String = "ZeroObject"
7769
}
78-
case class SuccClass(predecessor: NatTrait) extends NatTrait with SuccOpt {
79-
def isEmpty: Boolean = false
80-
def refinedScrutinee: this.type = this
81-
def get: NatTrait = this
82-
}
83-
84-
object SuccNoMatch extends SuccOpt {
85-
def isEmpty: Boolean = true
86-
def refinedScrutinee: Nothing = throw new NoSuchElementException
87-
def get: NatTrait = throw new NoSuchElementException
88-
}
70+
case class SuccClass(predecessor: NatTrait) extends NatTrait
8971

9072
type Nat = NatTrait
9173
type Zero = ZeroObject.type
@@ -109,8 +91,8 @@ object ClassNums extends Peano {
10991
object Succ extends SuccExtractor {
11092
def apply(nat: Nat): Succ = new SuccClass(nat)
11193
def unapply(nat: Nat) = nat match {
112-
case nat: (SuccClass & nat.type) => nat
113-
case _ => SuccNoMatch
94+
case nat: (SuccClass & nat.type) => RefinedScrutinee.matchOf(nat)(nat.predecessor)
95+
case _ => RefinedScrutinee.noMatch
11496
}
11597
}
11698

tests/run/refined-binding.scala

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -9,17 +9,8 @@ sealed trait Foo {
99
def f(y: Y) = println("ok")
1010

1111
object Z {
12-
def unapply(arg: X) = new Opt {
13-
type Scrutinee = arg.type
14-
def refinedScrutinee: Y & Scrutinee = arg.asInstanceOf[Y & Scrutinee]
15-
}
16-
}
17-
18-
abstract class Opt {
19-
type Scrutinee <: Singleton
20-
def refinedScrutinee: Y & Scrutinee
21-
def get: Int = 9
22-
def isEmpty: Boolean = false
12+
def unapply(arg: X): RefinedScrutinee[arg.type & Y, Int] =
13+
RefinedScrutinee.matchOf(arg.asInstanceOf[arg.type & Y])(9)
2314
}
2415
}
2516

0 commit comments

Comments
 (0)