Skip to content

Commit

Permalink
Implement fresh capabilities
Browse files Browse the repository at this point in the history 
These are represented as Fresh.Cap(hidden) where hidden is the set of
capabilities subsumed by a fresh. The underlying representation is as
an annotated type `T @annotation.internal.freshCapability`.
  • Loading branch information
@odersky
odersky committed Jan 11, 2025
1 parent ab6b979 commit 314cdc5
Show file tree
Hide file tree
Showing 18 changed files with 521 additions and 185 deletions.
40 changes: 34 additions & 6 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,14 @@ import config.Feature
import collection.mutable
import CCState.*
import reporting.Message
import CaptureSet.VarState

/** Attachment key for capturing type trees */
private val Captures: Key[CaptureSet] = Key()

/** Context property to print Fresh.Cap as "fresh" instead of "cap" */
val PrintFresh: Key[Unit] = Key()

object ccConfig:

/** If true, allow mapping capture set variables under captureChecking with maps that are neither
Expand Down Expand Up @@ -47,6 +52,10 @@ object ccConfig:
def useSealed(using Context) =
Feature.sourceVersion.stable != SourceVersion.`3.5`

/** If true, turn on separation checking */
def useFresh(using Context): Boolean =
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`future`)

end ccConfig

/** Are we at checkCaptures phase? */
Expand Down Expand Up @@ -193,10 +202,7 @@ extension (tp: Type)
case tp: TypeParamRef =>
tp.derivesFrom(defn.Caps_CapSet)
case AnnotatedType(parent, annot) =>
(annot.symbol == defn.ReachCapabilityAnnot
|| annot.symbol == defn.MaybeCapabilityAnnot
|| annot.symbol == defn.ReadOnlyCapabilityAnnot
) && parent.isTrackableRef
defn.capabilityWrapperAnnots.contains(annot.symbol) && parent.isTrackableRef
case _ =>
false

Expand Down Expand Up @@ -244,7 +250,7 @@ extension (tp: Type)
* the two capture sets are combined.
*/
def capturing(cs: CaptureSet)(using Context): Type =
if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, frozen = true).isOK)
if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, VarState.Separate).isOK)
&& !cs.keepAlways
then tp
else tp match
Expand Down Expand Up @@ -421,6 +427,10 @@ extension (tp: Type)
mapOver(t)
tm(tp)

def hasUseAnnot(using Context): Boolean = tp match
case AnnotatedType(_, ann) => ann.symbol == defn.UseAnnot
case _ => false

/** If `x` is a capture ref, its maybe capability `x?`, represented internally
* as `x @maybeCapability`. `x?` stands for a capability `x` that might or might
* not be part of a capture set. We have `{} <: {x?} <: {x}`. Maybe capabilities
Expand Down Expand Up @@ -512,6 +522,24 @@ extension (tp: Type)
tp
case _ =>
tp
end withReachCaptures

/** Does this type contain no-flip covariant occurrences of `cap`? */
def containsCap(using Context): Boolean =
val acc = new TypeAccumulator[Boolean]:
def apply(x: Boolean, t: Type) =
x
|| variance > 0 && t.dealiasKeepAnnots.match
case t @ CapturingType(p, cs) if cs.containsCap =>
true
case t @ AnnotatedType(parent, ann) =>
// Don't traverse annotations, which includes capture sets
this(x, parent)
case Existential(_, _) =>
false
case _ =>
foldOver(x, t)
acc(false, tp)

def level(using Context): Level =
tp match
Expand Down Expand Up @@ -690,7 +718,7 @@ abstract class AnnotatedCapability(annot: Context ?=> ClassSymbol):
case _ =>
AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
case AnnotatedType(parent: CaptureRef, ann) if ann.symbol == annot => Some(parent)
case AnnotatedType(parent: CaptureRef, ann) if ann.hasSymbol(annot) => Some(parent)
case _ => None
protected def unwrappable(using Context): Set[Symbol]

Expand Down
46 changes: 39 additions & 7 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import CCState.*
import Periods.NoRunId
import compiletime.uninitialized
import StdNames.nme
import CaptureSet.VarState

/** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
* as well as three kinds of AnnotatedTypes representing readOnly, reach, and maybe capabilities.
Expand Down Expand Up @@ -78,15 +79,24 @@ trait CaptureRef extends TypeProxy, ValueType:
case tp: TermRef => tp.name == nme.CAPTURE_ROOT && tp.symbol == defn.captureRoot
case _ => false

/** Is this reference a Fresh.Cap instance? */
final def isFresh(using Context): Boolean = this match
case Fresh.Cap(_) => true
case _ => false

/** Is this reference the generic root capability `cap` or a Fresh.Cap instance? */
final def isCapOrFresh(using Context): Boolean = isCap || isFresh

/** Is this reference one the generic root capabilities `cap` or `cap.rd` ? */
final def isRootCapability(using Context): Boolean = this match
case ReadOnlyCapability(tp1) => tp1.isCap
case _ => isCap
case ReadOnlyCapability(tp1) => tp1.isCapOrFresh
case _ => isCapOrFresh

/** Is this reference capability that does not derive from another capability ? */
final def isMaxCapability(using Context): Boolean = this match
case tp: TermRef => tp.isCap || tp.info.derivesFrom(defn.Caps_Exists)
case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
case Fresh.Cap(_) => true
case ReadOnlyCapability(tp1) => tp1.isMaxCapability
case _ => false

Expand Down Expand Up @@ -137,26 +147,27 @@ trait CaptureRef extends TypeProxy, ValueType:
* Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y
* Contains[X, y] ==> X subsumes y
*
* TODO: Document cases with more comments.
* TODO: Move to CaptureSet
*/
final def subsumes(y: CaptureRef)(using Context): Boolean =
final def subsumes(y: CaptureRef)(using ctx: Context, vs: VarState = VarState.Separate): Boolean =

def subsumingRefs(x: Type, y: Type): Boolean = x match
case x: CaptureRef => y match
case y: CaptureRef => x.subsumes(y)
case _ => false
case _ => false

def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.match
def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.dealias match
case info: SingletonCaptureRef => test(info)
case CapturingType(parent, _) => viaInfo(parent)(test)
case info: AndType => viaInfo(info.tp1)(test) || viaInfo(info.tp2)(test)
case info: OrType => viaInfo(info.tp1)(test) && viaInfo(info.tp2)(test)
case _ => false

(this eq y)
|| this.isCap
|| maxSubsumes(y, canAddHidden = !vs.isOpen)
|| y.match
case y: TermRef if !y.isRootCapability =>
case y: TermRef if !y.isCap =>
y.prefix.match
case ypre: CaptureRef =>
this.subsumes(ypre)
Expand Down Expand Up @@ -201,6 +212,27 @@ trait CaptureRef extends TypeProxy, ValueType:
case _ => false
end subsumes

/** This is a maximal capabaility that subsumes `y` in given context and VarState.
* @param canAddHidden If true we allow maximal capabilties to subsume all other capabilities.
* We add those capabilities to the hidden set if this is Fresh.Cap
* If false we only accept `y` elements that are already in the
* hidden set of this Fresh.Cap. The idea is that in a VarState that
* accepts additions we first run `maxSubsumes` with `canAddHidden = false`
* so that new variables get added to the sets. If that fails, we run
* the test again with canAddHidden = true as a last effort before we
* fail a comparison.
*/
def maxSubsumes(y: CaptureRef, canAddHidden: Boolean)(using ctx: Context, vs: VarState = VarState.Separate): Boolean =
this.match
case Fresh.Cap(hidden) =>
vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
|| !y.stripReadOnly.isCap && canAddHidden && vs.addHidden(hidden, y)
case _ =>
this.isCap && canAddHidden
|| y.match
case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
case _ => false

def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] =
CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)

Expand Down
Loading

0 comments on commit 314cdc5

Please sign in to comment.