Skip to content

Commit 8a504aa

Browse files
committed
Add @unboxed to failing tests and standard library file Buffer.scala
1 parent 8308b33 commit 8a504aa

15 files changed

+105
-44
lines changed

scala2-library-cc/src/scala/collection/mutable/Buffer.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ package mutable
1515

1616
import scala.annotation.nowarn
1717
import language.experimental.captureChecking
18-
18+
import caps.unboxed
1919

2020
/** A `Buffer` is a growable and shrinkable `Seq`. */
2121
trait Buffer[A]
@@ -180,7 +180,7 @@ trait IndexedBuffer[A] extends IndexedSeq[A]
180180

181181
override def iterableFactory: SeqFactory[IndexedBuffer] = IndexedBuffer
182182

183-
def flatMapInPlace(f: A => IterableOnce[A]^): this.type = {
183+
def flatMapInPlace(@unboxed f: A => IterableOnce[A]^): this.type = {
184184
// There's scope for a better implementation which copies elements in place.
185185
var i = 0
186186
val s = size

tests/neg-custom-args/captures/i15749a.scala

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,6 @@
11
import caps.cap
2+
import caps.unboxed
3+
24
class Unit
35
object u extends Unit
46

@@ -16,7 +18,7 @@ def test =
1618

1719
def force[A](thunk: Unit ->{cap} A): A = thunk(u)
1820

19-
def forceWrapper[A](mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
21+
def forceWrapper[A](@unboxed mx: Wrapper[Unit ->{cap} A]): Wrapper[A] =
2022
// Γ ⊢ mx: Wrapper[□ {cap} Unit => A]
2123
// `force` should be typed as ∀(□ {cap} Unit -> A) A, but it can not
2224
strictMap[Unit ->{mx*} A, A](mx)(t => force[A](t)) // error // should work
Lines changed: 22 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
1-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:23:11 --------------------------------------
2-
23 | cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:24:11 --------------------------------------
2+
24 | cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
33
| ^^^^^^^^^^^^^^^^^^^^^^^
44
| Found: List[box () ->{f} Unit]
55
| Required: List[box () ->{xs*} Unit]
66
|
77
| longer explanation available when compiling with `-explain`
8-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:34:7 ---------------------------------------
9-
34 | (() => f.write()) :: Nil // error since {f*} !<: {xs*}
8+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:35:7 ---------------------------------------
9+
35 | (() => f.write()) :: Nil // error since {f*} !<: {xs*}
1010
| ^^^^^^^^^^^^^^^^^^^^^^^
1111
| Found: List[box () ->{f} Unit]
1212
| Required: box List[box () ->{xs*} Unit]^?
@@ -15,34 +15,42 @@
1515
| cannot be included in outer capture set {xs*} of value cur
1616
|
1717
| longer explanation available when compiling with `-explain`
18-
-- Error: tests/neg-custom-args/captures/reaches.scala:37:6 ------------------------------------------------------------
19-
37 | var cur: List[Proc] = xs // error: Illegal type for var
18+
-- Error: tests/neg-custom-args/captures/reaches.scala:38:6 ------------------------------------------------------------
19+
38 | var cur: List[Proc] = xs // error: Illegal type for var
2020
| ^
2121
| Mutable variable cur cannot have type List[box () => Unit] since
2222
| the part box () => Unit of that type captures the root capability `cap`.
23-
-- Error: tests/neg-custom-args/captures/reaches.scala:44:15 -----------------------------------------------------------
24-
44 | val cur = Ref[List[Proc]](xs) // error: illegal type for type argument to Ref
23+
-- Error: tests/neg-custom-args/captures/reaches.scala:45:15 -----------------------------------------------------------
24+
45 | val cur = Ref[List[Proc]](xs) // error: illegal type for type argument to Ref
2525
| ^^^^^^^^^^^^^^^
2626
| Sealed type variable T cannot be instantiated to List[box () => Unit] since
2727
| the part box () => Unit of that type captures the root capability `cap`.
2828
| This is often caused by a local capability in an argument of constructor Ref
2929
| leaking as part of its result.
30-
-- Error: tests/neg-custom-args/captures/reaches.scala:54:31 -----------------------------------------------------------
31-
54 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
30+
-- Error: tests/neg-custom-args/captures/reaches.scala:55:31 -----------------------------------------------------------
31+
55 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error
3232
| ^^^^^^^^^^^^^^^^^^^^
3333
| Sealed type variable A cannot be instantiated to box () => Unit since
3434
| that type captures the root capability `cap`.
3535
| This is often caused by a local capability in an argument of constructor Id
3636
| leaking as part of its result.
37-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:63:27 --------------------------------------
38-
63 | val f1: File^{id*} = id(f) // error, since now id(f): File^
37+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:64:27 --------------------------------------
38+
64 | val f1: File^{id*} = id(f) // error, since now id(f): File^
3939
| ^^^^^
4040
| Found: File^{id, f}
4141
| Required: File^{id*}
4242
|
4343
| longer explanation available when compiling with `-explain`
44-
-- Error: tests/neg-custom-args/captures/reaches.scala:80:5 ------------------------------------------------------------
45-
80 | ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now)
44+
-- Error: tests/neg-custom-args/captures/reaches.scala:81:5 ------------------------------------------------------------
45+
81 | ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now) // error // error
4646
| ^^^^^^
4747
| Reach capability cap and universal capability cap cannot both
4848
| appear in the type [B](f: ((box A ->{ps*} A, box A ->{ps*} A)) => B): List[B] of this expression
49+
-- Error: tests/neg-custom-args/captures/reaches.scala:81:10 -----------------------------------------------------------
50+
81 | ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now) // error // error
51+
| ^
52+
| Local reach capability ps* leaks into capture scope of method mapCompose
53+
-- Error: tests/neg-custom-args/captures/reaches.scala:81:13 -----------------------------------------------------------
54+
81 | ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now) // error // error
55+
| ^
56+
| Local reach capability ps* leaks into capture scope of method mapCompose

tests/neg-custom-args/captures/reaches.scala

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
//> using options -source 3.4
22
// (to make sure we use the sealed policy)
3+
import caps.unboxed
34
class File:
45
def write(): Unit = ???
56

@@ -12,7 +13,7 @@ class Ref[T](init: T):
1213
def get: T = x
1314
def set(y: T) = { x = y }
1415

15-
def runAll0(xs: List[Proc]): Unit =
16+
def runAll0(@unboxed xs: List[Proc]): Unit =
1617
var cur: List[() ->{xs*} Unit] = xs // OK, by revised VAR
1718
while cur.nonEmpty do
1819
val next: () ->{xs*} Unit = cur.head
@@ -22,7 +23,7 @@ def runAll0(xs: List[Proc]): Unit =
2223
usingFile: f =>
2324
cur = (() => f.write()) :: Nil // error since {f*} !<: {xs*}
2425

25-
def runAll1(xs: List[Proc]): Unit =
26+
def runAll1(@unboxed xs: List[Proc]): Unit =
2627
val cur = Ref[List[() ->{xs*} Unit]](xs) // OK, by revised VAR
2728
while cur.get.nonEmpty do
2829
val next: () ->{xs*} Unit = cur.get.head
@@ -77,4 +78,4 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
7778
z => g(f(z))
7879

7980
def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
80-
ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now)
81+
ps.map((x, y) => compose1(x, y)) // error: cannot mix cap and * (should work now) // error // error

tests/neg-custom-args/captures/widen-reach.check

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,11 @@
1-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 ----------------------------------
1+
-- Error: tests/neg-custom-args/captures/widen-reach.scala:13:26 -------------------------------------------------------
22
13 | val y2: IO^ -> IO^ = y1.foo // error
33
| ^^^^^^
4-
| Found: IO^ ->{x*} IO^{x*}
5-
| Required: IO^ -> (ex$6: caps.Exists) -> IO^{ex$6}
6-
|
7-
| longer explanation available when compiling with `-explain`
8-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/widen-reach.scala:14:30 ----------------------------------
4+
| Local reach capability x* leaks into capture scope of method test
5+
-- Error: tests/neg-custom-args/captures/widen-reach.scala:14:30 -------------------------------------------------------
96
14 | val y3: IO^ -> IO^{x*} = y1.foo // error
107
| ^^^^^^
11-
| Found: IO^ ->{x*} IO^{x*}
12-
| Required: IO^ -> IO^{x*}
13-
|
14-
| longer explanation available when compiling with `-explain`
8+
| Local reach capability x* leaks into capture scope of method test
159
-- [E164] Declaration Error: tests/neg-custom-args/captures/widen-reach.scala:9:6 --------------------------------------
1610
9 | val foo: IO^ -> IO^ = x => x // error
1711
| ^

tests/neg/i20503.scala

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import language.experimental.captureChecking
2+
import caps.unboxed
23

34
class List[+A]:
45
def head: A = ???
@@ -7,10 +8,11 @@ class List[+A]:
78
def foreach[U](f: A => U): Unit = ???
89
def nonEmpty: Boolean = ???
910

10-
def runOps(ops: List[() => Unit]): Unit =
11+
def runOps(@unboxed ops: List[() => Unit]): Unit =
1112
// See i20156, due to limitation in expressiveness of current system,
1213
// we could map over the list of impure elements. OK with existentials.
1314
ops.foreach(op => op())
1415

1516
def main(): Unit =
16-
val f: List[() => Unit] -> Unit = runOps // error
17+
val f: List[() => Unit] -> Unit = (ops: List[() => Unit]) => runOps(ops) // error
18+
val _: List[() => Unit] -> Unit = runOps // error

tests/neg/leak-problem-unboxed.scala

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
import language.experimental.captureChecking
2+
import caps.unboxed
3+
4+
// Some capabilities that should be used locally
5+
trait Async:
6+
// some method
7+
def read(): Unit
8+
def usingAsync[X](op: Async^ => X): X = ???
9+
10+
case class Box[+T](get: T)
11+
12+
def useBoxedAsync(@unboxed x: Box[Async^]): Unit =
13+
val t0 = x
14+
val t1 = t0.get // ok
15+
t1.read()
16+
17+
def useBoxedAsync1(@unboxed x: Box[Async^]): Unit = x.get.read() // ok
18+
19+
def test(): Unit =
20+
21+
val f: Box[Async^] => Unit = (x: Box[Async^]) => useBoxedAsync(x) // error
22+
val _: Box[Async^] => Unit = useBoxedAsync(_) // error
23+
val _: Box[Async^] => Unit = useBoxedAsync // error
24+
val _ = useBoxedAsync(_) // error
25+
val _ = useBoxedAsync // error
26+
27+
def boom(x: Async^): () ->{f} Unit =
28+
() => f(Box(x))
29+
30+
val leaked = usingAsync[() ->{f} Unit](boom)
31+
32+
leaked() // scope violation

tests/pos-custom-args/captures/dep-reach.scala

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
1+
import caps.unboxed
12
object Test:
23
class C
34
type Proc = () => Unit
45

56
def f(c: C^, d: C^): () ->{c, d} Unit =
6-
def foo(xs: Proc*): () ->{xs*} Unit =
7+
def foo(@unboxed xs: Proc*): () ->{xs*} Unit =
78
xs.head
89
val a: () ->{c} Unit = () => ()
910
val b: () ->{d} Unit = () => ()
@@ -12,7 +13,7 @@ object Test:
1213

1314
def g(c: C^, d: C^): () ->{c, d} Unit =
1415

15-
def foo(xs: Seq[() => Unit]): () ->{xs*} Unit =
16+
def foo(@unboxed xs: Seq[() => Unit]): () ->{xs*} Unit =
1617
xs.head
1718

1819
val a: () ->{c} Unit = () => ()

tests/pos-custom-args/captures/reaches.scala

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
import caps.unboxed
2+
13
class C
24
def f(xs: List[C^]) =
35
val y = xs
@@ -20,7 +22,7 @@ extension [A](x: A) def :: (xs: List[A]): List[A] = ???
2022

2123
object Nil extends List[Nothing]
2224

23-
def runAll(xs: List[Proc]): Unit =
25+
def runAll(@unboxed xs: List[Proc]): Unit =
2426
var cur: List[() ->{xs*} Unit] = xs // OK, by revised VAR
2527
while cur.nonEmpty do
2628
val next: () ->{xs*} Unit = cur.head

tests/pos/cc-poly-source-capability.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import language.experimental.captureChecking
22
import annotation.experimental
33
import caps.{CapSet, Capability}
4+
import caps.unboxed
45

56
@experimental object Test:
67

@@ -17,7 +18,7 @@ import caps.{CapSet, Capability}
1718

1819
def allListeners: Set[Listener^{X^}] = listeners
1920

20-
def test1(async1: Async, others: List[Async]) =
21+
def test1(async1: Async, @unboxed others: List[Async]) =
2122
val src = Source[CapSet^{async1, others*}]
2223
val lst1 = listener(async1)
2324
val lsts = others.map(listener)

tests/pos/cc-poly-source.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import language.experimental.captureChecking
22
import annotation.experimental
33
import caps.{CapSet, Capability}
4+
import caps.unboxed
45

56
@experimental object Test:
67

@@ -24,7 +25,7 @@ import caps.{CapSet, Capability}
2425
val ls = src.allListeners
2526
val _: Set[Listener^{lbl1, lbl2}] = ls
2627

27-
def test2(lbls: List[Label^]) =
28+
def test2(@unboxed lbls: List[Label^]) =
2829
def makeListener(lbl: Label^): Listener^{lbl} = ???
2930
val listeners = lbls.map(makeListener)
3031
val src = Source[CapSet^{lbls*}]

tests/pos/gears-probem-1.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import language.experimental.captureChecking
2+
import caps.unboxed
23

34
trait Future[+T]:
45
def await: T
@@ -16,7 +17,7 @@ class Result[+T, +E]:
1617
case class Err[+E](e: E) extends Result[Nothing, E]
1718
case class Ok[+T](x: T) extends Result[T, Nothing]
1819

19-
extension [T](fs: Seq[Future[T]^])
20+
extension [T](@unboxed fs: Seq[Future[T]^])
2021
def awaitAll =
2122
val collector//: Collector[T]{val futures: Seq[Future[T]^{fs*}]}
2223
= Collector(fs)

tests/pos/i18699.scala

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
import language.experimental.captureChecking
2+
import caps.unboxed
3+
24
trait Cap:
35
def use: Int = 42
46

5-
def test2(cs: List[Cap^]): Unit =
7+
def test2(@unboxed cs: List[Cap^]): Unit =
68
val t0: Cap^{cs*} = cs.head // error
7-
var t1: Cap^{cs*} = cs.head // error
9+
var t1: Cap^{cs*} = cs.head // error

tests/pos/reach-capability.scala

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
import language.experimental.captureChecking
22
import annotation.experimental
3-
import caps.{Capability}
3+
import caps.Capability
4+
import caps.unboxed
45

56
@experimental object Test2:
67

@@ -11,7 +12,7 @@ import caps.{Capability}
1112

1213
class Listener
1314

14-
def test2(lbls: List[Label]) =
15+
def test2(@unboxed lbls: List[Label]) =
1516
def makeListener(lbl: Label): Listener^{lbl} = ???
1617
val listeners = lbls.map(makeListener) // should work
1718

tests/pos/reach-problem.scala

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,22 @@
11
import language.experimental.captureChecking
2+
import caps.unboxed
23

34
class Box[T](items: Seq[T^]):
45
def getOne: T^{items*} = ???
56

67
object Box:
7-
def getOne[T](items: Seq[T^]): T^{items*} =
8+
def getOne[T](@unboxed items: Seq[T^]): T^{items*} =
89
val bx = Box(items)
9-
bx.getOne
10+
bx.getOne
11+
/*
12+
def head[T](items: Seq[T^]): Unit =
13+
val is = items
14+
val x = is.head
15+
()
16+
17+
def head2[X^, T](items: Seq[T^{X^}]): T^{X^} =
18+
items.head
19+
20+
def head3[T](items: Seq[T^]): Unit =
21+
head2[caps.CapSet^{items*}, T](items)
22+
*/

0 commit comments

Comments
 (0)