@@ -770,28 +770,38 @@ object Capabilities:
770
770
* x covers y ==> x covers y.f
771
771
* x covers y ==> x* covers y*, x? covers y?
772
772
* x covers y ==> x.only[C] covers y, x covers y.only[C]
773
+ * x covers y ==> <fresh hiding x> covers y
773
774
* TODO what other clauses from subsumes do we need to port here?
774
775
*/
775
776
final def covers (y : Capability )(using Context ): Boolean =
776
- (this eq y)
777
- || y.match
778
- case y @ TermRef (ypre : Capability , _) =>
779
- this .covers(ypre)
780
- case Reach (y1) =>
781
- this match
782
- case Reach (x1) => x1.covers(y1)
783
- case _ => false
784
- case Maybe (y1) =>
785
- this match
786
- case Maybe (x1) => x1.covers(y1)
787
- case _ => false
788
- case Restricted (y1, _) =>
789
- this .covers(y1)
790
- case _ =>
791
- false
792
- || this .match
793
- case Restricted (x1, _) => x1.covers(y)
794
- case _ => false
777
+ val seen : util.EqHashSet [FreshCap ] = new util.EqHashSet
778
+
779
+ def recur (x : Capability , y : Capability ): Boolean =
780
+ (x eq y)
781
+ || y.match
782
+ case y @ TermRef (ypre : Capability , _) =>
783
+ recur(x, ypre)
784
+ case Reach (y1) =>
785
+ x match
786
+ case Reach (x1) => recur(x1, y1)
787
+ case _ => false
788
+ case Maybe (y1) =>
789
+ x match
790
+ case Maybe (x1) => recur(x1, y1)
791
+ case _ => false
792
+ case Restricted (y1, _) =>
793
+ recur(x, y1)
794
+ case _ =>
795
+ false
796
+ || x.match
797
+ case x : FreshCap if ! seen.contains(x) =>
798
+ seen.add(x)
799
+ x.hiddenSet.exists(recur(_, y))
800
+ case Restricted (x1, _) => recur(x1, y)
801
+ case _ => false
802
+
803
+ recur(this , y)
804
+ end covers
795
805
796
806
def assumedContainsOf (x : TypeRef )(using Context ): SimpleIdentitySet [Capability ] =
797
807
CaptureSet .assumedContains.getOrElse(x, SimpleIdentitySet .empty)
0 commit comments