1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
class Annot(obj: Any) extends Annotation with TypeConstraint
defined class Annot
-----
class A {
val x = "hello"
val y: Int @Annot(x) = 10
override def toString = "an A"
}
defined class A
-----
val a = new A
a: A = an A
-----
val y = a.y // should rewrite "this.x" to "a.x"
y: Int @Annot(a.x) = 10
-----
var a2 = new A
a2: A = an A
-----
val y2 = a2.y // should drop the annotation
y2: Int = 10
-----
object Stuff {
val x = "hello"
val y : Int @Annot(x) = 10
}
defined module Stuff
-----
val y = Stuff.y // should rewrite the annotation
y: Int @Annot(Stuff.x) = 10
-----
class B {
val y: Int @Annot(Stuff.x) = 10
override def toString = "a B"
}
defined class B
-----
val b = new B
b: B = a B
-----
val y = b.y // should keep the annotation
y: Int @Annot(Stuff.x) = 10
-----
def m(x: String): String @Annot(x) = x // m should be annotated with a debruijn
m: (x$0:String)String @Annot(x)
-----
val three = "three"
three: java.lang.String = three
-----
val three2 = m(three:three.type) // should change x to three
three2: String @Annot(three) = three
-----
var four = "four"
four: java.lang.String = four
-----
val four2 = m(four) // should have an existential bound
four2: String @Annot(x) forSome { val x: java.lang.String } = four
-----
val four3 = four2 // should have the same type as four2
four3: String @Annot(x) forSome { val x: java.lang.String } = four
-----
val stuff = m("stuff") // should not crash
stuff: String @Annot("stuff") = stuff
-----
class peer extends Annotation // should not crash
defined class peer
-----
class NPE[T <: NPE[T] @peer] // should not crash
error: illegal cyclic reference involving class NPE
-----
def m = {
val x = "three"
val y : String @Annot(x) = x
y
} // x should be existentially bound
m: String @Annot(x) forSome { val x: java.lang.String }
-----
def n(y: String) = {
def m(x: String) : String @Annot(x) = {
(if (x == "")
m("default")
else
x)
}
m("stuff".stripMargin)
} // x should be existentially bound
n: (String)String @Annot(x) forSome { val x: String }
-----
class rep extends Annotation
defined class rep
-----
object A { val x = "hello" : String @ rep }
defined module A
-----
val y = a.x // should drop the annotation
y: java.lang.String = hello
-----
val x = 3 : Int @Annot(e+f+g+h) //should have a graceful error message
<console>:5: error: not found: value e
val x = 3 : Int @Annot(e+f+g+h) //should have a graceful error message
^
-----
class Where(condition: Boolean) extends Annotation
defined class Where
-----
val x : Int @Where(self > 0 && self < 100) = 3
x: Int @Where(self.>(0).&&(self.<(100))) = 3
-----
|
