@@ -19,6 +19,7 @@ import Inferencing._
1919import ProtoTypes ._
2020import transform .SymUtils ._
2121import reporting .diagnostic .messages ._
22+ import reporting .trace
2223import config .Printers .{exhaustivity => debug }
2324import util .SourcePosition
2425
@@ -110,7 +111,7 @@ trait SpaceLogic {
110111 *
111112 * This reduces noise in counterexamples.
112113 */
113- def simplify (space : Space , aggressive : Boolean = false ): Space = space match {
114+ def simplify (space : Space , aggressive : Boolean = false )( implicit ctx : Context ) : Space = trace( s " simplify ${show(space)} , aggressive = $aggressive --> " , debug, x => show(x. asInstanceOf [ Space ]))( space match {
114115 case Prod (tp, fun, sym, spaces, full) =>
115116 val sp = Prod (tp, fun, sym, spaces.map(simplify(_)), full)
116117 if (sp.params.contains(Empty )) Empty
@@ -137,10 +138,10 @@ trait SpaceLogic {
137138 if (canDecompose(tp) && decompose(tp).isEmpty) Empty
138139 else space
139140 case _ => space
140- }
141+ })
141142
142143 /** Flatten space to get rid of `Or` for pretty print */
143- def flatten (space : Space ): List [Space ] = space match {
144+ def flatten (space : Space )( implicit ctx : Context ) : List [Space ] = space match {
144145 case Prod (tp, fun, sym, spaces, full) =>
145146 spaces.map(flatten) match {
146147 case Nil => Prod (tp, fun, sym, Nil , full) :: Nil
@@ -156,11 +157,11 @@ trait SpaceLogic {
156157 }
157158
158159 /** Is `a` a subspace of `b`? Equivalent to `a - b == Empty`, but faster */
159- def isSubspace (a : Space , b : Space ): Boolean = {
160+ def isSubspace (a : Space , b : Space )( implicit ctx : Context ) : Boolean = trace( s " ${show(a)} < ${show(b)} " , debug) {
160161 def tryDecompose1 (tp : Type ) = canDecompose(tp) && isSubspace(Or (decompose(tp)), b)
161162 def tryDecompose2 (tp : Type ) = canDecompose(tp) && isSubspace(a, Or (decompose(tp)))
162163
163- val res = (simplify(a), b) match {
164+ (simplify(a), b) match {
164165 case (Empty , _) => true
165166 case (_, Empty ) => false
166167 case (Or (ss), _) =>
@@ -179,18 +180,14 @@ trait SpaceLogic {
179180 case (Prod (_, fun1, sym1, ss1, _), Prod (_, fun2, sym2, ss2, _)) =>
180181 sym1 == sym2 && isEqualType(fun1, fun2) && ss1.zip(ss2).forall((isSubspace _).tupled)
181182 }
182-
183- debug.println(s " ${show(a)} < ${show(b)} = $res" )
184-
185- res
186183 }
187184
188185 /** Intersection of two spaces */
189- def intersect (a : Space , b : Space ): Space = {
186+ def intersect (a : Space , b : Space )( implicit ctx : Context ) : Space = trace( s " ${show(a)} & ${show(b)} " , debug, x => show(x. asInstanceOf [ Space ])) {
190187 def tryDecompose1 (tp : Type ) = intersect(Or (decompose(tp)), b)
191188 def tryDecompose2 (tp : Type ) = intersect(a, Or (decompose(tp)))
192189
193- val res : Space = (a, b) match {
190+ (a, b) match {
194191 case (Empty , _) | (_, Empty ) => Empty
195192 case (_, Or (ss)) => Or (ss.map(intersect(a, _)).filterConserve(_ ne Empty ))
196193 case (Or (ss), _) => Or (ss.map(intersect(_, b)).filterConserve(_ ne Empty ))
@@ -223,18 +220,14 @@ trait SpaceLogic {
223220 else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty )) Empty
224221 else Prod (tp1, fun1, sym1, ss1.zip(ss2).map((intersect _).tupled), full)
225222 }
226-
227- debug.println(s " ${show(a)} & ${show(b)} = ${show(res)}" )
228-
229- res
230223 }
231224
232225 /** The space of a not covered by b */
233- def minus (a : Space , b : Space ): Space = {
226+ def minus (a : Space , b : Space )( implicit ctx : Context ) : Space = trace( s " ${show(a)} - ${show(b)} " , debug, x => show(x. asInstanceOf [ Space ])) {
234227 def tryDecompose1 (tp : Type ) = minus(Or (decompose(tp)), b)
235228 def tryDecompose2 (tp : Type ) = minus(a, Or (decompose(tp)))
236229
237- val res = (a, b) match {
230+ (a, b) match {
238231 case (Empty , _) => Empty
239232 case (_, Empty ) => a
240233 case (Typ (tp1, _), Typ (tp2, _)) =>
@@ -273,10 +266,6 @@ trait SpaceLogic {
273266 })
274267
275268 }
276-
277- debug.println(s " ${show(a)} - ${show(b)} = ${show(res)}" )
278-
279- res
280269 }
281270}
282271
@@ -307,20 +296,19 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
307296 private val nullType = ConstantType (Constant (null ))
308297 private val nullSpace = Typ (nullType)
309298
310- override def intersectUnrelatedAtomicTypes (tp1 : Type , tp2 : Type ): Space = {
299+ override def intersectUnrelatedAtomicTypes (tp1 : Type , tp2 : Type ): Space = trace( s " atomic intersection: ${ AndType (tp1, tp2).show} " , debug) {
311300 // Precondition: !isSubType(tp1, tp2) && !isSubType(tp2, tp1)
312- if (tp1 == nullType || tp2 == nullType) {
313- // Since projections of types don't include null, intersection with null is empty.
314- return Empty
315- }
316- val res = ctx.typeComparer.disjoint(tp1, tp2)
317301
318- debug.println(s " atomic intersection: ${AndType (tp1, tp2).show} = ${! res}" )
302+ // Since projections of types don't include null, intersection with null is empty.
303+ if (tp1 == nullType || tp2 == nullType) Empty
304+ else {
305+ val res = ctx.typeComparer.disjoint(tp1, tp2)
319306
320- if (res) Empty
321- else if (tp1.isSingleton) Typ (tp1, true )
322- else if (tp2.isSingleton) Typ (tp2, true )
323- else Typ (AndType (tp1, tp2), true )
307+ if (res) Empty
308+ else if (tp1.isSingleton) Typ (tp1, true )
309+ else if (tp2.isSingleton) Typ (tp2, true )
310+ else Typ (AndType (tp1, tp2), true )
311+ }
324312 }
325313
326314 /** Return the space that represents the pattern `pat` */
@@ -635,7 +623,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
635623
636624 def doShow (s : Space , mergeList : Boolean = false ): String = s match {
637625 case Empty => " "
638- case Typ (c : ConstantType , _) => c.value.value.toString
626+ case Typ (c : ConstantType , _) => " " + c.value.value
639627 case Typ (tp : TermRef , _) => tp.symbol.showName
640628 case Typ (tp, decomposed) =>
641629 val sym = tp.widen.classSymbol
0 commit comments