@@ -15,63 +15,58 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
1515 import tpd .*
1616 import checker .*
1717
18- extension (cs : CaptureSet )
19- def footprint (using Context ): CaptureSet . Const =
20- def recur (elems : CaptureSet . Refs , newElems : List [CaptureRef ]): CaptureSet . Refs = newElems match
18+ extension (refs : Refs )
19+ def footprint (using Context ): Refs =
20+ def recur (elems : Refs , newElems : List [CaptureRef ]): Refs = newElems match
2121 case newElem :: newElems1 =>
2222 val superElems = newElem.captureSetOfInfo.elems.filter: superElem =>
2323 ! superElem.isMaxCapability && ! elems.contains(superElem)
2424 recur(elems ++ superElems, newElems1 ++ superElems.toList)
2525 case Nil => elems
26- val elems : CaptureSet . Refs = cs.elems .filter(! _.isMaxCapability)
27- CaptureSet ( recur(elems, elems.toList) )
26+ val elems : Refs = refs .filter(! _.isMaxCapability)
27+ recur(elems, elems.toList)
2828
29- def overlapWith (other : CaptureSet )(using Context ): CaptureSet . Refs =
30- val refs1 = cs.elems
31- val refs2 = other.elems
32- def common (refs1 : CaptureSet . Refs , refs2 : CaptureSet . Refs ) =
29+ def overlapWith (other : Refs )(using Context ): Refs =
30+ val refs1 = refs
31+ val refs2 = other
32+ def common (refs1 : Refs , refs2 : Refs ) =
3333 refs1.filter: ref =>
3434 ref.isExclusive && refs2.exists(_.stripReadOnly eq ref)
35- common(refs1, refs2 ) ++ common(refs2, refs1 )
35+ common(refs, other ) ++ common(other, refs )
3636
37- private def hidden (elem : CaptureRef )(using Context ): CaptureSet .Refs = elem match
38- case Fresh .Cap (hcs) => hcs.elems.filter(! _.isRootCapability) ++ hidden(hcs)
39- case ReadOnlyCapability (ref) => hidden(ref).map(_.readOnly)
40- case _ => emptySet
41-
42- private def hidden (cs : CaptureSet )(using Context ): CaptureSet .Refs =
37+ private def hidden (refs : Refs )(using Context ): Refs =
4338 val seen : util.EqHashSet [CaptureRef ] = new util.EqHashSet
4439
45- def hiddenByElem (elem : CaptureRef ): CaptureSet . Refs =
40+ def hiddenByElem (elem : CaptureRef ): Refs =
4641 if seen.add(elem) then elem match
47- case Fresh .Cap (hcs) => hcs.elems.filter(! _.isRootCapability) ++ recur(hcs)
42+ case Fresh .Cap (hcs) => hcs.elems.filter(! _.isRootCapability) ++ recur(hcs.elems )
4843 case ReadOnlyCapability (ref) => hiddenByElem(ref).map(_.readOnly)
4944 case _ => emptySet
5045 else emptySet
5146
52- def recur (cs : CaptureSet ): CaptureSet . Refs =
53- (emptySet /: cs.elems ): (elems, elem) =>
47+ def recur (cs : Refs ): Refs =
48+ (emptySet /: cs): (elems, elem) =>
5449 elems ++ hiddenByElem(elem)
5550
56- recur(cs )
51+ recur(refs )
5752 end hidden
5853
5954 /** The captures of an argument or prefix widened to the formal parameter, if
6055 * the latter contains a cap.
6156 */
62- def formalCaptures (arg : Tree )(using Context ): CaptureSet . Const =
57+ def formalCaptures (arg : Tree )(using Context ): Refs =
6358 val argType = arg.nuType
6459 (if argType.hasUseAnnot then argType.deepCaptureSet else argType.captureSet)
65- .toConst
60+ .elems
6661
6762 /** The captures of an argument of prefix. No widening takes place */
68- def actualCaptures (arg : Tree )(using Context ): CaptureSet . Const =
63+ def actualCaptures (arg : Tree )(using Context ): Refs =
6964 val argType = arg.actualType.orElse(arg.nuType)
7065 (if arg.nuType.hasUseAnnot then argType.deepCaptureSet else argType.captureSet)
71- .toConst
66+ .elems
7267
7368 private def sepError (fn : Tree , args : List [Tree ], argIdx : Int ,
74- overlap : Refs , hiddenInArg : CaptureSet , footprints : List [(CaptureSet , Int )],
69+ overlap : Refs , hiddenInArg : Refs , footprints : List [(Refs , Int )],
7570 deps : collection.Map [Tree , List [Tree ]])(using Context ): Unit =
7671 val arg = args(argIdx)
7772 def paramName (mt : Type , idx : Int ): Option [Name ] = mt match
@@ -102,53 +97,48 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
10297 def clashType =
10398 clashTree.actualType.orElse(clashTree.nuType)
10499 def clashCaptures = actualCaptures(clashTree)
105- def clashHidden = CaptureSet (hidden(formalCaptures(clashTree)))
106- def hiddenCaptures = CaptureSet (hidden(formalCaptures(arg)))
100+ def hiddenCaptures = hidden(formalCaptures(arg))
107101 def clashFootprint = clashCaptures.footprint
108102 def hiddenFootprint = hiddenCaptures.footprint
109- def declaredFootprint = CaptureSet (deps(arg).map(actualCaptures(_).elems).foldLeft(emptySet)(_ ++ _)).footprint
110- def footprintOverlap = CaptureSet (hiddenFootprint.overlapWith(clashFootprint) -- declaredFootprint.elems)
111- def clashHiddenStr =
112- if clashTree.needsSepCheck then
113- i " \n Hidden set of $whereStr : $clashHidden"
114- else " "
103+ def declaredFootprint = deps(arg).map(actualCaptures(_)).foldLeft(emptySet)(_ ++ _).footprint
104+ def footprintOverlap = hiddenFootprint.overlapWith(clashFootprint) -- declaredFootprint
115105 report.error(
116106 em """ Separation failure: argument of type ${arg.actualType}
117107 |to $funStr
118108 |corresponds to capture-polymorphic formal parameter ${formalName}of type ${arg.nuType}
119109 |and captures ${CaptureSet (overlap)}, but $whatStr also passed separately
120110 |in the ${whereStr.trim} with type $clashType.
121111 |
122- | Capture set of $whereStr : $clashCaptures
123- | Hidden set of current argument : $hiddenCaptures
124- | Footprint of $whereStr : $clashFootprint
125- | Hidden footprint of current argument : $hiddenFootprint
126- | Declared footprint of current argument: $declaredFootprint
127- | Undeclared overlap of footprints : $footprintOverlap""" ,
112+ | Capture set of $whereStr : ${ CaptureSet ( clashCaptures)}
113+ | Hidden set of current argument : ${ CaptureSet ( hiddenCaptures)}
114+ | Footprint of $whereStr : ${ CaptureSet ( clashFootprint)}
115+ | Hidden footprint of current argument : ${ CaptureSet ( hiddenFootprint)}
116+ | Declared footprint of current argument: ${ CaptureSet ( declaredFootprint)}
117+ | Undeclared overlap of footprints : ${ CaptureSet ( footprintOverlap)} """ ,
128118 arg.srcPos)
129119 end sepError
130120
131121 private def checkApply (fn : Tree , args : List [Tree ], deps : collection.Map [Tree , List [Tree ]])(using Context ): Unit =
132122 val fnCaptures = methPart(fn) match
133123 case Select (qual, _) => qual.nuType.captureSet
134124 case _ => CaptureSet .empty
135- capt.println(i " check separate $fn( $args), fnCaptures = $fnCaptures, argCaptures = ${args.map(formalCaptures)}, deps = ${deps.toList}" )
136- var footprint = fnCaptures.footprint
137- val footprints = mutable.ListBuffer [(CaptureSet , Int )]((footprint, 0 ))
125+ capt.println(i " check separate $fn( $args), fnCaptures = $fnCaptures, argCaptures = ${args.map(arg => CaptureSet ( formalCaptures(arg)) )}, deps = ${deps.toList}" )
126+ var footprint = fnCaptures.elems. footprint
127+ val footprints = mutable.ListBuffer [(Refs , Int )]((footprint, 0 ))
138128 val indexedArgs = args.zipWithIndex
139129
140130 def subtractDeps (elems : Refs , arg : Tree ): Refs =
141131 deps(arg).foldLeft(elems): (elems, dep) =>
142- elems -- actualCaptures(dep).footprint.elems
132+ elems -- actualCaptures(dep).footprint
143133
144134 for (arg, idx) <- indexedArgs do
145135 if ! arg.needsSepCheck then
146- footprint = footprint ++ CaptureSet ( subtractDeps(actualCaptures(arg).footprint.elems , arg) )
136+ footprint = footprint ++ subtractDeps(actualCaptures(arg).footprint, arg)
147137 footprints += ((footprint, idx + 1 ))
148138 for (arg, idx) <- indexedArgs do
149139 if arg.needsSepCheck then
150140 val ac = formalCaptures(arg)
151- val hiddenInArg = CaptureSet ( hidden(ac) ).footprint
141+ val hiddenInArg = hidden(ac).footprint
152142 // println(i"check sep $arg: $ac, footprint so far = $footprint, hidden = $hiddenInArg")
153143 val overlap = subtractDeps(hiddenInArg.overlapWith(footprint), arg)
154144 if ! overlap.isEmpty then
0 commit comments