Skip to content

Commit a0f1613

Browse files
oderskyodersky
committed
New test cases
1 parent c8f51e7 commit a0f1613

File tree

4 files changed

+121
-5
lines changed

4 files changed

+121
-5
lines changed

‎tests/neg-custom-args/captures/fresh-counter.check‎

Lines changed: 20 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
-- Error: tests/neg-custom-args/captures/fresh-counter.scala:22:6 ------------------------------------------------------
2-
22 | par(i, d) // error: separation failure
1+
-- Error: tests/neg-custom-args/captures/fresh-counter.scala:23:6 ------------------------------------------------------
2+
23 | par(i, d) // error: separation failure
33
| ^
44
|Separation failure: argument of type (i : () ->{c.incr} Unit)
55
|to method par: (p1: () => Unit, p2: () => Unit): Unit
@@ -10,7 +10,23 @@
1010
| Hidden set of current argument : {i}
1111
| Hidden footprint of current argument : {i, c.incr, c.count}
1212
| Capture set of second argument : {d}
13-
| Footprint set of second argument : {d, c.decr, c.count}
14-
| The two sets overlap at : {c.count}
13+
| Footprint set of second argument : {d, c.decr, c}
14+
| The two sets overlap at : {c.incr, c.count}
1515
|
1616
|where: => refers to a fresh root capability created in method test when checking argument to parameter p1 of method par
17+
-- Error: tests/neg-custom-args/captures/fresh-counter.scala:33:4 ------------------------------------------------------
18+
33 | () => count.put(count.get + 1), // error: separation failure
19+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
20+
|Separation failure: argument of type () ->{count} Unit
21+
|to constructor Pair: (a: () => Unit, b: () => Unit): Pair
22+
|corresponds to capture-polymorphic formal parameter a of type () => Unit
23+
|and hides capabilities {count}.
24+
|Some of these overlap with the captures of the second argument with type () ->{count} Unit.
25+
|
26+
| Hidden set of current argument : {count}
27+
| Hidden footprint of current argument : {count}
28+
| Capture set of second argument : {count}
29+
| Footprint set of second argument : {count}
30+
| The two sets overlap at : {count}
31+
|
32+
|where: => refers to a fresh root capability created in method mkCounter when checking argument to parameter a of constructor Pair

‎tests/neg-custom-args/captures/fresh-counter.scala‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,14 +10,26 @@ class Counter:
1010
private val count: Ref^ = Ref()
1111
val incr = () =>
1212
count.put(count.get + 1)
13-
val decr = () =>
13+
val decr: () ->{this} Unit = () =>
1414
count.put(count.get - 1)
1515

1616
def par(p1: () => Unit, p2: () => Unit) = ()
17+
def seq(p1: () => Unit, p2: () ->{cap, p1} Unit) = ()
1718

1819
def test() =
1920
val c = Counter()
2021
val i = c.incr
2122
val d = c.decr
2223
par(i, d) // error: separation failure
24+
seq(i, d)
25+
26+
type Proc = () => Unit
27+
28+
class Pair(val a: Proc, val b: Proc)
29+
30+
def mkCounter(): Pair^ =
31+
val count = Ref()
32+
Pair(
33+
() => count.put(count.get + 1), // error: separation failure
34+
() => count.put(count.get - 1))
2335

‎tests/neg-custom-args/captures/sep-curried-par.check‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-curried-par.scala:23:32 ------------------------------
2+
23 | val bar = (p1: () => Unit) => (p2: () ->{p1, cap} Unit) => par(p1, p2) // error, but error message could be better
3+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
4+
| Found: (p2: () ->{p1, cap} Unit) ->{p1} Unit
5+
| Required: (() ->'s1 Unit) ->'s2 Unit
6+
|
7+
| Note that capability p1, defined in method $anonfun
8+
| cannot be included in outer capture set 's2.
9+
|
10+
| where: cap is the universal root capability
11+
|
12+
| longer explanation available when compiling with `-explain`
13+
-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:6:48 ----------------------------------------------------
14+
6 |def parCurriedBad(p1: () => Unit): (() => Unit) => Unit = // error: consume failure
15+
| ^^^^^^^^^^^^^^^^^^^^
16+
| Separation failure: method parCurriedBad's result type (() => Unit) => Unit hides parameter p1.
17+
| The parameter needs to be annotated with consume to allow this.
18+
-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:15:6 ----------------------------------------------------
19+
15 | par(p, p) // error: separation
20+
| ^
21+
|Separation failure: argument of type (p : () => Unit)
22+
|to method par: (p1: () => Unit, p2: () => Unit): Unit
23+
|corresponds to capture-polymorphic formal parameter p1 of type () =>² Unit
24+
|and hides capabilities {p}.
25+
|Some of these overlap with the captures of the second argument with type (p : () => Unit).
26+
|
27+
| Hidden set of current argument : {p}
28+
| Hidden footprint of current argument : {p}
29+
| Capture set of second argument : {p}
30+
| Footprint set of second argument : {p}
31+
| The two sets overlap at : {p}
32+
|
33+
|where: => refers to a fresh root capability in the type of value p
34+
| =>² refers to a fresh root capability created in method test when checking argument to parameter p1 of method par
35+
-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:18:16 ---------------------------------------------------
36+
18 | parCurried(p)(p) // error: consume failure
37+
| ^
38+
| Separation failure: Illegal access to (p : () => Unit), which was passed to a
39+
| consume parameter or was used as a prefix to a consume method on line 18
40+
| and therefore is no longer available.
41+
|
42+
| where: => refers to a fresh root capability in the type of value p
43+
-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:21:9 ----------------------------------------------------
44+
21 | foo(c)(c) // error: separation
45+
| ^
46+
|Separation failure: argument of type (c : () => Unit)
47+
|to a function of type (() => Unit) ->{c} Unit
48+
|corresponds to capture-polymorphic formal parameter v1 of type () =>² Unit
49+
|and hides capabilities {c}.
50+
|Some of these overlap with the captures of the function prefix.
51+
|
52+
| Hidden set of current argument : {c}
53+
| Hidden footprint of current argument : {c}
54+
| Capture set of function prefix : {c}
55+
| Footprint set of function prefix : {c}
56+
| The two sets overlap at : {c}
57+
|
58+
|where: => refers to a fresh root capability in the type of parameter c
59+
| =>² refers to a fresh root capability created in method test when checking argument to parameter v1 of method apply

‎tests/neg-custom-args/captures/sep-curried-par.scala‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
import caps.cap
2+
3+
def par(p1: () => Unit, p2: () => Unit) = ()
4+
def seq(p1: () => Unit, p2: () ->{cap, p1} Unit) = ()
5+
6+
def parCurriedBad(p1: () => Unit): (() => Unit) => Unit = // error: consume failure
7+
(p2: () => Unit) => par(p1, p2)
8+
def parCurried(consume p1: () => Unit): (() => Unit) => Unit =
9+
(p2: () => Unit) => par(p1, p2)
10+
11+
type Proc = () => Unit
12+
13+
def test(c: () => Unit) =
14+
val p: Proc = ???
15+
par(p, p) // error: separation
16+
seq(p, p)
17+
parCurriedBad(p)(p) // ok, but parCurriedBad ill-typed
18+
parCurried(p)(p) // error: consume failure
19+
20+
val foo = (p1: () => Unit) => (p2: () ->{c, cap} Unit) => par(p1, p2)
21+
foo(c)(c) // error: separation
22+
23+
val bar = (p1: () => Unit) => (p2: () ->{p1, cap} Unit) => par(p1, p2) // error, but error message could be better
24+
bar(c)(c)
25+
26+
27+
28+
29+

0 commit comments

Comments
 (0)