Skip to content

Commit c492a63

Browse files
oderskyodersky
committed
Address review suggestions
1 parent f67c6fb commit c492a63

File tree

3 files changed

+48
-10
lines changed

3 files changed

+48
-10
lines changed

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

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -770,9 +770,14 @@ object Capabilities:
770770
* x covers x
771771
* x covers y ==> x covers y.f
772772
* x covers y ==> x* covers y*, x? covers y?
773-
* x covers y ==> x.only[C] covers y, x covers y.only[C]
774773
* x covers y ==> <fresh hiding x> covers y
774+
* x covers y ==> x.only[C] covers y, x covers y.only[C]
775+
*
775776
* TODO what other clauses from subsumes do we need to port here?
777+
* The last clause is a conservative over-approximation: basically, we can't achieve
778+
* separation by having different classifiers for now. It would be good to
779+
* have a test that would expect such separation, then we can try to refine
780+
* the clause to make the test pass.
776781
*/
777782
final def covers(y: Capability)(using Context): Boolean =
778783
val seen: util.EqHashSet[FreshCap] = new util.EqHashSet

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

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -118,9 +118,9 @@ object SepCheck:
118118

119119
def clashing(ref: Capability)(using Context): SrcPos | Null =
120120
val refPeaks = ref.directPeaks
121-
if !directPeaks .sharedPeaks(refPeaks).isEmpty then
121+
if !directPeaks.sharedPeaks(refPeaks).isEmpty then
122122
var i = 0
123-
while i < size && refs(i).directPeaks .sharedPeaks(refPeaks).isEmpty do
123+
while i < size && refs(i).directPeaks.sharedPeaks(refPeaks).isEmpty do
124124
i += 1
125125
assert(i < size)
126126
locs(i)
@@ -232,13 +232,12 @@ object SepCheck:
232232
* such that one of the following is true:
233233
* 1.
234234
* - one of the sets contains `r`
235-
* - the other contains a capability `s` or `s.rd` where `s` _covers_ `r`
235+
* - the other contains a capability `s` or `s.rd` where `s` covers `r`
236236
* 2.
237237
* - one of the sets contains `r.rd`
238-
* - the other contains a capability `s` where `s` _covers_ `r`
238+
* - the other contains a capability `s` where `s` covers `r`
239239
*
240-
* A capability `s` covers `r` if `r` can be seen as a path extension of `s`. E.g.
241-
* if `s = x.a` and `r = x.a.b.c` then `s` covers `a`.
240+
* @see covers in Capability
242241
*/
243242
private def overlapWith(other: Refs)(using Context): Refs =
244243
val refs1 = refs
@@ -343,11 +342,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
343342
private def formalCaptures(arg: Tree)(using Context): Refs =
344343
arg.formalType.orElse(arg.nuType).spanCaptureSet.elems
345344

346-
/** The span capture set if the type of `tree` */
345+
/** The span capture set of the type of `tree` */
347346
private def spanCaptures(tree: Tree)(using Context): Refs =
348347
tree.nuType.spanCaptureSet.elems
349348

350-
/** The deep capture set if the type of `tree` */
349+
/** The deep capture set of the type of `tree` */
351350
private def deepCaptures(tree: Tree)(using Context): Refs =
352351
tree.nuType.deepCaptureSet.elems
353352

@@ -588,7 +587,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
588587
for ref <- used do
589588
val pos = consumed.clashing(ref)
590589
if pos != null then
591-
// println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks .toList}, used = $used, exposed = ${ref.directPeaks }")
590+
// println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks.toList}, used = $used, exposed = ${ref.directPeaks }")
592591
consumeError(ref, pos, tree.srcPos)
593592
end checkUse
594593

‎tests/neg-custom-args/captures/cc-poly-varargs.check‎

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
-- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:11:13 ---------------------------------------------------
2+
11 | val left = src1.transformValuesWith(Left(_)) // error
3+
| ^^^^
4+
|Separation failure: argument of type (src1 : Source[T1, scala.caps.CapSet^{Cap}]^{Cap})
5+
|to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^]
6+
| (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f}
7+
|corresponds to capture-polymorphic formal parameter src of type Source[T1^'s3, scala.caps.CapSet^{Cap}]^
8+
|and hides capabilities {src1}.
9+
|Some of these overlap with the captures of the function result with type Source[Left[T1^'s1, Nothing]^'s2, scala.caps.CapSet^{Cap}]^{src1}.
10+
|
11+
| Hidden set of current argument : {src1}
12+
| Hidden footprint of current argument : {src1, Cap}
13+
| Capture set of function result : {src1, Cap}
14+
| Footprint set of function result : {src1, Cap}
15+
| The two sets overlap at : {src1, Cap}
16+
|
17+
|where: ^ refers to a fresh root capability created in value left when checking argument to parameter src of method transformValuesWith
18+
-- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:12:14 ---------------------------------------------------
19+
12 | val right = src2.transformValuesWith(Right(_)) // error
20+
| ^^^^
21+
|Separation failure: argument of type (src2 : Source[T2, scala.caps.CapSet^{Cap}]^{Cap})
22+
|to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^]
23+
| (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f}
24+
|corresponds to capture-polymorphic formal parameter src of type Source[T2^'s6, scala.caps.CapSet^{Cap}]^
25+
|and hides capabilities {src2}.
26+
|Some of these overlap with the captures of the function result with type Source[Right[Nothing, T2^'s4]^'s5, scala.caps.CapSet^{Cap}]^{src2}.
27+
|
28+
| Hidden set of current argument : {src2}
29+
| Hidden footprint of current argument : {src2, Cap}
30+
| Capture set of function result : {src2, Cap}
31+
| Footprint set of function result : {src2, Cap}
32+
| The two sets overlap at : {src2, Cap}
33+
|
34+
|where: ^ refers to a fresh root capability created in value right when checking argument to parameter src of method transformValuesWith

0 commit comments

Comments
 (0)