Skip to content

Commit 02b1b6d

Browse files
committed
Implement caps.Contains
1 parent e98b503 commit 02b1b6d

File tree

6 files changed

+75
-4
lines changed

6 files changed

+75
-4
lines changed

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

+23-1
Original file line numberDiff line numberDiff line change
@@ -674,7 +674,29 @@ class CheckCaptures extends Recheck, SymTransformer:
674674
i"Sealed type variable $pname", "be instantiated to",
675675
i"This is often caused by a local capability$where\nleaking as part of its result.",
676676
tree.srcPos)
677-
handleCall(meth, tree, () => Existential.toCap(super.recheckTypeApply(tree, pt)))
677+
val res = handleCall(meth, tree, () => Existential.toCap(super.recheckTypeApply(tree, pt)))
678+
if meth == defn.Caps_containsImpl then checkContains(tree)
679+
res
680+
end recheckTypeApply
681+
682+
/** Faced with a tree of form `caps.contansImpl[CS, r.type]`, check that `R` is a tracked
683+
* capability and assert that `{r} <:CS`.
684+
*/
685+
def checkContains(tree: TypeApply)(using Context): Unit =
686+
tree.fun.knownType.widen match
687+
case fntpe: PolyType =>
688+
tree.args match
689+
case csArg :: refArg :: Nil =>
690+
val cs = csArg.knownType.captureSet
691+
val ref = refArg.knownType
692+
capt.println(i"check contains $cs , $ref")
693+
ref match
694+
case ref: CaptureRef if ref.isTracked =>
695+
checkElem(ref, cs, tree.srcPos)
696+
case _ =>
697+
report.error(em"$refArg is not a tracked capability", refArg.srcPos)
698+
case _ =>
699+
case _ =>
678700

679701
override def recheckBlock(tree: Block, pt: Type)(using Context): Type =
680702
inNestedLevel(super.recheckBlock(tree, pt))

compiler/src/dotty/tools/dotc/core/Definitions.scala

+4-2
Original file line numberDiff line numberDiff line change
@@ -993,15 +993,17 @@ class Definitions {
993993
@tu lazy val CapsModule: Symbol = requiredModule("scala.caps")
994994
@tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap")
995995
@tu lazy val Caps_Capability: TypeSymbol = CapsModule.requiredType("Capability")
996-
@tu lazy val Caps_CapSet = requiredClass("scala.caps.CapSet")
996+
@tu lazy val Caps_CapSet: ClassSymbol = requiredClass("scala.caps.CapSet")
997997
@tu lazy val Caps_reachCapability: TermSymbol = CapsModule.requiredMethod("reachCapability")
998998
@tu lazy val Caps_capsOf: TermSymbol = CapsModule.requiredMethod("capsOf")
999-
@tu lazy val Caps_Exists = requiredClass("scala.caps.Exists")
999+
@tu lazy val Caps_Exists: ClassSymbol = requiredClass("scala.caps.Exists")
10001000
@tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
10011001
@tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure")
10021002
@tu lazy val Caps_unsafeBox: Symbol = CapsUnsafeModule.requiredMethod("unsafeBox")
10031003
@tu lazy val Caps_unsafeUnbox: Symbol = CapsUnsafeModule.requiredMethod("unsafeUnbox")
10041004
@tu lazy val Caps_unsafeBoxFunArg: Symbol = CapsUnsafeModule.requiredMethod("unsafeBoxFunArg")
1005+
@tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Capability")
1006+
@tu lazy val Caps_containsImpl: TermSymbol = CapsModule.requiredMethod("containsImpl")
10051007

10061008
@tu lazy val PureClass: Symbol = requiredClass("scala.Pure")
10071009

library/src/scala/caps.scala

+11-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
package scala
22

3-
import annotation.{experimental, compileTimeOnly}
3+
import annotation.{experimental, compileTimeOnly, retainsCap}
44

55
@experimental object caps:
66

@@ -19,6 +19,16 @@ import annotation.{experimental, compileTimeOnly}
1919
/** Carrier trait for capture set type parameters */
2020
trait CapSet extends Any
2121

22+
/** A type constraint expressing that the capture set `C` needs to contain
23+
* the capability `R`
24+
*/
25+
sealed trait Contains[C <: CapSet @retainsCap, R <: Singleton]
26+
27+
/** The only implementation of `Contains`. The constraint that `{R} <: C` is
28+
* added separately by the capture checker.
29+
*/
30+
given containsImpl[C <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()
31+
2232
@compileTimeOnly("Should be be used only internally by the Scala compiler")
2333
def capsOf[CS]: Any = ???
2434

Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
-- Error: tests/neg-custom-args/captures/i21313.scala:6:27 -------------------------------------------------------------
2+
6 |def foo(x: Async) = x.await(???) // error
3+
| ^
4+
| (x : Async) is not a tracked capability
5+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21313.scala:15:12 ---------------------------------------
6+
15 | ac1.await(src2) // error
7+
| ^^^^
8+
| Found: (src2 : Source[Int, caps.CapSet^{ac2}]^?)
9+
| Required: Source[Int, caps.CapSet^{ac1}]^
10+
|
11+
| longer explanation available when compiling with `-explain`
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
import caps.CapSet
2+
3+
trait Async:
4+
def await[T, Cap^](using caps.Contains[Cap, this.type])(src: Source[T, Cap]^): T
5+
6+
def foo(x: Async) = x.await(???) // error
7+
8+
trait Source[+T, Cap^]:
9+
final def await(using ac: Async^{Cap^}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
10+
11+
def test(using ac1: Async^, ac2: Async^, x: String) =
12+
val src1 = new Source[Int, CapSet^{ac1}] {}
13+
ac1.await(src1) // ok
14+
val src2 = new Source[Int, CapSet^{ac2}] {}
15+
ac1.await(src2) // error
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
import caps.CapSet
2+
3+
trait Async:
4+
def await[T, Cap^](using caps.Contains[Cap, this.type])(src: Source[T, Cap]^): T
5+
6+
trait Source[+T, Cap^]:
7+
final def await(using ac: Async^{Cap^}) = ac.await[T, Cap](this) // Contains[Cap, ac] is assured because {ac} <: Cap.
8+
9+
def test(using ac1: Async^, ac2: Async^, x: String) =
10+
val src1 = new Source[Int, CapSet^{ac1}] {}
11+
ac1.await(src1)

0 commit comments

Comments
 (0)