@@ -51,23 +51,23 @@ extension (tree: Tree)
5151 * map CapSet^{refs} to the `refs` references,
5252 * throw IllegalCaptureRef otherwise
5353 */
54- def toCapabilities (using Context ): List [Capability ] = tree match
55- case ReachCapabilityApply (arg) =>
56- arg.toCapabilities.map(_.reach)
57- case ReadOnlyCapabilityApply (arg) =>
58- arg.toCapabilities.map(_.readOnly)
59- case CapsOfApply (arg) =>
60- arg.toCapabilities
61- case _ => tree.tpe.dealiasKeepAnnots match
62- case ref : TermRef if ref.isCapRef =>
63- GlobalCap :: Nil
64- case ref : Capability if ref.isTrackableRef =>
65- ref :: Nil
66- case AnnotatedType (parent, ann)
67- if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet ) =>
68- ann.tree.toCaptureSet.elems.toList
69- case tpe =>
70- throw IllegalCaptureRef (tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
54+ // def toCapabilities(using Context): List[Capability] = tree match
55+ // case ReachCapabilityApply(arg) =>
56+ // arg.toCapabilities.map(_.reach)
57+ // case ReadOnlyCapabilityApply(arg) =>
58+ // arg.toCapabilities.map(_.readOnly)
59+ // case CapsOfApply(arg) =>
60+ // arg.toCapabilities
61+ // case _ => tree.tpe.dealiasKeepAnnots match
62+ // case ref: TermRef if ref.isCapRef =>
63+ // GlobalCap :: Nil
64+ // case ref: Capability if ref.isTrackableRef =>
65+ // ref :: Nil
66+ // case AnnotatedType(parent, ann)
67+ // if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
68+ // ann.tree.toCaptureSet.elems.toList
69+ // case tpe =>
70+ // throw IllegalCaptureRef(tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
7171
7272 /** Convert a @retains or @retainsByName annotation tree to the capture set it represents.
7373 * For efficience, the result is cached as an Attachment on the tree.
@@ -76,28 +76,41 @@ extension (tree: Tree)
7676 tree.getAttachment(Captures ) match
7777 case Some (refs) => refs
7878 case None =>
79- val refs = CaptureSet (tree.retainedElems.flatMap(_.toCapabilities)* )
80- // .showing(i"toCaptureSet $tree --> $result", capt)
79+ val refs = CaptureSet (tree.retainedSet.retainedElements* )
8180 tree.putAttachment(Captures , refs)
8281 refs
83-
84- /** The arguments of a @retains, @retainsCap or @retainsByName annotation */
85- def retainedElems (using Context ): List [Tree ] = tree match
86- case Apply (_, Typed (SeqLiteral (elems, _), _) :: Nil ) =>
87- elems
88- case _ =>
89- if tree.symbol.maybeOwner == defn.RetainsCapAnnot
90- then ref(defn.captureRoot) :: Nil
91- else Nil
82+ /** The type representing the capture set of retains annotation.
83+ */
84+ def retainedSet (using Context ): Type =
85+ tree match
86+ case Apply (TypeApply (_, refs :: Nil ), _) => refs.tpe
87+ case _ =>
88+ if tree.symbol.maybeOwner == defn.RetainsCapAnnot
89+ then ref(defn.captureRoot) else NoType
9290
9391extension (tp : Type )
9492
93+ def retainedElementsRaw (using Context ): List [Type ] = tp match
94+ case ReachCapability (tp1) =>
95+ tp1.reach :: Nil
96+ case ReadOnlyCapability (tp1) =>
97+ tp1.readOnly :: Nil
98+ case OrType (tp1, tp2) =>
99+ tp1.retainedElementsRaw ++ tp2.retainedElementsRaw
100+ case tp =>
101+ // Nothing is a special type to represent the empty set
102+ if tp.isNothingType then Nil
103+ else tp :: Nil // should be checked by wellformedness
104+
105+ def retainedElements (using Context ): List [Capability ] =
106+ retainedElementsRaw.map:
107+ case tp : CaptureRef => tp
108+ case tp => throw IllegalCaptureRef (tp)
109+
95110 /** Is this type a Capability that can be tracked?
96111 * This is true for
97112 * - all ThisTypes and all TermParamRef,
98113 * - stable TermRefs with NoPrefix or ThisTypes as prefixes,
99- * - the root capability `caps.cap`
100- * - abstract or parameter TypeRefs that derive from caps.CapSet
101114 * - annotated types that represent reach or maybe capabilities
102115 */
103116 final def isTrackableRef (using Context ): Boolean = tp match
@@ -408,7 +421,7 @@ extension (cls: ClassSymbol)
408421 || bc.is(CaptureChecked )
409422 && bc.givenSelfType.dealiasKeepAnnots.match
410423 case CapturingType (_, refs) => refs.isAlwaysEmpty
411- case RetainingType (_, refs) => refs.isEmpty
424+ case RetainingType (_, refs) => refs.retainedElements. isEmpty
412425 case selfType =>
413426 isCaptureChecking // At Setup we have not processed self types yet, so
414427 // unless a self type is explicitly given, we can't tell
@@ -523,32 +536,60 @@ class CleanupRetains(using Context) extends TypeMap:
523536 def apply (tp : Type ): Type =
524537 tp match
525538 case AnnotatedType (tp, annot) if annot.symbol == defn.RetainsAnnot || annot.symbol == defn.RetainsByNameAnnot =>
526- RetainingType (tp, Nil , byName = annot.symbol == defn.RetainsByNameAnnot )
539+ RetainingType (tp, defn. NothingType , byName = annot.symbol == defn.RetainsByNameAnnot )
527540 case _ => mapOver(tp)
528541
529- /** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
530- * capability as a tree in a @retains annotation.
531- */
532- object ReachCapabilityApply :
533- def unapply (tree : Apply )(using Context ): Option [Tree ] = tree match
534- case Apply (reach, arg :: Nil ) if reach.symbol == defn.Caps_reachCapability => Some (arg)
542+ // /** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
543+ // * capability as a tree in a @retains annotation.
544+ // */
545+ // object ReachCapabilityApply:
546+ // def unapply(tree: Apply)(using Context): Option[Tree] = tree match
547+ // case Apply(reach, arg :: Nil) if reach.symbol == defn.Caps_reachCapability => Some(arg)
548+ // case _ => None
549+
550+ // /** An extractor for `caps.readOnlyCapability(ref)`, which is used to express a read-only
551+ // * capability as a tree in a @retains annotation.
552+ // */
553+ // object ReadOnlyCapabilityApply:
554+ // def unapply(tree: Apply)(using Context): Option[Tree] = tree match
555+ // case Apply(ro, arg :: Nil) if ro.symbol == defn.Caps_readOnlyCapability => Some(arg)
556+ // case _ => None
557+
558+ abstract class AnnotatedCapability (annotCls : Context ?=> ClassSymbol ):
559+ def apply (tp : Type )(using Context ): AnnotatedType =
560+ assert(tp.isTrackableRef, i " not a trackable ref: $tp" )
561+ tp match
562+ case AnnotatedType (_, annot) =>
563+ assert(! unwrappable.contains(annot.symbol), i " illegal combination of derived capabilities: $annotCls over ${annot.symbol}" )
564+ case _ =>
565+ tp match
566+ case tp : Capability => tp.derivedRef(annotCls)
567+ case _ => AnnotatedType (tp, Annotation (annotCls, util.Spans .NoSpan ))
568+
569+ def unapply (tree : AnnotatedType )(using Context ): Option [Capability ] = tree match
570+ case AnnotatedType (parent : Capability , ann) if ann.hasSymbol(annotCls) => Some (parent)
535571 case _ => None
536572
537- /** An extractor for `caps.readOnlyCapability(ref)`, which is used to express a read-only
538- * capability as a tree in a @retains annotation.
539- */
540- object ReadOnlyCapabilityApply :
541- def unapply (tree : Apply )(using Context ): Option [Tree ] = tree match
542- case Apply (ro, arg :: Nil ) if ro.symbol == defn.Caps_readOnlyCapability => Some (arg)
573+ protected def unwrappable (using Context ): Set [Symbol ]
574+ end AnnotatedCapability
575+
576+ object QualifiedCapability :
577+ def unapply (tree : AnnotatedType )(using Context ): Option [Capability ] = tree match
578+ case AnnotatedType (parent : Capability , ann)
579+ if defn.capabilityQualifierAnnots.contains(ann.symbol) => Some (parent)
543580 case _ => None
544581
545- /** An extractor for `caps.capsOf[X] `, which is used to express a generic capture set
546- * as a tree in a @retains annotation .
582+ /** An extractor for `ref @readOnlyCapability `, which is used to express
583+ * the read-only capability `ref.rd` as a type .
547584 */
548- object CapsOfApply :
549- def unapply (tree : TypeApply )(using Context ): Option [Tree ] = tree match
550- case TypeApply (capsOf, arg :: Nil ) if capsOf.symbol == defn.Caps_capsOf => Some (arg)
551- case _ => None
585+ object ReadOnlyCapability extends AnnotatedCapability (defn.ReadOnlyCapabilityAnnot ):
586+ protected def unwrappable (using Context ) = Set ()
587+
588+ /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
589+ * the reach capability `ref*` as a type.
590+ */
591+ object ReachCapability extends AnnotatedCapability (defn.ReachCapabilityAnnot ):
592+ protected def unwrappable (using Context ) = Set (defn.ReadOnlyCapabilityAnnot )
552593
553594/** An extractor for all kinds of function types as well as method and poly types.
554595 * It includes aliases of function types such as `=>`. TODO: Can we do without?
0 commit comments