Reorganize CC docs

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

@@ -703,14 +703,6 @@ object Capabilities:
       (this eq y)
       || this.match
         case x: FreshCap =>
-          def levelOK =
-            if ccConfig.useFreshLevels && !CCState.collapseFresh then
-              val yOwner = y.levelOwner
-              yOwner.isStaticOwner || x.ccOwner.isContainedIn(yOwner)
-            else y.core match
-              case ResultCap(_) | _: ParamRef => false
-              case _ => true
-
           vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y)))
           || x.acceptsLevelOf(y)
               && ( y.tryClassifyAs(x.hiddenSet.classifier)
@@ -788,6 +780,9 @@ object Capabilities:
           case _: Maybe => MaybeCapability(c1)
           case _ => c1
 
+    def showAsCapability(using Context) =
+      i"capability ${ctx.printer.toTextCapability(this).show}"
+
     def toText(printer: Printer): Text = printer.toTextCapability(this)
   end Capability
 

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

@@ -20,6 +20,8 @@ import CCState.*
 import TypeOps.AvoidMap
 import compiletime.uninitialized
 import Capabilities.*
+import Names.Name
+import NameKinds.CapsetName
 
 /** A class for capture sets. Capture sets can be constants or variables.
  *  Capture sets support inclusion constraints <:< where <:< is subcapturing.
@@ -738,6 +740,17 @@ object CaptureSet:
 
     var description: String = ""
 
+    private var myRepr: Name | Null = null
+
+    /** A represtentation of this capture set as a unique name. We print
+     *  empty capture set variables in this representation. Bimapped sets have
+     *  the representation of their source set.
+     */
+    def repr(using Context): Name = {
+      if (myRepr == null) myRepr = CapsetName.fresh()
+      myRepr.nn
+    }
+
     /** Check that all maps recorded in skippedMaps map `elem` to itself
      *  or something subsumed by it.
      */
@@ -1028,6 +1041,7 @@ object CaptureSet:
     override def isMaybeSet: Boolean = bimap.isInstanceOf[MaybeMap]
     override def toString = s"BiMapped$id($source, elems = $elems)"
     override def summarize = bimap.getClass.toString
+    override def repr(using Context): Name = source.repr
   end BiMapped
 
   /** A variable with elements given at any time as { x <- source.elems | p(x) } */
@@ -1300,24 +1314,23 @@ object CaptureSet:
         case cs: Var =>
           if !cs.levelOK(elem) then
             val levelStr = elem match
-              case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}"
-              case _ => ""
-            i"""capability ${elem}$levelStr
-                |cannot be included in outer capture set $cs"""
+              case ref: TermRef => i", defined in ${ref.symbol.maybeOwner}\n"
+              case _ => " "
+            i"""${elem.showAsCapability}${levelStr}cannot be included in outer capture set $cs"""
           else if !elem.tryClassifyAs(cs.classifier) then
-            i"""capability ${elem} is not classified as ${cs.classifier}, therefore it
+            i"""${elem.showAsCapability} is not classified as ${cs.classifier}, therefore it
                 |cannot be included in capture set $cs of ${cs.classifier.name} elements"""
           else if cs.isBadRoot(elem) then
             elem match
               case elem: FreshCap =>
-                i"""local capability $elem created in ${elem.ccOwner}
+                i"""local ${elem.showAsCapability} created in ${elem.ccOwner}
                   |cannot be included in outer capture set $cs"""
               case _ =>
-                i"universal capability $elem cannot be included in capture set $cs"
+                i"universal ${elem.showAsCapability} cannot be included in capture set $cs"
           else
-            i"capability $elem cannot be included in capture set $cs"
+            i"${elem.showAsCapability} cannot be included in capture set $cs"
         case _ =>
-          i"capability $elem is not included in capture set $cs$why"
+          i"${elem.showAsCapability} is not included in capture set $cs$why"
 
     override def toText(printer: Printer): Text =
       inContext(printer.printerContext):

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

@@ -328,6 +328,7 @@ object NameKinds {
   val ExceptionBinderName: UniqueNameKind    = new UniqueNameKind("ex")
   val ExistentialBinderName: UniqueNameKind  = new UniqueNameKind("ex$")
   val SkolemName: UniqueNameKind             = new UniqueNameKind("?")
+  val CapsetName: UniqueNameKind             = new UniqueNameKind("'s")
   val SuperArgName: UniqueNameKind           = new UniqueNameKind("$superArg$")
   val DocArtifactName: UniqueNameKind        = new UniqueNameKind("$doc")
   val UniqueInlineName: UniqueNameKind       = new UniqueNameKind("$i")

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

@@ -173,10 +173,11 @@ class PlainPrinter(_ctx: Context) extends Printer {
     else if cs == CaptureSet.Fluid then "<fluid>"
     else
       val core: Text =
-        if !cs.isConst && cs.elems.isEmpty then "?"
-        else "{" ~ Text(cs.processElems(_.toList.map(toTextCapability)), ", ") ~ "}"
+        if !cs.isConst && cs.elems.isEmpty then cs.asVar.repr.show
+        else
+          Str("'").provided(ccVerbose && !cs.isConst)
+           ~ "{" ~ Text(cs.processElems(_.toList.map(toTextCapability)), ", ") ~ "}"
            ~ Str(".reader").provided(ccVerbose && cs.mutability == Mutability.Reader)
-           ~ Str("?").provided(ccVerbose && !cs.isConst)
            ~ Str(s"#${cs.asVar.id}").provided(showUniqueIds && !cs.isConst)
       core ~ cs.optionalInfo
 
@@ -243,8 +244,6 @@ class PlainPrinter(_ctx: Context) extends Printer {
           selectionString(tp)
         else
           toTextPrefixOf(tp) ~ selectionString(tp)
-      case tp: TermParamRef =>
-        ParamRefNameString(tp) ~ hashStr(tp.binder) ~ ".type"
       case tp: TypeParamRef =>
         val suffix =
           if showNestingLevel then

docs/_docs/internals/exclusive-capabilities.md

@@ -6,21 +6,19 @@ Language design draft
 ## Capability Kinds
 
 A capability is called
-  - _exclusive_ if it is `cap` or it has an exclusive capability in its capture set.
-  - _shared_ otherwise.
-
-There is a new top capability `shared` which can be used as a capability for deriving shared capture sets. Other shared capabilities are created as read-only versions of exclusive capabilities.
+  - _shared_ if it is classified as a `SharedCapability`
+  - _exclusive_ otherwise.
 
 ## Update Methods
 
 We introduce a new trait
 ```scala
-trait Mutable
+trait Mutable extends ExclusiveCapability, Classifier
 ```
 It is used as a base trait for types that define _update methods_ using
 a new soft modifier `update`.
 
-`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are  defined locally or passed to it in parameters.
+`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters.
 
 **Example:**
 ```scala
@@ -115,11 +113,6 @@ a method that accesses exclusive capabilities.
 
 If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated, shared _read-only_ capability.
 
-`shared` can be understood as the read-only capability corresponding to `cap`.
-```scala
-  shared = cap.rd
-```
-
 A _top capability_ is either `cap` or `shared`.
 
 
@@ -134,7 +127,7 @@ The meaning of `^` and `=>` is the same as before:
 
 **Implicitly added capture sets**
 
-A reference to a type extending any of the traits `Capability` or `Mutable` gets an implicit capture set `{shared}` in case no explicit capture set is given.
+A reference to a type extending trait `Mutable` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given.
 
 For instance, a matrix multiplication method can be expressed as follows:
 
@@ -148,7 +141,7 @@ def mul(a: Matrix, b: Matrix, c: Matrix^): Unit =
 ```
 Here, `a` and `b` are implicitly read-only, and `c`'s type has capture set `cap`. I.e. with explicit capture sets this would read:
 ```scala
-def mul(a: Matrix^{shared}, b: Matrix^{shared}, c: Matrix^{cap}): Unit
+def mul(a: Matrix^{cap.rd}, b: Matrix^{cap.rd}, c: Matrix^{cap}): Unit
 ```
 Separation checking will then make sure that `a` and `b` must be different from `c`.
 
@@ -173,8 +166,6 @@ The read-only function `ro` maps capture sets to read-only capture sets. It is d
  - `ro(x)    =  x` if `x` is shared
  - `ro(x)    =  x.rd` if `x` is exclusive
 
-
-
 ## Subcapturing
 
 Subcapturing has to take the mode of capture sets into account. We let `m` stand for arbitrary modes.
@@ -271,7 +262,7 @@ A reference `p.m` to an update method or class `m` of a mutable type is allowed
 
 If `e` is an expression of a type `T^cs` extending `Mutable` and the expected type is a value type that is not a mutable type, then the type of `e` is mapped to `T^ro(cs)`.
 
-
+<!--
 ## Expression Typing
 
 An expression's type should never contain a top capability in its deep capture set. This is achieved by the following rules:
@@ -302,7 +293,6 @@ An expression's type should never contain a top capability in its deep capture s
    where the capture set of `x` contains a top capability,
    replace `x` by a fresh skolem `val sk: T`. Alternatively: keep it as is, but don't widen it.
 
-
 ## Post Processing Right Hand Sides
 
 The type of the right hand sides of `val`s or `def`s is post-processed before it becomes the inferred type or is compared with the declared type. Post processing
@@ -340,7 +330,7 @@ Since expression types can't mention cap, widening happens only
 
 **Definitions:**
 
- - The _transitive capture set_ `tcs(c)` of a capability `c` with underlying capture set `C` is `c` itself, plus the transitive capture set of `C`, but excluding `cap` or `shared`.
+ - The _transitive capture set_ `tcs(c)` of a capability `c` with underlying capture set `C` is `c` itself, plus the transitive capture set of `C`.
 
  - The _transitive capture set_ `tcs(C)` of a capture set C is the union
    of `tcs(c)` for all elements `c` of `C`.
@@ -356,7 +346,9 @@ Since expression types can't mention cap, widening happens only
 
 **Algorithm outline:**
 
- - Associate _shadowed sets_ with blocks, template statement sequences, applications, and val symbols. The idea is that a shadowed set gets populated when a capture reference is widened to cap. In that case the original references that were widened get added to the set.
+
+
+ Associate _shadowed sets_ with blocks, template statement sequences, applications, and val symbols. The idea is that a shadowed set gets populated when a capture reference is widened to cap. In that case the original references that were widened get added to the set.
 
  - After processing a `val x: T2 = t` with `t: T1` after post-processing:
 

docs/_docs/reference/experimental/cc-advanced.md → docs/_docs/reference/experimental/capture-checking/advanced.md

@@ -1,9 +1,10 @@
 ---
 layout: doc-page
-title: "Capture Checking -- Advanced Use Cases"
-nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/cc-advanced.html
+title: "Capability Polymorphism"
+nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/advanced.html
 ---
 
+Advanced use cases.
 
 ## Access Control
 Analogously to type parameters, we can lower- and upper-bound capability parameters where the bounds consist of concrete capture sets:
@@ -75,4 +76,4 @@ By leveraging capability polymorphism, capability members, and path-dependent ca
 * `Label`s store the free capabilities `C` of the `block` passed to `boundary` in their capability member `Fv`.
 * When suspending on a given label, the suspension handler can capture at most the capabilities that occur freely at the `boundary` that introduced the label. That prevents mentioning nested bound labels.
 
-[Back to Capture Checking](cc.md)
+[Back to Capability Polymorphism](polymorphism.md)