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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
package dotty.tools.dotc
package core
import Symbols._, Types._, Contexts._, Decorators._
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
private[core] var skolemsState = Skolemization.SkolemsDisallowed
final def ensureStableSingleton(tp: Type): SingletonType = tp.stripTypeVar match {
case tp: SingletonType if tp.isStable =>
tp
case tp: ValueType =>
assert(skolemsState != Skolemization.SkolemsDisallowed)
skolemsState = Skolemization.SkolemsEncountered
SkolemType(tp)
case tp: TypeProxy =>
ensureStableSingleton(tp.underlying)
}
/*@@@
/** If skolems were encountered, 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 deSkolemizeIfSkolemsSeen(tp: Type, toSuper: Boolean): Type =
if (skolemsState == Skolemization.SkolemsEncountered)
deSkolemize(tp, if (toSuper) 1 else -1, Set())
else tp
/** Approximate a type `tp` with a type that does not contain skolem types.
*/
final def deSkolemize(tp: Type): Type = deSkolemize(tp, 1, Set())
private def deSkolemize(tp: Type, variance: Int, seen: Set[SkolemType]): Type =
ctx.traceIndented(i"deskolemize $tp, variance = $variance, seen = $seen = ", show = true) {
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 eq tp.prefix) tp
else {
val d = tp.prefix.member(tp.name)
d.info match {
case TypeAlias(alias) => deSkolemize(alias, variance, seen)
case _ =>
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
}
}
}*/
}
object Skolemization extends Enumeration {
val SkolemsDisallowed, SkolemsAllowed, SkolemsEncountered = Value
}
|
