Skip to content

Commit 850ceb4

Browse files
nicolasstuckinicolasstucki
committed
Implement RefinedScrutinee with def refinedScrutinee
1 parent 717a198 commit 850ceb4

13 files changed

+263
-24
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -689,7 +689,7 @@ 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")
692+
lazy val RefinedScrutineeType: TypeRef = ctx.requiredClassRef("scala.RefinedScrutinee")
693693
def RefinedScrutineeClass(implicit ctx: Context) = RefinedScrutineeType.symbol.asClass
694694

695695
lazy val EqType = ctx.requiredClassRef("scala.Eq")

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -491,6 +491,7 @@ object StdNames {
491491
val raw_ : N = "raw"
492492
val readResolve: N = "readResolve"
493493
val reflect : N = "reflect"
494+
val refinedScrutinee: N = "refinedScrutinee"
494495
val reflectiveSelectable: N = "reflectiveSelectable"
495496
val reify : N = "reify"
496497
val rootMirror : N = "rootMirror"

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,17 @@ class FirstTransform extends MiniPhase with InfoTransformer { thisPhase =>
127127
""".stripMargin, ddef.tpt.pos)
128128
}
129129
case _ =>
130+
val refinedType = resultType.select(nme.refinedScrutinee).widen.resultType
131+
if (refinedType.exists && !(refinedType <:< mt.paramRefs.head)) {
132+
val paramName = mt.paramNames.head
133+
val paramTpe = mt.paramRefs.head
134+
val paramInfo = mt.paramInfos.head
135+
ctx.error(
136+
i"""Extractor with ${nme.refinedScrutinee} should refine the result type of that member.
137+
|The result type of ${nme.refinedScrutinee} should be a subtype of $paramTpe:
138+
| def unapply($paramName: $paramInfo): ${resultType.widenDealias.classSymbol.name} { def ${nme.refinedScrutinee}: $refinedType & $paramTpe }
139+
""".stripMargin, ddef.tpt.pos)
140+
}
130141
}
131142
case _ =>
132143
}

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1352,11 +1352,9 @@ 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-
resultType match {
1356-
case resultType: AppliedType if resultType.derivesFrom(defn.RefinedScrutineeClass) =>
1357-
resultType.args.head
1358-
case _ => symTp0
1359-
}
1355+
val refinedType = resultType.select(nme.refinedScrutinee).widen.resultType
1356+
if (refinedType.exists) refinedType
1357+
else symTp0
13601358
case _ =>
13611359
symTp0
13621360
}

‎library/src/scala/RefinedScrutinee.scala

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,20 @@ final class RefinedScrutinee[+Scrutinee /*<: Singleton*/, +Result] private (val
66
/** There is no result */
77
def isEmpty: Boolean = result == RefinedScrutinee.NoResult
88

9-
/** Get the result */
9+
/** When non-empty, get the result */
1010
def get: Result = result.asInstanceOf[Result]
11+
12+
/** Scrutinee type on a successful match */
13+
/*erased*/ def refinedScrutinee: Scrutinee = null.asInstanceOf[Scrutinee] // evaluated in RefinedScrutinee.matchOf
14+
1115
}
1216

1317
object RefinedScrutinee {
18+
1419
private[RefinedScrutinee] object NoResult
1520

1621
def matchOf[Scrutinee <: Singleton, Result](scrutinee: Scrutinee)(result: Result): RefinedScrutinee[Scrutinee, Result] = new RefinedScrutinee(result)
22+
1723
def noMatch[Scrutinee <: Singleton, Result]: RefinedScrutinee[Scrutinee, Result] = new RefinedScrutinee(NoResult)
24+
1825
}

‎tests/neg/refined-binding-nat-2.scala

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
2+
trait Peano {
3+
type Nat
4+
type Zero <: Nat
5+
type Succ <: Nat
6+
7+
val Zero: Zero
8+
9+
val Succ: SuccExtractor
10+
trait SuccExtractor {
11+
def apply(nat: Nat): Succ
12+
def unapply(nat: Nat): RefinedScrutinee[Succ, Nat] // error: Extractor with RefinedScrutinee should refine the result type of that member ...
13+
}
14+
}
15+
16+
object IntNums extends Peano {
17+
type Nat = Int
18+
type Zero = Int
19+
type Succ = Int
20+
21+
val Zero: Zero = 0
22+
23+
object Succ extends SuccExtractor {
24+
def apply(nat: Nat): Succ = nat + 1
25+
def unapply(nat: Nat) = // error: Extractor with RefinedScrutinee should refine the result type of that member ...
26+
if (nat == 0) RefinedScrutinee.noMatch
27+
else RefinedScrutinee.matchOf(nat)(nat - 1)
28+
}
29+
30+
}
31+
32+
object IntNums2 extends Peano {
33+
type Nat = Int
34+
type Zero = Int
35+
type Succ = Int
36+
37+
val Zero: Zero = 0
38+
39+
object Succ extends SuccExtractor {
40+
def apply(nat: Nat): Succ = nat + 1
41+
def unapply(nat: Nat): RefinedScrutinee[nat.type & Succ, Nat] =
42+
if (nat == 0) RefinedScrutinee.noMatch
43+
else RefinedScrutinee.matchOf(nat)(nat - 1)
44+
}
45+
46+
}

‎tests/neg/refined-binding-nat.scala

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,12 @@ trait Peano {
99
val Succ: SuccExtractor
1010
trait SuccExtractor {
1111
def apply(nat: Nat): Succ
12-
def unapply(nat: Nat): RefinedScrutinee[Succ, Nat] // error
12+
def unapply(nat: Nat): SuccOpt // error: Extractor with refinedScrutinee should refine the result type of that member ...
13+
}
14+
trait SuccOpt {
15+
def isEmpty: Boolean
16+
def refinedScrutinee: Succ
17+
def get: Nat
1318
}
1419
}
1520

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

2328
object Succ extends SuccExtractor {
2429
def apply(nat: Nat): Succ = nat + 1
25-
def unapply(nat: Nat) = // error
26-
if (nat == 0) RefinedScrutinee.noMatch
27-
else RefinedScrutinee.matchOf(nat)(nat - 1)
30+
def unapply(nat: Nat) = new SuccOpt { // error: Extractor with refinedScrutinee should refine the result type of that member ...
31+
def isEmpty: Boolean = nat == 0
32+
def refinedScrutinee: Succ & nat.type = nat
33+
def get: Int = nat - 1
34+
}
2835
}
2936

3037
}
@@ -38,9 +45,11 @@ object IntNums2 extends Peano {
3845

3946
object Succ extends SuccExtractor {
4047
def apply(nat: Nat): Succ = nat + 1
41-
def unapply(nat: Nat): RefinedScrutinee[nat.type & Succ, Nat] =
42-
if (nat == 0) RefinedScrutinee.noMatch
43-
else RefinedScrutinee.matchOf(nat)(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+
}
4453
}
4554

46-
}
55+
}

‎tests/run/refined-binding-2.check

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
ok
2+
9

‎tests/run/refined-binding-2.scala

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
2+
sealed trait Foo {
3+
4+
type X
5+
type Y <: X
6+
7+
def x: X
8+
9+
def f(y: Y) = println("ok")
10+
11+
object Z {
12+
def unapply(arg: X): RefinedScrutinee[arg.type & Y, Int] =
13+
RefinedScrutinee.matchOf(arg.asInstanceOf[arg.type & Y])(9)
14+
}
15+
}
16+
17+
object Test {
18+
def main(args: Array[String]): Unit = {
19+
test(new Foo { type X = Int; type Y = Int; def x: X = 1 })
20+
}
21+
22+
def test(foo: Foo): Unit = {
23+
foo.x match {
24+
case x @ foo.Z(i) => // `x` is refined to type `Y`
25+
foo.f(x)
26+
println(i)
27+
}
28+
}
29+
}

‎tests/run/refined-binding-nat-2.check

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
Some((SuccClass(SuccClass(ZeroObject)),SuccClass(ZeroObject)))
2+
Some((ZeroObject,SuccClass(SuccClass(ZeroObject))))
3+
None
4+
Some((2,1))
5+
Some((0,2))
6+
None

‎tests/run/refined-binding-nat-2.scala

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
2+
object Test {
3+
def main(args: Array[String]): Unit = {
4+
app(ClassNums)
5+
app(IntNums)
6+
}
7+
8+
def app(peano: Peano): Unit = {
9+
import peano._
10+
def divOpt(m: Nat, n: Nat): Option[(Nat, Nat)] = {
11+
n match {
12+
case Zero => None
13+
case s @ Succ(_) => Some(safeDiv(m, s))
14+
}
15+
}
16+
val two = Succ(Succ(Zero))
17+
val five = Succ(Succ(Succ(two)))
18+
println(divOpt(five, two))
19+
println(divOpt(two, five))
20+
println(divOpt(two, Zero))
21+
}
22+
}
23+
24+
trait Peano {
25+
type Nat
26+
type Zero <: Nat
27+
type Succ <: Nat
28+
29+
def safeDiv(m: Nat, n: Succ): (Nat, Nat)
30+
31+
implicit def succDeco(succ: Succ): SuccAPI
32+
trait SuccAPI {
33+
def pred: Nat
34+
}
35+
36+
val Zero: Zero
37+
38+
val Succ: SuccExtractor
39+
trait SuccExtractor {
40+
def apply(nat: Nat): Succ
41+
def unapply(nat: Nat): RefinedScrutinee[nat.type & Succ, Nat]
42+
}
43+
}
44+
45+
object IntNums extends Peano {
46+
type Nat = Int
47+
type Zero = Int
48+
type Succ = Int
49+
50+
def safeDiv(m: Nat, n: Succ): (Nat, Nat) = (m / n, m % n)
51+
52+
val Zero: Zero = 0
53+
54+
object Succ extends SuccExtractor {
55+
def apply(nat: Nat): Succ = nat + 1
56+
def unapply(nat: Nat) =
57+
if (nat == 0) RefinedScrutinee.noMatch
58+
else RefinedScrutinee.matchOf(nat)(nat - 1)
59+
}
60+
def succDeco(succ: Succ): SuccAPI = new SuccAPI {
61+
def pred: Nat = succ - 1
62+
}
63+
}
64+
65+
object ClassNums extends Peano {
66+
trait NatTrait
67+
object ZeroObject extends NatTrait {
68+
override def toString: String = "ZeroObject"
69+
}
70+
case class SuccClass(predecessor: NatTrait) extends NatTrait
71+
72+
type Nat = NatTrait
73+
type Zero = ZeroObject.type
74+
type Succ = SuccClass
75+
76+
def safeDiv(m: Nat, n: Succ): (Nat, Nat) = {
77+
def intValue(x: Nat, acc: Int): Int = x match {
78+
case nat: SuccClass => intValue(nat.predecessor, acc + 1)
79+
case _ => acc
80+
}
81+
def natValue(x: Int): Nat =
82+
if (x == 0) ZeroObject
83+
else new SuccClass(natValue(x - 1))
84+
val i = intValue(m, 0)
85+
val j = intValue(n, 0)
86+
(natValue(i / j), natValue(i % j))
87+
}
88+
89+
val Zero: Zero = ZeroObject
90+
91+
object Succ extends SuccExtractor {
92+
def apply(nat: Nat): Succ = new SuccClass(nat)
93+
def unapply(nat: Nat) = nat match {
94+
case nat: (SuccClass & nat.type) => RefinedScrutinee.matchOf(nat)(nat.predecessor)
95+
case _ => RefinedScrutinee.noMatch
96+
}
97+
}
98+
99+
def succDeco(succ: Succ): SuccAPI = new SuccAPI {
100+
def pred: Nat = succ.predecessor
101+
}
102+
103+
}

‎tests/run/refined-binding-nat.scala

Lines changed: 25 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,12 @@ trait Peano {
3838
val Succ: SuccExtractor
3939
trait SuccExtractor {
4040
def apply(nat: Nat): Succ
41-
def unapply(nat: Nat): RefinedScrutinee[nat.type & Succ, Nat]
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
4247
}
4348
}
4449

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

5459
object Succ extends SuccExtractor {
5560
def apply(nat: Nat): Succ = nat + 1
56-
def unapply(nat: Nat) =
57-
if (nat == 0) RefinedScrutinee.noMatch
58-
else RefinedScrutinee.matchOf(nat)(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+
}
5966
}
67+
6068
def succDeco(succ: Succ): SuccAPI = new SuccAPI {
6169
def pred: Nat = succ - 1
6270
}
@@ -67,7 +75,17 @@ object ClassNums extends Peano {
6775
object ZeroObject extends NatTrait {
6876
override def toString: String = "ZeroObject"
6977
}
70-
case class SuccClass(predecessor: NatTrait) extends NatTrait
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+
}
7189

7290
type Nat = NatTrait
7391
type Zero = ZeroObject.type
@@ -91,8 +109,8 @@ object ClassNums extends Peano {
91109
object Succ extends SuccExtractor {
92110
def apply(nat: Nat): Succ = new SuccClass(nat)
93111
def unapply(nat: Nat) = nat match {
94-
case nat: (SuccClass & nat.type) => RefinedScrutinee.matchOf(nat)(nat.predecessor)
95-
case _ => RefinedScrutinee.noMatch
112+
case nat: (SuccClass & nat.type) => nat
113+
case _ => SuccNoMatch
96114
}
97115
}
98116

‎tests/run/refined-binding.scala

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

1111
object Z {
12-
def unapply(arg: X): RefinedScrutinee[arg.type & Y, Int] =
13-
RefinedScrutinee.matchOf(arg.asInstanceOf[arg.type & Y])(9)
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
1423
}
1524
}
1625

0 commit comments

Comments
 (0)