@@ -97,12 +97,58 @@ sealed abstract class CaptureSet extends Showable:
97
97
* @return CompareResult.OK if elements were added, or a conflicting
98
98
* capture set that prevents addition otherwise.
99
99
*/
100
- protected def addNewElems (newElems : Refs , origin : CaptureSet )(using Context , VarState ): CompareResult =
100
+ protected final def tryInclude (newElems : Refs , origin : CaptureSet )(using Context , VarState ): CompareResult =
101
101
(CompareResult .OK /: newElems): (r, elem) =>
102
- r.andAlso(addNewElem (elem, origin))
102
+ r.andAlso(tryInclude (elem, origin))
103
103
104
- /** Add a single element, with the same meaning as in `addNewElems` */
105
- protected def addNewElem (elem : CaptureRef , origin : CaptureSet )(using Context , VarState ): CompareResult
104
+ /** Try to include an element in this capture set.
105
+ * @param elem The element to be added
106
+ * @param origin The set that originated the request, or `empty` if the request came from outside.
107
+ *
108
+ * If the set already accounts for the element, return OK.
109
+ * Otherwise, try to add a new element to the set. This is OK if
110
+ * - the set is a variable, and
111
+ * - the element is not at a deeper nesting level than the set, and
112
+ * - the element can also be added (in mapped/filtered form) to all
113
+ * dependent sets.
114
+ * If the `origin` is the same as the `source` of the set variable, the
115
+ * element might be filtered or mapped according to the class of the variable.
116
+ * Otherwise, the element might have to be back-propagated to the source
117
+ * of the variable.
118
+ *
119
+ * If the element itself cannot be added to the set for some reason, and the
120
+ * element is not the root capability, try instead to include its underlying
121
+ * capture set.
122
+ */
123
+ protected def tryInclude (elem : CaptureRef , origin : CaptureSet )(using Context , VarState ): CompareResult =
124
+ if accountsFor(elem) then CompareResult .OK
125
+ else addNewElem(elem)
126
+
127
+ /** Add an element to this capture set, assuming it is not already accounted for,
128
+ * and omitting any mapping or filtering.
129
+ *
130
+ * If the element itself cannot be added to the set for some reason, and the
131
+ * element is not the root capability, try instead to include its underlying
132
+ * capture set.
133
+ */
134
+ protected final def addNewElem (elem : CaptureRef )(using Context , VarState ): CompareResult =
135
+ if elem.isRootCapability || summon[VarState ] == FrozenState then addThisElem(elem)
136
+ else addThisElem(elem).orElse:
137
+ val underlying = elem.captureSetOfInfo
138
+ tryInclude(underlying.elems, this ).andAlso:
139
+ underlying.addDependent(this )
140
+ CompareResult .OK
141
+
142
+ /** Add new elements one by one using `addNewElem`, abort on first failure */
143
+ protected final def addNewElems (newElems : Refs )(using Context , VarState ): CompareResult =
144
+ (CompareResult .OK /: newElems): (r, elem) =>
145
+ r.andAlso(addNewElem(elem))
146
+
147
+ /** Add a specific element, assuming it is not already accounted for,
148
+ * and omitting any mapping or filtering, without possibility to backtrack
149
+ * to underlying capture set
150
+ */
151
+ protected def addThisElem (elem : CaptureRef )(using Context , VarState ): CompareResult
106
152
107
153
/** If this is a variable, add `cs` as a dependent set */
108
154
protected def addDependent (cs : CaptureSet )(using Context , VarState ): CompareResult
@@ -111,7 +157,7 @@ sealed abstract class CaptureSet extends Showable:
111
157
protected def addAsDependentTo (cs : CaptureSet )(using Context ): this .type =
112
158
cs.addDependent(this )(using ctx, UnrecordedState )
113
159
this
114
-
160
+ /*
115
161
/** Try to include all references of `elems` that are not yet accounted for by this
116
162
* capture set. Inclusion is via `addNewElems`.
117
163
* @param origin The set where the elements come from, or `empty` if not known.
@@ -121,13 +167,13 @@ sealed abstract class CaptureSet extends Showable:
121
167
protected final def tryInclude(elems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
122
168
val unaccounted = elems.filter(!accountsFor(_))
123
169
if unaccounted.isEmpty then CompareResult.OK
124
- else addNewElems (unaccounted, origin)
170
+ else tryInclude (unaccounted, origin)
125
171
126
172
/** Equivalent to `tryInclude({elem}, origin)`, but more efficient */
127
173
protected final def tryInclude(elem: CaptureRef, origin: CaptureSet)(using Context, VarState): CompareResult =
128
174
if accountsFor(elem) then CompareResult.OK
129
- else addNewElems (elem.singletonCaptureSet.elems , origin)
130
-
175
+ else tryInclude (elem, origin)
176
+ */
131
177
/* x subsumes y if one of the following is true:
132
178
* - x is the same as y,
133
179
* - x is a this reference and y refers to a field of x
@@ -208,21 +254,13 @@ sealed abstract class CaptureSet extends Showable:
208
254
209
255
/** The subcapturing test, using a given VarState */
210
256
private def subCaptures (that : CaptureSet )(using Context , VarState ): CompareResult =
211
- def recur (elems : List [CaptureRef ]): CompareResult = elems match
212
- case elem :: elems1 =>
213
- var result = that.tryInclude(elem, this )
214
- if ! result.isOK then
215
- ccState.levelError = ccState.levelError.orElse(result.levelError)
216
- if ! elem.isRootCapability && summon[VarState ] != FrozenState then
217
- result = result.orElse(elem.captureSetOfInfo.subCaptures(that))
218
- if result.isOK then
219
- recur(elems1)
220
- else
221
- varState.rollBack()
222
- result
223
- case Nil =>
224
- addDependent(that)
225
- recur(elems.toList)
257
+ val result = that.tryInclude(elems, this )
258
+ if result.isOK then
259
+ addDependent(that)
260
+ else
261
+ ccState.levelError = ccState.levelError.orElse(result.levelError)
262
+ varState.rollBack()
263
+ result
226
264
// .showing(i"subcaptures $this <:< $that = ${result.show}", capt)
227
265
228
266
/** Two capture sets are considered =:= equal if they mutually subcapture each other
@@ -400,7 +438,7 @@ object CaptureSet:
400
438
def isConst = true
401
439
def isAlwaysEmpty = elems.isEmpty
402
440
403
- def addNewElem (elem : CaptureRef , origin : CaptureSet )(using Context , VarState ): CompareResult =
441
+ def addThisElem (elem : CaptureRef )(using Context , VarState ): CompareResult =
404
442
CompareResult .Fail (this :: Nil )
405
443
406
444
def addDependent (cs : CaptureSet )(using Context , VarState ) = CompareResult .OK
@@ -422,7 +460,7 @@ object CaptureSet:
422
460
*/
423
461
object Fluid extends Const (emptySet):
424
462
override def isAlwaysEmpty = false
425
- override def addNewElem (elem : CaptureRef , origin : CaptureSet )(using Context , VarState ) = CompareResult .OK
463
+ override def addThisElem (elem : CaptureRef )(using Context , VarState ) = CompareResult .OK
426
464
override def accountsFor (x : CaptureRef )(using Context ): Boolean = true
427
465
override def mightAccountFor (x : CaptureRef )(using Context ): Boolean = true
428
466
override def toString = " <fluid>"
@@ -489,24 +527,23 @@ object CaptureSet:
489
527
def resetDeps ()(using state : VarState ): Unit =
490
528
deps = state.deps(this )
491
529
492
- final def addNewElem (elem : CaptureRef , origin : CaptureSet )(using Context , VarState ): CompareResult =
530
+ final def addThisElem (elem : CaptureRef )(using Context , VarState ): CompareResult =
493
531
if isConst || ! recordElemsState() then
494
532
CompareResult .Fail (this :: Nil ) // fail if variable is solved or given VarState is frozen
495
533
else if ! levelOK(elem) then
496
- val res = CompareResult .LevelError (this , elem)
497
- if elem.isRootCapability then res
498
- else res.orElse(addNewElems(elem.captureSetOfInfo.elems, origin))
534
+ CompareResult .LevelError (this , elem)
499
535
else
500
536
// assert(id != 19 || !elem.isLocalRootCapability, elem.asInstanceOf[TermRef].localRootOwner)
501
537
elems += elem
502
- if elem.isUniversalRootCapability then rootAddedHandler()
538
+ if elem.isUniversalRootCapability then
539
+ rootAddedHandler()
503
540
newElemAddedHandler(elem)
504
541
// assert(id != 5 || elems.size != 3, this)
505
- val res = (CompareResult .OK /: deps) { (r, dep) =>
542
+ val res = (CompareResult .OK /: deps): (r, dep) =>
506
543
r.andAlso(dep.tryInclude(elem, this ))
507
- }.addToTrace( this )
508
- if ! res.isOK then elems -= elem
509
- res
544
+ res.orElse :
545
+ elems -= elem
546
+ res.addToTrace( this )
510
547
511
548
private def levelOK (elem : CaptureRef )(using Context ): Boolean =
512
549
if elem.isUniversalRootCapability then ! noUniversal
@@ -569,7 +606,7 @@ object CaptureSet:
569
606
.showing(i " solve $this = $result" , capt)
570
607
// println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
571
608
val newElems = approx.elems -- elems
572
- if newElems.isEmpty || addNewElems (newElems, empty)(using ctx, VarState ()).isOK then
609
+ if tryInclude (newElems, empty)(using ctx, VarState ()).isOK then
573
610
markSolved()
574
611
575
612
/** Mark set as solved and propagate this info to all dependent sets */
@@ -652,39 +689,43 @@ object CaptureSet:
652
689
|Stack trace of variable creation:"
653
690
| ${stack.mkString(" \n " )}"""
654
691
655
- override def addNewElems (newElems : Refs , origin : CaptureSet )(using Context , VarState ): CompareResult =
656
- val added =
657
- if origin eq source then // elements have to be mapped
658
- mapRefs(newElems, tm, variance)
692
+ override def tryInclude (elem : CaptureRef , origin : CaptureSet )(using Context , VarState ): CompareResult =
693
+ def propagate : CompareResult =
694
+ if (origin ne source) && (origin ne initial) && mapIsIdempotent then
695
+ // `tm` is idempotent, propagate back elems from image set.
696
+ // This is sound, since we know that for `r in newElems: tm(r) = r`, hence
697
+ // `r` is _one_ possible solution in `source` that would make an `r` appear in this set.
698
+ // It's not necessarily the only possible solution, so the scheme is incomplete.
699
+ source.tryInclude(elem, this )
700
+ else if ! mapIsIdempotent && variance <= 0 && ! origin.isConst && (origin ne initial) && (origin ne source) then
701
+ // The map is neither a BiTypeMap nor an idempotent type map.
702
+ // In that case there's no much we can do.
703
+ // The scheme then does not propagate added elements back to source and rejects adding
704
+ // elements from variable sources in contra- and non-variant positions. In essence,
705
+ // we approximate types resulting from such maps by returning a possible super type
706
+ // from the actual type. But this is neither sound nor complete.
707
+ report.warning(em " trying to add $elem from unrecognized source $origin of mapped set $this$whereCreated" )
708
+ CompareResult .Fail (this :: Nil )
659
709
else
660
- // elements are added by subcapturing propagation with this Mapped set
661
- // as superset; no mapping is necessary or allowed.
662
- Const (newElems)
663
- super .addNewElems(added.elems, origin)
664
- .andAlso {
665
- if added.isConst then CompareResult .OK
666
- else if added.asVar.recordDepsState() then { addAsDependentTo(added); CompareResult .OK }
667
- else CompareResult .Fail (this :: Nil )
668
- }
669
- .andAlso {
670
- if (origin ne source) && (origin ne initial) && mapIsIdempotent then
671
- // `tm` is idempotent, propagate back elems from image set.
672
- // This is sound, since we know that for `r in newElems: tm(r) = r`, hence
673
- // `r` is _one_ possible solution in `source` that would make an `r` appear in this set.
674
- // It's not necessarily the only possible solution, so the scheme is incomplete.
675
- source.tryInclude(newElems, this )
676
- else if ! mapIsIdempotent && variance <= 0 && ! origin.isConst && (origin ne initial) && (origin ne source) then
677
- // The map is neither a BiTypeMap nor an idempotent type map.
678
- // In that case there's no much we can do.
679
- // The scheme then does not propagate added elements back to source and rejects adding
680
- // elements from variable sources in contra- and non-variant positions. In essence,
681
- // we approximate types resulting from such maps by returning a possible super type
682
- // from the actual type. But this is neither sound nor complete.
683
- report.warning(em " trying to add elems ${CaptureSet (newElems)} from unrecognized source $origin of mapped set $this$whereCreated" )
684
- CompareResult .Fail (this :: Nil )
685
- else
686
- CompareResult .OK
687
- }
710
+ CompareResult .OK
711
+ def propagateIf (cond : Boolean ): CompareResult =
712
+ if cond then propagate else CompareResult .OK
713
+
714
+ if origin eq source then // elements have to be mapped
715
+ val mapped = extrapolateCaptureRef(elem, tm, variance)
716
+ val added = mapped.elems.filter(! accountsFor(_))
717
+ addNewElems(added)
718
+ .andAlso:
719
+ if mapped.isConst then CompareResult .OK
720
+ else if mapped.asVar.recordDepsState() then { addAsDependentTo(mapped); CompareResult .OK }
721
+ else CompareResult .Fail (this :: Nil )
722
+ .andAlso:
723
+ propagateIf(! added.isEmpty)
724
+ else if accountsFor(elem) then
725
+ CompareResult .OK
726
+ else
727
+ addNewElem(elem).andAlso(propagate)
728
+ end tryInclude
688
729
689
730
override def computeApprox (origin : CaptureSet )(using Context ): CaptureSet =
690
731
if source eq origin then
@@ -707,15 +748,17 @@ object CaptureSet:
707
748
(val source : Var , bimap : BiTypeMap , initialElems : Refs )(using @ constructorOnly ctx : Context )
708
749
extends DerivedVar (source.levelLimit, initialElems):
709
750
710
- override def addNewElems ( newElems : Refs , origin : CaptureSet )(using Context , VarState ): CompareResult =
751
+ override def tryInclude ( elem : CaptureRef , origin : CaptureSet )(using Context , VarState ): CompareResult =
711
752
if origin eq source then
712
- super .addNewElems(newElems.map(bimap.forward), origin)
753
+ val mappedElem = bimap.forward(elem)
754
+ if accountsFor(mappedElem) then CompareResult .OK
755
+ else addNewElem(mappedElem)
756
+ else if accountsFor(elem) then
757
+ CompareResult .OK
713
758
else
714
- super .addNewElems(newElems, origin)
715
- .andAlso {
716
- source.tryInclude(newElems.map(bimap.backward), this )
717
- .showing(i " propagating new elems ${CaptureSet (newElems)} backward from $this to $source" , capt)
718
- }
759
+ addNewElem(elem).andAlso:
760
+ source.tryInclude(bimap.backward(elem), this )
761
+ .showing(i " propagating new elem $elem backward from $this to $source" , capt)
719
762
720
763
/** For a BiTypeMap, supertypes of the mapped type also constrain
721
764
* the source via the inverse type mapping and vice versa. That is, if
@@ -737,18 +780,17 @@ object CaptureSet:
737
780
(val source : Var , p : Context ?=> CaptureRef => Boolean )(using @ constructorOnly ctx : Context )
738
781
extends DerivedVar (source.levelLimit, source.elems.filter(p)):
739
782
740
- override def addNewElems (newElems : Refs , origin : CaptureSet )(using Context , VarState ): CompareResult =
741
- val filtered = newElems.filter(p)
742
- if origin eq source then
743
- super .addNewElems(filtered, origin)
783
+ override def tryInclude (elem : CaptureRef , origin : CaptureSet )(using Context , VarState ): CompareResult =
784
+ if accountsFor(elem) then
785
+ CompareResult .OK
786
+ else if origin eq source then
787
+ if p(elem) then addNewElem(elem)
788
+ else CompareResult .OK
744
789
else
745
790
// Filtered elements have to be back-propagated to source.
746
791
// Elements that don't satisfy `p` are not allowed.
747
- super .addNewElems(newElems, origin)
748
- .andAlso {
749
- if filtered.size == newElems.size then source.tryInclude(newElems, this )
750
- else CompareResult .Fail (this :: Nil )
751
- }
792
+ if p(elem) then source.tryInclude(elem, this )
793
+ else CompareResult .Fail (this :: Nil )
752
794
753
795
override def computeApprox (origin : CaptureSet )(using Context ): CaptureSet =
754
796
if source eq origin then
@@ -772,14 +814,13 @@ object CaptureSet:
772
814
deps += cs1
773
815
deps += cs2
774
816
775
- override def addNewElems (newElems : Refs , origin : CaptureSet )(using Context , VarState ): CompareResult =
776
- val added =
777
- if origin eq cs1 then newElems.filter(cs2.accountsFor)
778
- else if origin eq cs2 then newElems.filter(cs1.accountsFor)
779
- else newElems
780
- // If origin is not cs1 or cs2, then newElems will be propagated to
781
- // cs1, cs2 since they are in deps.
782
- super .addNewElems(added, origin)
817
+ override def tryInclude (elem : CaptureRef , origin : CaptureSet )(using Context , VarState ): CompareResult =
818
+ val present =
819
+ if origin eq cs1 then cs2.accountsFor(elem)
820
+ else if origin eq cs2 then cs1.accountsFor(elem)
821
+ else true
822
+ if present && ! accountsFor(elem) then addNewElem(elem)
823
+ else CompareResult .OK
783
824
784
825
override def computeApprox (origin : CaptureSet )(using Context ): CaptureSet =
785
826
if (origin eq cs1) || (origin eq cs2) then
@@ -882,7 +923,7 @@ object CaptureSet:
882
923
if alt.isOK then alt
883
924
else this
884
925
885
- inline def addToTrace (cs : CaptureSet ) = this match
926
+ inline def addToTrace (cs : CaptureSet ): CompareResult = this match
886
927
case Fail (trace) => Fail (cs :: trace)
887
928
case _ => this
888
929
end CompareResult
0 commit comments