1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
package dotty.tools.dotc
package core
import Symbols._, Types._, Contexts._
import collection.mutable
/** Methods to add and remove skolemtypes.
*
* Skolem types are generated when comparing refinements.
* A skolem type is simply a fresh singleton type that has a given type
* as underlying type.
* Two skolem types are equal if they refer to the same underlying type.
* To avoid unsoundness, skolem types have to be kept strictly local to the
* comparison, they are not allowed to escape the lifetime of a comparison
* by surviving in a context or in GADT bounds.
*/
trait Skolemization {
implicit val ctx: Context
protected var skolemsOutstanding = false
def ensureSingleton(tp: Type): SingletonType = tp.stripTypeVar match {
case tp: SingletonType =>
tp
case tp: ValueType =>
skolemsOutstanding = true
SkolemType(tp)
case tp: TypeProxy =>
ensureSingleton(tp.underlying)
}
/** Approximate a type `tp` with a type that does not contain skolem types.
* @param toSuper if true, return the smallest supertype of `tp` with this property
* else return the largest subtype.
*/
final def deSkolemize(tp: Type, toSuper: Boolean): Type =
if (skolemsOutstanding) deSkolemize(tp, if (toSuper) 1 else -1, Set())
else tp
private def deSkolemize(tp: Type, variance: Int, seen: Set[SkolemType]): Type =
ctx.traceIndented(s"deskolemize $tp, variance = $variance, seen = $seen = ") {
def approx(lo: Type = defn.NothingType, hi: Type = defn.AnyType, newSeen: Set[SkolemType] = seen) =
if (variance == 0) NoType
else deSkolemize(if (variance < 0) lo else hi, variance, newSeen)
tp match {
case tp: SkolemType =>
if (seen contains tp) NoType
else approx(hi = tp.binder, newSeen = seen + tp)
case tp: NamedType =>
val sym = tp.symbol
if (sym.isStatic) tp
else {
val pre1 = deSkolemize(tp.prefix, variance, seen)
if (pre1.exists && !pre1.isRef(defn.NothingClass)) tp.derivedSelect(pre1)
else {
ctx.log(s"deskolem: $tp: ${tp.info}")
tp.info match {
case TypeBounds(lo, hi) => approx(lo, hi)
case info => approx(defn.NothingType, info)
}
}
}
case _: ThisType | _: BoundType | _: SuperType | NoType | NoPrefix =>
tp
case tp: RefinedType =>
val parent1 = deSkolemize(tp.parent, variance, seen)
if (parent1.exists) {
val refinedInfo1 = deSkolemize(tp.refinedInfo, variance, seen)
if (refinedInfo1.exists)
tp.derivedRefinedType(parent1, tp.refinedName, refinedInfo1)
else
approx(hi = parent1)
}
else approx()
case tp: TypeAlias =>
val alias1 = deSkolemize(tp.alias, variance * tp.variance, seen)
if (alias1.exists) tp.derivedTypeAlias(alias1)
else approx(hi = TypeBounds.empty)
case tp: TypeBounds =>
val lo1 = deSkolemize(tp.lo, -variance, seen)
val hi1 = deSkolemize(tp.hi, variance, seen)
if (lo1.exists && hi1.exists) tp.derivedTypeBounds(lo1, hi1)
else approx(hi =
if (lo1.exists) TypeBounds.lower(lo1)
else if (hi1.exists) TypeBounds.upper(hi1)
else TypeBounds.empty)
case tp: ClassInfo =>
val pre1 = deSkolemize(tp.prefix, variance, seen)
if (pre1.exists) tp.derivedClassInfo(pre1)
else NoType
case tp: AndOrType =>
val tp1d = deSkolemize(tp.tp1, variance, seen)
val tp2d = deSkolemize(tp.tp2, variance, seen)
if (tp1d.exists && tp2d.exists)
tp.derivedAndOrType(tp1d, tp2d)
else if (tp.isAnd)
approx(hi = tp1d & tp2d) // if one of tp1d, tp2d exists, it is the result of tp1d & tp2d
else
approx(lo = tp1d & tp2d)
case tp: WildcardType =>
val bounds1 = deSkolemize(tp.optBounds, variance, seen)
if (bounds1.exists) tp.derivedWildcardType(bounds1)
else WildcardType
case _ =>
if (tp.isInstanceOf[MethodicType]) assert(variance != 0, tp)
deSkolemizeMap.mapOver(tp, variance, seen)
}
}
object deSkolemizeMap extends TypeMap {
private var seen: Set[SkolemType] = _
def apply(tp: Type) = deSkolemize(tp, variance, seen)
def mapOver(tp: Type, variance: Int, seen: Set[SkolemType]) = {
val savedVariance = this.variance
val savedSeen = this.seen
this.variance = variance
this.seen = seen
try super.mapOver(tp)
finally {
this.variance = savedVariance
this.seen = savedSeen
}
}
}
}
|
