Skip to content

Commit 33ef293

Browse files
committed
Classify existential variables as root capabilities
Allows some simplifications in the zoo of classification methods.
1 parent 58baf53 commit 33ef293

File tree

7 files changed

+24
-42
lines changed

7 files changed

+24
-42
lines changed

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

+7
Original file line numberDiff line numberDiff line change
@@ -434,6 +434,13 @@ extension (tp: Type)
434434
&& tp.membersBasedOnFlags(Mutable | Method, EmptyFlags)
435435
.exists(_.hasAltWith(_.symbol.isUpdateMethod))
436436

437+
/** Knowing that `tp` is a function type, is it an alias to a function other
438+
* than `=>`?
439+
*/
440+
def isAliasFun(using Context) = tp match
441+
case AppliedType(tycon, _) => !defn.isFunctionSymbol(tycon.typeSymbol)
442+
case _ => false
443+
437444
/** Tests whether the type derives from `caps.Capability`, which means
438445
* references of this type are maximal capabilities.
439446
*/

compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

+4-13
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ trait CaptureRef extends TypeProxy, ValueType:
4242
* set of the underlying type is not always empty.
4343
*/
4444
final def isTracked(using Context): Boolean =
45-
this.isTrackableRef && (isMaxCapability || !captureSetOfInfo.isAlwaysEmpty)
45+
this.isTrackableRef && (isRootCapability || !captureSetOfInfo.isAlwaysEmpty)
4646

4747
/** Is this a maybe reference of the form `x?`? */
4848
final def isMaybe(using Context): Boolean = this ne stripMaybe
@@ -102,25 +102,16 @@ trait CaptureRef extends TypeProxy, ValueType:
102102

103103
/** Is this reference one of the generic root capabilities `cap` or `cap.rd` ? */
104104
final def isRootCapability(using Context): Boolean = this match
105-
case ReadOnlyCapability(tp1) => tp1.isCapOrFresh
106-
case _ => isCapOrFresh
107-
108-
/** Is this reference a capability that does not derive from another capability?
109-
* Includes read-only versions of maximal capabilities.
110-
*/
111-
final def isMaxCapability(using Context): Boolean = this match
112-
case tp: TermRef => tp.isCap || tp.info.derivesFrom(defn.Caps_Exists)
105+
case ReadOnlyCapability(tp1) => tp1.isRootCapability
113106
case Existential.Vble(_) => true
114-
case Fresh(_) => true
115-
case ReadOnlyCapability(tp1) => tp1.isMaxCapability
116-
case _ => false
107+
case _ => isCapOrFresh
117108

118109
/** An exclusive capability is a capability that derives
119110
* indirectly from a maximal capability without going through
120111
* a read-only capability first.
121112
*/
122113
final def isExclusive(using Context): Boolean =
123-
!isReadOnly && (isMaxCapability || captureSetOfInfo.isExclusive)
114+
!isReadOnly && (isRootCapability || captureSetOfInfo.isExclusive)
124115

125116
// With the support of paths, we don't need to normalize the `TermRef`s anymore.
126117
// /** Normalize reference so that it can be compared with `eq` for equality */

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

+6-15
Original file line numberDiff line numberDiff line change
@@ -91,22 +91,13 @@ sealed abstract class CaptureSet extends Showable:
9191
final def isUniversal(using Context) =
9292
elems.exists(_.isCap)
9393

94-
/** Does this capture set contain the root reference `cap` as element? */
95-
final def isUniversalOrFresh(using Context) =
96-
elems.exists(_.isCapOrFresh)
97-
9894
/** Does this capture set contain a root reference `cap` or `cap.rd` as element? */
9995
final def containsRootCapability(using Context) =
10096
elems.exists(_.isRootCapability)
10197

10298
final def containsCap(using Context) =
10399
elems.exists(_.stripReadOnly.isCap)
104100

105-
final def isUnboxable(using Context) =
106-
elems.exists:
107-
case Existential.Vble(_) => true
108-
case elem => elem.isRootCapability
109-
110101
final def isReadOnly(using Context): Boolean =
111102
elems.forall(_.isReadOnly)
112103

@@ -151,7 +142,7 @@ sealed abstract class CaptureSet extends Showable:
151142
* capture set.
152143
*/
153144
protected final def addNewElem(elem: CaptureRef)(using ctx: Context, vs: VarState): CompareResult =
154-
if elem.isMaxCapability || !vs.isOpen then
145+
if elem.isRootCapability || !vs.isOpen then
155146
addThisElem(elem)
156147
else
157148
addThisElem(elem).orElse:
@@ -195,7 +186,7 @@ sealed abstract class CaptureSet extends Showable:
195186
elems.exists(_.subsumes(x))
196187
|| // Even though subsumes already follows captureSetOfInfo, this is not enough.
197188
// For instance x: C^{y, z}. Then neither y nor z subsumes x but {y, z} accounts for x.
198-
!x.isMaxCapability
189+
!x.isRootCapability
199190
&& !x.derivesFrom(defn.Caps_CapSet)
200191
&& !(vs.isSeparating && x.captureSetOfInfo.containsRootCapability)
201192
// in VarState.Separate, don't try to widen to cap since that might succeed with {cap} <: {cap}
@@ -216,7 +207,7 @@ sealed abstract class CaptureSet extends Showable:
216207
def mightAccountFor(x: CaptureRef)(using Context): Boolean =
217208
reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
218209
elems.exists(_.subsumes(x)(using ctx, VarState.ClosedUnrecorded))
219-
|| !x.isMaxCapability
210+
|| !x.isRootCapability
220211
&& {
221212
val elems = x.captureSetOfInfo.elems
222213
!elems.isEmpty && elems.forall(mightAccountFor)
@@ -352,7 +343,7 @@ sealed abstract class CaptureSet extends Showable:
352343

353344
/** Invoke handler if this set has (or later aquires) the root capability `cap` */
354345
def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
355-
if isUnboxable then handler()
346+
if containsRootCapability then handler()
356347
this
357348

358349
/** Invoke handler on the elements to ensure wellformedness of the capture set.
@@ -1302,7 +1293,7 @@ object CaptureSet:
13021293
case ReadOnlyCapability(ref1) =>
13031294
ref1.captureSetOfInfo.map(ReadOnlyMap())
13041295
case _ =>
1305-
if ref.isMaxCapability then ref.singletonCaptureSet
1296+
if ref.isRootCapability then ref.singletonCaptureSet
13061297
else ofType(ref.underlying, followResult = false)
13071298

13081299
/** Capture set of a type
@@ -1435,7 +1426,7 @@ object CaptureSet:
14351426
override def toAdd(using Context) =
14361427
for CompareResult.LevelError(cs, ref) <- ccState.levelError.toList yield
14371428
ccState.levelError = None
1438-
if ref.isRootCapability then
1429+
if ref.stripReadOnly.isCapOrFresh then
14391430
def capStr = if ref.isReadOnly then "cap.rd" else "cap"
14401431
i"""
14411432
|

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -496,7 +496,7 @@ class CheckCaptures extends Recheck, SymTransformer:
496496
val underlying = CaptureSet.ofTypeDeeply(c1.widen)
497497
capt.println(i"Widen reach $c to $underlying in ${env.owner}")
498498
if ccConfig.useSepChecks then
499-
recur(underlying.filter(!_.isMaxCapability), env, null)
499+
recur(underlying.filter(!_.isRootCapability), env, null)
500500
// we don't want to disallow underlying Fresh instances, since these are typically locally created
501501
// fresh capabilities. We don't need to also follow the hidden set since separation
502502
// checking makes ure that locally hidden references need to go to @consume parameters.
@@ -1771,7 +1771,7 @@ class CheckCaptures extends Recheck, SymTransformer:
17711771
case ref: TermParamRef
17721772
if !allowed.contains(ref) && !seen.contains(ref) =>
17731773
seen += ref
1774-
if ref.isMaxCapability then
1774+
if ref.isRootCapability then
17751775
report.error(i"escaping local reference $ref", tree.srcPos)
17761776
else
17771777
val widened = ref.captureSetOfInfo

compiler/src/dotty/tools/dotc/cc/Existential.scala

+1-8
Original file line numberDiff line numberDiff line change
@@ -250,13 +250,6 @@ object Existential:
250250
subst(tp)
251251
end toCap
252252

253-
/** Knowing that `tp` is a function type, is it an alias to a function other
254-
* than `=>`?
255-
*/
256-
private def isAliasFun(tp: Type)(using Context) = tp match
257-
case AppliedType(tycon, _) => !defn.isFunctionSymbol(tycon.typeSymbol)
258-
case _ => false
259-
260253
/** Replace all occurrences of `cap` (or fresh) in parts of this type by an existentially bound
261254
* variable bound by `mt`.
262255
* Stop at function or method types since these have been mapped before.
@@ -265,7 +258,7 @@ object Existential:
265258

266259
abstract class CapMap extends BiTypeMap:
267260
override def mapOver(t: Type): Type = t match
268-
case t @ FunctionOrMethod(args, res) if variance > 0 && !isAliasFun(t) =>
261+
case t @ FunctionOrMethod(args, res) if variance > 0 && !t.isAliasFun =>
269262
t // `t` should be mapped in this case by a different call to `mapCap`.
270263
case t: (LazyRef | TypeVar) =>
271264
mapConserveSuper(t)

compiler/src/dotty/tools/dotc/cc/SepCheck.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -185,7 +185,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
185185
* 3. if `f in F` then the footprint of `f`'s info is also in `F`.
186186
*/
187187
private def footprint(includeMax: Boolean = false)(using Context): Refs =
188-
def retain(ref: CaptureRef) = includeMax || !ref.isMaxCapability
188+
def retain(ref: CaptureRef) = includeMax || !ref.isRootCapability
189189
def recur(elems: Refs, newElems: List[CaptureRef]): Refs = newElems match
190190
case newElem :: newElems1 =>
191191
val superElems = newElem.captureSetOfInfo.elems.filter: superElem =>
@@ -210,7 +210,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
210210
else hidden.superCaps
211211
recur(seen + newElem, acc, superCaps ++ newElems)
212212
case _ =>
213-
if newElem.isMaxCapability
213+
if newElem.isRootCapability
214214
//|| newElem.isInstanceOf[TypeRef | TypeParamRef]
215215
then recur(seen + newElem, acc, newElems1)
216216
else recur(seen + newElem, acc, newElem.captureSetOfInfo.elems.toList ++ newElems1)

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -926,7 +926,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
926926
def apply(t: Type) = t match
927927
case t @ CapturingType(parent, refs) =>
928928
val parent1 = this(parent)
929-
if refs.isUniversalOrFresh then t.derivedCapturingType(parent1, CaptureSet.Fluid)
929+
if refs.containsRootCapability then t.derivedCapturingType(parent1, CaptureSet.Fluid)
930930
else t
931931
case _ => mapFollowingAliases(t)
932932

@@ -982,7 +982,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
982982
for
983983
j <- 0 until retained.length if j != i
984984
r <- retained(j).toCaptureRefs
985-
if !r.isMaxCapability
985+
if !r.isRootCapability
986986
yield r
987987
val remaining = CaptureSet(others*)
988988
check(remaining, remaining)

0 commit comments

Comments
 (0)