@@ -136,6 +136,8 @@ extension (tree: Tree)
136
136
def toCaptureRefs (using Context ): List [CaptureRef ] = tree match
137
137
case ReachCapabilityApply (arg) =>
138
138
arg.toCaptureRefs.map(_.reach)
139
+ case ReadOnlyCapabilityApply (arg) =>
140
+ arg.toCaptureRefs.map(_.readOnly)
139
141
case CapsOfApply (arg) =>
140
142
arg.toCaptureRefs
141
143
case _ => tree.tpe.dealiasKeepAnnots match
@@ -184,7 +186,7 @@ extension (tp: Type)
184
186
case tp : TermRef =>
185
187
((tp.prefix eq NoPrefix )
186
188
|| tp.symbol.isField && ! tp.symbol.isStatic && tp.prefix.isTrackableRef
187
- || tp.isRootCapability
189
+ || tp.isCap
188
190
) && ! tp.symbol.isOneOf(UnstableValueFlags )
189
191
case tp : TypeRef =>
190
192
tp.symbol.isType && tp.derivesFrom(defn.Caps_CapSet )
@@ -193,6 +195,7 @@ extension (tp: Type)
193
195
case AnnotatedType (parent, annot) =>
194
196
(annot.symbol == defn.ReachCapabilityAnnot
195
197
|| annot.symbol == defn.MaybeCapabilityAnnot
198
+ || annot.symbol == defn.ReadOnlyCapabilityAnnot
196
199
) && parent.isTrackableRef
197
200
case _ =>
198
201
false
@@ -222,6 +225,8 @@ extension (tp: Type)
222
225
else tp match
223
226
case tp @ ReachCapability (_) =>
224
227
tp.singletonCaptureSet
228
+ case ReadOnlyCapability (ref) =>
229
+ ref.deepCaptureSet(includeTypevars)
225
230
case tp : SingletonCaptureRef if tp.isTrackableRef =>
226
231
tp.reach.singletonCaptureSet
227
232
case _ =>
@@ -345,7 +350,8 @@ extension (tp: Type)
345
350
def forceBoxStatus (boxed : Boolean )(using Context ): Type = tp.widenDealias match
346
351
case tp @ CapturingType (parent, refs) if tp.isBoxed != boxed =>
347
352
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
349
355
case _ => refs
350
356
CapturingType (parent, refs1, boxed)
351
357
case _ =>
@@ -379,23 +385,32 @@ extension (tp: Type)
379
385
case _ =>
380
386
false
381
387
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
+
382
394
/** Tests whether the type derives from `caps.Capability`, which means
383
395
* references of this type are maximal capabilities.
384
396
*/
385
- def derivesFromCapability (using Context ): Boolean = tp.dealias match
397
+ def derivesFromCapTrait ( cls : ClassSymbol ) (using Context ): Boolean = tp.dealias match
386
398
case tp : (TypeRef | AppliedType ) =>
387
399
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)
390
402
case tp : (TypeProxy & ValueType ) =>
391
- tp.superType.derivesFromCapability
403
+ tp.superType.derivesFromCapTrait(cls)
392
404
case tp : AndType =>
393
- tp.tp1.derivesFromCapability || tp.tp2.derivesFromCapability
405
+ tp.tp1.derivesFromCapTrait(cls) || tp.tp2.derivesFromCapTrait(cls)
394
406
case tp : OrType =>
395
- tp.tp1.derivesFromCapability && tp.tp2.derivesFromCapability
407
+ tp.tp1.derivesFromCapTrait(cls) && tp.tp2.derivesFromCapTrait(cls)
396
408
case _ =>
397
409
false
398
410
411
+ def derivesFromCapability (using Context ): Boolean = derivesFromCapTrait(defn.Caps_Capability )
412
+ def derivesFromMutable (using Context ): Boolean = derivesFromCapTrait(defn.Caps_Mutable )
413
+
399
414
/** Drop @retains annotations everywhere */
400
415
def dropAllRetains (using Context ): Type = // TODO we should drop retains from inferred types before unpickling
401
416
val tm = new TypeMap :
@@ -406,17 +421,6 @@ extension (tp: Type)
406
421
mapOver(t)
407
422
tm(tp)
408
423
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
-
420
424
/** If `x` is a capture ref, its maybe capability `x?`, represented internally
421
425
* as `x @maybeCapability`. `x?` stands for a capability `x` that might or might
422
426
* not be part of a capture set. We have `{} <: {x?} <: {x}`. Maybe capabilities
@@ -436,52 +440,54 @@ extension (tp: Type)
436
440
* but it has fewer issues with type inference.
437
441
*/
438
442
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)
441
445
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*`.
475
480
*/
476
481
def withReachCaptures (ref : Type )(using Context ): Type =
477
482
object narrowCaps extends TypeMap :
478
483
var change = false
479
484
def apply (t : Type ) =
480
485
if variance <= 0 then t
481
486
else t.dealiasKeepAnnots match
482
- case t @ CapturingType (p, cs) if cs.isUniversal =>
487
+ case t @ CapturingType (p, cs) if cs.containsRootCapability =>
483
488
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)
485
491
case t @ AnnotatedType (parent, ann) =>
486
492
// Don't map annotations, which includes capture sets
487
493
t.derivedAnnotatedType(this (parent), ann)
@@ -615,6 +621,16 @@ extension (sym: Symbol)
615
621
case c : TypeRef => c.symbol == sym
616
622
case _ => false
617
623
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
+
618
634
extension (tp : AnnotatedType )
619
635
/** Is this a boxed capturing type? */
620
636
def isBoxed (using Context ): Boolean = tp.annot match
@@ -637,6 +653,14 @@ object ReachCapabilityApply:
637
653
case Apply (reach, arg :: Nil ) if reach.symbol == defn.Caps_reachCapability => Some (arg)
638
654
case _ => None
639
655
656
+ /** An extractor for `caps.readOnlyCapability(ref)`, which is used to express a read-only
657
+ * capability as a tree in a @retains annotation.
658
+ */
659
+ object ReadOnlyCapabilityApply :
660
+ def unapply (tree : Apply )(using Context ): Option [Tree ] = tree match
661
+ case Apply (ro, arg :: Nil ) if ro.symbol == defn.Caps_readOnlyCapability => Some (arg)
662
+ case _ => None
663
+
640
664
/** An extractor for `caps.capsOf[X]`, which is used to express a generic capture set
641
665
* as a tree in a @retains annotation.
642
666
*/
@@ -645,22 +669,35 @@ object CapsOfApply:
645
669
case TypeApply (capsOf, arg :: Nil ) if capsOf.symbol == defn.Caps_capsOf => Some (arg)
646
670
case _ => None
647
671
648
- class AnnotatedCapability (annot : Context ?=> ClassSymbol ):
649
- def apply (tp : Type )(using Context ) =
672
+ abstract class AnnotatedCapability (annot : Context ?=> ClassSymbol ):
673
+ def apply (tp : Type )(using Context ): AnnotatedType =
674
+ assert(tp.isTrackableRef)
675
+ tp match
676
+ case AnnotatedType (_, annot) => assert(! unwrappable.contains(annot.symbol))
677
+ case _ =>
650
678
AnnotatedType (tp, Annotation (annot, util.Spans .NoSpan ))
651
679
def unapply (tree : AnnotatedType )(using Context ): Option [CaptureRef ] = tree match
652
680
case AnnotatedType (parent : CaptureRef , ann) if ann.symbol == annot => Some (parent)
653
681
case _ => None
654
-
655
- /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
656
- * the reach capability `ref*` as a type.
657
- */
658
- object ReachCapability extends AnnotatedCapability (defn.ReachCapabilityAnnot )
682
+ protected def unwrappable (using Context ): Set [Symbol ]
659
683
660
684
/** An extractor for `ref @maybeCapability`, which is used to express
661
685
* the maybe capability `ref?` as a type.
662
686
*/
663
- object MaybeCapability extends AnnotatedCapability (defn.MaybeCapabilityAnnot )
687
+ object MaybeCapability extends AnnotatedCapability (defn.MaybeCapabilityAnnot ):
688
+ protected def unwrappable (using Context ) = Set ()
689
+
690
+ /** An extractor for `ref @readOnlyCapability`, which is used to express
691
+ * the rad-only capability `ref.rd` as a type.
692
+ */
693
+ object ReadOnlyCapability extends AnnotatedCapability (defn.ReadOnlyCapabilityAnnot ):
694
+ protected def unwrappable (using Context ) = Set (defn.MaybeCapabilityAnnot )
695
+
696
+ /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
697
+ * the reach capability `ref*` as a type.
698
+ */
699
+ object ReachCapability extends AnnotatedCapability (defn.ReachCapabilityAnnot ):
700
+ protected def unwrappable (using Context ) = Set (defn.MaybeCapabilityAnnot , defn.ReadOnlyCapabilityAnnot )
664
701
665
702
/** Offers utility method to be used for type maps that follow aliases */
666
703
trait ConservativeFollowAliasMap (using Context ) extends TypeMap :
0 commit comments