@@ -301,96 +301,6 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
301
301
}
302
302
}
303
303
304
- /** A type is volatile if its DNF contains an alternative of the form
305
- * {P1, ..., Pn}, {N1, ..., Nk}, where the Pi are parent typerefs and the
306
- * Nj are refinement names, and one the 4 following conditions is met:
307
- *
308
- * 1. At least two of the parents Pi are abstract types.
309
- * 2. One of the parents Pi is an abstract type, and one other type Pj,
310
- * j != i has an abstract member which has the same name as an
311
- * abstract member of the whole type.
312
- * 3. One of the parents Pi is an abstract type, and one of the refinement
313
- * names Nj refers to an abstract member of the whole type.
314
- * 4. One of the parents Pi is an an alias type with a volatile alias
315
- * or an abstract type with a volatile upper bound.
316
- *
317
- * Lazy values are not allowed to have volatile type, as otherwise
318
- * unsoundness can result.
319
- */
320
- final def isVolatile (tp : Type ): Boolean = {
321
-
322
- /** Pre-filter to avoid expensive DNF computation
323
- * If needsChecking returns false it is guaranteed that
324
- * DNF does not contain intersections, or abstract types with upper
325
- * bounds that themselves need checking.
326
- */
327
- def needsChecking (tp : Type , isPart : Boolean ): Boolean = tp match {
328
- case tp : TypeRef =>
329
- tp.info match {
330
- case TypeAlias (alias) =>
331
- needsChecking(alias, isPart)
332
- case TypeBounds (lo, hi) =>
333
- isPart || tp.controlled(isVolatile(hi))
334
- case _ => false
335
- }
336
- case tp : RefinedType =>
337
- needsChecking(tp.parent, true )
338
- case tp : TypeProxy =>
339
- needsChecking(tp.underlying, isPart)
340
- case tp : AndType =>
341
- true
342
- case tp : OrType =>
343
- isPart || needsChecking(tp.tp1, isPart) && needsChecking(tp.tp2, isPart)
344
- case _ =>
345
- false
346
- }
347
-
348
- needsChecking(tp, false ) && {
349
- DNF (tp) forall { case (parents, refinedNames) =>
350
- val absParents = parents filter (_.symbol is Deferred )
351
- absParents.nonEmpty && {
352
- absParents.lengthCompare(2 ) >= 0 || {
353
- val ap = absParents.head
354
- ((parents exists (p =>
355
- (p ne ap)
356
- || p.memberNames(abstractTypeNameFilter, tp).nonEmpty
357
- || p.memberNames(abstractTermNameFilter, tp).nonEmpty))
358
- || (refinedNames & tp.memberNames(abstractTypeNameFilter, tp)).nonEmpty
359
- || (refinedNames & tp.memberNames(abstractTermNameFilter, tp)).nonEmpty
360
- || isVolatile(ap))
361
- }
362
- }
363
- }
364
- }
365
- }
366
-
367
- /** The disjunctive normal form of this type.
368
- * This collects a set of alternatives, each alternative consisting
369
- * of a set of typerefs and a set of refinement names. Both sets are represented
370
- * as lists, to obtain a deterministic order. Collected are
371
- * all type refs reachable by following aliases and type proxies, and
372
- * collecting the elements of conjunctions (&) and disjunctions (|).
373
- * The set of refinement names in each alternative
374
- * are the set of names in refinement types encountered during the collection.
375
- */
376
- final def DNF (tp : Type ): List [(List [TypeRef ], Set [Name ])] = ctx.traceIndented(s " DNF( $this) " , checks) {
377
- tp.dealias match {
378
- case tp : TypeRef =>
379
- (tp :: Nil , Set [Name ]()) :: Nil
380
- case RefinedType (parent, name) =>
381
- for ((ps, rs) <- DNF (parent)) yield (ps, rs + name)
382
- case tp : TypeProxy =>
383
- DNF (tp.underlying)
384
- case AndType (l, r) =>
385
- for ((lps, lrs) <- DNF (l); (rps, rrs) <- DNF (r))
386
- yield (lps | rps, lrs | rrs)
387
- case OrType (l, r) =>
388
- DNF (l) | DNF (r)
389
- case tp =>
390
- emptyDNF
391
- }
392
- }
393
-
394
304
/** The realizability status of given type `tp`*/
395
305
def realizability (tp : Type ): Realizability = tp.dealias match {
396
306
case tp : TermRef =>
@@ -411,7 +321,7 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
411
321
else boundsRealizability(tp)
412
322
}
413
323
414
- /** `Realizable` is `tp` has good bounds, a `HasProblemBounds` instance
324
+ /** `Realizable` if `tp` has good bounds, a `HasProblemBounds` instance
415
325
* pointing to a bad bounds member otherwise.
416
326
*/
417
327
def boundsRealizability (tp : Type )(implicit ctx : Context ) = {
0 commit comments