Skip to content

Commit bd650dc

Browse files
author
Aleksander Boruch-Gruszecki
committed
Add GADT compilation tests
1 parent cedef0d commit bd650dc

10 files changed

+206
-0
lines changed

‎compiler/test/dotty/tools/dotc/GadtTests.scala

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
package dotty
2+
package tools
3+
package dotc
4+
5+
import org.junit.{AfterClass, Test}
6+
import vulpix._
7+
8+
import scala.concurrent.duration._
9+
import java.io.{File => JFile}
10+
11+
class GadtTests extends ParallelTesting {
12+
import TestConfiguration._
13+
import GadtTests._
14+
15+
// Test suite configuration --------------------------------------------------
16+
17+
def maxDuration = 30.seconds
18+
def numberOfSlaves = 5
19+
def safeMode = Properties.testsSafeMode
20+
def isInteractive = SummaryReport.isInteractive
21+
def testFilter = Properties.testsFilter
22+
23+
24+
// @Test def posTestFromTasty: Unit = {
25+
// // Can be reproduced with
26+
// // > sbt
27+
// // > dotc -Ythrough-tasty -Ycheck:all <source>
28+
29+
// implicit val testGroup: TestGroup = TestGroup("posTestFromTasty")
30+
// compileTastyInDir("tests/pos", defaultOptions,
31+
// fromTastyFilter = FileFilter.exclude(TestSources.posFromTastyBlacklisted),
32+
// decompilationFilter = FileFilter.exclude(TestSources.posDecompilationBlacklisted),
33+
// recompilationFilter = FileFilter.include(TestSources.posRecompilationWhitelist)
34+
// ).checkCompile()
35+
// }
36+
37+
@Test def compileGadtTests: Unit = {
38+
implicit val testGroup: TestGroup = TestGroup("compileGadtTests")
39+
compileFilesInDir("tests/gadt+noCheckOptions", TestFlags(basicClasspath, noCheckOptions)).checkCompile()
40+
}
41+
42+
@Test def compileGadtCheckOptionsTests: Unit = {
43+
implicit val testGroup: TestGroup = TestGroup("compileGadtCheckOptionsTests")
44+
compileFilesInDir("tests/gadt+checkOptions", TestFlags(basicClasspath, noCheckOptions ++ checkOptions)).checkCompile()
45+
}
46+
47+
@Test def compileGadtDefaultOptionsTests: Unit = {
48+
implicit val testGroup: TestGroup = TestGroup("compileGadtDefaultOptionsTests")
49+
compileFilesInDir("tests/gadt+defaultOptions", defaultOptions).checkCompile()
50+
}
51+
}
52+
53+
object GadtTests {
54+
implicit val summaryReport: SummaryReporting = new SummaryReport
55+
@AfterClass def cleanup(): Unit = summaryReport.echoSummary()
56+
}

‎tests/gadt+checkOptions

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
gadt

‎tests/gadt+defaultOptions

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
gadt

‎tests/gadt+noCheckOptions

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
gadt

‎tests/gadt/NatsVects.ignore

+90
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
object NatsVects {
2+
sealed trait TNat
3+
case class TZero() extends TNat
4+
case class TSucc[N <: TNat] extends TNat
5+
6+
object TNatSum {
7+
sealed trait TSum[M, N, R]
8+
case class TSumZero[N]() extends TSum[TZero, N, N]
9+
case class TSumM[M <: TNat, N, R <: TNat](sum: TSum[M, N, R]) extends TSum[TSucc[M], N, TSucc[R]]
10+
}
11+
import TNatSum._
12+
13+
implicit def tSumZero[N]: TSum[TZero, N, N] =
14+
TSumZero()
15+
//new TSum[TZero, N, N]() {}
16+
implicit def tSumM[M <: TNat, N, R <: TNat](implicit sum: TSum[M, N, R]): TSum[TSucc[M], N, TSucc[R]] =
17+
TSumM(sum)
18+
//new TSum[TSucc[M], N, TSucc[R]] {}
19+
20+
sealed trait Vec[+T, N <: TNat]
21+
case object VNil extends Vec[Nothing, TZero] // fails but in refchecks
22+
case class VCons[T, N <: TNat](x: T, xs: Vec[T, N]) extends Vec[T, TSucc[N]]
23+
24+
implicit class vecOps[T, M <: TNat]($this: Vec[T, M]) extends AnyVal {
25+
def append[N <: TNat, R <: TNat](that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] = {
26+
// tsum match {
27+
// case _: TSumZero[N] => // Here N = R
28+
// $this match {
29+
// case VNil =>
30+
// //that
31+
// that.asInstanceOf[Vec[T, R]]
32+
// case VCons(x, xs) =>
33+
// ???
34+
// }
35+
// case TSumM(sum) =>
36+
// ???
37+
// }
38+
$this match {
39+
case VNil => // M = TZero
40+
tsum match {
41+
case TSumZero() => that
42+
//* case _: TSumZero[TZero] =>
43+
//* that
44+
//* // that.asInstanceOf[Vec[T, R]]
45+
case _: TSumM[_, _, _] => // Impossible, this forces M = TSucc[M1]
46+
???
47+
}
48+
//* case vxs: VCons[T, m1] => // M = TSucc[m1], xs: Vec[T, m1]
49+
//* val x = vxs.x
50+
//* val xs = vxs.xs
51+
//* //case VCons(x, xs) =>
52+
//* tsum match {
53+
//* case _: TSumZero[TZero] => // impossible, since this forces M = TZero.
54+
//* ???
55+
//* // fails
56+
//* // case tsum1: TSumM[`m1`, n, r] => // M = TSucc[m1], R = TSucc[r]
57+
//* // implicit val tsum2 = tsum1.sum
58+
//* // val appended = xs append that
59+
//* // VCons(x, appended) // Vec[T, TSucc[r]]
60+
//* //works
61+
//* case tsum1: TSumM[`m1`, N, r] => // M = TSucc[m1], R = TSucc[r]
62+
//* implicit val tsum2 = tsum1.sum
63+
//* // I should be able to return:
64+
//* VCons(x, xs append that) // Vec[T, TSucc[r]] = Vec[T, R]
65+
66+
//* // val vxs1 = xs append that
67+
//* // val vxs2 = VCons(x, vxs1)
68+
//* // vxs1
69+
//* // [error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/gadtVect.scala:65:14
70+
//* // [error] 65 | vxs1
71+
//* // [error] | ^^^^
72+
//* // [error] | found: NatsVects.Vec[T, r](vxs1)
73+
//* // [error] | required: NatsVects.Vec[T, R]
74+
//* // [error] |
75+
//* // [error] | where: r is a type in method append with bounds <: NatsVects.TNat
76+
//* // vxs2
77+
//* // [error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/gadtVect.scala:71:14
78+
//* // [error] 71 | vxs2
79+
//* // [error] | ^^^^
80+
//* // [error] | found: NatsVects.VCons[T, r](vxs2)
81+
//* // [error] | required: NatsVects.Vec[T, R]
82+
//* // [error] |
83+
//* // [error] | where: r is a type in method append with bounds <: NatsVects.TNat
84+
85+
//* // vxs2.asInstanceOf // sorry this works
86+
//* }
87+
}
88+
}
89+
}
90+
}

‎tests/gadt/banal.scala

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
object banal {
2+
sealed trait T[A]
3+
final case class StrLit(v: String) extends T[String]
4+
final case class IntLit(v: Int) extends T[Int]
5+
6+
def eval[A](t: T[A]): A = t match {
7+
case StrLit(v) => v
8+
case IntLit(v) => v
9+
}
10+
11+
def evul[A](t: T[A]): A = t match {
12+
case StrLit(_) => ""
13+
case IntLit(_) => 0
14+
}
15+
}

‎tests/gadt/foo.scala

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
object foo {
2+
sealed trait Exp[T]
3+
case class Var[T](name: String) extends Exp[T]
4+
5+
def env[T](x: Var[T]): T = ???
6+
7+
def eval[S](e: Exp[S]) = e match {
8+
case v: Var[foo] =>
9+
env(v)
10+
}
11+
}

‎tests/gadt/injectivity.scala

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
object injectivity {
2+
sealed trait EQ[A, B]
3+
final case class Refl[A](u: Unit) extends EQ[A, A]
4+
5+
def conform[A, B, C, D](a: A, b: B, eq: EQ[(A, B), (C, D)]): C =
6+
eq match {
7+
case Refl(()) => a
8+
}
9+
}

‎tests/gadt/one.scala

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
object one {
2+
case class One[T](fst: T)
3+
def bad[T](e: One[T]) = e match {
4+
case foo: One[a] =>
5+
val t: T = e.fst
6+
// val nok: Nothing = t // should not compile
7+
val ok: a = t // does compile
8+
}
9+
}

‎tests/gadt/simpleEQ.scala

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
object simpleEQ {
2+
sealed trait EQ[A, B]
3+
final case class Refl[A](u: Unit) extends EQ[A, A]
4+
5+
def conform[A, B](a: A, eq: EQ[A, B]): B = eq match {
6+
case Refl(()) => a
7+
}
8+
9+
def conform2[A, B, C, D](a: A, b: B, eq: EQ[(A, B), (C, D)]): (C, D) =
10+
eq match {
11+
case Refl(()) => (a, b)
12+
}
13+
}

0 commit comments

Comments
 (0)