@@ -136,6 +136,8 @@ extension (tree: Tree)
136136 def toCaptureRefs (using Context ): List [CaptureRef ] = tree match
137137 case ReachCapabilityApply (arg) =>
138138 arg.toCaptureRefs.map(_.reach)
139+ case ReadOnlyCapabilityApply (arg) =>
140+ arg.toCaptureRefs.map(_.readOnly)
139141 case CapsOfApply (arg) =>
140142 arg.toCaptureRefs
141143 case _ => tree.tpe.dealiasKeepAnnots match
@@ -184,7 +186,7 @@ extension (tp: Type)
184186 case tp : TermRef =>
185187 ((tp.prefix eq NoPrefix )
186188 || tp.symbol.isField && ! tp.symbol.isStatic && tp.prefix.isTrackableRef
187- || tp.isRootCapability
189+ || tp.isCap
188190 ) && ! tp.symbol.isOneOf(UnstableValueFlags )
189191 case tp : TypeRef =>
190192 tp.symbol.isType && tp.derivesFrom(defn.Caps_CapSet )
@@ -193,6 +195,7 @@ extension (tp: Type)
193195 case AnnotatedType (parent, annot) =>
194196 (annot.symbol == defn.ReachCapabilityAnnot
195197 || annot.symbol == defn.MaybeCapabilityAnnot
198+ || annot.symbol == defn.ReadOnlyCapabilityAnnot
196199 ) && parent.isTrackableRef
197200 case _ =>
198201 false
@@ -222,6 +225,8 @@ extension (tp: Type)
222225 else tp match
223226 case tp @ ReachCapability (_) =>
224227 tp.singletonCaptureSet
228+ case ReadOnlyCapability (ref) =>
229+ ref.deepCaptureSet(includeTypevars)
225230 case tp : SingletonCaptureRef if tp.isTrackableRef =>
226231 tp.reach.singletonCaptureSet
227232 case _ =>
@@ -345,7 +350,8 @@ extension (tp: Type)
345350 def forceBoxStatus (boxed : Boolean )(using Context ): Type = tp.widenDealias match
346351 case tp @ CapturingType (parent, refs) if tp.isBoxed != boxed =>
347352 val refs1 = tp match
348- case ref : CaptureRef if ref.isTracked || ref.isReach => ref.singletonCaptureSet
353+ case ref : CaptureRef if ref.isTracked || ref.isReach || ref.isReadOnly =>
354+ ref.singletonCaptureSet
349355 case _ => refs
350356 CapturingType (parent, refs1, boxed)
351357 case _ =>
@@ -379,23 +385,32 @@ extension (tp: Type)
379385 case _ =>
380386 false
381387
388+ /** Is this a type extending `Mutable` that has update methods? */
389+ def isMutableType (using Context ): Boolean =
390+ tp.derivesFrom(defn.Caps_Mutable )
391+ && tp.membersBasedOnFlags(Mutable | Method , EmptyFlags )
392+ .exists(_.hasAltWith(_.symbol.isUpdateMethod))
393+
382394 /** Tests whether the type derives from `caps.Capability`, which means
383395 * references of this type are maximal capabilities.
384396 */
385- def derivesFromCapability (using Context ): Boolean = tp.dealias match
397+ def derivesFromCapTrait ( cls : ClassSymbol ) (using Context ): Boolean = tp.dealias match
386398 case tp : (TypeRef | AppliedType ) =>
387399 val sym = tp.typeSymbol
388- if sym.isClass then sym.derivesFrom(defn. Caps_Capability )
389- else tp.superType.derivesFromCapability
400+ if sym.isClass then sym.derivesFrom(cls )
401+ else tp.superType.derivesFromCapTrait(cls)
390402 case tp : (TypeProxy & ValueType ) =>
391- tp.superType.derivesFromCapability
403+ tp.superType.derivesFromCapTrait(cls)
392404 case tp : AndType =>
393- tp.tp1.derivesFromCapability || tp.tp2.derivesFromCapability
405+ tp.tp1.derivesFromCapTrait(cls) || tp.tp2.derivesFromCapTrait(cls)
394406 case tp : OrType =>
395- tp.tp1.derivesFromCapability && tp.tp2.derivesFromCapability
407+ tp.tp1.derivesFromCapTrait(cls) && tp.tp2.derivesFromCapTrait(cls)
396408 case _ =>
397409 false
398410
411+ def derivesFromCapability (using Context ): Boolean = derivesFromCapTrait(defn.Caps_Capability )
412+ def derivesFromMutable (using Context ): Boolean = derivesFromCapTrait(defn.Caps_Mutable )
413+
399414 /** Drop @retains annotations everywhere */
400415 def dropAllRetains (using Context ): Type = // TODO we should drop retains from inferred types before unpickling
401416 val tm = new TypeMap :
@@ -406,17 +421,6 @@ extension (tp: Type)
406421 mapOver(t)
407422 tm(tp)
408423
409- /** If `x` is a capture ref, its reach capability `x*`, represented internally
410- * as `x @reachCapability`. `x*` stands for all capabilities reachable through `x`".
411- * We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x`
412- * is the union of all capture sets that appear in covariant position in the
413- * type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
414- * are unrelated.
415- */
416- def reach (using Context ): CaptureRef = tp match
417- case tp : CaptureRef if tp.isTrackableRef =>
418- if tp.isReach then tp else ReachCapability (tp)
419-
420424 /** If `x` is a capture ref, its maybe capability `x?`, represented internally
421425 * as `x @maybeCapability`. `x?` stands for a capability `x` that might or might
422426 * not be part of a capture set. We have `{} <: {x?} <: {x}`. Maybe capabilities
@@ -436,52 +440,54 @@ extension (tp: Type)
436440 * but it has fewer issues with type inference.
437441 */
438442 def maybe (using Context ): CaptureRef = tp match
439- case tp : CaptureRef if tp.isTrackableRef =>
440- if tp.isMaybe then tp else MaybeCapability (tp)
443+ case tp @ AnnotatedType (_, annot) if annot.symbol == defn. MaybeCapabilityAnnot => tp
444+ case _ => MaybeCapability (tp)
441445
442- /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a
443- * universal capture set, replace all these occurrences by `{ref*}`. This implements
444- * the new aspect of the (Var) rule, which can now be stated as follows:
445- *
446- * x: T in E
447- * -----------
448- * E |- x: T'
449- *
450- * where T' is T with (1) the toplevel capture set replaced by `{x}` and
451- * (2) all covariant occurrences of cap replaced by `x*`, provided there
452- * are no occurrences in `T` at other variances. (1) is standard, whereas
453- * (2) is new.
454- *
455- * For (2), multiple-flipped covariant occurrences of cap won't be replaced.
456- * In other words,
457- *
458- * - For xs: List[File^] ==> List[File^{xs*}], the cap is replaced;
459- * - while f: [R] -> (op: File^ => R) -> R remains unchanged.
460- *
461- * Without this restriction, the signature of functions like withFile:
462- *
463- * (path: String) -> [R] -> (op: File^ => R) -> R
464- *
465- * could be refined to
466- *
467- * (path: String) -> [R] -> (op: File^{withFile*} => R) -> R
468- *
469- * which is clearly unsound.
470- *
471- * Why is this sound? Covariant occurrences of cap must represent capabilities
472- * that are reachable from `x`, so they are included in the meaning of `{x*}`.
473- * At the same time, encapsulation is still maintained since no covariant
474- * occurrences of cap are allowed in instance types of type variables.
446+ /** If `x` is a capture ref, its reach capability `x*`, represented internally
447+ * as `x @reachCapability`. `x*` stands for all capabilities reachable through `x`".
448+ * We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x`
449+ * is the union of all capture sets that appear in covariant position in the
450+ * type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
451+ * are unrelated.
452+ */
453+ def reach (using Context ): CaptureRef = tp match
454+ case tp @ AnnotatedType (tp1 : CaptureRef , annot)
455+ if annot.symbol == defn.MaybeCapabilityAnnot =>
456+ tp.derivedAnnotatedType(tp1.reach, annot)
457+ case tp @ AnnotatedType (tp1 : CaptureRef , annot)
458+ if annot.symbol == defn.ReachCapabilityAnnot =>
459+ tp
460+ case _ =>
461+ ReachCapability (tp)
462+
463+ /** If `x` is a capture ref, its read-only capability `x.rd`, represented internally
464+ * as `x @readOnlyCapability`. We have {x.rd} <: {x}. If `x` is a reach capability `y*`,
465+ * then its read-only version is `x.rd*`.
466+ */
467+ def readOnly (using Context ): CaptureRef = tp match
468+ case tp @ AnnotatedType (tp1 : CaptureRef , annot)
469+ if annot.symbol == defn.MaybeCapabilityAnnot
470+ || annot.symbol == defn.ReachCapabilityAnnot =>
471+ tp.derivedAnnotatedType(tp1.readOnly, annot)
472+ case tp @ AnnotatedType (tp1 : CaptureRef , annot)
473+ if annot.symbol == defn.ReadOnlyCapabilityAnnot =>
474+ tp
475+ case _ =>
476+ ReadOnlyCapability (tp)
477+
478+ /** If `x` is a capture ref, replacxe all no-flip covariant occurrences of `cap`
479+ * in type `tp` with `x*`.
475480 */
476481 def withReachCaptures (ref : Type )(using Context ): Type =
477482 object narrowCaps extends TypeMap :
478483 var change = false
479484 def apply (t : Type ) =
480485 if variance <= 0 then t
481486 else t.dealiasKeepAnnots match
482- case t @ CapturingType (p, cs) if cs.isUniversal =>
487+ case t @ CapturingType (p, cs) if cs.containsRootCapability =>
483488 change = true
484- t.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
489+ val reachRef = if cs.isReadOnly then ref.reach.readOnly else ref.reach
490+ t.derivedCapturingType(apply(p), reachRef.singletonCaptureSet)
485491 case t @ AnnotatedType (parent, ann) =>
486492 // Don't map annotations, which includes capture sets
487493 t.derivedAnnotatedType(this (parent), ann)
@@ -615,6 +621,16 @@ extension (sym: Symbol)
615621 case c : TypeRef => c.symbol == sym
616622 case _ => false
617623
624+ def isUpdateMethod (using Context ): Boolean =
625+ sym.isAllOf(Mutable | Method , butNot = Accessor )
626+
627+ def isReadOnlyMethod (using Context ): Boolean =
628+ sym.is(Method , butNot = Mutable | Accessor ) && sym.owner.derivesFrom(defn.Caps_Mutable )
629+
630+ def isInReadOnlyMethod (using Context ): Boolean =
631+ if sym.is(Method ) && sym.owner.isClass then isReadOnlyMethod
632+ else sym.owner.isInReadOnlyMethod
633+
618634extension (tp : AnnotatedType )
619635 /** Is this a boxed capturing type? */
620636 def isBoxed (using Context ): Boolean = tp.annot match
@@ -650,6 +666,14 @@ object ReachCapabilityApply:
650666 case Apply (reach, arg :: Nil ) if reach.symbol == defn.Caps_reachCapability => Some (arg)
651667 case _ => None
652668
669+ /** An extractor for `caps.readOnlyCapability(ref)`, which is used to express a read-only
670+ * capability as a tree in a @retains annotation.
671+ */
672+ object ReadOnlyCapabilityApply :
673+ def unapply (tree : Apply )(using Context ): Option [Tree ] = tree match
674+ case Apply (ro, arg :: Nil ) if ro.symbol == defn.Caps_readOnlyCapability => Some (arg)
675+ case _ => None
676+
653677/** An extractor for `caps.capsOf[X]`, which is used to express a generic capture set
654678 * as a tree in a @retains annotation.
655679 */
@@ -658,22 +682,35 @@ object CapsOfApply:
658682 case TypeApply (capsOf, arg :: Nil ) if capsOf.symbol == defn.Caps_capsOf => Some (arg)
659683 case _ => None
660684
661- class AnnotatedCapability (annot : Context ?=> ClassSymbol ):
662- def apply (tp : Type )(using Context ) =
685+ abstract class AnnotatedCapability (annot : Context ?=> ClassSymbol ):
686+ def apply (tp : Type )(using Context ): AnnotatedType =
687+ assert(tp.isTrackableRef)
688+ tp match
689+ case AnnotatedType (_, annot) => assert(! unwrappable.contains(annot.symbol))
690+ case _ =>
663691 AnnotatedType (tp, Annotation (annot, util.Spans .NoSpan ))
664692 def unapply (tree : AnnotatedType )(using Context ): Option [CaptureRef ] = tree match
665693 case AnnotatedType (parent : CaptureRef , ann) if ann.symbol == annot => Some (parent)
666694 case _ => None
667-
668- /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
669- * the reach capability `ref*` as a type.
670- */
671- object ReachCapability extends AnnotatedCapability (defn.ReachCapabilityAnnot )
695+ protected def unwrappable (using Context ): Set [Symbol ]
672696
673697/** An extractor for `ref @maybeCapability`, which is used to express
674698 * the maybe capability `ref?` as a type.
675699 */
676- object MaybeCapability extends AnnotatedCapability (defn.MaybeCapabilityAnnot )
700+ object MaybeCapability extends AnnotatedCapability (defn.MaybeCapabilityAnnot ):
701+ protected def unwrappable (using Context ) = Set ()
702+
703+ /** An extractor for `ref @readOnlyCapability`, which is used to express
704+ * the rad-only capability `ref.rd` as a type.
705+ */
706+ object ReadOnlyCapability extends AnnotatedCapability (defn.ReadOnlyCapabilityAnnot ):
707+ protected def unwrappable (using Context ) = Set (defn.MaybeCapabilityAnnot )
708+
709+ /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
710+ * the reach capability `ref*` as a type.
711+ */
712+ object ReachCapability extends AnnotatedCapability (defn.ReachCapabilityAnnot ):
713+ protected def unwrappable (using Context ) = Set (defn.MaybeCapabilityAnnot , defn.ReadOnlyCapabilityAnnot )
677714
678715/** Offers utility method to be used for type maps that follow aliases */
679716trait ConservativeFollowAliasMap (using Context ) extends TypeMap :
0 commit comments