Skip to content

Commit ae49d34

Browse files
oderskyodersky
committed
Introduce only-capabilities
Basic representations and definitions, so that we can parse only-capabilities, convert them to internal representation `Restrict(c, cls)`, not crash on them during capture checking and print them out correctly.
1 parent d6a9d44 commit ae49d34

File tree

15 files changed

+144
-28
lines changed

15 files changed

+144
-28
lines changed

‎compiler/src/dotty/tools/dotc/ast/untpd.scala‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -556,6 +556,9 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
556556
def makeReadOnlyAnnot()(using Context): Tree =
557557
New(ref(defn.ReadOnlyCapabilityAnnot.typeRef), Nil :: Nil)
558558

559+
def makeOnlyAnnot(qid: Tree)(using Context) =
560+
New(AppliedTypeTree(ref(defn.OnlyCapabilityAnnot.typeRef), qid :: Nil), Nil :: Nil)
561+
559562
def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
560563
DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)
561564

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

Lines changed: 59 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,9 @@ import annotation.internal.sharable
3939
* | +-- SetCapability -----+-- TypeRef
4040
* | +-- TypeParamRef
4141
* |
42-
* +-- DerivedCapability -+-- ReadOnly
43-
* +-- Reach
42+
* +-- DerivedCapability -+-- Reach
43+
* +-- Only
44+
* +-- ReadOnly
4445
* +-- Maybe
4546
*
4647
* All CoreCapabilities are Types, or, more specifically instances of TypeProxy.
@@ -96,9 +97,18 @@ object Capabilities:
9697
* but they can wrap reach capabilities. We have
9798
* (x?).readOnly = (x.rd)?
9899
*/
99-
case class ReadOnly(underlying: ObjectCapability | RootCapability | Reach)
100-
extends DerivedCapability:
101-
assert(!underlying.isInstanceOf[Maybe])
100+
case class ReadOnly(underlying: ObjectCapability | RootCapability | Reach | Restricted)
101+
extends DerivedCapability
102+
103+
/** The restricted capability `x.only[C]`. We have {x.only[C]} <: {x}.
104+
*
105+
* Restricted capabilities cannot wrap maybe capabilities or read-only capabilities
106+
* but they can wrap reach capabilities. We have
107+
* (x?).restrict[T] = (x.restrict[T])?
108+
* (x.rd).restrict[T] = (x.restrict[T]).rd
109+
*/
110+
case class Restricted(underlying: ObjectCapability | RootCapability | Reach, cls: ClassSymbol)
111+
extends DerivedCapability
102112

103113
/** If `x` is a capability, its reach capability `x*`. `x*` stands for all
104114
* capabilities reachable through `x`.
@@ -109,11 +119,11 @@ object Capabilities:
109119
*
110120
* Reach capabilities cannot wrap read-only capabilities or maybe capabilities.
111121
* We have
112-
* (x.rd).reach = x*.rd
113-
* (x.rd)? = (x*)?
122+
* (x?).reach = (x.reach)?
123+
* (x.rd).reach = (x.reach).rd
124+
* (x.only[T]).reach = (x*).only[T]
114125
*/
115-
case class Reach(underlying: ObjectCapability) extends DerivedCapability:
116-
assert(!underlying.isInstanceOf[Maybe | ReadOnly])
126+
case class Reach(underlying: ObjectCapability) extends DerivedCapability
117127

118128
/** The global root capability referenced as `caps.cap`
119129
* `cap` does not subsume other capabilities, except in arguments of
@@ -124,6 +134,7 @@ object Capabilities:
124134
def descr(using Context) = "the universal root capability"
125135
override val maybe = Maybe(this)
126136
override val readOnly = ReadOnly(this)
137+
override def restrict(cls: ClassSymbol)(using Context) = Restricted(this, cls)
127138
override def reach = unsupported("cap.reach")
128139
override def singletonCaptureSet(using Context) = CaptureSet.universal
129140
override def captureSetOfInfo(using Context) = singletonCaptureSet
@@ -242,7 +253,7 @@ object Capabilities:
242253
/** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
243254
* as well as three kinds of AnnotatedTypes representing readOnly, reach, and maybe capabilities.
244255
* If there are several annotations they come with an order:
245-
* `*` first, `.rd` next, `?` last.
256+
* `*` first, `.only` next, `.rd` next, `?` last.
246257
*/
247258
trait Capability extends Showable:
248259

@@ -254,7 +265,15 @@ object Capabilities:
254265
protected def cached[C <: DerivedCapability](newRef: C): C =
255266
def recur(refs: List[DerivedCapability]): C = refs match
256267
case ref :: refs1 =>
257-
if ref.getClass == newRef.getClass then ref.asInstanceOf[C] else recur(refs1)
268+
val exists = ref match
269+
case Restricted(_, cls) =>
270+
newRef match
271+
case Restricted(_, newCls) => cls == newCls
272+
case _ => false
273+
case _ =>
274+
ref.getClass == newRef.getClass
275+
if exists then ref.asInstanceOf[C]
276+
else recur(refs1)
258277
case Nil =>
259278
myDerived = newRef :: myDerived
260279
newRef
@@ -267,11 +286,24 @@ object Capabilities:
267286
def readOnly: ReadOnly | Maybe = this match
268287
case Maybe(ref1) => Maybe(ref1.readOnly)
269288
case self: ReadOnly => self
270-
case self: (ObjectCapability | RootCapability | Reach) => cached(ReadOnly(self))
271-
272-
def reach: Reach | ReadOnly | Maybe = this match
289+
case self: (ObjectCapability | RootCapability | Reach | Restricted) => cached(ReadOnly(self))
290+
291+
def restrict(cls: ClassSymbol)(using Context): Restricted | ReadOnly | Maybe = this match
292+
case Maybe(ref1) => Maybe(ref1.restrict(cls))
293+
case ReadOnly(ref1) => ReadOnly(ref1.restrict(cls).asInstanceOf[Restricted])
294+
case self @ Restricted(ref1, prevCls) =>
295+
val combinedCls =
296+
if prevCls.isSubClass(cls) then prevCls
297+
else if cls.isSubClass(prevCls) then cls
298+
else defn.NothingClass
299+
if combinedCls == prevCls then self
300+
else cached(Restricted(ref1, combinedCls))
301+
case self: (ObjectCapability | RootCapability | Reach) => cached(Restricted(self, cls))
302+
303+
def reach: Reach | Restricted | ReadOnly | Maybe = this match
273304
case Maybe(ref1) => Maybe(ref1.reach)
274-
case ReadOnly(ref1) => ReadOnly(ref1.reach.asInstanceOf[Reach])
305+
case ReadOnly(ref1) => ReadOnly(ref1.reach.asInstanceOf[Reach | Restricted])
306+
case Restricted(ref1, cls) => Restricted(ref1.reach.asInstanceOf[Reach], cls)
275307
case self: Reach => self
276308
case self: ObjectCapability => cached(Reach(self))
277309

@@ -285,6 +317,12 @@ object Capabilities:
285317
case tp: SetCapability => tp.captureSetOfInfo.isReadOnly
286318
case _ => this ne stripReadOnly
287319

320+
final def restriction(using Context): Symbol = this match
321+
case Restricted(_, cls) => cls
322+
case ReadOnly(ref1) => ref1.restriction
323+
case Maybe(ref1) => ref1.restriction
324+
case _ => NoSymbol
325+
288326
/** Is this a reach reference of the form `x*` or a readOnly or maybe variant
289327
* of a reach reference?
290328
*/
@@ -299,6 +337,12 @@ object Capabilities:
299337
case Maybe(ref1) => ref1.stripReadOnly.maybe
300338
case _ => this
301339

340+
final def stripRestricted(using Context): Capability = this match
341+
case Restricted(ref1, _) => ref1
342+
case ReadOnly(ref1) => ref1.stripRestricted.readOnly
343+
case Maybe(ref1) => ref1.stripRestricted.maybe
344+
case _ => this
345+
302346
final def stripReach(using Context): Capability = this match
303347
case Reach(ref1) => ref1
304348
case ReadOnly(ref1) => ref1.stripReach.readOnly

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

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,8 @@ extension (tp: Type)
8080
tp1.toCapability.reach
8181
case ReadOnlyCapability(tp1) =>
8282
tp1.toCapability.readOnly
83+
case OnlyCapability(tp1, cls) =>
84+
tp1.toCapability.restrict(cls) // for now
8385
case ref: TermRef if ref.isCapRef =>
8486
GlobalCap
8587
case ref: Capability if ref.isTrackableRef =>
@@ -587,7 +589,6 @@ abstract class AnnotatedCapability(annotCls: Context ?=> ClassSymbol):
587589
def unapply(tree: AnnotatedType)(using Context): Option[Type] = tree match
588590
case AnnotatedType(parent: Type, ann) if ann.hasSymbol(annotCls) => Some(parent)
589591
case _ => None
590-
591592
end AnnotatedCapability
592593

593594
/** An extractor for `ref @readOnlyCapability`, which is used to express
@@ -605,6 +606,17 @@ object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot)
605606
*/
606607
object MaybeCapability extends AnnotatedCapability(defn.MaybeCapabilityAnnot)
607608

609+
object OnlyCapability:
610+
def apply(tp: Type, cls: ClassSymbol)(using Context): AnnotatedType =
611+
AnnotatedType(tp,
612+
Annotation(defn.OnlyCapabilityAnnot.typeRef.appliedTo(cls.typeRef), Nil, util.Spans.NoSpan))
613+
614+
def unapply(tree: AnnotatedType)(using Context): Option[(Type, ClassSymbol)] = tree match
615+
case AnnotatedType(parent: Type, ann) if ann.hasSymbol(defn.OnlyCapabilityAnnot) =>
616+
Some((parent, ann.tree.tpe.argTypes.head.classSymbol.asClass))
617+
case _ => None
618+
end OnlyCapability
619+
608620
/** An extractor for all kinds of function types as well as method and poly types.
609621
* It includes aliases of function types such as `=>`. TODO: Can we do without?
610622
* @return 1st half: The argument types or empty if this is a type function

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

Lines changed: 16 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -403,6 +403,8 @@ sealed abstract class CaptureSet extends Showable:
403403

404404
def maybe(using Context): CaptureSet = map(MaybeMap())
405405

406+
def restrict(cls: ClassSymbol)(using Context): CaptureSet = map(RestrictMap(cls))
407+
406408
def readOnly(using Context): CaptureSet =
407409
val res = map(ReadOnlyMap())
408410
if mutability != Ignored then res.mutability = Reader
@@ -1344,9 +1346,10 @@ object CaptureSet:
13441346

13451347
/** A template for maps on capabilities where f(c) <: c and f(f(c)) = c */
13461348
private abstract class NarrowingCapabilityMap(using Context) extends BiTypeMap:
1347-
13481349
def apply(t: Type) = mapOver(t)
13491350

1351+
protected def isSameMap(other: BiTypeMap) = other.getClass == getClass
1352+
13501353
override def fuse(next: BiTypeMap)(using Context) = next match
13511354
case next: Inverse if next.inverse.getClass == getClass => Some(IdentityTypeMap)
13521355
case next: NarrowingCapabilityMap if next.getClass == getClass => Some(this)
@@ -1358,8 +1361,8 @@ object CaptureSet:
13581361
def inverse = NarrowingCapabilityMap.this
13591362
override def toString = NarrowingCapabilityMap.this.toString ++ ".inverse"
13601363
override def fuse(next: BiTypeMap)(using Context) = next match
1361-
case next: NarrowingCapabilityMap if next.inverse.getClass == getClass => Some(IdentityTypeMap)
1362-
case next: NarrowingCapabilityMap if next.getClass == getClass => Some(this)
1364+
case next: NarrowingCapabilityMap if isSameMap(next.inverse) => Some(IdentityTypeMap)
1365+
case next: NarrowingCapabilityMap if isSameMap(next) => Some(this)
13631366
case _ => None
13641367

13651368
lazy val inverse = Inverse()
@@ -1375,6 +1378,13 @@ object CaptureSet:
13751378
override def mapCapability(c: Capability, deep: Boolean) = c.readOnly
13761379
override def toString = "ReadOnly"
13771380

1381+
private class RestrictMap(val cls: ClassSymbol)(using Context) extends NarrowingCapabilityMap:
1382+
override def mapCapability(c: Capability, deep: Boolean) = c.restrict(cls)
1383+
override def toString = "Restrict"
1384+
override def isSameMap(other: BiTypeMap) = other match
1385+
case other: RestrictMap => cls == other.cls
1386+
case _ => false
1387+
13781388
/* Not needed:
13791389
def ofClass(cinfo: ClassInfo, argTypes: List[Type])(using Context): CaptureSet =
13801390
CaptureSet.empty
@@ -1402,6 +1412,9 @@ object CaptureSet:
14021412
case Reach(c1) =>
14031413
c1.widen.deepCaptureSet(includeTypevars = true)
14041414
.showing(i"Deep capture set of $c: ${c1.widen} = ${result}", capt)
1415+
case Restricted(c1, cls) =>
1416+
if cls == defn.NothingClass then CaptureSet.empty
1417+
else c1.captureSetOfInfo.restrict(cls) // todo: should we simplify using subsumption here?
14051418
case ReadOnly(c1) =>
14061419
c1.captureSetOfInfo.readOnly
14071420
case Maybe(c1) =>

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -113,6 +113,8 @@ object CheckCaptures:
113113
report.error(em"Cannot form a reach capability from `cap`", ann.srcPos)
114114
case ReadOnlyCapability(ref) =>
115115
check(ref)
116+
case OnlyCapability(ref, cls) =>
117+
check(ref)
116118
case tpe =>
117119
report.error(em"$elem: $tpe is not a legal element of a capture set", ann.srcPos)
118120
ann.retainedSet.retainedElementsRaw.foreach(check)

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,7 @@ object SepCheck:
256256

257257
def hiddenByElem(elem: Capability): Refs = elem match
258258
case elem: FreshCap => elem.hiddenSet.elems ++ recur(elem.hiddenSet.elems)
259+
case Restricted(elem1, cls) => hiddenByElem(elem1).map(_.restrict(cls))
259260
case ReadOnly(elem1) => hiddenByElem(elem1).map(_.readOnly)
260261
case _ => emptyRefs
261262

‎compiler/src/dotty/tools/dotc/core/Definitions.scala‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1092,6 +1092,7 @@ class Definitions {
10921092
@tu lazy val ReachCapabilityAnnot = requiredClass("scala.annotation.internal.reachCapability")
10931093
@tu lazy val RootCapabilityAnnot = requiredClass("scala.caps.internal.rootCapability")
10941094
@tu lazy val ReadOnlyCapabilityAnnot = requiredClass("scala.annotation.internal.readOnlyCapability")
1095+
@tu lazy val OnlyCapabilityAnnot = requiredClass("scala.annotation.internal.onlyCapability")
10951096
@tu lazy val RequiresCapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.internal.requiresCapability")
10961097
@tu lazy val RetainsAnnot: ClassSymbol = requiredClass("scala.annotation.retains")
10971098
@tu lazy val RetainsCapAnnot: ClassSymbol = requiredClass("scala.annotation.retainsCap")

‎compiler/src/dotty/tools/dotc/core/StdNames.scala‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -568,6 +568,7 @@ object StdNames {
568568
val null_ : N = "null"
569569
val ofDim: N = "ofDim"
570570
val on: N = "on"
571+
val only: N = "only"
571572
val opaque: N = "opaque"
572573
val open: N = "open"
573574
val ordinal: N = "ordinal"

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6282,6 +6282,10 @@ object Types extends TypeUtils {
62826282
case c: RootCapability => c
62836283
case Reach(c1) =>
62846284
mapCapability(c1, deep = true)
6285+
case Restricted(c1, cls) =>
6286+
mapCapability(c1) match
6287+
case c2: Capability => c2.restrict(cls)
6288+
case (cs: CaptureSet, exact) => (cs.restrict(cls), exact)
62856289
case ReadOnly(c1) =>
62866290
assert(!deep)
62876291
mapCapability(c1) match

‎compiler/src/dotty/tools/dotc/parsing/Parsers.scala‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1587,24 +1587,35 @@ object Parsers {
15871587
case _ => None
15881588
}
15891589

1590-
/** CaptureRef ::= { SimpleRef `.` } SimpleRef [`*`] [`.` `rd`] -- under captureChecking
1590+
/** CaptureRef ::= { SimpleRef `.` } SimpleRef [`*`] [CapFilter] [`.` `rd`] -- under captureChecking
1591+
* CapFilter ::= `.` `as` `[` QualId `]`
15911592
*/
15921593
def captureRef(): Tree =
15931594

1594-
def derived(ref: Tree, ann: () => Tree) =
1595-
in.nextToken()
1596-
atSpan(startOffset(ref)) { Annotated(ref, ann()) }
1595+
def derived(ref: Tree): Tree =
1596+
atSpan(startOffset(ref)):
1597+
if in.isIdent(nme.raw.STAR) then
1598+
in.nextToken()
1599+
Annotated(ref, makeReachAnnot())
1600+
else if in.isIdent(nme.rd) then
1601+
in.nextToken()
1602+
Annotated(ref, makeReadOnlyAnnot())
1603+
else if in.isIdent(nme.only) then
1604+
in.nextToken()
1605+
Annotated(ref, makeOnlyAnnot(inBrackets(convertToTypeId(qualId()))))
1606+
else assert(false)
15971607

15981608
def recur(ref: Tree): Tree =
15991609
if in.token == DOT then
16001610
in.nextToken()
1601-
if in.isIdent(nme.rd) then derived(ref, makeReadOnlyAnnot)
1611+
if in.isIdent(nme.rd) || in.isIdent(nme.only) then derived(ref)
16021612
else recur(selector(ref))
16031613
else if in.isIdent(nme.raw.STAR) then
1604-
val reachRef = derived(ref, makeReachAnnot)
1605-
if in.token == DOT && in.lookahead.isIdent(nme.rd) then
1614+
val reachRef = derived(ref)
1615+
val next = in.lookahead
1616+
if in.token == DOT && (next.isIdent(nme.rd) || next.isIdent(nme.only)) then
16061617
in.nextToken()
1607-
derived(reachRef, makeReadOnlyAnnot)
1618+
derived(reachRef)
16081619
else reachRef
16091620
else ref
16101621

0 commit comments

Comments
 (0)