@@ -13,6 +13,7 @@ import CCState.*
13
13
import Periods .NoRunId
14
14
import compiletime .uninitialized
15
15
import StdNames .nme
16
+ import CaptureSet .VarState
16
17
17
18
/** A trait for references in CaptureSets. These can be NamedTypes, ThisTypes or ParamRefs,
18
19
* as well as three kinds of AnnotatedTypes representing readOnly, reach, and maybe capabilities.
@@ -78,15 +79,24 @@ trait CaptureRef extends TypeProxy, ValueType:
78
79
case tp : TermRef => tp.name == nme.CAPTURE_ROOT && tp.symbol == defn.captureRoot
79
80
case _ => false
80
81
82
+ /** Is this reference a Fresh.Cap instance? */
83
+ final def isFresh (using Context ): Boolean = this match
84
+ case Fresh .Cap (_) => true
85
+ case _ => false
86
+
87
+ /** Is this reference the generic root capability `cap` or a Fresh.Cap instance? */
88
+ final def isCapOrFresh (using Context ): Boolean = isCap || isFresh
89
+
81
90
/** Is this reference one the generic root capabilities `cap` or `cap.rd` ? */
82
91
final def isRootCapability (using Context ): Boolean = this match
83
- case ReadOnlyCapability (tp1) => tp1.isCap
84
- case _ => isCap
92
+ case ReadOnlyCapability (tp1) => tp1.isCapOrFresh
93
+ case _ => isCapOrFresh
85
94
86
95
/** Is this reference capability that does not derive from another capability ? */
87
96
final def isMaxCapability (using Context ): Boolean = this match
88
97
case tp : TermRef => tp.isCap || tp.info.derivesFrom(defn.Caps_Exists )
89
98
case tp : TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists )
99
+ case Fresh .Cap (_) => true
90
100
case ReadOnlyCapability (tp1) => tp1.isMaxCapability
91
101
case _ => false
92
102
@@ -137,26 +147,27 @@ trait CaptureRef extends TypeProxy, ValueType:
137
147
* Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y
138
148
* Contains[X, y] ==> X subsumes y
139
149
*
140
- * TODO: Document cases with more comments.
150
+ * TODO: Move to CaptureSet
141
151
*/
142
- final def subsumes (y : CaptureRef )(using Context ): Boolean =
152
+ final def subsumes (y : CaptureRef )(using ctx : Context , vs : VarState = VarState . Separate ): Boolean =
143
153
144
154
def subsumingRefs (x : Type , y : Type ): Boolean = x match
145
155
case x : CaptureRef => y match
146
156
case y : CaptureRef => x.subsumes(y)
147
157
case _ => false
148
158
case _ => false
149
159
150
- def viaInfo (info : Type )(test : Type => Boolean ): Boolean = info.match
160
+ def viaInfo (info : Type )(test : Type => Boolean ): Boolean = info.dealias match
151
161
case info : SingletonCaptureRef => test(info)
162
+ case CapturingType (parent, _) => viaInfo(parent)(test)
152
163
case info : AndType => viaInfo(info.tp1)(test) || viaInfo(info.tp2)(test)
153
164
case info : OrType => viaInfo(info.tp1)(test) && viaInfo(info.tp2)(test)
154
165
case _ => false
155
166
156
167
(this eq y)
157
- || this .isCap
168
+ || maxSubsumes(y, canAddHidden = ! vs.isOpen)
158
169
|| y.match
159
- case y : TermRef if ! y.isRootCapability =>
170
+ case y : TermRef if ! y.isCap =>
160
171
y.prefix.match
161
172
case ypre : CaptureRef =>
162
173
this .subsumes(ypre)
@@ -201,6 +212,27 @@ trait CaptureRef extends TypeProxy, ValueType:
201
212
case _ => false
202
213
end subsumes
203
214
215
+ /** This is a maximal capabaility that subsumes `y` in given context and VarState.
216
+ * @param canAddHidden If true we allow maximal capabilties to subsume all other capabilities.
217
+ * We add those capabilities to the hidden set if this is Fresh.Cap
218
+ * If false we only accept `y` elements that are already in the
219
+ * hidden set of this Fresh.Cap. The idea is that in a VarState that
220
+ * accepts additions we first run `maxSubsumes` with `canAddHidden = false`
221
+ * so that new variables get added to the sets. If that fails, we run
222
+ * the test again with canAddHidden = true as a last effort before we
223
+ * fail a comparison.
224
+ */
225
+ def maxSubsumes (y : CaptureRef , canAddHidden : Boolean )(using ctx : Context , vs : VarState = VarState .Separate ): Boolean =
226
+ this .match
227
+ case Fresh .Cap (hidden) =>
228
+ vs.ifNotSeen(this )(hidden.elems.exists(_.subsumes(y)))
229
+ || ! y.stripReadOnly.isCap && canAddHidden && vs.addHidden(hidden, y)
230
+ case _ =>
231
+ this .isCap && canAddHidden
232
+ || y.match
233
+ case ReadOnlyCapability (y1) => this .stripReadOnly.maxSubsumes(y1, canAddHidden)
234
+ case _ => false
235
+
204
236
def assumedContainsOf (x : TypeRef )(using Context ): SimpleIdentitySet [CaptureRef ] =
205
237
CaptureSet .assumedContains.getOrElse(x, SimpleIdentitySet .empty)
206
238
0 commit comments