Skip to content

Prepare for Type/Capability split #23171

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CaptureAnnotation.scala
Original file line number Diff line number Diff line change
Expand Up @@ -63,9 +63,11 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte

override def mapWith(tm: TypeMap)(using Context) =
val elems = refs.elems.toList
val elems1 = elems.mapConserve(tm)
val elems1 = elems.mapConserve(tm.mapCapability(_))
if elems1 eq elems then this
else if elems1.forall(_.isTrackableRef)
else if elems1.forall:
case elem1: CaptureRef => elem1.isTrackableRef
case _ => false
then derivedAnnotation(CaptureSet(elems1.asInstanceOf[List[CaptureRef]]*), boxed)
else EmptyAnnotation

Expand Down
17 changes: 11 additions & 6 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,7 @@ extension (tp: Type)
!tp.underlying.exists // might happen during construction of lambdas
|| tp.derivesFrom(defn.Caps_CapSet)
case root.Result(_) => true
case root.Fresh(_) => true
case AnnotatedType(parent, annot) =>
defn.capabilityWrapperAnnots.contains(annot.symbol) && parent.isTrackableRef
case _ =>
Expand Down Expand Up @@ -143,9 +144,9 @@ extension (tp: Type)
if dcs.isAlwaysEmpty then tp.captureSet
else tp match
case tp @ ReachCapability(_) =>
tp.singletonCaptureSet
assert(false); tp.singletonCaptureSet
case ReadOnlyCapability(ref) =>
ref.deepCaptureSet(includeTypevars).readOnly
assert(false); ref.deepCaptureSet(includeTypevars).readOnly
case tp: SingletonCaptureRef if tp.isTrackableRef =>
tp.reach.singletonCaptureSet
case _ =>
Expand Down Expand Up @@ -195,9 +196,12 @@ extension (tp: Type)
* are of the form this.C but their pathroot is still this.C, not this.
*/
final def pathRoot(using Context): Type = tp.dealias match
case tp1: NamedType
if tp1.symbol.maybeOwner.isClass && tp1.symbol != defn.captureRoot && !tp1.symbol.is(TypeParam) =>
tp1.prefix.pathRoot
case tp1: NamedType =>
if tp1.symbol.maybeOwner.isClass && tp1.symbol != defn.captureRoot && !tp1.symbol.is(TypeParam) then
tp1.prefix match
case pre: CaptureRef => pre.pathRoot
case _ => tp1
else tp1
case tp1 => tp1

/** If this part starts with `C.this`, the class `C`.
Expand All @@ -214,7 +218,8 @@ extension (tp: Type)
tp1.prefix match
case _: ThisType | NoPrefix =>
tp1.symbol.is(Param) || tp1.symbol.is(ParamAccessor)
case prefix => prefix.isParamPath
case prefix: CaptureRef => prefix.isParamPath
case _ => false
case _: ParamRef => true
case _ => false

Expand Down
44 changes: 24 additions & 20 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -139,9 +139,10 @@ trait CaptureRef extends TypeProxy, ValueType:
hidden.owner
case ref: NamedType =>
if ref.isCap then NoSymbol
else ref.prefix match
case prefix: CaptureRef => prefix.ccOwner
case _ => ref.symbol
else ref.pathRoot match
case ref: ThisType => ref.cls
case ref: NamedType => ref.symbol
case _ => NoSymbol
case ref: ThisType =>
ref.cls
case QualifiedCapability(ref1) =>
Expand Down Expand Up @@ -222,7 +223,7 @@ trait CaptureRef extends TypeProxy, ValueType:
def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.dealias match
case info: SingletonCaptureRef => test(info)
case CapturingType(parent, _) =>
if this.derivesFrom(defn.Caps_CapSet) then test(info)
if this.derivesFrom(defn.Caps_CapSet) && false then test(info)
/*
If `this` is a capture set variable `C^`, then it is possible that it can be
reached from term variables in a reachability chain through the context.
Expand All @@ -235,7 +236,7 @@ trait CaptureRef extends TypeProxy, ValueType:
case info: OrType => viaInfo(info.tp1)(test) && viaInfo(info.tp2)(test)
case _ => false

(this eq y)
try (this eq y)
|| maxSubsumes(y, canAddHidden = !vs.isOpen)
|| y.match
case y: TermRef if !y.isCap =>
Expand All @@ -262,9 +263,13 @@ trait CaptureRef extends TypeProxy, ValueType:
// They can be other capture set variables, which are bounded by `CapSet`,
// like `def test[X^, Y^, Z >: X <: Y]`.
y.info match
case TypeBounds(_, hi: CaptureRef) => this.subsumes(hi)
case TypeBounds(_, hi @ CapturingType(parent, refs)) if parent.derivesFrom(defn.Caps_CapSet) =>
refs.elems.forall(this.subsumes)
case TypeBounds(_, hi: CaptureRef) =>
this.subsumes(hi)
case _ => y.captureSetOfInfo.elems.forall(this.subsumes)
case CapturingType(parent, refs) if parent.derivesFrom(defn.Caps_CapSet) || this.derivesFrom(defn.Caps_CapSet) =>
assert(false, this)
/* The second condition in the guard is for `this` being a `CapSet^{a,b...}` and etablishing a
potential reachability chain through `y`'s capture to a binding with
`this`'s capture set (cf. `CapturingType` case in `def viaInfo` above for more context).
Expand All @@ -277,13 +282,18 @@ trait CaptureRef extends TypeProxy, ValueType:
case x: TypeRef if assumedContainsOf(x).contains(y) => true
case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
x.info match
case TypeBounds(lo @ CapturingType(parent, refs), _) if parent.derivesFrom(defn.Caps_CapSet) =>
refs.elems.exists(_.subsumes(y))
case TypeBounds(lo: CaptureRef, _) =>
lo.subsumes(y)
case _ =>
x.captureSetOfInfo.elems.exists(_.subsumes(y))
case CapturingType(parent, refs) if parent.derivesFrom(defn.Caps_CapSet) =>
refs.elems.exists(_.subsumes(y))
assert(false, this)
case _ => false
catch case ex: AssertionError =>
println(i"error while subsumes $this >> $y")
throw ex
end subsumes

/** This is a maximal capability that subsumes `y` in given context and VarState.
Expand Down Expand Up @@ -312,7 +322,7 @@ trait CaptureRef extends TypeProxy, ValueType:
else
!y.stripReadOnly.isCap
&& !yIsExistential
&& !y.isInstanceOf[ParamRef]
&& !y.stripReadOnly.isInstanceOf[ParamRef]

vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
|| levelOK
Expand All @@ -325,21 +335,15 @@ trait CaptureRef extends TypeProxy, ValueType:
if !result then
ccState.addNote(CaptureSet.ExistentialSubsumesFailure(x, y))
result
case _ if this.isCap =>
if y.isCap then true
else if yIsExistential then false
else y.derivesFromSharedCapability
|| canAddHidden && vs != VarState.HardSeparate && CCState.capIsRoot
case _ =>
y match
case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
case _ if this.isCap =>
y.isCap
|| y.derivesFromSharedCapability
|| !yIsExistential
&& canAddHidden
&& vs != VarState.HardSeparate
&& (CCState.capIsRoot
// || { println(i"no longer $this maxSubsumes $y, ${y.isCap}"); false } // debug
)
|| false
case _ =>
false
case _ => false

/** `x covers y` if we should retain `y` when computing the overlap of
* two footprints which have `x` respectively `y` as elements.
Expand Down
34 changes: 16 additions & 18 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,7 @@ sealed abstract class CaptureSet extends Showable:
def map(tm: TypeMap)(using Context): CaptureSet =
tm match
case tm: BiTypeMap =>
val mappedElems = elems.map(tm.forward)
val mappedElems = elems.map(tm.mapCapability(_))
if isConst then
if mappedElems == elems then this
else Const(mappedElems)
Expand Down Expand Up @@ -487,7 +487,7 @@ object CaptureSet:
override def toString = elems.toString
end Const

case class EmptyWithProvenance(ref: CaptureRef, mapped: Type) extends Const(SimpleIdentitySet.empty):
case class EmptyWithProvenance(ref: CaptureRef, mapped: CaptureSet) extends Const(SimpleIdentitySet.empty):
override def optionalInfo(using Context): String =
if ctx.settings.YccDebug.value
then i" under-approximating the result of mapping $ref to $mapped"
Expand Down Expand Up @@ -587,8 +587,7 @@ object CaptureSet:
*/
private def checkSkippedMaps(elem: CaptureRef)(using Context): Unit =
for tm <- skippedMaps do
val elem1 = tm(elem)
for elem1 <- tm(elem).captureSet.elems do
for elem1 <- extrapolateCaptureRef(elem, tm, variance = 1).elems do
assert(elem.subsumes(elem1),
i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this")

Expand Down Expand Up @@ -817,14 +816,14 @@ object CaptureSet:

override def tryInclude(elem: CaptureRef, origin: CaptureSet)(using Context, VarState): CompareResult =
if origin eq source then
val mappedElem = bimap.forward(elem)
val mappedElem = bimap.mapCapability(elem)
if accountsFor(mappedElem) then CompareResult.OK
else addNewElem(mappedElem)
else if accountsFor(elem) then
CompareResult.OK
else
try
source.tryInclude(bimap.backward(elem), this)
source.tryInclude(bimap.inverse.mapCapability(elem), this)
.showing(i"propagating new elem $elem backward from $this to $source = $result", captDebug)
.andAlso(addNewElem(elem))
catch case ex: AssertionError =>
Expand Down Expand Up @@ -1031,15 +1030,12 @@ object CaptureSet:
* - Otherwise assertion failure
*/
def extrapolateCaptureRef(r: CaptureRef, tm: TypeMap, variance: Int)(using Context): CaptureSet =
val r1 = tm(r)
val upper = r1.captureSet
def isExact =
upper.isAlwaysEmpty
|| upper.isConst && upper.elems.size == 1 && upper.elems.contains(r1)
|| r.derivesFrom(defn.Caps_CapSet)
if variance > 0 || isExact then upper
else if variance < 0 then CaptureSet.EmptyWithProvenance(r, r1)
else upper.maybe
tm.mapCapability(r) match
case c: CaptureRef => c.captureSet
case (cs: CaptureSet, exact) =>
if cs.isAlwaysEmpty || exact || variance > 0 then cs
else if variance < 0 then CaptureSet.EmptyWithProvenance(r, cs)
else cs.maybe

/** Apply `f` to each element in `xs`, and join result sets with `++` */
def mapRefs(xs: Refs, f: CaptureRef => CaptureSet)(using Context): CaptureSet =
Expand Down Expand Up @@ -1289,9 +1285,11 @@ object CaptureSet:

def mapRef(ref: CaptureRef): CaptureRef

def apply(t: Type) = t match
case t: CaptureRef if t.isTrackableRef => mapRef(t)
case _ => mapOver(t)
def apply(t: Type) = mapOver(t)

override def mapCapability(c: CaptureRef, deep: Boolean): CaptureRef = c match
case c: CaptureRef if c.isTrackableRef => mapRef(c)
case _ => super.mapCapability(c, deep)

override def fuse(next: BiTypeMap)(using Context) = next match
case next: Inverse if next.inverse.getClass == getClass => assert(false); Some(IdentityTypeMap)
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -441,7 +441,7 @@ class CheckCaptures extends Recheck, SymTransformer:
markFree(sym, sym.termRef, tree)

def markFree(sym: Symbol, ref: CaptureRef, tree: Tree)(using Context): Unit =
if sym.exists && ref.isTracked then markFree(ref.captureSet, tree)
if sym.exists && ref.isTracked then markFree(ref.singletonCaptureSet, tree)

/** Make sure the (projected) `cs` is a subset of the capture sets of all enclosing
* environments. At each stage, only include references from `cs` that are outside
Expand Down
28 changes: 19 additions & 9 deletions compiler/src/dotty/tools/dotc/cc/Setup.scala
Original file line number Diff line number Diff line change
Expand Up @@ -209,6 +209,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
innerApply(tp)
finally isTopLevel = saved

override def mapArg(arg: Type, tparam: ParamInfo): Type =
super.mapArg(Recheck.mapExprType(arg), tparam)

/** Map parametric functions with results that have a capture set somewhere
* to dependent functions.
*/
Expand Down Expand Up @@ -504,12 +507,15 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
def add = new TypeTraverser:
var reach = false
def traverse(t: Type): Unit = t match
case root.Fresh(hidden) =>
if reach then hidden.elems += ref.reach
else if ref.isTracked then hidden.elems += ref
case t @ CapturingType(_, _) if t.isBoxed && !reach =>
reach = true
try traverseChildren(t) finally reach = false
case t @ CapturingType(parent, refs) =>
val saved = reach
reach |= t.isBoxed
try
traverse(parent)
for case root.Fresh(hidden) <- refs.elems.iterator do
if reach then hidden.elems += ref.reach
else if ref.isTracked then hidden.elems += ref
finally reach = saved
case _ =>
traverseChildren(t)
if ref.isTrackableRef then add.traverse(tp)
Expand Down Expand Up @@ -660,9 +666,13 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:

def paramsToCap(mt: Type)(using Context): Type = mt match
case mt: MethodType =>
mt.derivedLambdaType(
paramInfos = mt.paramInfos.map(root.freshToCap),
resType = paramsToCap(mt.resType))
try
mt.derivedLambdaType(
paramInfos = mt.paramInfos.map(root.freshToCap),
resType = paramsToCap(mt.resType))
catch case ex: AssertionError =>
println(i"error while mapping params ${mt.paramInfos} of $sym")
throw ex
case mt: PolyType =>
mt.derivedLambdaType(resType = paramsToCap(mt.resType))
case _ => mt
Expand Down
Loading
Loading