Skip to content

Commit 521432f

Browse files
committed
Add a prefix to FreshCaps
The prefix is mapped as a normal type. It determines whether the hidden set allows to add new elements. ThisType and NoPrefix prefixes allow it, other prefixes forbid it. The pathRoot and ccOwner of a FreshCap now depend on the prefix.
1 parent 23f5e32 commit 521432f

File tree

13 files changed

+118
-52
lines changed

13 files changed

+118
-52
lines changed

compiler/src/dotty/tools/dotc/ast/tpd.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -517,7 +517,7 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
517517
def singleton(tp: Type, needLoad: Boolean = true)(using Context): Tree = tp.dealias match {
518518
case tp: TermRef => ref(tp, needLoad)
519519
case tp: ThisType => This(tp.cls)
520-
case tp: SkolemType => singleton(tp.narrow, needLoad)
520+
case tp: SkolemType => singleton(tp.narrow(), needLoad)
521521
case SuperType(qual, _) => singleton(qual, needLoad)
522522
case ConstantType(value) => Literal(value)
523523
}

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

Lines changed: 52 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ import printing.Texts.Text
2323
import reporting.{Message, trace}
2424
import NameOps.isImpureFunction
2525
import annotation.internal.sharable
26+
import collection.immutable
2627

2728
/** Capabilities are members of capture sets. They partially overlap with types
2829
* as shown in the trait hierarchy below.
@@ -147,10 +148,30 @@ object Capabilities:
147148
* @param origin an indication where and why the FreshCap was created, used
148149
* for diagnostics
149150
*/
150-
case class FreshCap (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability:
151-
val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked)
151+
case class FreshCap(val prefix: Type)
152+
(val owner: Symbol, val origin: Origin, origHidden: CaptureSet.HiddenSet | Null)
153+
(using @constructorOnly ctx: Context)
154+
extends RootCapability:
155+
val hiddenSet =
156+
if origHidden == null then CaptureSet.HiddenSet(owner, this: @unchecked)
157+
else origHidden
152158
// fails initialization check without the @unchecked
153159

160+
def derivedFreshCap(newPrefix: Type)(using Context): FreshCap =
161+
if newPrefix eq prefix then this
162+
else if newPrefix eq hiddenSet.owningCap.prefix then
163+
hiddenSet.owningCap
164+
else
165+
hiddenSet.derivedCaps
166+
.getOrElseUpdate(newPrefix, FreshCap(newPrefix)(owner, origin, hiddenSet))
167+
168+
/** A map from context owners to skolem TermRefs that were created by ensurePath
169+
* TypeMap's mapCapability.
170+
*/
171+
var skolems: immutable.Map[Symbol, TermRef] = immutable.HashMap.empty
172+
173+
//assert(rootId != 10, i"fresh $prefix, ${ctx.owner}")
174+
154175
/** Is this fresh cap (definitely) classified? If that's the case, the
155176
* classifier cannot be changed anymore.
156177
* We need to distinguish `FreshCap`s that can still be classified from
@@ -167,12 +188,6 @@ object Capabilities:
167188
case _ => false
168189

169190
/** Is this fresh cap at the right level to be able to subsume `ref`?
170-
* Only outer freshes can be subsumed.
171-
* TODO Can we merge this with levelOK? Right now we use two different schemes:
172-
* - For level checking capsets with levelOK: Check that the visibility of the element
173-
* os not properly contained in the captset owner.
174-
* - For level checking elements subsumed by FreshCaps: Check that the widened scope
175-
* (using levelOwner) of the elements contains the owner of the FreshCap.
176191
*/
177192
def acceptsLevelOf(ref: Capability)(using Context): Boolean =
178193
if ccConfig.useFreshLevels && !CCState.collapseFresh then
@@ -203,8 +218,12 @@ object Capabilities:
203218
i"a fresh root capability$classifierStr$originStr"
204219

205220
object FreshCap:
221+
def apply(owner: Symbol, prefix: Type, origin: Origin)(using Context): FreshCap =
222+
new FreshCap(prefix)(owner, origin, null)
223+
def apply(owner: Symbol, origin: Origin)(using Context): FreshCap =
224+
apply(owner, owner.skipWeakOwner.thisType, origin)
206225
def apply(origin: Origin)(using Context): FreshCap =
207-
FreshCap(ctx.owner, origin)
226+
apply(ctx.owner, origin)
208227

209228
/** A root capability associated with a function type. These are conceptually
210229
* existentially quantified over the function's result type.
@@ -441,6 +460,7 @@ object Capabilities:
441460
* the form this.C but their pathroot is still this.C, not this.
442461
*/
443462
final def pathRoot(using Context): Capability = this match
463+
case FreshCap(pre: Capability) => pre.pathRoot
444464
case _: RootCapability => this
445465
case self: DerivedCapability => self.underlying.pathRoot
446466
case self: CoreCapability => self.dealias match
@@ -485,7 +505,13 @@ object Capabilities:
485505
case TermRef(prefix: Capability, _) => prefix.ccOwner
486506
case self: NamedType => self.symbol
487507
case self: DerivedCapability => self.underlying.ccOwner
488-
case self: FreshCap => self.hiddenSet.owner
508+
case self: FreshCap =>
509+
val setOwner = self.hiddenSet.owner
510+
self.prefix match
511+
case prefix: ThisType if setOwner.isTerm && setOwner.owner == prefix.cls =>
512+
setOwner
513+
case prefix: Capability => prefix.ccOwner
514+
case _ => setOwner
489515
case _ /* : GlobalCap | ResultCap | ParamRef */ => NoSymbol
490516

491517
final def visibility(using Context): Symbol = this match
@@ -732,12 +758,25 @@ object Capabilities:
732758
(this eq y)
733759
|| this.match
734760
case x: FreshCap =>
761+
def classifierOK =
762+
if y.tryClassifyAs(x.hiddenSet.classifier) then true
763+
else
764+
capt.println(i"$y cannot be classified as $x")
765+
false
766+
767+
def prefixAllowsAddHidden: Boolean =
768+
CCState.collapseFresh || x.prefix.match
769+
case NoPrefix => true
770+
case pre: ThisType => x.ccOwner.isContainedIn(pre.cls)
771+
case pre =>
772+
capt.println(i"fresh not open $x, ${x.rootId}, $pre, ${x.ccOwner.skipWeakOwner.thisType}")
773+
false
774+
735775
vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y)))
736776
|| x.acceptsLevelOf(y)
737-
&& ( y.tryClassifyAs(x.hiddenSet.classifier)
738-
|| { capt.println(i"$y cannot be classified as $x"); false }
739-
)
777+
&& classifierOK
740778
&& canAddHidden
779+
&& prefixAllowsAddHidden
741780
&& vs.addHidden(x.hiddenSet, y)
742781
case x: ResultCap =>
743782
val result = y match

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

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ import annotation.internal.sharable
1212
import reporting.trace
1313
import printing.{Showable, Printer}
1414
import printing.Texts.*
15-
import util.{SimpleIdentitySet, Property}
15+
import util.{SimpleIdentitySet, Property, EqHashMap}
1616
import typer.ErrorReporting.Addenda
1717
import scala.collection.{mutable, immutable}
1818
import TypeComparer.ErrorNote
@@ -560,8 +560,10 @@ object CaptureSet:
560560
def universal(using Context): Const =
561561
Const(SimpleIdentitySet(GlobalCap))
562562

563+
def fresh(owner: Symbol, prefix: Type, origin: Origin)(using Context): Const =
564+
FreshCap(owner, prefix, origin).singletonCaptureSet
563565
def fresh(origin: Origin)(using Context): Const =
564-
FreshCap(origin).singletonCaptureSet
566+
fresh(ctx.owner, ctx.owner.thisType, origin)
565567

566568
/** The shared capture set `{cap.rd}` */
567569
def shared(using Context): Const =
@@ -990,7 +992,7 @@ object CaptureSet:
990992
case _ => isSubsumed
991993
if !isSubsumed then
992994
if elem.origin != Origin.InDecl(owner) || elem.hiddenSet.isConst then
993-
val fc = new FreshCap(owner, Origin.InDecl(owner))
995+
val fc = FreshCap(owner, Origin.InDecl(owner))
994996
assert(fc.tryClassifyAs(elem.hiddenSet.classifier), fail)
995997
hideIn(fc)
996998
super.includeElem(fc)
@@ -1225,6 +1227,9 @@ object CaptureSet:
12251227

12261228
override def owner = givenOwner
12271229

1230+
/** The FreshCaps generated by derivedFreshCap, indexed by prefix */
1231+
val derivedCaps = new EqHashMap[Type, FreshCap]()
1232+
12281233
//assert(id != 3)
12291234

12301235
description = i"of elements subsumed by a fresh cap in $initialOwner"

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1939,6 +1939,7 @@ class CheckCaptures extends Recheck, SymTransformer:
19391939
private val setup: SetupAPI = thisPhase.prev.asInstanceOf[Setup]
19401940

19411941
override def checkUnit(unit: CompilationUnit)(using Context): Unit =
1942+
capt.println(i"cc check ${unit.source}")
19421943
ccState.start()
19431944
setup.setupUnit(unit.tpdTree, this)
19441945
collectCapturedMutVars.traverse(unit.tpdTree)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -690,7 +690,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
690690
if cls.derivesFrom(defn.Caps_Capability) then
691691
// If cls is a capability class, we need to add a fresh readonly capability to
692692
// ensure we cannot treat the class as pure.
693-
CaptureSet.fresh(Origin.InDecl(cls)).readOnly.subCaptures(cs)
693+
CaptureSet.fresh(cls, cls.thisType, Origin.InDecl(cls)).readOnly.subCaptures(cs)
694694
CapturingType(cinfo.selfType, cs)
695695

696696
// Compute new parent types

compiler/src/dotty/tools/dotc/core/Symbols.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -900,8 +900,8 @@ object Symbols extends SymUtils {
900900
/** Create a new skolem symbol. This is not the same as SkolemType, even though the
901901
* motivation (create a singleton referencing to a type) is similar.
902902
*/
903-
def newSkolem(tp: Type)(using Context): TermSymbol =
904-
newSymbol(defn.RootClass, nme.SKOLEM, SyntheticArtifact | NonMember | Permanent, tp)
903+
def newSkolem(owner: Symbol, tp: Type)(using Context): TermSymbol =
904+
newSymbol(owner, nme.SKOLEM, SyntheticArtifact | NonMember | Permanent, tp)
905905

906906
def newErrorSymbol(owner: Symbol, name: Name, msg: Message)(using Context): Symbol = {
907907
val errType = ErrorType(msg)

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

Lines changed: 27 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1706,11 +1706,10 @@ object Types extends TypeUtils {
17061706
if hasNext then current = f(current.asInstanceOf[TypeProxy])
17071707
res
17081708

1709-
/** A prefix-less refined this or a termRef to a new skolem symbol
1710-
* that has the given type as info.
1709+
/** A prefix-less TermRef to a new skolem symbol that has this type as info.
17111710
*/
1712-
def narrow(using Context): TermRef =
1713-
TermRef(NoPrefix, newSkolem(this))
1711+
def narrow(using Context)(owner: Symbol = defn.RootClass): TermRef =
1712+
TermRef(NoPrefix, newSkolem(owner, this))
17141713

17151714
/** Useful for diagnostics: The underlying type if this type is a type proxy,
17161715
* otherwise NoType
@@ -2319,14 +2318,14 @@ object Types extends TypeUtils {
23192318
override def dropIfProto = WildcardType
23202319
}
23212320

2322-
/** Implementations of this trait cache the results of `narrow`. */
2323-
trait NarrowCached extends Type {
2321+
/** Implementations of this trait cache the results of `narrow` if the owner is RootClass. */
2322+
trait NarrowCached extends Type:
23242323
private var myNarrow: TermRef | Null = null
2325-
override def narrow(using Context): TermRef = {
2326-
if (myNarrow == null) myNarrow = super.narrow
2327-
myNarrow.nn
2328-
}
2329-
}
2324+
override def narrow(using Context)(owner: Symbol): TermRef =
2325+
if owner == defn.RootClass then
2326+
if myNarrow == null then myNarrow = super.narrow(owner)
2327+
myNarrow.nn
2328+
else super.narrow(owner)
23302329

23312330
// --- NamedTypes ------------------------------------------------------------------
23322331

@@ -6330,6 +6329,23 @@ object Types extends TypeUtils {
63306329
null
63316330

63326331
def mapCapability(c: Capability, deep: Boolean = false): Capability | (CaptureSet, Boolean) = c match
6332+
case c @ FreshCap(prefix) =>
6333+
// If `pre` is not a path, transform it to a path starting with a skolem TermRef.
6334+
// We create at most one such skolem per FreshCap/context owner pair.
6335+
// This approximates towards creating fewer skolems than otherwise needed,
6336+
// which means we might get more separation conflicts than otherwise. But
6337+
// it's not clear we will get such conflicts anyway.
6338+
def ensurePath(pre: Type)(using Context): Type = pre match
6339+
case pre @ TermRef(pre1, _) => pre.withPrefix(ensurePath(pre1))
6340+
case NoPrefix | _: SingletonType => pre
6341+
case pre =>
6342+
c.skolems.get(ctx.owner) match
6343+
case Some(skolem) => skolem
6344+
case None =>
6345+
val skolem = pre.narrow(ctx.owner)
6346+
c.skolems = c.skolems.updated(ctx.owner, skolem)
6347+
skolem
6348+
c.derivedFreshCap(ensurePath(apply(prefix)))
63336349
case c: RootCapability => c
63346350
case Reach(c1) =>
63356351
mapCapability(c1, deep = true)

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

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -491,8 +491,13 @@ class PlainPrinter(_ctx: Context) extends Printer {
491491
def classified =
492492
if c.hiddenSet.classifier == defn.AnyClass then ""
493493
else s" classified as ${c.hiddenSet.classifier.name.show}"
494-
if ccVerbose then s"<fresh$idStr in ${c.ccOwner} hiding " ~ toTextCaptureSet(c.hiddenSet) ~ classified ~ ">"
495-
else "cap"
494+
def prefixTxt: Text = c.prefix match
495+
case NoPrefix | _: ThisType => ""
496+
case pre => pre.show ~ "."
497+
def core: Text =
498+
if ccVerbose then s"<fresh$idStr in ${c.ccOwner} hiding " ~ toTextCaptureSet(c.hiddenSet) ~ classified ~ ">"
499+
else "cap"
500+
prefixTxt ~ core
496501
case tp: TypeProxy =>
497502
homogenize(tp) match
498503
case tp: SingletonType => toTextRef(tp)

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -395,7 +395,7 @@ object SpaceEngine {
395395

396396
case _ =>
397397
// Pattern is an arbitrary expression; assume a skolem (i.e. an unknown value) of the pattern type
398-
Typ(pat.tpe.narrow, decomposed = false)
398+
Typ(pat.tpe.narrow(), decomposed = false)
399399
})
400400

401401
private def project(tp: Type)(using Context): Space = tp match {

compiler/src/dotty/tools/dotc/typer/Applications.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -337,7 +337,7 @@ object Applications {
337337
case pre: SingletonType => singleton(pre, needLoad = !testOnly)
338338
case pre if testOnly =>
339339
// In this case it is safe to skolemize now; we will produce a stable prefix for the actual call.
340-
ref(pre.narrow)
340+
ref(pre.narrow())
341341
case _ => EmptyTree
342342

343343
if fn.symbol.hasDefaultParams then
@@ -1845,7 +1845,7 @@ trait Applications extends Compatibility {
18451845
case methRef: TermRef if methRef.widenSingleton.isInstanceOf[MethodicType] =>
18461846
p(methRef)
18471847
case mt: MethodicType =>
1848-
p(mt.narrow)
1848+
p(mt.narrow())
18491849
case _ =>
18501850
followApply && tp.member(nme.apply).hasAltWith(d => p(TermRef(tp, nme.apply, d)))
18511851
}

0 commit comments

Comments
 (0)