Make consume a soft modifier

compiler/src/dotty/tools/dotc/ast/untpd.scala

@@ -559,6 +559,9 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
   def makeOnlyAnnot(qid: Tree)(using Context) =
     New(AppliedTypeTree(ref(defn.OnlyCapabilityAnnot.typeRef), qid :: Nil), Nil :: Nil)
 
+  def makeConsumeAnnot()(using Context): Tree =
+    New(ref(defn.ConsumeAnnot.typeRef), Nil :: Nil)
+
   def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
     DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)
 

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

@@ -22,9 +22,9 @@ import Capabilities.*
  *
  *   - Hidden sets of arguments must not be referred to in the same application
  *   - Hidden sets of (result-) types must not be referred to alter in the same scope.
- *   - Returned hidden sets can only refer to @consume parameters.
+ *   - Returned hidden sets can only refer to consume parameters.
  *   - If returned hidden sets refer to an encloding this, the reference must be
- *     from a @consume method.
+ *     from a consume method.
  *   - Consumed entities cannot be used subsequently.
  *   - Entitites cannot be consumed in a loop.
  */
@@ -422,7 +422,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
   def consumeError(ref: Capability, loc: SrcPos, pos: SrcPos)(using Context): Unit =
     report.error(
       em"""Separation failure: Illegal access to $ref, which was passed to a
-          |@consume parameter or was used as a prefix to a @consume method on line ${loc.line + 1}
+          |consume parameter or was used as a prefix to a consume method on line ${loc.line + 1}
           |and therefore is no longer available.""",
       pos)
 
@@ -433,7 +433,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
   def consumeInLoopError(ref: Capability, pos: SrcPos)(using Context): Unit =
     report.error(
       em"""Separation failure: $ref appears in a loop, therefore it cannot
-          |be passed to a @consume parameter or be used as a prefix of a @consume method call.""",
+          |be passed to a consume parameter or be used as a prefix of a consume method call.""",
       pos)
 
   // ------------ Checks -----------------------------------------------------
@@ -587,16 +587,16 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
 
   /** Check validity of consumed references `refsToCheck`. The references are consumed
    *  because they are hidden in a Fresh result type or they are referred
-   *  to in an argument to a @consume parameter or in a prefix of a @consume method --
+   *  to in an argument to a consume parameter or in a prefix of a consume method --
    *  which one applies is determined by the role parameter.
    *
    *  This entails the following checks:
    *   - The reference must be defined in the same as method or class as
    *     the access.
    *   - If the reference is to a term parameter, that parameter must be
-   *     marked as @consume as well.
+   *     marked as consume as well.
    *   - If the reference is to a this type of the enclosing class, the
-   *     access must be in a @consume method.
+   *     access must be in a consume method.
    *
    *  References that extend caps.Sharable are excluded from checking.
    *  As a side effect, add all checked references with the given position `pos`
@@ -631,7 +631,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             then
               report.error(
                 em"""Separation failure: $descr non-local this of class ${ref.cls}.
-                    |The access must be in a @consume method to allow this.""",
+                    |The access must be in a consume method to allow this.""",
                 pos)
           case _ =>
 
@@ -643,7 +643,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       val (pluralS, singleS) = if badParams.tail.isEmpty then ("", "s") else ("s", "")
       report.error(
         em"""Separation failure: $descr parameter$pluralS ${paramsStr(badParams.toList)}.
-            |The parameter$pluralS need$singleS to be annotated with @consume to allow this.""",
+            |The parameter$pluralS need$singleS to be annotated with consume to allow this.""",
           pos)
 
     role match
@@ -769,7 +769,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
 
     /** If `tpe` appears as a (result-) type of a definition, treat its
      *  hidden set minus its explicitly declared footprint as consumed.
-     *  If `tpe` appears as an argument to a @consume parameter, treat
+     *  If `tpe` appears as an argument to a consume parameter, treat
      *  its footprint as consumed.
      */
     def checkLegalRefs() = role match
@@ -786,7 +786,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       case TypeRole.Argument(arg) =>
         if tpe.hasAnnotation(defn.ConsumeAnnot) then
           val capts = captures(arg).footprint
-          checkConsumedRefs(capts, tpe, role, i"argument to @consume parameter with type ${arg.nuType} refers to", pos)
+          checkConsumedRefs(capts, tpe, role, i"argument to consume parameter with type ${arg.nuType} refers to", pos)
       case _ =>
 
     if !tpe.hasAnnotation(defn.UntrackedCapturesAnnot) then
@@ -910,7 +910,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           checkConsumedRefs(
               captures(qual).footprint, qual.nuType,
               TypeRole.Qualifier(qual, tree.symbol),
-              i"call prefix of @consume ${tree.symbol} refers to", qual.srcPos)
+              i"call prefix of consume ${tree.symbol} refers to", qual.srcPos)
         case tree: GenericApply =>
           traverseChildren(tree)
           tree.tpe match

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

@@ -758,8 +758,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
               && !(sym.is(Method) && sym.owner.isClass)
             then
               report.error(
-                em"""@consume cannot be used here. Only member methods and their term parameters
-                    |can have @consume annotations.""",
+                em"""consume cannot be used here. Only member methods and their term parameters
+                    |can have a consume modifier.""",
                 tree.srcPos)
           else if annotCls == defn.UseAnnot then
             if !ccConfig.allowUse then

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

@@ -1076,8 +1076,8 @@ class Definitions {
   @tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
   @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 ReserveAnnot: ClassSymbol = requiredClass("scala.caps.reserve")
+  @tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.internal.consume")
   @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")

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

@@ -454,6 +454,7 @@ object StdNames {
     val compiletime : N         = "compiletime"
     val compose: N              = "compose"
     val conforms_ : N           = "$conforms"
+    val consume: N              = "consume"
     val contents: N             = "contents"
     val copy: N                 = "copy"
     val create: N               = "create"

compiler/src/dotty/tools/dotc/parsing/Parsers.scala

@@ -35,6 +35,7 @@ import config.SourceVersion.*
 import config.SourceVersion
 import dotty.tools.dotc.config.MigrationVersion
 import dotty.tools.dotc.util.chaining.*
+import dotty.tools.dotc.config.Feature.ccEnabled
 
 object Parsers {
 
@@ -216,6 +217,8 @@ object Parsers {
     def isPureArrow: Boolean = isPureArrow(nme.PUREARROW) || isPureArrow(nme.PURECTXARROW)
     def isErased =
       isIdent(nme.erased) && in.erasedEnabled && in.isSoftModifierInParamModifierPosition
+    def isConsume =
+      isIdent(nme.consume) && ccEnabled //\&& in.isSoftModifierInParamModifierPosition
     def isSimpleLiteral =
       simpleLiteralTokens.contains(in.token)
       || isIdent(nme.raw.MINUS) && numericLitTokens.contains(in.lookahead.token)
@@ -3325,11 +3328,15 @@ object Parsers {
     private def addModifier(mods: Modifiers): Modifiers = {
       val tok = in.token
       val name = in.name
-      val mod = atSpan(in.skipToken()) { modOfToken(tok, name) }
-
-      if mods.isOneOf(mod.flags) then
-        syntaxError(RepeatedModifier(mod.flags.flagsString, source, mod.span), mod.span)
-      addMod(mods, mod)
+      if isConsume then
+        val consumeAnnot = atSpan(in.skipToken())(makeConsumeAnnot())
+        mods.withAddedAnnotation(consumeAnnot)
+      else
+        val mod = atSpan(in.skipToken()):
+          modOfToken(tok, name)
+        if mods.isOneOf(mod.flags) then
+          syntaxError(RepeatedModifier(mod.flags.flagsString, source, mod.span), mod.span)
+        addMod(mods, mod)
     }
 
     def addFlag(mods: Modifiers, flag: FlagSet): Modifiers =
@@ -3555,7 +3562,8 @@ object Parsers {
      *  UsingParamClause  ::=  ‘(’ ‘using’ (DefTermParams | ContextTypes) ‘)’
      *  DefImplicitClause ::=  [nl] ‘(’ ‘implicit’ DefTermParams ‘)’
      *  DefTermParams     ::=  DefTermParam {‘,’ DefTermParam}
-     *  DefTermParam      ::=  {Annotation} [‘erased’] [‘inline’] Param
+     *  DefTermParam      ::=  {Annotation} TermParamMods Param
+     *  TermParamMods     ::=  [‘erased‘] [‘inline’] | [‘consume‘]
      *
      *  Param             ::=  id `:' ParamType [`=' Expr]
      *
@@ -3592,7 +3600,7 @@ object Parsers {
       def param(): ValDef = {
         val start = in.offset
         var mods = impliedMods.withAnnotations(annotations())
-        if isErased then
+        if isConsume || isErased then
           mods = addModifier(mods)
         if paramOwner.isClass then
           mods = addFlag(modifiers(start = mods), ParamAccessor)
@@ -3664,6 +3672,7 @@ object Parsers {
                 var mods = EmptyModifiers
                 if in.lookahead.isColon then
                   (mods, true)
+                else if isConsume then (mods, true)
                 else
                   if isErased then mods = addModifier(mods)
                   val paramsAreNamed =

compiler/src/dotty/tools/dotc/parsing/Scanners.scala

@@ -1228,7 +1228,8 @@ object Scanners {
       && (softModifierNames.contains(name)
         || name == nme.erased && erasedEnabled
         || name == nme.tracked && trackedEnabled
-        || name == nme.update && Feature.ccEnabled)
+        || name == nme.update && Feature.ccEnabled
+        || name == nme.consume && Feature.ccEnabled)
 
     def isSoftModifierInModifierPosition: Boolean =
       isSoftModifier && inModifierPosition()

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

@@ -15,7 +15,7 @@ import util.SourcePosition
 import scala.util.control.NonFatal
 import scala.annotation.switch
 import config.{Config, Feature}
-import ast.tpd
+import ast.{tpd, untpd}
 import cc.*
 import CaptureSet.Mutability
 import Capabilities.*
@@ -716,8 +716,12 @@ class PlainPrinter(_ctx: Context) extends Printer {
     case _ => literalText(String.valueOf(const.value))
   }
 
-  /** Usual target for `Annotation#toText`, overridden in RefinedPrinter */
-  def annotText(annot: Annotation): Text = s"@${annot.symbol.name}"
+  /** Usual target for `Annotation#toText`, overridden in RefinedPrinter, which also
+   *  looks at trees.
+   */
+  override def annotText(annot: Annotation): Text = annotText(annot.symbol)
+
+  protected def annotText(sym: Symbol): Text = s"@${sym.name}"
 
   def toText(annot: Annotation): Text = annot.toText(this)
 

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

@@ -1140,6 +1140,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
   /** Textual representation of an instance creation expression without the leading `new` */
   protected def constrText(tree: untpd.Tree): Text = toTextLocal(tree).stripPrefix(keywordStr("new ")) // DD
 
+  override def annotText(annot: Annotation): Text = annotText(annot.symbol, annot.tree)
+
   protected def annotText(sym: Symbol, tree: untpd.Tree): Text =
     def recur(t: untpd.Tree): Text = t match
       case Apply(fn, Nil) => recur(fn)
@@ -1152,9 +1154,12 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case New(tpt) => recur(tpt)
       case _ =>
         val annotSym = sym.orElse(tree.symbol.enclosingClass)
-        s"@${if annotSym.exists then annotSym.name.toString else t.show}"
+        if annotSym.exists then annotText(annotSym) else s"@${t.show}"
     recur(tree)
 
+  protected override def annotText(sym: Symbol): Text =
+    if sym == defn.ConsumeAnnot then "consume" else super.annotText(sym)
+
   protected def modText(mods: untpd.Modifiers, sym: Symbol, kw: String, isType: Boolean): Text = { // DD
     val suppressKw = if (enclDefIsClass) mods.isAllOf(LocalParam) else mods.is(Param)
     var flagMask =
@@ -1175,8 +1180,6 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
     Text(annotTexts, " ") ~~ flagsText ~~ (Str(kw) provided !suppressKw)
   }
 
-  override def annotText(annot: Annotation): Text = annotText(annot.symbol, annot.tree)
-
   def optText(name: Name)(encl: Text => Text): Text =
     if (name.isEmpty) "" else encl(toText(name))
 

compiler/src/dotty/tools/dotc/typer/Namer.scala

@@ -995,6 +995,10 @@ class Namer { typer: Typer =>
       end if
     }
 
+    private def normalizeFlags(denot: SymDenotation)(using Context): Unit =
+      if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot) then
+        denot.setFlag(Mutable)
+
     /** Intentionally left without `using Context` parameter. We need
      *  to pick up the context at the point where the completer was created.
      */
@@ -1004,6 +1008,7 @@ class Namer { typer: Typer =>
       addInlineInfo(sym)
       denot.info = typeSig(sym)
       invalidateIfClashingSynthetic(denot)
+      normalizeFlags(denot)
       Checking.checkWellFormed(sym)
       denot.info = avoidPrivateLeaks(sym)
     }

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: