Skip to content

Commit cf6b045

Browse files
Linyxusodersky
authored andcommitted
Revise freeze signature to take a Mutable parameter
That way we can also freeze read-only Mutables. Also: Adapt boxes and double flip tests
1 parent d8e4b60 commit cf6b045

File tree

6 files changed

+112
-2
lines changed

6 files changed

+112
-2
lines changed

library/src/scala/caps/package.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -195,7 +195,7 @@ end internal
195195
* result of pure operation `op`, turning them into immutable types.
196196
*/
197197
@experimental
198-
def freeze[T](@internal.consume x: Mutable^): x.type = x
198+
def freeze[T](@internal.consume x: Mutable): x.type = x
199199

200200
@experimental
201201
object unsafe:
Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-boxes.scala:22:4 ----------------------------------
2+
21 | val xs: Box[Ref^{}] = freeze:
3+
22 | Box(a) // error
4+
| ^
5+
| Found: Box[Ref^{a.rd}]^{}
6+
| Required: Box[Ref^{}]^{cap.rd}
7+
|
8+
| Note that capability a.rd is not included in capture set {}.
9+
|
10+
| where: cap is a fresh root capability classified as Unscoped in the type of value xs
11+
|
12+
| longer explanation available when compiling with `-explain`
13+
-- Error: tests/neg-custom-args/captures/freeze-boxes.scala:29:7 -------------------------------------------------------
14+
29 | Box(a) // error
15+
| ^^^^^^
16+
|Separation failure: Illegal access to {cap of value a} which is hidden by the previous definition
17+
|of value a with type Ref^.
18+
|This type hides capabilities {cap}
19+
|
20+
|where: ^ refers to a fresh root capability classified as Unscoped in the type of value a
21+
| cap is a fresh root capability classified as Unscoped created in value a when instantiating method allocRef's type (): Ref^²
22+
-- Error: tests/neg-custom-args/captures/freeze-boxes.scala:31:6 -------------------------------------------------------
23+
31 | par(() => a.set(42), () => println(b.get)) // error
24+
| ^^^^^^^^^^^^^^^
25+
|Separation failure: argument of type () ->{a} Unit
26+
|to method par: (op1: () => Unit, op2: () => Unit): Unit
27+
|corresponds to capture-polymorphic formal parameter op1 of type () => Unit
28+
|and hides capabilities {a}.
29+
|Some of these overlap with the captures of the second argument with type () ->{b.rd} Unit.
30+
|
31+
| Hidden set of current argument : {a}
32+
| Hidden footprint of current argument : {a}
33+
| Capture set of second argument : {b.rd}
34+
| Footprint set of second argument : {b.rd, a.rd}
35+
| The two sets overlap at : {a}
36+
|
37+
|where: => refers to a fresh root capability created in method test2 when checking argument to parameter op1 of method par
38+
-- Error: tests/neg-custom-args/captures/freeze-boxes.scala:37:12 ------------------------------------------------------
39+
37 | par(() => a.set(42), () => println(b.get)) // error
40+
| ^
41+
| Separation failure: Illegal access to (a : Ref^), which was passed as a consume parameter to method freeze
42+
| on line 36 and therefore is no longer available.
43+
|
44+
| where: ^ refers to a fresh root capability classified as Unscoped in the type of value a
Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.{Mutable, freeze}
4+
5+
// A mutable ref and its immutable version
6+
class Ref extends Mutable:
7+
private var data: Int = 0
8+
def get: Int = data
9+
update def set(x: Int): Unit = data = x
10+
def allocRef(): Ref^ = Ref()
11+
type IRef = Ref^{}
12+
13+
// Boxes
14+
case class Box[+T](unbox: T) extends caps.Mutable
15+
16+
// Parallelism
17+
def par(op1: () => Unit, op2: () => Unit): Unit = ()
18+
19+
def test1(): Unit =
20+
val a = allocRef()
21+
val xs: Box[Ref^{}] = freeze:
22+
Box(a) // error
23+
val b = xs.unbox
24+
par(() => a.set(42), () => println(b.get))
25+
26+
def test2(): Unit =
27+
val a = allocRef()
28+
val xs = freeze:
29+
Box(a) // error
30+
val b = xs.unbox
31+
par(() => a.set(42), () => println(b.get)) // error
32+
33+
def test3(): Unit =
34+
val a = allocRef()
35+
val b = freeze:
36+
a
37+
par(() => a.set(42), () => println(b.get)) // error
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-double-flip.scala:16:48 ---------------------------
2+
16 | val reallybad: Ref^ -> Ref^{} = x => magic(x)(x => x) // error
3+
| ^^^^^^
4+
|Found: (x: Ref^'s1) ->'s2 Ref^{x.rd}
5+
|Required: Ref^ => Ref^{cap.rd}
6+
|
7+
|Note that capability x.rd is not included in capture set {cap.rd}.
8+
|
9+
|where: => refers to a fresh root capability created in anonymous function of type (x: Ref^): Ref^{} when checking argument to parameter x$0 of method apply
10+
| ^ refers to the universal root capability
11+
| cap is a fresh root capability created in anonymous function of type (x: Ref^): Ref^{} when checking argument to parameter x$0 of method apply
12+
|
13+
| longer explanation available when compiling with `-explain`
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
import language.experimental.captureChecking
2+
import language.experimental.separationChecking
3+
import caps.{Mutable, freeze}
4+
5+
// A mutable ref and its immutable version
6+
class Ref extends Mutable:
7+
private var data: Int = 0
8+
def get: Int = data
9+
update def set(x: Int): Unit = data = x
10+
def allocRef(): Ref^ = Ref()
11+
type IRef = Ref^{}
12+
13+
def test1(): Unit =
14+
val magic = freeze:
15+
(x: Ref^) => (op: Ref^ => IRef) => op(x)
16+
val reallybad: Ref^ -> Ref^{} = x => magic(x)(x => x) // error

tests/neg-custom-args/captures/freeze.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,6 @@
22
11 | val b = freeze((a, a)) // error
33
| ^^^^^^
44
| Found: (Arr[String], Arr[String])
5-
| Required: scala.caps.Mutable^
5+
| Required: scala.caps.Mutable
66
|
77
| longer explanation available when compiling with `-explain`

0 commit comments

Comments
 (0)