Represent read-only with a classifier

`x.rd` is now a shorthand for `x.only[caps.Read]`.

Author: odersky

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

@@ -91,33 +91,33 @@ object Capabilities:
    */
   case class Maybe(underlying: Capability) extends DerivedCapability
 
-  /** The readonly capability `x.rd`. We have {x.rd} <: {x}.
-   *
-   *  Read-only capabilities cannot wrap maybe capabilities
-   *  but they can wrap reach capabilities. We have
-   *      (x?).readOnly = (x.rd)?
-   */
-  case class ReadOnly(underlying: ObjectCapability | RootCapability | Reach | Restricted)
-  extends DerivedCapability
-
   /** The restricted capability `x.only[C]`. We have {x.only[C]} <: {x}.
    *
-   *  Restricted capabilities cannot wrap maybe capabilities or read-only capabilities
+   *  Restricted capabilities cannot wrap maybe capabilities
    *  but they can wrap reach capabilities. We have
    *      (x?).restrict[T] = (x.restrict[T])?
    *      (x.rd).restrict[T] = (x.restrict[T]).rd
    */
-  case class Restricted(underlying: ObjectCapability | RootCapability | Reach, cls: ClassSymbol)
+  case class Restricted(underlying: CoreCapability | RootCapability | Reach, cls: ClassSymbol)
   extends DerivedCapability
 
+  /** An extractor for the read-only capability `x.rd`. `x.rd` is represented as
+   *  `c.only[caps.Read]`.
+   */
+  object ReadOnly:
+    def apply(underlying: CoreCapability | RootCapability | Reach | Restricted)(using Context): Restricted =
+      Restricted(underlying.stripRestricted.asInstanceOf, defn.Caps_Read)
+    def unapply(ref: Restricted)(using Context): Option[CoreCapability | RootCapability | Reach] =
+      if ref.cls == defn.Caps_Read then Some(ref.underlying) else None
+
   /** If `x` is a capability, its reach capability `x*`. `x*` stands for all
    *  capabilities reachable through `x`.
    *  We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x`
    *  is the union of all capture sets that appear in covariant position in the
    *  type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
    *  are unrelated.
    *
-   *  Reach capabilities cannot wrap read-only capabilities or maybe capabilities.
+   *  Reach capabilities cannot wrap restricted capabilities or maybe capabilities.
    *  We have
    *      (x?).reach        = (x.reach)?
    *      (x.rd).reach      = (x.reach).rd
@@ -133,7 +133,7 @@ object Capabilities:
   object GlobalCap extends RootCapability:
     def descr(using Context) = "the universal root capability"
     override val maybe = Maybe(this)
-    override val readOnly = ReadOnly(this)
+    override def readOnly(using Context) = ReadOnly(this)
     override def restrict(cls: ClassSymbol)(using Context) = Restricted(this, cls)
     override def reach = unsupported("cap.reach")
     override def singletonCaptureSet(using Context) = CaptureSet.universal
@@ -347,23 +347,21 @@ object Capabilities:
       case self: Maybe => self
       case _ => cached(Maybe(this))
 
-    def readOnly: ReadOnly | Maybe = this match
+    def readOnly(using Context): Restricted | Maybe = this match
       case Maybe(ref1) => Maybe(ref1.readOnly)
-      case self: ReadOnly => self
-      case self: (ObjectCapability | RootCapability | Reach | Restricted) => cached(ReadOnly(self))
+      case self @ ReadOnly(_) => self
+      case self: (CoreCapability | RootCapability | Reach | Restricted) => cached(ReadOnly(self))
 
-    def restrict(cls: ClassSymbol)(using Context): Restricted | ReadOnly | Maybe = this match
+    def restrict(cls: ClassSymbol)(using Context): Restricted | Maybe = this match
       case Maybe(ref1) => Maybe(ref1.restrict(cls))
-      case ReadOnly(ref1) => ReadOnly(ref1.restrict(cls).asInstanceOf[Restricted])
       case self @ Restricted(ref1, prevCls) =>
         val combinedCls = leastClassifier(prevCls, cls)
         if combinedCls == prevCls then self
         else cached(Restricted(ref1, combinedCls))
-      case self: (ObjectCapability | RootCapability | Reach) => cached(Restricted(self, cls))
+      case self: (CoreCapability | RootCapability | Reach) => cached(Restricted(self, cls))
 
-    def reach: Reach | Restricted | ReadOnly | Maybe = this match
+    def reach: Reach | Restricted | Maybe = this match
       case Maybe(ref1) => Maybe(ref1.reach)
-      case ReadOnly(ref1) => ReadOnly(ref1.reach.asInstanceOf[Reach | Restricted])
       case Restricted(ref1, cls) => Restricted(ref1.reach.asInstanceOf[Reach], cls)
       case self: Reach => self
       case self: ObjectCapability => cached(Reach(self))
@@ -893,7 +891,7 @@ object Capabilities:
       case c: DerivedCapability =>
         val c1 = c.underlying.toType
         c match
-          case _: ReadOnly => ReadOnlyCapability(c1)
+          case ReadOnly(_) => ReadOnlyCapability(c1)
           case Restricted(_, cls) => OnlyCapability(c1, cls)
           case _: Reach => ReachCapability(c1)
           case _: Maybe => MaybeCapability(c1)

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

@@ -94,5 +94,5 @@
 -- Error: tests/neg-custom-args/captures/mutability.scala:45:9 ---------------------------------------------------------
 45 |  r6().x.set(33) // error
    |  ^^^^^^^^^^
-   |  Cannot call update method set of Ref[Int]^{cap.rd}
-   |  since its capture set {cap.rd} is read-only.
+   |  Cannot call update method set of Ref[Int]^{r6*.rd}
+   |  since its capture set {r6*.rd} is read-only.

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

@@ -94,5 +94,5 @@
 -- Error: tests/neg-custom-args/captures/mutvars.scala:44:13 -----------------------------------------------------------
 44 |  r6().x.fld = 33 // error
    |  ^^^^^^^^^^^^^^^
-   |  Cannot assign to field fld of Ref[Int]^{cap.rd}
-   |  since its capture set {cap.rd} is read-only.
+   |  Cannot assign to field fld of Ref[Int]^{r6*.rd}
+   |  since its capture set {r6*.rd} is read-only.