diff options
| -rw-r--r-- | src/dotty/tools/dotc/core/Skolemization.scala | 145 |
1 files changed, 0 insertions, 145 deletions
diff --git a/src/dotty/tools/dotc/core/Skolemization.scala b/src/dotty/tools/dotc/core/Skolemization.scala deleted file mode 100644 index 8baf612ba..000000000 --- a/src/dotty/tools/dotc/core/Skolemization.scala +++ /dev/null @@ -1,145 +0,0 @@ -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 -} |