Skip to content
Merged
Show file tree
Hide file tree
Changes from 6 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion compiler/src/dotty/tools/dotc/ast/untpd.scala
Original file line number Diff line number Diff line change
Expand Up @@ -521,14 +521,17 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
def scalaUnit(implicit src: SourceFile): Select = scalaDot(tpnme.Unit)
def scalaAny(implicit src: SourceFile): Select = scalaDot(tpnme.Any)

def capsInternalDot(name: Name)(using SourceFile): Select =
Select(Select(scalaDot(nme.caps), nme.internal), name)

def captureRoot(using Context): Select =
Select(scalaDot(nme.caps), nme.CAPTURE_ROOT)

def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated =
Annotated(parent, New(scalaAnnotationDot(annotName), List(refs)))

def makeCapsOf(tp: RefTree)(using Context): Tree =
TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
TypeApply(capsInternalDot(nme.capsOf), tp :: Nil)

// Capture set variable `[C^]` becomes: `[C >: CapSet <: CapSet^{cap}]`
def makeCapsBound()(using Context): TypeBoundsTree =
Expand Down
22 changes: 14 additions & 8 deletions compiler/src/dotty/tools/dotc/core/Definitions.scala
Original file line number Diff line number Diff line change
Expand Up @@ -993,18 +993,20 @@ class Definitions {
@tu lazy val LabelClass: Symbol = requiredClass("scala.util.boundary.Label")
@tu lazy val BreakClass: Symbol = requiredClass("scala.util.boundary.Break")

@tu lazy val CapsModule: Symbol = requiredModule("scala.caps")
@tu lazy val CapsModule: Symbol = requiredPackage("scala.caps")
@tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap")
@tu lazy val Caps_Capability: ClassSymbol = requiredClass("scala.caps.Capability")
@tu lazy val Caps_CapSet: ClassSymbol = requiredClass("scala.caps.CapSet")
@tu lazy val Caps_reachCapability: TermSymbol = CapsModule.requiredMethod("reachCapability")
@tu lazy val Caps_readOnlyCapability: TermSymbol = CapsModule.requiredMethod("readOnlyCapability")
@tu lazy val Caps_capsOf: TermSymbol = CapsModule.requiredMethod("capsOf")
@tu lazy val CapsInternalModule: Symbol = requiredModule("scala.caps.internal")
@tu lazy val Caps_reachCapability: TermSymbol = CapsInternalModule.requiredMethod("reachCapability")
@tu lazy val Caps_readOnlyCapability: TermSymbol = CapsInternalModule.requiredMethod("readOnlyCapability")
@tu lazy val Caps_capsOf: TermSymbol = CapsInternalModule.requiredMethod("capsOf")
@tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
@tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure")
@tu lazy val Caps_unsafeAssumeSeparate: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumeSeparate")
@tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
@tu lazy val Caps_containsImpl: TermSymbol = CapsModule.requiredMethod("containsImpl")
@tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains")
@tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl")
@tu lazy val Caps_Mutable: ClassSymbol = requiredClass("scala.caps.Mutable")
@tu lazy val Caps_SharedCapability: ClassSymbol = requiredClass("scala.caps.SharedCapability")

Expand Down Expand Up @@ -1066,10 +1068,10 @@ class Definitions {
@tu lazy val UncheckedStableAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedStable")
@tu lazy val UncheckedVarianceAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedVariance")
@tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
@tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.untrackedCaptures")
@tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.unsafe.untrackedCaptures")
@tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use")
@tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.consume")
@tu lazy val RefineOverrideAnnot: ClassSymbol = requiredClass("scala.caps.refineOverride")
@tu lazy val RefineOverrideAnnot: ClassSymbol = requiredClass("scala.caps.internal.refineOverride")
@tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
@tu lazy val LanguageFeatureMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.languageFeature")
@tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter")
Expand All @@ -1085,7 +1087,7 @@ class Definitions {
@tu lazy val TargetNameAnnot: ClassSymbol = requiredClass("scala.annotation.targetName")
@tu lazy val VarargsAnnot: ClassSymbol = requiredClass("scala.annotation.varargs")
@tu lazy val ReachCapabilityAnnot = requiredClass("scala.annotation.internal.reachCapability")
@tu lazy val RootCapabilityAnnot = requiredClass("scala.caps.rootCapability")
@tu lazy val RootCapabilityAnnot = requiredClass("scala.caps.internal.rootCapability")
@tu lazy val ReadOnlyCapabilityAnnot = requiredClass("scala.annotation.internal.readOnlyCapability")
@tu lazy val RequiresCapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.internal.requiresCapability")
@tu lazy val RetainsAnnot: ClassSymbol = requiredClass("scala.annotation.retains")
Expand Down Expand Up @@ -2097,6 +2099,10 @@ class Definitions {
@tu lazy val ccExperimental: Set[Symbol] = Set(
CapsModule, CapsModule.moduleClass, PureClass,
RequiresCapabilityAnnot,
captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, UseAnnot,
Caps_Mutable, Caps_SharedCapability, ConsumeAnnot,
CapsUnsafeModule, CapsUnsafeModule.moduleClass,
CapsInternalModule, CapsInternalModule.moduleClass,
RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot)

/** Experimental language features defined in `scala.runtime.stdLibPatches.language.experimental`.
Expand Down
114 changes: 0 additions & 114 deletions library/src/scala/caps.scala

This file was deleted.

155 changes: 155 additions & 0 deletions library/src/scala/caps/package.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,155 @@
package scala
package caps

import annotation.{experimental, compileTimeOnly, retainsCap}

/**
* Base trait for classes that represent capabilities in the
* [object-capability model](https://en.wikipedia.org/wiki/Object-capability_model).
*
* A capability is a value representing a permission, access right, resource or effect.
* Capabilities are typically passed to code as parameters; they should not be global objects.
* Often, they come with access restrictions such as scoped lifetimes or limited sharing.
*
* An example is the [[scala.util.boundary.Label Label]] class in [[scala.util.boundary]].
* It represents a capability in the sense that it gives permission to [[scala.util.boundary.break break]]
* to the enclosing boundary represented by the `Label`. It has a scoped lifetime, since breaking to
* a `Label` after the associated `boundary` was exited gives a runtime exception.
*
* [[Capability]] has a formal meaning when
* [[scala.language.experimental.captureChecking Capture Checking]]
* is turned on.
* But even without capture checking, extending this trait can be useful for documenting the intended purpose
* of a class.
*/
trait Capability extends Any

/** The universal capture reference. */
@experimental
val cap: Capability = new Capability() {}

/** The universal capture reference (deprecated) */
@deprecated("Use `cap` instead")
@experimental
val `*`: Capability = cap

@deprecated("Use `Capability` instead")
@experimental
type Cap = Capability

/** Marker trait for classes with methods that requires an exclusive reference. */
@experimental
trait Mutable extends Capability

/** Marker trait for capabilities that can be safely shared in a concurrent context.
* During separation checking, shared capabilities are not taken into account.
*/
@experimental
trait SharedCapability extends Capability

/** Carrier trait for capture set type parameters */
@experimental
trait CapSet extends Any

/** A type constraint expressing that the capture set `C` needs to contain
* the capability `R`
*/
@experimental
sealed trait Contains[+C >: CapSet <: CapSet @retainsCap, R <: Singleton]

@experimental
object Contains:
/** The only implementation of `Contains`. The constraint that `{R} <: C` is
* added separately by the capture checker.
*/
@experimental
given containsImpl[C >: CapSet <: CapSet @retainsCap, R <: Singleton]: Contains[C, R]()

/** An annotation on parameters `x` stating that the method's body makes
* use of the reach capability `x*`. Consequently, when calling the method
* we need to charge the deep capture set of the actual argiment to the
* environment.
*
* Note: This should go into annotations. For now it is here, so that we
* can experiment with it quickly between minor releases
*/
@experimental
final class use extends annotation.StaticAnnotation

/** An annotations on parameters and update methods.
* On a parameter it states that any capabilties passed in the argument
* are no longer available afterwards, unless they are of class `SharableCapabilitty`.
* On an update method, it states that the `this` of the enclosing class is
* consumed, which means that any capabilities of the method prefix are
* no longer available afterwards.
*/
@experimental
final class consume extends annotation.StaticAnnotation

/** A trait that used to allow expressing existential types. Replaced by
* root.Result instances.
*/
@deprecated
sealed trait Exists extends Capability

@experimental
object internal:

/** A wrapper indicating a type variable in a capture argument list of a
* @retains annotation. E.g. `^{x, Y^}` is represented as `@retains(x, capsOf[Y])`.
*/
@compileTimeOnly("Should be be used only internally by the Scala compiler")
def capsOf[CS >: CapSet <: CapSet @retainsCap]: Any = ???

/** Reach capabilities x* which appear as terms in @retains annotations are encoded
* as `caps.reachCapability(x)`. When converted to CaptureRef types in capture sets
* they are represented as `x.type @annotation.internal.reachCapability`.
*/
extension (x: Any) def reachCapability: Any = x

/** Read-only capabilities x.rd which appear as terms in @retains annotations are encoded
* as `caps.readOnlyCapability(x)`. When converted to CaptureRef types in capture sets
* they are represented as `x.type @annotation.internal.readOnlyCapability`.
*/
extension (x: Any) def readOnlyCapability: Any = x

/** An internal annotation placed on a refinement created by capture checking.
* Refinements with this annotation unconditionally override any
* info from the parent type, so no intersection needs to be formed.
* This could be useful for tracked parameters as well.
*/
final class refineOverride extends annotation.StaticAnnotation

/** An annotation used internally for root capability wrappers of `cap` that
* represent either Fresh or Result capabilities.
* A capability is encoded as `caps.cap @rootCapability(...)` where
* `rootCapability(...)` is a special kind of annotation of type `root.Annot`
* that contains either a hidden set for Fresh instances or a method type binder
* for Result instances.
*/
final class rootCapability extends annotation.StaticAnnotation

@experimental
object unsafe:
/**
* Marks the constructor parameter as untracked.
* The capture set of this parameter will not be included in
* the capture set of the constructed object.
*
* @note This should go into annotations. For now it is here, so that we
* can experiment with it quickly between minor releases
*/
final class untrackedCaptures extends annotation.StaticAnnotation

extension [T](x: T)
/** A specific cast operation to remove a capture set.
* If argument is of type `T^C`, assume it is of type `T` instead.
* Calls to this method are treated specially by the capture checker.
*/
def unsafeAssumePure: T = x

/** A wrapper around code for which separation checks are suppressed.
*/
def unsafeAssumeSeparate(op: Any): op.type = op

end unsafe
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/cc-poly-1.check
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-1.scala:12:6 -------------------------------------
12 | f[Any](D()) // error
| ^
| Type argument Any does not conform to upper bound caps.CapSet^
| Type argument Any does not conform to upper bound scala.caps.CapSet^
|
| longer explanation available when compiling with `-explain`
-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/cc-poly-1.scala:13:6 -------------------------------------
13 | f[String](D()) // error
| ^
| Type argument String does not conform to upper bound caps.CapSet^
| Type argument String does not conform to upper bound scala.caps.CapSet^
|
| longer explanation available when compiling with `-explain`
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/cc-this2.check
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
-- Error: tests/neg-custom-args/captures/cc-this2/D_2.scala:3:8 --------------------------------------------------------
3 | this: D^ => // error
| ^^
|reference (caps.cap : caps.Capability) captured by this self type is not included in the allowed capture set {} of pure base class class C
|reference (scala.caps.cap : scala.caps.Capability) captured by this self type is not included in the allowed capture set {} of pure base class class C
-- [E058] Type Mismatch Error: tests/neg-custom-args/captures/cc-this2/D_2.scala:2:6 -----------------------------------
2 |class D extends C: // error
| ^
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/exception-definitions.check
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
-- Error: tests/neg-custom-args/captures/exception-definitions.scala:3:8 -----------------------------------------------
3 | self: Err^ => // error
| ^^^^
|reference (caps.cap : caps.Capability) captured by this self type is not included in the allowed capture set {} of pure base class class Throwable
|reference (scala.caps.cap : scala.caps.Capability) captured by this self type is not included in the allowed capture set {} of pure base class class Throwable
-- Error: tests/neg-custom-args/captures/exception-definitions.scala:7:12 ----------------------------------------------
7 | val x = c // error
| ^
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/i21313.check
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21313.scala:15:12 ---------------------------------------
15 | ac1.await(src2) // error
| ^^^^
| Found: (src2 : Source[Int, caps.CapSet^{ac2}]^?)
| Required: Source[Int, caps.CapSet^{ac1}]^
| Found: (src2 : Source[Int, scala.caps.CapSet^{ac2}]^?)
| Required: Source[Int, scala.caps.CapSet^{ac1}]^
|
| longer explanation available when compiling with `-explain`
3 changes: 2 additions & 1 deletion tests/pos-custom-args/captures/untracked-captures.scala
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
import caps.untrackedCaptures
import caps.unsafe.untrackedCaptures

class LL[+A] private (@untrackedCaptures lazyState: () => LL.State[A]^):
private val res = lazyState()

Expand Down
Loading