-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Be more careful computing underlying types of reach capabilities
We can use the dcs only if there are no type variables.
- Loading branch information
Showing
11 changed files
with
165 additions
and
46 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:19:62 -------------------------------- | ||
| 19 | val fut: Future[T]^{fs*} = collector.results.read().right.get // error | ||
| | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
| | Found: Future[T]^{collector.futures*} | ||
| | Required: Future[T]^{fs*} | ||
| | | ||
| | longer explanation available when compiling with `-explain` | ||
| -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/gears-problem.scala:24:34 -------------------------------- | ||
| 24 | val fut2: Future[T]^{fs*} = r.get // error | ||
| | ^^^^^ | ||
| | Found: Future[box T^?]^{collector.futures*} | ||
| | Required: Future[T]^{fs*} | ||
| | | ||
| | longer explanation available when compiling with `-explain` | ||
| there were 4 deprecation warnings; re-run with -deprecation for details |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| import language.experimental.captureChecking | ||
| import caps.{cap, use} | ||
|
|
||
| trait IO | ||
| trait Async | ||
|
|
||
| def main(io: IO^, async: Async^) = | ||
| def bad[X](ops: List[(X, () ->{io} Unit)])(f: () ->{ops*} Unit): () ->{io} Unit = f // error | ||
| def runOps(@use ops: List[(() => Unit, () => Unit)]): () ->{ops*} Unit = | ||
| () => ops.foreach((f1, f2) => { f1(); f2() }) | ||
| def delayOps(@use ops: List[(() ->{async} Unit, () ->{io} Unit)]): () ->{io} Unit = | ||
| val runner: () ->{ops*} Unit = runOps(ops) | ||
| val badRunner: () ->{io} Unit = bad[() ->{async} Unit](ops)(runner) | ||
| // it uses both async and io, but we losed track of async. | ||
| badRunner |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| -- Error: tests/neg-custom-args/captures/use-capset.scala:7:50 --------------------------------------------------------- | ||
| 7 |private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error | ||
| | ^^^^^^^ | ||
| | Capture set parameter C leaks into capture scope of method g. | ||
| | To allow this, the type C should be declared with a @use annotation | ||
| -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:13:22 ----------------------------------- | ||
| 13 | val _: () -> Unit = h // error: should be ->{io} | ||
| | ^ | ||
| | Found: (h : () ->{io} Unit) | ||
| | Required: () -> Unit | ||
| | | ||
| | longer explanation available when compiling with `-explain` | ||
| -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/use-capset.scala:15:50 ----------------------------------- | ||
| 15 | val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io} | ||
| | ^^ | ||
| | Found: () ->? (x$0: List[box Object^{io}]^{}) ->{io} (ex$13: caps.Exists) -> Object^{io} | ||
| | Required: () -> List[box Object^{io}] -> Object^{io} | ||
| | | ||
| | longer explanation available when compiling with `-explain` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,16 @@ | ||
| import caps.{use, CapSet} | ||
|
|
||
|
|
||
|
|
||
| def f[C^](@use xs: List[Object^{C^}]): Unit = ??? | ||
|
|
||
| private def g[C^] = (xs: List[Object^{C^}]) => xs.head // error | ||
|
|
||
| private def g2[@use C^] = (xs: List[Object^{C^}]) => xs.head // ok | ||
|
|
||
| def test(io: Object^)(@use xs: List[Object^{io}]): Unit = | ||
| val h = () => f(xs) | ||
| val _: () -> Unit = h // error: should be ->{io} | ||
| val h2 = () => g[CapSet^{io}] | ||
| val _: () -> List[Object^{io}] -> Object^{io} = h2 // error, should be ->{io} | ||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| import language.experimental.captureChecking | ||
| import caps.{use, CapSet} | ||
|
|
||
| trait Future[+T]: | ||
| def await: T | ||
|
|
||
| trait Channel[+T]: | ||
| def read(): Ok[T] | ||
|
|
||
| class Collector[T, C^](val futures: Seq[Future[T]^{C^}]): | ||
| val results: Channel[Future[T]^{C^}] = ??? | ||
| end Collector | ||
|
|
||
| class Result[+T, +E]: | ||
| def get: T = ??? | ||
|
|
||
| case class Err[+E](e: E) extends Result[Nothing, E] | ||
| case class Ok[+T](x: T) extends Result[T, Nothing] | ||
|
|
||
| extension [T, C^](@use fs: Seq[Future[T]^{C^}]) | ||
| def awaitAllPoly = | ||
| val collector = Collector(fs) | ||
| val fut: Future[T]^{C^} = collector.results.read().get | ||
|
|
||
| extension [T](@use fs: Seq[Future[T]^]) | ||
| def awaitAll = fs.awaitAllPoly | ||
|
|
||
| def awaitExplicit[T](@use fs: Seq[Future[T]^]): Unit = | ||
| awaitAllPoly[T, CapSet^{fs*}](fs) |