@@ -770,28 +770,38 @@ object Capabilities:
770770 * x covers y ==> x covers y.f
771771 * x covers y ==> x* covers y*, x? covers y?
772772 * x covers y ==> x.only[C] covers y, x covers y.only[C]
773+ * x covers y ==> <fresh hiding x> covers y
773774 * TODO what other clauses from subsumes do we need to port here?
774775 */
775776 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
795805
796806 def assumedContainsOf (x : TypeRef )(using Context ): SimpleIdentitySet [Capability ] =
797807 CaptureSet .assumedContains.getOrElse(x, SimpleIdentitySet .empty)
0 commit comments