Skip to content

Commit beffc7e

Browse files
oderskyodersky
committed
Add reach capabilities
This adds reach capabilities x* as described in the proposal.
1 parent b58ae96 commit beffc7e

File tree

16 files changed

+242
-38
lines changed

16 files changed

+242
-38
lines changed

‎compiler/src/dotty/tools/dotc/cc/CaptureOps.scala‎

Lines changed: 47 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -166,7 +166,7 @@ extension (tp: Type)
166166
def forceBoxStatus(boxed: Boolean)(using Context): Type = tp.widenDealias match
167167
case tp @ CapturingType(parent, refs) if tp.isBoxed != boxed =>
168168
val refs1 = tp match
169-
case ref: CaptureRef if ref.isTracked => ref.singletonCaptureSet
169+
case ref: CaptureRef if ref.isTracked || ref.isReach => ref.singletonCaptureSet
170170
case _ => refs
171171
CapturingType(parent, refs1, boxed)
172172
case _ =>
@@ -222,6 +222,52 @@ extension (tp: Type)
222222
mapOver(t)
223223
tm(tp)
224224

225+
/** If `x` is a capture ref, its reach capability `x*`, represented internally
226+
* as `x.$reach`. `x*` stands for all capabilities reachable through `x`".
227+
* We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x`
228+
* is the union of all capture sets that appear in covariant position in the
229+
* type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
230+
* are unrelated.
231+
*/
232+
def reach(using Context): TermRef =
233+
assert(tp.isTrackableRef)
234+
TermRef(tp, nme.CC_REACH, defn.Any_ccReach)
235+
236+
/** If `ref` is a trackable capture ref, replace all covariant occurrences of a
237+
* universal capture set in `tp` by `{ref*}`. This implements the new aspect of
238+
* the (Var) rule, which can now be stated as follows:
239+
*
240+
* x: T in E
241+
* -----------
242+
* E |- x: T'
243+
*
244+
* where T' is T with (1) the toplevel capture set replaced by `{x}` and
245+
* (2) all covariant occurrences of cap replaced by `x*`. (1) is standard,
246+
* whereas (2) is new.
247+
*
248+
* Why is this sound? Covariant occurrences of cap must represent capabilities
249+
* that are reachable from `x`, so they are included in the meaning of `{x*}`.
250+
* At the same time, encapsulation is still maintained since no covariant
251+
* occurrences of cap are allowed in instance types of type variables.
252+
*/
253+
def withReachCaptures(ref: Type)(using Context): Type =
254+
val narrowCaps = new TypeMap:
255+
def apply(t: Type) = t.dealias match
256+
case t1 @ CapturingType(p, cs) if cs.isUniversal && variance > 0 =>
257+
t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
258+
case _ => t match
259+
case t @ CapturingType(p, cs) =>
260+
t.derivedCapturingType(apply(p), cs) // don't map capture set variables
261+
case t =>
262+
mapOver(t)
263+
ref match
264+
case ref: CaptureRef if ref.isTrackableRef =>
265+
val tp1 = narrowCaps(tp)
266+
if tp1 ne tp then capt.println(i"narrow $tp of $ref to $tp1")
267+
tp1
268+
case _ =>
269+
tp
270+
225271
extension (cls: ClassSymbol)
226272

227273
def pureBaseClass(using Context): Option[Symbol] =

‎compiler/src/dotty/tools/dotc/cc/CaptureSet.scala‎

Lines changed: 27 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -156,17 +156,24 @@ sealed abstract class CaptureSet extends Showable:
156156

157157
extension (x: CaptureRef)(using Context)
158158

159-
/* x subsumes y if one of the following is true:
160-
* - x is the same as y,
161-
* - x is a this reference and y refers to a field of x
162-
* - x is a super root of y
159+
/** x subsumes x
160+
* this subsumes this.f
161+
* x subsumes y ==> x* subsumes y
162+
* x subsumes y ==> x* subsumes y*
163163
*/
164-
private def subsumes(y: CaptureRef) =
164+
private def subsumes(y: CaptureRef): Boolean =
165165
(x eq y)
166166
|| x.isSuperRootOf(y)
167167
|| y.match
168-
case y: TermRef => y.prefix eq x
168+
case y: TermRef => !y.isReach && (y.prefix eq x)
169169
case _ => false
170+
|| x.match
171+
case x: TermRef if x.isReach =>
172+
y.match
173+
case y: TermRef if y.isReach => x.reachPrefix.subsumes(y.reachPrefix)
174+
case _ => x.reachPrefix.subsumes(y)
175+
case _ =>
176+
false
170177

171178
/** x <:< cap, cap[x] <:< cap
172179
* cap[y] <:< cap[x] if y encloses x
@@ -530,7 +537,8 @@ object CaptureSet:
530537
if elem.isUniversalRootCapability then !noUniversal
531538
else elem match
532539
case elem: TermRef =>
533-
if levelLimit.exists then
540+
if elem.isReach then levelOK(elem.reachPrefix)
541+
else if levelLimit.exists then
534542
var sym = elem.symbol
535543
if sym.isLevelOwner then sym = sym.owner
536544
levelLimit.isContainedIn(sym.levelOwner)
@@ -1037,6 +1045,8 @@ object CaptureSet:
10371045
/** The capture set of the type underlying CaptureRef */
10381046
def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
10391047
case ref: TermRef if ref.isRootCapability => ref.singletonCaptureSet
1048+
case ref: TermRef if ref.isReach => deepCaptureSet(ref.prefix.widen)
1049+
.showing(i"Deep capture set of $ref: ${ref.prefix.widen} = $result", capt)
10401050
case _ => ofType(ref.underlying, followResult = true)
10411051

10421052
/** Capture set of a type */
@@ -1078,6 +1088,16 @@ object CaptureSet:
10781088
recur(tp)
10791089
.showing(i"capture set of $tp = $result", captDebug)
10801090

1091+
private def deepCaptureSet(tp: Type)(using Context): CaptureSet =
1092+
val collect = new TypeAccumulator[CaptureSet]:
1093+
def apply(cs: CaptureSet, t: Type) = t.dealias match
1094+
case t @ CapturingType(p, cs1) =>
1095+
val cs2 = apply(cs, p)
1096+
if variance > 0 then cs2 ++ cs1 else cs2
1097+
case _ =>
1098+
foldOver(cs, t)
1099+
collect(CaptureSet.empty, tp)
1100+
10811101
private val ShownVars: Property.Key[mutable.Set[Var]] = Property.Key()
10821102

10831103
/** Perform `op`. Under -Ycc-debug, collect and print info about all variables reachable

‎compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1152,7 +1152,7 @@ class CheckCaptures extends Recheck, SymTransformer:
11521152
// given `a: T^C`, improve `T^C` to `T^{a}`
11531153
case _ =>
11541154
case _ =>
1155-
val adapted = adapt(actualw, expected, covariant = true)
1155+
val adapted = adapt(actualw.withReachCaptures(actual), expected, covariant = true)
11561156
if adapted ne actualw then
11571157
capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
11581158
adapted

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

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -333,15 +333,17 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
333333

334334
def apply(t: Type): Type = t match
335335
case t: NamedType =>
336-
val sym = t.symbol
337-
def outer(froms: List[List[Symbol]], tos: List[LambdaType]): Type =
338-
def inner(from: List[Symbol], to: List[ParamRef]): Type =
339-
if from.isEmpty then outer(froms.tail, tos.tail)
340-
else if sym eq from.head then to.head
341-
else inner(from.tail, to.tail)
342-
if tos.isEmpty then t
343-
else inner(froms.head, tos.head.paramRefs)
344-
outer(from, to)
336+
if t.prefix == NoPrefix then
337+
val sym = t.symbol
338+
def outer(froms: List[List[Symbol]], tos: List[LambdaType]): Type =
339+
def inner(from: List[Symbol], to: List[ParamRef]): Type =
340+
if from.isEmpty then outer(froms.tail, tos.tail)
341+
else if sym eq from.head then to.head
342+
else inner(from.tail, to.tail)
343+
if tos.isEmpty then t
344+
else inner(froms.head, tos.head.paramRefs)
345+
outer(from, to)
346+
else t.derivedSelect(apply(t.prefix))
345347
case _ =>
346348
mapOver(t)
347349

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

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -304,6 +304,15 @@ class Definitions {
304304
@tu lazy val Any_typeCast: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOfPM, _.paramRefs(0), Final | SyntheticArtifact | StableRealizable)
305305
// generated by pattern matcher and explicit nulls, eliminated by erasure
306306

307+
@tu lazy val Any_ccReach =
308+
newPermanentSymbol(AnyClass, nme.CC_REACH, Final | SyntheticArtifact | StableRealizable,
309+
info = new LazyType:
310+
def complete(denot: SymDenotation)(using Context): Unit =
311+
denot.info = Caps_Cap.typeRef
312+
).entered
313+
// The internal representation of a reach capability `x*` is `x.$reach`.
314+
// See doc comment in CaptureOps.reach for more info on reach capabilities
315+
307316
/** def getClass[A >: this.type](): Class[? <: A] */
308317
@tu lazy val Any_getClass: TermSymbol =
309318
enterPolyMethod(
@@ -313,7 +322,8 @@ class Definitions {
313322
bounds = TypeBounds.lower(AnyClass.thisType))
314323

315324
def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
316-
Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest, Any_typeCast)
325+
Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest,
326+
Any_typeCast, Any_ccReach)
317327

318328
@tu lazy val ObjectClass: ClassSymbol = {
319329
val cls = requiredClass("java.lang.Object")

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,7 @@ object StdNames {
120120
val BITMAP_TRANSIENT: N = s"${BITMAP_PREFIX}trans$$" // initialization bitmap for transient lazy vals
121121
val BITMAP_CHECKINIT: N = s"${BITMAP_PREFIX}init$$" // initialization bitmap for checkinit values
122122
val BITMAP_CHECKINIT_TRANSIENT: N = s"${BITMAP_PREFIX}inittrans$$" // initialization bitmap for transient checkinit values
123+
val CC_REACH: N = "$reach"
123124
val DEFAULT_GETTER: N = str.DEFAULT_GETTER
124125
val DEFAULT_GETTER_INIT: N = "$lessinit$greater"
125126
val DO_WHILE_PREFIX: N = "doWhile$"

‎compiler/src/dotty/tools/dotc/core/TypeComparer.scala‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -980,11 +980,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
980980

981981
def tp1widened =
982982
val tp1w = tp1.underlying.widenExpr
983-
tp1 match
984-
case tp1: CaptureRef if isCaptureCheckingOrSetup && tp1.isTracked =>
985-
CapturingType(tp1w.stripCapturing, tp1.singletonCaptureSet)
986-
case _ =>
987-
tp1w
983+
if isCaptureCheckingOrSetup then
984+
tp1
985+
.match
986+
case tp1: CaptureRef if tp1.isTracked =>
987+
CapturingType(tp1w.stripCapturing, tp1.singletonCaptureSet)
988+
case _ =>
989+
tp1w
990+
.withReachCaptures(tp1)
991+
else tp1w
988992

989993
comparePaths || isSubType(tp1widened, tp2, approx.addLow)
990994
case tp1: RefinedType =>

‎compiler/src/dotty/tools/dotc/core/Types.scala‎

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2174,6 +2174,9 @@ object Types {
21742174
final def isTracked(using Context): Boolean =
21752175
isTrackableRef && (isRootCapability || !captureSetOfInfo.isAlwaysEmpty)
21762176

2177+
/** Is this a reach reference of the form `x*`? */
2178+
def isReach(using Context): Boolean = false // overridden in TermRef
2179+
21772180
/** Is this reference the generic root capability `cap` ? */
21782181
def isUniversalRootCapability(using Context): Boolean = false
21792182

@@ -2918,8 +2921,14 @@ object Types {
29182921
((prefix eq NoPrefix)
29192922
|| symbol.is(ParamAccessor) && (prefix eq symbol.owner.thisType)
29202923
|| isRootCapability
2924+
|| isReach
29212925
) && !symbol.isOneOf(UnstableValueFlags)
29222926

2927+
override def isReach(using Context): Boolean =
2928+
name == nme.CC_REACH && symbol == defn.Any_ccReach
2929+
2930+
def reachPrefix: CaptureRef = prefix.asInstanceOf[CaptureRef]
2931+
29232932
override def isUniversalRootCapability(using Context): Boolean =
29242933
name == nme.CAPTURE_ROOT && symbol == defn.captureRoot
29252934

@@ -2930,7 +2939,9 @@ object Types {
29302939
if name == nme.LOCAL_CAPTURE_ROOT then normOwner else NoSymbol
29312940

29322941
override def normalizedRef(using Context): CaptureRef =
2933-
if isTrackableRef then symbol.termRef else this
2942+
if isReach then TermRef(reachPrefix.normalizedRef, name, denot)
2943+
else if isTrackableRef then symbol.termRef
2944+
else this
29342945
}
29352946

29362947
abstract case class TypeRef(override val prefix: Type,

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

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1476,6 +1476,7 @@ object Parsers {
14761476
if in.token == THIS then simpleRef()
14771477
else termIdent() match
14781478
case id @ Ident(nme.CAPTURE_ROOT) =>
1479+
// TODO drop
14791480
if in.token == LBRACKET then
14801481
val ref = atSpan(id.span.start)(captureRootIn)
14811482
val qual =
@@ -1486,7 +1487,11 @@ object Parsers {
14861487
else
14871488
atSpan(id.span.start)(captureRoot)
14881489
case id =>
1489-
id
1490+
if isIdent(nme.raw.STAR) then
1491+
in.nextToken()
1492+
atSpan(startOffset(id)):
1493+
Select(id, nme.CC_REACH)
1494+
else id
14901495

14911496
/** CaptureSet ::= `{` CaptureRef {`,` CaptureRef} `}` -- under captureChecking
14921497
*/

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

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -168,7 +168,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
168168
toText(ref)
169169

170170
private def toTextRetainedElems[T <: Untyped](refs: List[Tree[T]]): Text =
171-
"{" ~ Text(refs.map(ref => toTextRetainedElem(ref))) ~ "}"
171+
"{" ~ Text(refs.map(ref => toTextRetainedElem(ref)), ", ") ~ "}"
172172

173173
/** Print capturing type, overridden in RefinedPrinter to account for
174174
* capturing function types.
@@ -393,7 +393,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
393393
case tp: TermRef =>
394394
if tp.symbol.name == nme.LOCAL_CAPTURE_ROOT then // TODO: Move to toTextCaptureRef
395395
Str(s"cap[${nameString(tp.localRootOwner)}]")
396-
else toTextPrefixOf(tp) ~ selectionString(tp)
396+
else if tp.isReach then
397+
toTextRef(tp.reachPrefix) ~ "*"
398+
else
399+
toTextPrefixOf(tp) ~ selectionString(tp)
397400
case tp: ThisType =>
398401
nameString(tp.cls) + ".this"
399402
case SuperType(thistpe: SingletonType, _) =>

0 commit comments

Comments
 (0)