@@ -59,9 +59,6 @@ class IllegalCaptureRef(tpe: Type) extends Exception(tpe.toString)
5959/** Capture checking state, which is known to other capture checking components */
6060class CCState :
6161
62- /** Associates nesting level owners with the local roots valid in their scopes. */
63- val localRoots : mutable.HashMap [Symbol , Symbol ] = new mutable.HashMap
64-
6562 /** The last pair of capture reference and capture set where
6663 * the reference could not be added to the set due to a level conflict.
6764 */
@@ -81,13 +78,13 @@ extension (tree: Tree)
8178
8279 /** Map tree with CaptureRef type to its type, throw IllegalCaptureRef otherwise */
8380 def toCaptureRef (using Context ): CaptureRef = tree match
84- case QualifiedRoot (outer) =>
85- ctx.owner.levelOwnerNamed(outer)
86- .orElse(defn.RootClass ) // non-existing outer roots are reported in Setup's checkQualifiedRoots
87- .localRoot.termRef
81+ case ReachCapabilityApply (arg) =>
82+ arg.toCaptureRef.reach
8883 case _ => tree.tpe match
89- case ref : CaptureRef => ref
90- case tpe => throw IllegalCaptureRef (tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
84+ case ref : CaptureRef if ref.isTrackableRef =>
85+ ref
86+ case tpe =>
87+ throw IllegalCaptureRef (tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
9188
9289 /** Convert a @retains or @retainsByName annotation tree to the capture set it represents.
9390 * For efficience, the result is cached as an Attachment on the tree.
@@ -166,7 +163,7 @@ extension (tp: Type)
166163 def forceBoxStatus (boxed : Boolean )(using Context ): Type = tp.widenDealias match
167164 case tp @ CapturingType (parent, refs) if tp.isBoxed != boxed =>
168165 val refs1 = tp match
169- case ref : CaptureRef if ref.isTracked => ref.singletonCaptureSet
166+ case ref : CaptureRef if ref.isTracked || ref.isReach => ref.singletonCaptureSet
170167 case _ => refs
171168 CapturingType (parent, refs1, boxed)
172169 case _ =>
@@ -206,12 +203,6 @@ extension (tp: Type)
206203 case _ : TypeRef | _ : AppliedType => tp.typeSymbol.hasAnnotation(defn.CapabilityAnnot )
207204 case _ => false
208205
209- def isSealed (using Context ): Boolean = tp match
210- case tp : TypeParamRef => tp.underlying.isSealed
211- case tp : TypeBounds => tp.hi.hasAnnotation(defn.Caps_SealedAnnot )
212- case tp : TypeRef => tp.symbol.is(Sealed ) || tp.info.isSealed // TODO: drop symbol flag?
213- case _ => false
214-
215206 /** Drop @retains annotations everywhere */
216207 def dropAllRetains (using Context ): Type = // TODO we should drop retains from inferred types before unpickling
217208 val tm = new TypeMap :
@@ -222,6 +213,62 @@ extension (tp: Type)
222213 mapOver(t)
223214 tm(tp)
224215
216+ /** If `x` is a capture ref, its reach capability `x*`, represented internally
217+ * as `x @reachCapability`. `x*` stands for all capabilities reachable through `x`".
218+ * We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x`
219+ * is the union of all capture sets that appear in covariant position in the
220+ * type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
221+ * are unrelated.
222+ */
223+ def reach (using Context ): CaptureRef =
224+ assert(tp.isTrackableRef)
225+ AnnotatedType (tp, Annotation (defn.ReachCapabilityAnnot , util.Spans .NoSpan ))
226+
227+ /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a
228+ * universal capture set, replace all these occurrences by `{ref*}`. This implements
229+ * the new aspect of the (Var) rule, which can now be stated as follows:
230+ *
231+ * x: T in E
232+ * -----------
233+ * E |- x: T'
234+ *
235+ * where T' is T with (1) the toplevel capture set replaced by `{x}` and
236+ * (2) all covariant occurrences of cap replaced by `x*`, provided there
237+ * are no occurrences in `T` at other variances. (1) is standard, whereas
238+ * (2) is new.
239+ *
240+ * Why is this sound? Covariant occurrences of cap must represent capabilities
241+ * that are reachable from `x`, so they are included in the meaning of `{x*}`.
242+ * At the same time, encapsulation is still maintained since no covariant
243+ * occurrences of cap are allowed in instance types of type variables.
244+ */
245+ def withReachCaptures (ref : Type )(using Context ): Type =
246+ object narrowCaps extends TypeMap :
247+ var ok = true
248+ def apply (t : Type ) = t.dealias match
249+ case t1 @ CapturingType (p, cs) if cs.isUniversal =>
250+ if variance > 0 then
251+ t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
252+ else
253+ ok = false
254+ t
255+ case _ => t match
256+ case t @ CapturingType (p, cs) =>
257+ t.derivedCapturingType(apply(p), cs) // don't map capture set variables
258+ case t =>
259+ mapOver(t)
260+ ref match
261+ case ref : CaptureRef if ref.isTrackableRef =>
262+ val tp1 = narrowCaps(tp)
263+ if narrowCaps.ok then
264+ if tp1 ne tp then capt.println(i " narrow $tp of $ref to $tp1" )
265+ tp1
266+ else
267+ capt.println(i " cannot narrow $tp of $ref to $tp1" )
268+ tp
269+ case _ =>
270+ tp
271+
225272extension (cls : ClassSymbol )
226273
227274 def pureBaseClass (using Context ): Option [Symbol ] =
@@ -281,24 +328,13 @@ extension (sym: Symbol)
281328 && sym != defn.Caps_unsafeBox
282329 && sym != defn.Caps_unsafeUnbox
283330
284- /** Can this symbol possibly own a local root?
285- * TODO: Disallow anonymous functions ?
331+ /** Does this symbol define a level where we do not want to let local variables
332+ * escape into outer capture sets ?
286333 */
287334 def isLevelOwner (using Context ): Boolean =
288335 sym.isClass
289336 || sym.is(Method , butNot = Accessor )
290337
291- /** The level owner enclosing `sym` which has the given name, or NoSymbol
292- * if none exists.
293- */
294- def levelOwnerNamed (name : String )(using Context ): Symbol =
295- def recur (sym : Symbol ): Symbol =
296- if sym.name.toString == name then
297- if sym.isLevelOwner then sym else NoSymbol
298- else if sym == defn.RootClass then NoSymbol
299- else recur(sym.owner)
300- recur(sym)
301-
302338 /** The owner of the current level. Qualifying owners are
303339 * - methods other than constructors and anonymous functions
304340 * - anonymous functions, provided they either define a local
@@ -313,14 +349,6 @@ extension (sym: Symbol)
313349 else recur(sym.owner)
314350 recur(sym)
315351
316- /** The local root corresponding to sym's level owner */
317- def localRoot (using Context ): Symbol =
318- val owner = sym.levelOwner
319- assert(owner.exists)
320- def newRoot = newSymbol(if owner.isClass then newLocalDummy(owner) else owner,
321- nme.LOCAL_CAPTURE_ROOT , Synthetic , defn.Caps_Cap .typeRef)
322- ccState.localRoots.getOrElseUpdate(owner, newRoot)
323-
324352 /** The outermost symbol owned by both `sym` and `other`. if none exists
325353 * since the owning scopes of `sym` and `other` are not nested, invoke
326354 * `onConflict` to return a symbol.
@@ -342,3 +370,21 @@ extension (tp: AnnotatedType)
342370 def isBoxed (using Context ): Boolean = tp.annot match
343371 case ann : CaptureAnnotation => ann.boxed
344372 case _ => false
373+
374+ /** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
375+ * capability as a tree in a @retains annotation.
376+ */
377+ object ReachCapabilityApply :
378+ def unapply (tree : Apply )(using Context ): Option [Tree ] = tree match
379+ case Apply (reach, arg :: Nil ) if reach.symbol == defn.Caps_reachCapability => Some (arg)
380+ case _ => None
381+
382+ /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
383+ * the reach capability `ref*` as a type.
384+ */
385+ object ReachCapability :
386+ def unapply (tree : AnnotatedType )(using Context ): Option [SingletonCaptureRef ] = tree match
387+ case AnnotatedType (parent : SingletonCaptureRef , ann)
388+ if ann.symbol == defn.ReachCapabilityAnnot => Some (parent)
389+ case _ => None
390+
0 commit comments