Skip to content

Commit 399b220

Browse files
committed
Merge Existential and Fresh into root module
1 parent 12047d8 commit 399b220

File tree

10 files changed

+340
-310
lines changed

10 files changed

+340
-310
lines changed

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

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ import CaptureSet.VarState
2121
/** Attachment key for capturing type trees */
2222
private val Captures: Key[CaptureSet] = Key()
2323

24-
/** Context property to print Fresh(...) as "fresh" instead of "cap" */
24+
/** Context property to print root.Fresh(...) as "fresh" instead of "cap" */
2525
val PrintFresh: Key[Unit] = Key()
2626

2727
object ccConfig:
@@ -225,7 +225,7 @@ extension (tp: Type)
225225
tp.symbol.isType && tp.derivesFrom(defn.Caps_CapSet)
226226
case tp: TypeParamRef =>
227227
tp.derivesFrom(defn.Caps_CapSet)
228-
case Existential.Vble(_) => true
228+
case root.Result(_) => true
229229
case AnnotatedType(parent, annot) =>
230230
defn.capabilityWrapperAnnots.contains(annot.symbol) && parent.isTrackableRef
231231
case _ =>
@@ -557,7 +557,7 @@ extension (tp: Type)
557557
if args.forall(_.isAlwaysPure) then
558558
// Also map existentials in results to reach capabilities if all
559559
// preceding arguments are known to be always pure
560-
t.derivedFunctionOrMethod(args, apply(Existential.toCap(res)))
560+
t.derivedFunctionOrMethod(args, apply(root.resultToFresh(res)))
561561
else
562562
t
563563
case _ =>
@@ -720,6 +720,9 @@ extension (tp: AnnotatedType)
720720
case ann: CaptureAnnotation => ann.boxed
721721
case _ => false
722722

723+
def rootAnnot: root.Annot = (tp.annot: @unchecked) match
724+
case ann: root.Annot => ann
725+
723726
/** Drop retains annotations in the type. */
724727
class CleanupRetains(using Context) extends TypeMap:
725728
def apply(tp: Type): Type =

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ trait CaptureRef extends TypeProxy, ValueType:
9494

9595
/** Is this reference a Fresh instance? */
9696
final def isFresh(using Context): Boolean = this match
97-
case Fresh(_) => true
97+
case root.Fresh(_) => true
9898
case _ => false
9999

100100
/** Is this reference the generic root capability `cap` or a Fresh instance? */
@@ -103,8 +103,8 @@ trait CaptureRef extends TypeProxy, ValueType:
103103
/** Is this reference one of the generic root capabilities `cap` or `cap.rd` ? */
104104
final def isRootCapability(using Context): Boolean = this match
105105
case ReadOnlyCapability(tp1) => tp1.isRootCapability
106-
case Existential.Vble(_) => true
107-
case _ => isCapOrFresh
106+
case root(_) => true
107+
case _ => isCap
108108

109109
/** An exclusive capability is a capability that derives
110110
* indirectly from a maximal capability without going through
@@ -244,16 +244,16 @@ trait CaptureRef extends TypeProxy, ValueType:
244244
*/
245245
def maxSubsumes(y: CaptureRef, canAddHidden: Boolean)(using ctx: Context, vs: VarState = VarState.Separate): Boolean =
246246
def yIsExistential = y.stripReadOnly match
247-
case Existential.Vble(_) =>
247+
case root.Result(_) =>
248248
capt.println(i"failed existential $this >: $y")
249249
true
250250
case _ => false
251251
(this eq y)
252252
|| this.match
253-
case Fresh(hidden) =>
253+
case root.Fresh(hidden) =>
254254
vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
255255
|| !y.stripReadOnly.isCap && !yIsExistential && canAddHidden && vs.addHidden(hidden, y)
256-
case Existential.Vble(binder) =>
256+
case root.Result(binder) =>
257257
if y.derivesFromSharedCapability then true
258258
else
259259
ccState.existentialSubsumesFailure =
@@ -288,7 +288,7 @@ trait CaptureRef extends TypeProxy, ValueType:
288288
this match
289289
case MaybeCapability(x1) => x1.covers(y1)
290290
case _ => false
291-
case Fresh(hidden) =>
291+
case root.Fresh(hidden) =>
292292
hidden.superCaps.exists(this covers _)
293293
case _ =>
294294
false

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -410,7 +410,7 @@ object CaptureSet:
410410
defn.captureRoot.termRef.singletonCaptureSet
411411

412412
def fresh(owner: Symbol = NoSymbol)(using Context): CaptureSet =
413-
Fresh.withOwner(owner).singletonCaptureSet
413+
root.Fresh.withOwner(owner).singletonCaptureSet
414414

415415
/** The shared capture set `{cap.rd}` */
416416
def shared(using Context): CaptureSet =
@@ -556,12 +556,12 @@ object CaptureSet:
556556
elems -= elem
557557
res.addToTrace(this)
558558

559-
// TODO: Also track allowable TermParamRefs and Existential.Vbles in capture sets
559+
// TODO: Also track allowable TermParamRefs and root.Results in capture sets
560560
private def levelOK(elem: CaptureRef)(using Context): Boolean =
561561
if elem.isRootCapability then
562562
!noUniversal
563563
else elem match
564-
case elem @ Existential.Vble(mt) =>
564+
case elem @ root.Result(mt) =>
565565
!noUniversal
566566
&& !CCState.openExistentialScopes.contains(elem)
567567
// Opened existentials on the left cannot be added to nested capture sets on the right
@@ -619,7 +619,7 @@ object CaptureSet:
619619
try
620620
val approx = computeApprox(origin).ensuring(_.isConst)
621621
if approx.elems.exists:
622-
case Existential.Vble(_) => true
622+
case root.Result(_) => true
623623
case _ => false
624624
then
625625
ccState.approxWarnings +=
@@ -640,7 +640,7 @@ object CaptureSet:
640640
def solve()(using Context): Unit =
641641
if !isConst then
642642
val approx = upperApprox(empty)
643-
.map(Fresh.FromCap(NoSymbol).inverse) // Fresh --> cap
643+
.map(root.CapToFresh(NoSymbol).inverse) // Fresh --> cap
644644
.showing(i"solve $this = $result", capt)
645645
//println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
646646
val newElems = approx.elems -- elems
@@ -955,14 +955,14 @@ object CaptureSet:
955955
private def aliasRef: AnnotatedType | Null =
956956
if myElems.size == 1 then
957957
myElems.nth(0) match
958-
case al @ Fresh(hidden) if deps.contains(hidden) => al
958+
case al @ root.Fresh(hidden) if deps.contains(hidden) => al
959959
case _ => null
960960
else null
961961

962962
private def aliasSet: HiddenSet =
963963
if myElems.size == 1 then
964964
myElems.nth(0) match
965-
case Fresh(hidden) if deps.contains(hidden) => hidden
965+
case root.Fresh(hidden) if deps.contains(hidden) => hidden
966966
case _ => this
967967
else this
968968

@@ -993,7 +993,7 @@ object CaptureSet:
993993
assert(dep != this)
994994
vs.addHidden(dep.asInstanceOf[HiddenSet], elem)
995995
elem match
996-
case Fresh(hidden) =>
996+
case root.Fresh(hidden) =>
997997
if this ne hidden then
998998
val alias = hidden.aliasRef
999999
if alias != null then
@@ -1313,7 +1313,7 @@ object CaptureSet:
13131313
case tp: (TypeRef | TypeParamRef) =>
13141314
if tp.derivesFrom(defn.Caps_CapSet) then tp.captureSet
13151315
else empty
1316-
case tp @ Existential.Vble(_) =>
1316+
case tp @ root.Result(_) =>
13171317
tp.captureSet
13181318
case CapturingType(parent, refs) =>
13191319
recur(parent) ++ refs
@@ -1331,7 +1331,7 @@ object CaptureSet:
13311331
++ recur(rinfo.resType) // add capture set of result
13321332
.filter:
13331333
case TermParamRef(binder, _) => binder ne rinfo
1334-
case Existential.Vble(binder) => binder ne rinfo
1334+
case root.Result(binder) => binder ne rinfo
13351335
case _ => true
13361336
case tpd @ AppliedType(tycon, args) =>
13371337
if followResult && defn.isNonRefinedFunction(tpd) then
@@ -1377,7 +1377,7 @@ object CaptureSet:
13771377
if includeTypevars && upper.isExactlyAny then CaptureSet.fresh(t.symbol)
13781378
else this(cs, upper)
13791379
case t @ FunctionOrMethod(args, res) =>
1380-
if args.forall(_.isAlwaysPure) then this(cs, Existential.toCap(res))
1380+
if args.forall(_.isAlwaysPure) then this(cs, root.resultToFresh(res))
13811381
else cs
13821382
case _ =>
13831383
foldOver(cs, t)

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

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -325,7 +325,7 @@ class CheckCaptures extends Recheck, SymTransformer:
325325
case t @ CapturingType(parent, refs) =>
326326
for ref <- refs.elems do
327327
ref match
328-
case Fresh(hidden) if !hidden.givenOwner.exists =>
328+
case root.Fresh(hidden) if !hidden.givenOwner.exists =>
329329
hidden.givenOwner = sym
330330
case _ =>
331331
traverse(parent)
@@ -353,7 +353,7 @@ class CheckCaptures extends Recheck, SymTransformer:
353353
/** If `res` is not CompareResult.OK, report an error */
354354
def checkOK(res: CompareResult, prefix: => String, added: CaptureRef | CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit =
355355
if !res.isOK then
356-
inContext(Fresh.printContext(added, res.blocking)):
356+
inContext(root.printContext(added, res.blocking)):
357357
def toAdd: String = CaptureSet.levelErrors.toAdd.mkString
358358
def descr: String =
359359
val d = res.blocking.description
@@ -714,7 +714,7 @@ class CheckCaptures extends Recheck, SymTransformer:
714714
* charge the deep capture set of the actual argument to the environment.
715715
*/
716716
protected override def recheckArg(arg: Tree, formal: Type)(using Context): Type =
717-
val freshenedFormal = Fresh.fromCap(formal)
717+
val freshenedFormal = root.capToFresh(formal)
718718
val argType = recheck(arg, freshenedFormal)
719719
.showing(i"recheck arg $arg vs $freshenedFormal", capt)
720720
if formal.hasAnnotation(defn.UseAnnot) || formal.hasAnnotation(defn.ConsumeAnnot) then
@@ -748,7 +748,7 @@ class CheckCaptures extends Recheck, SymTransformer:
748748
*/
749749
protected override
750750
def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
751-
val appType = Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes))
751+
val appType = root.resultToFresh(super.recheckApplication(tree, qualType, funType, argTypes))
752752
val qualCaptures = qualType.captureSet
753753
val argCaptures =
754754
for (argType, formal) <- argTypes.lazyZip(funType.paramInfos) yield
@@ -809,14 +809,14 @@ class CheckCaptures extends Recheck, SymTransformer:
809809
*
810810
* Second half: union of initial capture set and all capture sets of arguments
811811
* to tracked parameters. The initial capture set `initCs` is augmented with
812-
* - Fresh(...) if `core` extends Mutable
813-
* - Fresh(...).rd if `core` extends Capability
812+
* - root.Fresh(...) if `core` extends Mutable
813+
* - root.Fresh(...).rd if `core` extends Capability
814814
*/
815815
def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
816816
var refined: Type = core
817817
var allCaptures: CaptureSet =
818818
if core.derivesFromMutable then initCs ++ CaptureSet.fresh()
819-
else if core.derivesFromCapability then initCs ++ Fresh.withOwner(core.classSymbol).readOnly.singletonCaptureSet
819+
else if core.derivesFromCapability then initCs ++ root.Fresh.withOwner(core.classSymbol).readOnly.singletonCaptureSet
820820
else initCs
821821
for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
822822
val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol
@@ -857,7 +857,7 @@ class CheckCaptures extends Recheck, SymTransformer:
857857
case fun @ Select(qual, nme.apply) => qual.symbol.orElse(fun.symbol)
858858
case fun => fun.symbol
859859
disallowCapInTypeArgs(tree.fun, meth, tree.args)
860-
val res = Existential.toCap(super.recheckTypeApply(tree, pt))
860+
val res = root.resultToFresh(super.recheckTypeApply(tree, pt))
861861
includeCallCaptures(tree.symbol, res, tree)
862862
checkContains(tree)
863863
res
@@ -909,8 +909,8 @@ class CheckCaptures extends Recheck, SymTransformer:
909909
// which are less intelligible. An example is the line `a = x` in
910910
// neg-custom-args/captures/vars.scala. That's why this code is conditioned.
911911
// to apply only to closures that are not eta expansions.
912-
val res1 = Existential.toCap(res) // TODO: why deep = true?
913-
val pt1 = Existential.toCap(pt)
912+
val res1 = root.resultToFresh(res) // TODO: why deep = true?
913+
val pt1 = root.resultToFresh(pt)
914914
// We need to open existentials here in order not to get vars mixed up in them
915915
// We do the proper check with existentials when we are finished with the closure block.
916916
capt.println(i"pre-check closure $expr of type $res1 against $pt1")
@@ -1220,13 +1220,13 @@ class CheckCaptures extends Recheck, SymTransformer:
12201220

12211221
private def existentialSubsumesFailureAddenda(using Context): Addenda =
12221222
ccState.existentialSubsumesFailure match
1223-
case Some((ex @ Existential.Vble(binder), other)) =>
1223+
case Some((ex @ root.Result(binder), other)) =>
12241224
new Addenda:
12251225
override def toAdd(using Context): List[String] =
1226-
val ann = ex.annot.asInstanceOf[Fresh.Annot]
1226+
val ann = ex.rootAnnot
12271227
i"""
12281228
|
1229-
|Note that the existential capture root in ${ann.originalBinder.resType}
1229+
|Note that the existential capture root in ${ex.rootAnnot.originalBinder.resType}
12301230
|cannot subsume the capability $other"""
12311231
:: Nil
12321232
case _ => NothingToAdd
@@ -1279,7 +1279,7 @@ class CheckCaptures extends Recheck, SymTransformer:
12791279
actualBoxed
12801280
else
12811281
capt.println(i"conforms failed for ${tree}: $actual vs $expected")
1282-
inContext(Fresh.printContext(actualBoxed, expected1)):
1282+
inContext(root.printContext(actualBoxed, expected1)):
12831283
err.typeMismatch(tree.withType(actualBoxed), expected1,
12841284
addApproxAddenda(
12851285
addenda

0 commit comments

Comments
 (0)