Skip to content

Commit e27c461

Browse files
oderskyodersky
committed
Use TypeComparer's undolog for capture set elements and dependencies
1 parent 496018f commit e27c461

File tree

7 files changed

+41
-65
lines changed

7 files changed

+41
-65
lines changed

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

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -695,6 +695,18 @@ object CaptureSet:
695695
assert(elem.subsumes(elem1),
696696
i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this")
697697

698+
protected def includeElem(elem: Capability)(using Context): Unit =
699+
if !elems.contains(elem) then
700+
elems += elem
701+
TypeComparer.logUndoAction: () =>
702+
elems -= elem
703+
704+
def includeDep(cs: CaptureSet)(using Context): Unit =
705+
if !deps.contains(cs) then
706+
deps += cs
707+
TypeComparer.logUndoAction: () =>
708+
deps -= cs
709+
698710
final def addThisElem(elem: Capability)(using Context, VarState): Boolean =
699711
if isConst || !recordElemsState() then // Fail if variable is solved or given VarState is frozen
700712
addIfHiddenOrFail(elem)
@@ -704,7 +716,7 @@ object CaptureSet:
704716
// id == 108 then assert(false, i"trying to add $elem to $this")
705717
assert(elem.isWellformed, elem)
706718
assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState])
707-
elems += elem
719+
includeElem(elem)
708720
if isBadRoot(rootLimit, elem) then
709721
rootAddedHandler()
710722
newElemAddedHandler(elem)
@@ -772,7 +784,7 @@ object CaptureSet:
772784
(cs eq this)
773785
|| cs.isUniversal
774786
|| isConst
775-
|| recordDepsState() && { deps += cs; true }
787+
|| recordDepsState() && { includeDep(cs); true }
776788

777789
override def disallowRootCapability(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
778790
rootLimit = upto
@@ -1126,7 +1138,7 @@ object CaptureSet:
11261138
if alias ne this then alias.add(elem)
11271139
else
11281140
def addToElems() =
1129-
elems += elem
1141+
includeElem(elem)
11301142
deps.foreach: dep =>
11311143
assert(dep != this)
11321144
vs.addHidden(dep.asInstanceOf[HiddenSet], elem)
@@ -1142,7 +1154,7 @@ object CaptureSet:
11421154
deps = SimpleIdentitySet(elem.hiddenSet)
11431155
else
11441156
addToElems()
1145-
elem.hiddenSet.deps += this
1157+
elem.hiddenSet.includeDep(this)
11461158
case _ =>
11471159
addToElems()
11481160

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

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
5353
needsGc = false
5454
maxErrorLevel = -1
5555
errorNotes = Nil
56-
logSize = 0
56+
undoLog.clear()
5757
if Config.checkTypeComparerReset then checkReset()
5858

5959
private var pendingSubTypes: util.MutableSet[(Type, Type)] | Null = null
@@ -63,8 +63,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
6363
private var maxErrorLevel: Int = -1
6464
protected var errorNotes: List[(Int, ErrorNote)] = Nil
6565

66-
private val undoLog = mutable.ArrayBuffer[() => Unit]()
67-
private var logSize = 0
66+
val undoLog = mutable.ArrayBuffer[() => Unit]()
6867

6968
private var needsGc = false
7069

@@ -1588,18 +1587,20 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
15881587
undoLog(i)()
15891588
i += 1
15901589
undoLog.takeInPlace(prevSize)
1590+
assert(undoLog.size == prevSize)
15911591

15921592
// begin recur
15931593
if tp2 eq NoType then false
15941594
else if tp1 eq tp2 then true
15951595
else
15961596
val savedCstr = constraint
15971597
val savedGadt = ctx.gadt
1598-
val savedLogSize = logSize
1598+
val savedLogSize = undoLog.size
15991599
inline def restore() =
16001600
state.constraint = savedCstr
16011601
ctx.gadtState.restore(savedGadt)
16021602
if undoLog.size != savedLogSize then
1603+
//println(i"ROLLBACK $tp1 <:< $tp2")
16031604
rollBack(savedLogSize)
16041605
val savedSuccessCount = successCount
16051606
try

‎tests/neg-custom-args/captures/capt-depfun.check‎

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,9 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:11:43 ----------------------------------
2-
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon
2+
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error
33
| ^^^^^^^
44
| Found: Str^{} ->{ac, y, z} Str^{y, z}
55
| Required: Str^{y, z} => Str^{y, z}
66
|
77
| where: => refers to a fresh root capability in the type of value dc
88
|
99
| longer explanation available when compiling with `-explain`
10-
-- Error: tests/neg-custom-args/captures/capt-depfun.scala:11:24 -------------------------------------------------------
11-
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon
12-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
13-
| Separation failure: value dc's type Str^{y, z} => Str^{y, z} hides parameters y and z.
14-
| The parameters need to be annotated with @consume to allow this.

‎tests/neg-custom-args/captures/capt-depfun.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,4 @@ class Str
88
def f(y: Cap, z: Cap) =
99
def g(): C @retains[y.type | z.type] = ???
1010
val ac: ((x: Cap) => Str @retains[x.type] => Str @retains[x.type]) = ???
11-
val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon
11+
val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error

‎tests/neg-custom-args/captures/depfun-reach.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ def test(io: Object^, async: Object^) =
1515
compose(op)
1616

1717
def foo[X](op: (xs: List[(X, () ->{io} Unit)]) => List[() ->{xs*} Unit])
18-
: (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] = // error
18+
: (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] =
1919
op // error
2020

2121
def boom(op: List[(() ->{async} Unit, () ->{io} Unit)]): List[() ->{} Unit] =

‎tests/neg-custom-args/captures/lazyref.check‎

Lines changed: 13 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -34,51 +34,19 @@
3434
| This type hides capabilities {LazyRef.this.elem}
3535
|
3636
| where: => refers to a fresh root capability in the type of value get
37-
-- Error: tests/neg-custom-args/captures/lazyref.scala:23:13 -----------------------------------------------------------
38-
23 | val ref3 = ref1.map(g) // error: separation failure
39-
| ^^^^
40-
| Separation failure: Illegal access to {cap1} which is hidden by the previous definition
41-
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
42-
| This type hides capabilities {LazyRef.this.elem, cap1}
43-
|
44-
| where: => refers to a fresh root capability in the type of value elem
45-
-- Error: tests/neg-custom-args/captures/lazyref.scala:26:9 ------------------------------------------------------------
46-
26 | if cap1 == cap2 // error: separation failure // error: separation failure
47-
| ^^^^
48-
| Separation failure: Illegal access to {cap1} which is hidden by the previous definition
49-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
50-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
51-
|
52-
| where: => refers to a fresh root capability in the type of value elem
53-
-- Error: tests/neg-custom-args/captures/lazyref.scala:26:17 -----------------------------------------------------------
54-
26 | if cap1 == cap2 // error: separation failure // error: separation failure
55-
| ^^^^
56-
| Separation failure: Illegal access to {cap2} which is hidden by the previous definition
57-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
58-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
59-
|
60-
| where: => refers to a fresh root capability in the type of value elem
61-
-- Error: tests/neg-custom-args/captures/lazyref.scala:27:11 -----------------------------------------------------------
62-
27 | then ref1 // error: separation failure
63-
| ^^^^
64-
| Separation failure: Illegal access to {cap1, ref1} which is hidden by the previous definition
65-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
66-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
67-
|
68-
| where: => refers to a fresh root capability in the type of value elem
69-
-- Error: tests/neg-custom-args/captures/lazyref.scala:28:11 -----------------------------------------------------------
70-
28 | else ref2) // error: separation failure
71-
| ^^^^
72-
| Separation failure: Illegal access to {cap1, cap2, ref1} which is hidden by the previous definition
73-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
74-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
75-
|
76-
| where: => refers to a fresh root capability in the type of value elem
7737
-- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------
7838
29 | .map(g) // error: separation failure
7939
| ^
80-
| Separation failure: Illegal access to {cap2} which is hidden by the previous definition
81-
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
82-
| This type hides capabilities {LazyRef.this.elem, ref2*, cap1}
83-
|
84-
| where: => refers to a fresh root capability in the type of value elem
40+
|Separation failure: argument of type (x: Int) ->{cap2} Int
41+
|to method map: [U](f: T => U): LazyRef[U]^{f, LazyRef.this}
42+
|corresponds to capture-polymorphic formal parameter f of type Int => Int
43+
|and hides capabilities {cap2}.
44+
|Some of these overlap with the captures of the function prefix with type (LazyRef[Int]{val elem: () ->{ref2*} Int} | (ref1 : LazyRef[Int]{val elem: () ->{cap1} Int}^{cap1}))^{ref2}.
45+
|
46+
| Hidden set of current argument : {cap2}
47+
| Hidden footprint of current argument : {cap2}
48+
| Capture set of function prefix : {ref1, ref2, ref2*}
49+
| Footprint set of function prefix : {ref1, ref2, ref2*, cap1, cap2}
50+
| The two sets overlap at : {cap2}
51+
|
52+
|where: => refers to a fresh root capability created in value ref4 when checking argument to parameter f of method map

‎tests/neg-custom-args/captures/lazyref.scala‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,11 @@ def test(cap1: Cap, cap2: Cap) =
2020
val ref1c: LazyRef[Int] = ref1 // error
2121
val ref2 = map(ref1, g)
2222
val ref2c: LazyRef[Int]^{cap2} = ref2 // error
23-
val ref3 = ref1.map(g) // error: separation failure
23+
val ref3 = ref1.map(g)
2424
val ref3c: LazyRef[Int]^{ref1} = ref3 // error
2525
val ref4 = (
26-
if cap1 == cap2 // error: separation failure // error: separation failure
27-
then ref1 // error: separation failure
28-
else ref2) // error: separation failure
26+
if cap1 == cap2
27+
then ref1
28+
else ref2)
2929
.map(g) // error: separation failure
3030
val ref4c: LazyRef[Int]^{cap1} = ref4 // error

0 commit comments

Comments
 (0)