diff options
author | Martin Odersky <odersky@gmail.com> | 2015-01-18 18:35:02 +0100 |
---|---|---|
committer | Martin Odersky <odersky@gmail.com> | 2015-01-18 18:38:12 +0100 |
commit | fbe4171404ac56a0fe8e6d54fa06bbd53e85bd97 (patch) | |
tree | bd05c10e99a025ea8cde678203af1c4dfbe11b60 /src/dotty | |
parent | 566dd6e8a44090168ebe8e6703fea27152802286 (diff) | |
download | dotty-fbe4171404ac56a0fe8e6d54fa06bbd53e85bd97.tar.gz dotty-fbe4171404ac56a0fe8e6d54fa06bbd53e85bd97.tar.bz2 dotty-fbe4171404ac56a0fe8e6d54fa06bbd53e85bd97.zip |
New constraint handling
New constraint handling scheme using constraints that distinguish more between
parameter and non-parameter bounds and which track parameter bounds separately.
This allows a co-inductive formulation of satisfiability checking without fishy
cyclicity checks. It should also scale better for long chains of dependent type
variables.
Diffstat (limited to 'src/dotty')
-rw-r--r-- | src/dotty/tools/dotc/config/Config.scala | 6 | ||||
-rw-r--r-- | src/dotty/tools/dotc/config/ScalaSettings.scala | 2 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/Constants.scala | 2 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/Constraint.scala | 91 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/ConstraintHandling.scala | 394 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/NaiveConstraint.scala | 378 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/TrackingConstraint.scala | 283 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/TypeComparer.scala | 32 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/TyperState.scala | 4 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/Types.scala | 2 | ||||
-rw-r--r-- | src/dotty/tools/dotc/printing/PlainPrinter.scala | 8 | ||||
-rw-r--r-- | src/dotty/tools/dotc/typer/Inferencing.scala | 2 | ||||
-rw-r--r-- | src/dotty/tools/dotc/typer/ProtoTypes.scala | 3 |
13 files changed, 382 insertions, 825 deletions
diff --git a/src/dotty/tools/dotc/config/Config.scala b/src/dotty/tools/dotc/config/Config.scala index 29d5f7922..81c1af5c9 100644 --- a/src/dotty/tools/dotc/config/Config.scala +++ b/src/dotty/tools/dotc/config/Config.scala @@ -58,12 +58,6 @@ object Config { /** The recursion depth for showing a summarized string */ final val summarizeDepth = 2 - /** Track dependencies for constraint propagation satisfiability checking - * If turned off, constraint checking is simpler but potentially slower - * for large constraints. - */ - final val trackConstrDeps = true - /** Check that variances of lambda arguments match the * variance of the underlying lambda class. */ diff --git a/src/dotty/tools/dotc/config/ScalaSettings.scala b/src/dotty/tools/dotc/config/ScalaSettings.scala index 35c3ac16a..281a4b6c7 100644 --- a/src/dotty/tools/dotc/config/ScalaSettings.scala +++ b/src/dotty/tools/dotc/config/ScalaSettings.scala @@ -167,7 +167,7 @@ class ScalaSettings extends Settings.SettingGroup { val Yrepldebug = BooleanSetting("-Yrepl-debug", "Trace all repl activity.") val Ytyperdebug = BooleanSetting("-Ytyper-debug", "Trace all type assignments.") val Ypatmatdebug = BooleanSetting("-Ypatmat-debug", "Trace pattern matching translation.") - val Yexplainlowlevel = BooleanSetting("-Yexplainlowlevel", "When explaining type errors, show types at a lower level.") + val Yexplainlowlevel = BooleanSetting("-Yexplain-lowlevel", "When explaining type errors, show types at a lower level.") val YnoDoubleBindings = BooleanSetting("-YnoDoubleBindings", "Assert no namedtype is bound twice (should be enabled only if program is error-free).") val optimise = BooleanSetting("-optimise", "Generates faster bytecode by applying optimisations to the program") withAbbreviation "-optimize" diff --git a/src/dotty/tools/dotc/core/Constants.scala b/src/dotty/tools/dotc/core/Constants.scala index 48c832c4b..61a23bb9e 100644 --- a/src/dotty/tools/dotc/core/Constants.scala +++ b/src/dotty/tools/dotc/core/Constants.scala @@ -169,7 +169,7 @@ object Constants { def convertTo(pt: Type)(implicit ctx: Context): Constant = { def lowerBound(pt: Type): Type = pt.dealias.stripTypeVar match { case tref: TypeRef if !tref.symbol.isClass => lowerBound(tref.info.bounds.lo) - case param: PolyParam => lowerBound(ctx.typeComparer.bounds(param).lo) + case param: PolyParam => lowerBound(ctx.typerState.constraint.nonParamBounds(param).lo) case pt => pt } val target = lowerBound(pt).typeSymbol diff --git a/src/dotty/tools/dotc/core/Constraint.scala b/src/dotty/tools/dotc/core/Constraint.scala index f7e7a2e13..10e6d0d5a 100644 --- a/src/dotty/tools/dotc/core/Constraint.scala +++ b/src/dotty/tools/dotc/core/Constraint.scala @@ -31,30 +31,46 @@ abstract class Constraint extends Showable { /** Does this constraint contain the type variable `tvar` and is it uninstantiated? */ def contains(tvar: TypeVar): Boolean - /** The constraint for given type parameter `param`, or NoType if `param` is not part of + /** The constraint entry for given type parameter `param`, or NoType if `param` is not part of * the constraint domain. */ - def at(param: PolyParam)(implicit ctx: Context): Type + def entry(param: PolyParam): Type /** The type variable corresponding to parameter `param`, or * NoType, if `param` is not in constrained or is not paired with a type variable. */ def typeVarOfParam(param: PolyParam): Type - + + /** Is it known that `param1 <:< param2`? */ + def isLess(param1: PolyParam, param2: PolyParam)(implicit ctx: Context): Boolean + + /** The parameters that are known to be smaller wrt <: than `param` */ + def lower(param: PolyParam): List[PolyParam] + + /** The parameters that are known to be greater wrt <: than `param` */ + def upper(param: PolyParam): List[PolyParam] + + /** lower(param) \ lower(butNot) */ + def exclusiveLower(param: PolyParam, butNot: PolyParam): List[PolyParam] + + /** upper(param) \ upper(butNot) */ + def exclusiveUpper(param: PolyParam, butNot: PolyParam): List[PolyParam] + /** The constraint bounds for given type parameter `param`. + * Poly params that are known to be smaller or greater than `param` + * are not contained in the return bounds. * @pre `param` is not part of the constraint domain. */ - def bounds(param: PolyParam)(implicit ctx: Context): TypeBounds + def nonParamBounds(param: PolyParam): TypeBounds + + /** The lower bound of `param` including all known-to-be-smaller parameters */ + def fullLowerBound(param: PolyParam)(implicit ctx: Context): Type - /** The non-parameter bounds of this constraint. - * Poly params that are `related` are not contained in the return bounds. - */ - def nonParamBounds(param: PolyParam)(implicit ctx: Context): TypeBounds + /** The upper bound of `param` including all known-to-be-greater parameters */ + def fullUpperBound(param: PolyParam)(implicit ctx: Context): Type - /** If `firstIsLower` is `param1 <:< param2`? - * Otherwise, is `param2 <:< param1`? - */ - def related(param1: PolyParam, param2: PolyParam, firstIsLower: Boolean)(implicit ctx: Context): Boolean + /** The bounds of `param` including all known-to-be-smaller and -greater parameters */ + def fullBounds(param: PolyParam)(implicit ctx: Context): TypeBounds /** A new constraint which is derived from this constraint by adding * entries for all type parameters of `poly`. @@ -66,26 +82,28 @@ abstract class Constraint extends Showable { def add(poly: PolyType, tvars: List[TypeVar])(implicit ctx: Context): This /** A new constraint which is derived from this constraint by updating - * the entry for parameter `param` to `tpe`. - * @pre `this contains param`. - * + * the entry for parameter `param` to `tp`. * `tp` can be one of the following: * * - A TypeBounds value, indicating new constraint bounds * - Another type, indicating a solution for the parameter + * + * @pre `this contains param`. */ - def updated(param: PolyParam, tp: Type)(implicit ctx: Context): This + def updateEntry(param: PolyParam, tp: Type)(implicit ctx: Context): This - /** A constraint that includes a the relationship `param <: bound` if `inOrder` is true - * or else `bound <: param` if `inOrdxer` is false. + /** A constraint that includes the relationship `p1 <: p2` */ - def order(param: PolyParam, bound: PolyParam, inOrder: Boolean)(implicit ctx: Context): This + def addLess(p1: PolyParam, p2: PolyParam)(implicit ctx: Context): This + + /** A constraint resulting by adding p2 = p1 to this constraint, and at the same + * time transferring all bounds of p2 to p1 + */ + def unify(p1: PolyParam, p2: PolyParam)(implicit ctx: Context): This /** A new constraint which is derived from this constraint by removing * the type parameter `param` from the domain and replacing all occurrences * of the parameter elsewhere in the constraint by type `tp`. - * If `tp` is another polyparam, applies the necessary unifications to avoid a cyclic - * constraint. */ def replace(param: PolyParam, tp: Type)(implicit ctx: Context): This @@ -99,11 +117,6 @@ abstract class Constraint extends Showable { /** A new constraint with all entries coming from `pt` removed. */ def remove(pt: PolyType)(implicit ctx: Context): This - /** A constraint resulting by adding p2 = p1 to this constraint, and at the same - * time transferring all bounds of p2 to p1 - */ - def unify(p1: PolyParam, p2: PolyParam)(implicit ctx: Context): This - /** The polytypes constrained by this constraint */ def domainPolys: List[PolyType] @@ -121,32 +134,6 @@ abstract class Constraint extends Showable { /** The uninstantiated typevars of this constraint */ def uninstVars: collection.Seq[TypeVar] - /** Check that no constrained parameter in `pt` contains itself as a bound */ - def checkNonCyclic(pt: PolyType, entries: Array[Type])(implicit ctx: Context): Unit - /** Check that no constrained parameter contains itself as a bound */ def checkNonCyclic()(implicit ctx: Context): Unit - - /** Check that no constrained parameter contains itself as a bound, - * either directly or indirectly. This should be not a stricter criterion - * than checkNonCyclic because transitivity should be eliminated always, - * but it's good to be paranoid. - */ - def checkNonCyclicTrans()(implicit ctx: Context): Unit - - protected def splitParams(tp: Type, seenFromBelow: Boolean, handleParam: PolyParam => Unit)(implicit ctx: Context): Type = tp match { - case tp: PolyParam if contains(tp) => - handleParam(tp) - NoType - case tp: AndOrType if seenFromBelow == tp.isAnd => - val tp1 = splitParams(tp.tp1, seenFromBelow, handleParam) - val tp2 = splitParams(tp.tp2, seenFromBelow, handleParam) - if (tp1.exists) - if (tp2.exists) tp.derivedAndOrType(tp1, tp2) - else tp1 - else if (tp2.exists) tp2 - else NoType - case _ => - tp - } } diff --git a/src/dotty/tools/dotc/core/ConstraintHandling.scala b/src/dotty/tools/dotc/core/ConstraintHandling.scala index 96174ad1c..530bbfce4 100644 --- a/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -36,219 +36,118 @@ trait ConstraintHandling { implicit val ctx: Context def isSubType(tp1: Type, tp2: Type): Boolean - def deSkolemize(tp: Type, toSuper: Boolean): Type val state: TyperState import state.constraint + + private var addConstraintInvocations = 0 /** If the constraint is frozen we cannot add new bounds to the constraint. */ protected var frozenConstraint = false - /** If the constraint is ignored, subtype checks only take into account - * declared bounds of PolyParams. Used when forming unions and intersectons - * of constraint bounds - */ - private var ignoreConstraint = false - - private def ignoringConstraint[T](op: => T): T = { - val savedIgnore = ignoreConstraint - val savedFrozen = frozenConstraint - ignoreConstraint = true - frozenConstraint = true - try op - finally { - ignoreConstraint = savedIgnore - frozenConstraint = savedFrozen + private def addOneUpperBound(param: PolyParam, bound: Type): Boolean = + constraint.entry(param) match { + case oldBounds @ TypeBounds(lo, hi) => + val newHi = hi & bound + (newHi eq hi) || { + val newBounds = oldBounds.derivedTypeBounds(lo, newHi) + constraint = constraint.updateEntry(param, newBounds) + isSubType(lo, newHi) + } + case _ => + true + } + + private def addOneLowerBound(param: PolyParam, bound: Type): Boolean = + constraint.entry(param) match { + case oldBounds @ TypeBounds(lo, hi) => + val newLo = lo | bound + (newLo eq lo) || { + val newBounds = oldBounds.derivedTypeBounds(newLo, hi) + constraint = constraint.updateEntry(param, newBounds) + isSubType(newLo, hi) + } + case _ => + true + } + + protected def addUpperBound(param: PolyParam, bound: Type): Boolean = { + def description = i"constraint $param <: $bound to\n$constraint" + if (bound.isRef(defn.NothingClass) && ctx.typerState.isGlobalCommittable) { + def msg = s"!!! instantiated to Nothing: $param, constraint = ${constraint.show}" + if (Config.flagInstantiationToNothing) assert(false, msg) + else ctx.log(msg) } + constr.println(i"adding $description") + val lower = constraint.lower(param) + val res = addOneUpperBound(param, bound) && lower.forall(addOneUpperBound(_, bound)) + constr.println(i"added $description = $res") + res } - - protected def isSubTypeWhenFrozen(tp1: Type, tp2: Type): Boolean = { - val saved = frozenConstraint - frozenConstraint = true - try isSubType(tp1, tp2) - finally frozenConstraint = saved + + protected def addLowerBound(param: PolyParam, bound: Type): Boolean = { + def description = i"constraint $param >: $bound to\n$constraint" + constr.println(i"adding $description") + val upper = constraint.upper(param) + val res = addOneLowerBound(param, bound) && upper.forall(addOneLowerBound(_, bound)) + constr.println(i"added $description = $res") + res } - - protected def constraintImpliesSub(param: PolyParam, tp: Type): Boolean = - isSubTypeWhenFrozen(bounds(param).hi, tp) - - protected def constraintImpliesSuper(param: PolyParam, tp: Type): Boolean = - isSubTypeWhenFrozen(tp, bounds(param).lo) - - /** The current bounds of type parameter `param` */ - final def bounds(param: PolyParam): TypeBounds = constraint at param match { - case bounds: TypeBounds if !ignoreConstraint => bounds - case _ => param.binder.paramBounds(param.paramNum) + + protected def addLess(p1: PolyParam, p2: PolyParam): Boolean = { + def description = i"ordering $p1 <: $p2 to\n$constraint" + val res = + if (constraint.isLess(p2, p1)) unify(p2, p1) + // !!! this is direction dependent - unify(p1, p2) makes i94-nada loop forever. + // Need to investigate why this is the case. + // The symptom is that we get a subtyping constraint of the form P { ... } <: P + else { + val down1 = p1 :: constraint.exclusiveLower(p1, p2) + val up2 = p2 :: constraint.exclusiveUpper(p2, p1) + val lo1 = constraint.nonParamBounds(p1).lo + val hi2 = constraint.nonParamBounds(p2).hi + constr.println(i"adding $description down1 = $down1, up2 = $up2") + constraint = constraint.addLess(p1, p2) + down1.forall(addOneUpperBound(_, hi2)) && up2.forall(addOneLowerBound(_, lo1)) + } + constr.println(i"added $description = $res") + res } - - /** Compare a solution of the constraint instead of the constrained parameters. - * The solution maps every parameter to its lower bound. + + /** Make p2 = p1, transfer all bounds of p2 to p1 + * @pre less(p1)(p2) */ - protected var solvedConstraint = false - - /** The parameters currently being constrained by addConstraint */ - private var pendingParams: Set[PolyParam] = Set() - - /** Make p2 = p1, transfer all bounds of p2 to p1 */ private def unify(p1: PolyParam, p2: PolyParam): Boolean = { constr.println(s"unifying $p1 $p2") - val constraint1 = constraint.unify(p1, p2) - val bounds = constraint1.bounds(p1) - isSubType(bounds.lo, bounds.hi) && { constraint = constraint1; true } + val down = constraint.exclusiveLower(p2, p1) + val up = constraint.exclusiveUpper(p1, p2) + constraint = constraint.unify(p1, p2) + val bounds = constraint.nonParamBounds(p1) + val lo = bounds.lo + val hi = bounds.hi + isSubType(lo, hi) && + down.forall(addOneUpperBound(_, hi)) && + up.forall(addOneLowerBound(_, lo)) } - - /** If current constraint set is not frozen, add the constraint - * - * param >: bound if fromBelow is true - * param <: bound otherwise - * - * to the bounds of `param`. If `bound` is itself a constrained parameter, also - * add the dual constraint to `bound`. - * @pre `param` is in the constraint's domain - * @return Whether the augmented constraint is still satisfiable. - */ - def addConstraint(param: PolyParam, bound0: Type, fromBelow: Boolean): Boolean = { - - /** Add bidirectional constraint. If new constraint implies 'A <: B' we also - * make sure 'B >: A' gets added and vice versa. Furthermore, if the constraint - * implies 'A <: B <: A', A and B get unified. - */ - def addc(param: PolyParam, bound: Type, fromBelow: Boolean): Boolean = { - val pbounds0 = constraint.bounds(param) - bound match { - case bound: PolyParam if constraint contains bound => - val bbounds0 @ TypeBounds(lo, hi) = constraint.bounds(bound) - if (lo eq hi) - addc(param, lo, fromBelow) - else if (param == bound) - true - else if (fromBelow && param.occursIn(lo, fromBelow = true)) - unify(param, bound) - else if (!fromBelow && param.occursIn(hi, fromBelow = false)) - unify(bound, param) - else { - val pbounds = prepare(param, bound, fromBelow) - val bbounds = prepare(bound, param, !fromBelow) - pbounds.exists && bbounds.exists && { - install(param, pbounds.bounds, pbounds0) - install(bound, bbounds.bounds, bbounds0) - true - } - } - case bound: AndOrType if fromBelow != bound.isAnd => - addc(param, bound.tp1, fromBelow) && - addc(param, bound.tp2, fromBelow) - case bound: WildcardType => - true - case bound => // !!! remove to keep the originals - val pbounds = prepare(param, bound, fromBelow) - pbounds.exists && { - install(param, pbounds.bounds, pbounds0) - true - } - } - } - - /** Install bounds for param */ - def install(param: PolyParam, newBounds: TypeBounds, oldBounds: TypeBounds): Unit = { - val curBounds = constraint.bounds(param) - try { - constraint = constraint.updated(param, newBounds) - } catch { - case ex: AssertionError => - println(i"error while updating $param $newBounds\n$constraint") - throw ex - } - if (curBounds ne oldBounds) { - // In this case the bounds were updated previously by a recursive isSubType in - // the satisfiability check of prepare. Reapply the previously added bounds, but - // go through a full addConstraint in order to eliminate any cyclic dependencies - // via unification. - if (!ignoringConstraint(isSubType(curBounds.lo, newBounds.lo))) - addConstraint(param, curBounds.lo, fromBelow) - if (!ignoringConstraint(isSubType(newBounds.hi, curBounds.hi))) - addConstraint(param, curBounds.hi, !fromBelow) - } - } - - /** Compute new bounds for `param` and check whether they are - * satisfiable. The check might in turn trigger other additions to the constraint. - * @return The new bounds for `param` (which are not installed yet), or - * NoType, if the new constraint would not be satisfiable. - */ - def prepare(param: PolyParam, bound: Type, fromBelow: Boolean): Type = { - constr.println(s"prepare ${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show}") - val oldBounds = constraint.bounds(param) - val newBounds = ignoringConstraint { - if (fromBelow) oldBounds.derivedTypeBounds(oldBounds.lo | bound, oldBounds.hi) - else oldBounds.derivedTypeBounds(oldBounds.lo, oldBounds.hi & bound) - } - val ok = - (param == bound) || - (oldBounds eq newBounds) || - { - if (pendingParams contains param) { - // Why the pendingParams test? It is possible that recursive subtype invocations - // come back with another constraint for `param`. An example came up when compiling - // ElimRepeated where we got the constraint - // - // Coll <: IterableLike[Tree, Coll] - // - // and added - // - // List[Tree] <: Coll - // - // The recursive bounds test is then - // - // List[Tree] <: IterableLike[Tree, Coll] - // - // and because of the F-bounded polymorphism in the supertype of List, - // i.e. List[T] <: IterableLike[T, List[T]], this leads again to - // - // List[Tree] <: Coll - // - // If a parameter is already pending, we avoid revisiting it here. - // Instead we combine the bounds computed here with the originally - // computed bounds when installing the original type. - constr.println(i"deferred bounds: $param $newBounds") - true - } else { - pendingParams += param - try isSubType(newBounds.lo, newBounds.hi) - finally pendingParams -= param - } - } - if (ok) newBounds else NoType - } - val bound = deSkolemize(bound0, toSuper = fromBelow).dealias.stripTypeVar - def description = s"${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show} to ${constraint.show}" - constr.println(s"adding $description") - val res = addc(param, bound, fromBelow) - constr.println(s"added $description") - if (Config.checkConstraintsNonCyclicTrans) constraint.checkNonCyclicTrans() - res + + protected final def isSubTypeWhenFrozen(tp1: Type, tp2: Type): Boolean = { + val saved = frozenConstraint + frozenConstraint = true + try isSubType(tp1, tp2) + finally frozenConstraint = saved } - final def canConstrain(param: PolyParam): Boolean = - !frozenConstraint && !solvedConstraint && (constraint contains param) - /** Test whether the lower bounds of all parameters in this * constraint are a solution to the constraint. */ - final def isSatisfiable: Boolean = { - val saved = solvedConstraint - solvedConstraint = true - try - constraint.forallParams { param => - val TypeBounds(lo, hi) = constraint.at(param) - isSubType(lo, hi) || { - ctx.log(i"sub fail $lo <:< $hi") - ctx.log(i"approximated = ${approxParams(lo)} <:< ${approxParams(hi)}") - false - } + protected final def isSatisfiable: Boolean = + constraint.forallParams { param => + val TypeBounds(lo, hi) = constraint.entry(param) + isSubType(lo, hi) || { + ctx.log(i"sub fail $lo <:< $hi") + false } - finally solvedConstraint = saved - } + } /** Solve constraint set for given type parameter `param`. * If `fromBelow` is true the parameter is approximated by its lower bound, @@ -269,22 +168,113 @@ trait ConstraintHandling { } } } - val bounds = constraint.bounds(param) - val bound = if (fromBelow) bounds.lo else bounds.hi + val bound = if (fromBelow) constraint.fullLowerBound(param) else constraint.fullUpperBound(param) val inst = avoidParam(bound) typr.println(s"approx ${param.show}, from below = $fromBelow, bound = ${bound.show}, inst = ${inst.show}") inst } - /** Map that approximates each param in constraint by its lower bound. - * Currently only used for diagnostics. + /** Constraint `c1` subsumes constraint `c2`, if under `c2` as constraint we have + * for all poly params `p` defined in `c2` as `p >: L2 <: U2`: + * + * c1 defines p with bounds p >: L1 <: U1, and + * L2 <: L1, and + * U1 <: U2 + * + * Both `c1` and `c2` are required to derive from constraint `pre`, possibly + * narrowing it with further bounds. */ - final def approxParams = new TypeMap { // !!! Dotty problem: Turn this def into a val => -Ycheck:mix fails - def apply(tp: Type): Type = tp.stripTypeVar match { - case tp: PolyParam if constraint contains tp => - this(constraint.bounds(tp).lo) - case tp => - mapOver(tp) + protected final def subsumes(c1: Constraint, c2: Constraint, pre: Constraint): Boolean = + if (c2 eq pre) true + else if (c1 eq pre) false + else { + val saved = constraint + try + c2.forallParams(p => + c1.contains(p) && + c2.upper(p).forall(c1.isLess(p, _)) && + isSubTypeWhenFrozen(c1.nonParamBounds(p), c2.nonParamBounds(p))) + finally constraint = saved + } + + protected def solvedConstraint = false + + /** The current bounds of type parameter `param` */ + final def bounds(param: PolyParam): TypeBounds = constraint.entry(param) match { + case bounds: TypeBounds => bounds + case _ => param.binder.paramBounds(param.paramNum) + } + + def initialize(pt: PolyType): Boolean = { + //println(i"INIT**! $pt") + checkPropagated(i"initialized $pt") { + pt.paramNames.indices.forall { i => + val param = PolyParam(pt, i) + val bounds = constraint.nonParamBounds(param) + val lower = constraint.lower(param) + val upper = constraint.upper(param) + if (lower.nonEmpty && !bounds.lo.isRef(defn.NothingClass) || + upper.nonEmpty && !bounds.hi.isRef(defn.AnyClass)) println(i"INIT*** $pt") + lower.forall(addOneUpperBound(_, bounds.hi)) && + upper.forall(addOneLowerBound(_, bounds.lo)) + } + } + } + + protected def constraintImpliesSub(param: PolyParam, tp: Type): Boolean = + isSubTypeWhenFrozen(bounds(param).hi, tp) + + protected def constraintImpliesSuper(param: PolyParam, tp: Type): Boolean = + isSubTypeWhenFrozen(tp, bounds(param).lo) + + final def canConstrain(param: PolyParam): Boolean = + !frozenConstraint && !solvedConstraint && (constraint contains param) + + protected def addConstraint(param: PolyParam, bound: Type, fromBelow: Boolean): Boolean = { + def description = i"constr $param ${if (fromBelow) ">:" else "<:"} $bound:\n$constraint" + checkPropagated(s"adding $description")(true) + checkPropagated(s"added $description") { + addConstraintInvocations += 1 + try bound.dealias.stripTypeVar match { + case bound: PolyParam if constraint contains bound => + if (fromBelow) addLess(bound, param) else addLess(param, bound) + case bound: AndOrType if fromBelow != bound.isAnd => + addConstraint(param, bound.tp1, fromBelow) && addConstraint(param, bound.tp2, fromBelow) + case bound: WildcardType => + true + case bound: ErrorType => + true + case _ => + if (occursAtToplevel(param, bound)) fromBelow + else if (fromBelow) addLowerBound(param, bound) + else addUpperBound(param, bound) + } + finally addConstraintInvocations -= 1 + } + } + + private def occursAtToplevel(param: Type, tp: Type): Boolean = tp match { + case tp: PolyParam => + param == tp + case bound: TypeProxy => + occursAtToplevel(param, bound.underlying) + case bound: AndOrType => + occursAtToplevel(param, bound.tp1) || occursAtToplevel(param, bound.tp2) + case _ => + false + } + + def checkPropagated(msg: => String)(result: Boolean): Boolean = { + if (result && addConstraintInvocations == 0) { + frozenConstraint = true + for (p <- constraint.domainParams) { + for (u <- constraint.upper(p)) + assert(bounds(p).hi <:< bounds(u).hi, i"propagation failure for upper $p subsumes $u\n$msg") + for (l <- constraint.lower(p)) + assert(bounds(l).lo <:< bounds(p).lo, i"propagation failure for lower $p subsumes $l\n$msg") + } + frozenConstraint = false } + result } } diff --git a/src/dotty/tools/dotc/core/NaiveConstraint.scala b/src/dotty/tools/dotc/core/NaiveConstraint.scala deleted file mode 100644 index ae5d5b0f1..000000000 --- a/src/dotty/tools/dotc/core/NaiveConstraint.scala +++ /dev/null @@ -1,378 +0,0 @@ -package dotty.tools -package dotc -package core - -import Types._, Contexts._, Symbols._ -import util.SimpleMap -import collection.mutable -import printing.{Printer, Showable} -import printing.Texts._ -import config.Config -import config.Printers._ - -object NaiveConstraint { - - /** The type of `Constraint#myMap` */ - type ParamInfo = SimpleMap[PolyType, Array[Type]] - - /** The type of `Constraint#dependents */ - type DependentMap = SimpleMap[PolyType, Array[Set[PolyParam]]] - - /** The type of functions that include or exclude a `PolyParam` in or from a set*/ - private type DepDelta = (Set[PolyParam], PolyParam) => Set[PolyParam] - - private val addDep: DepDelta = (_ + _) - private val removeDep: DepDelta = (_ - _) - - private val NoTypeBounds = new TypeBounds(WildcardType, WildcardType) { - override def computeHash = unsupported("computeHash") - } - - /** An accumulator that changes dependencies on `param`. - * @param param The parameter to which changed dependencies refer. - * @param ofVariance Include `PolyParams` occurring at this variance in the dependencies. - * @param delta The dependency change to perform (add or remove). - */ - private class ChangeDependencies(param: PolyParam, ofVariance: Int, delta: DepDelta)(implicit ctx: Context) - extends TypeAccumulator[DependentMap] { - def apply(deps: DependentMap, tp: Type): DependentMap = tp match { - case tp @ PolyParam(pt, n) if - this.variance == 0 || this.variance == ofVariance => - val oldDeps = deps(pt) - val original = safeSelect(oldDeps, n) - val changed = delta(original, param) - if (original eq changed) deps - else { - val newDeps = - if (oldDeps == null) new Array[Set[PolyParam]](pt.paramBounds.length) - else oldDeps.clone - newDeps(n) = changed - deps.updated(pt, newDeps) - } - case _ => foldOver(deps, tp) - } - } - - /** `deps(n)`, except that `Set()` is returned if `deps` or `deps(n)` are null */ - private def safeSelect(deps: Array[Set[PolyParam]], n: Int) : Set[PolyParam] = - if (deps == null || deps(n) == null) Set() - else deps(n) - - private def ignoreParam(p: PolyParam): Unit = {} -} - -import NaiveConstraint._ - -/** Constraint over undetermined type parameters - * @param myMap a map from PolyType to arrays. - * Each array contains twice the number of entries as there a type parameters - * in the PolyType. The first half of the array contains the type bounds that constrain the - * polytype's type parameters. The second half might contain type variables that - * track the corresponding parameters, or is left empty (filled with nulls). - * An instantiated type parameter is represented by having its instance type in - * the corresponding array entry. - */ -class NaiveConstraint(private val myMap: ParamInfo) extends Constraint { - - type This = NaiveConstraint - - def contains(pt: PolyType): Boolean = myMap(pt) != null - - def contains(param: PolyParam): Boolean = { - val entries = myMap(param.binder) - entries != null && entries(param.paramNum).isInstanceOf[TypeBounds] - } - - def contains(tvar: TypeVar): Boolean = { - val origin = tvar.origin - val entries = myMap(origin.binder) - val pnum = origin.paramNum - entries != null && isBounds(entries(pnum)) && (typeVar(entries, pnum) eq tvar) - } - - /** The number of type parameters in the given entry array */ - private def paramCount(entries: Array[Type]) = entries.length >> 1 - - /** The type variable corresponding to parameter numbered `n`, null if none was created */ - private def typeVar(entries: Array[Type], n: Int): Type = - entries(paramCount(entries) + n) - - private def isBounds(tp: Type) = tp.isInstanceOf[TypeBounds] - - def at(param: PolyParam)(implicit ctx: Context): Type = { - val entries = myMap(param.binder) - if (entries == null) NoType else entries(param.paramNum) - } - - def entry(param: PolyParam) = { - val entries = myMap(param.binder) - if (entries == null) NoType else entries(param.paramNum) - } - - def bounds(param: PolyParam)(implicit ctx: Context): TypeBounds = at(param).asInstanceOf[TypeBounds] - - def nonParamBounds(param: PolyParam)(implicit ctx: Context): TypeBounds = { - val bs @ TypeBounds(lo, hi) = bounds(param) - val lo1 = splitParams(lo, seenFromBelow = false, ignoreParam) - val hi1 = splitParams(hi, seenFromBelow = true, ignoreParam) - bs.derivedTypeBounds(lo1.orElse(defn.NothingType), hi1.orElse(defn.AnyType)) - } - - def related(param1: PolyParam, param2: PolyParam, inOrder: Boolean)(implicit ctx: Context): Boolean = { - var isRelated = false - def registerParam(p: PolyParam) = if (p == param2) isRelated = true - val TypeBounds(lo, hi) = bounds(param1) - if (inOrder) splitParams(hi, seenFromBelow = true, registerParam) - else splitParams(lo, seenFromBelow = false, registerParam) - isRelated - } - - def typeVarOfParam(param: PolyParam): Type = { - val entries = myMap(param.binder) - if (entries == null) NoType - else { - val tvar = typeVar(entries, param.paramNum) - if (tvar != null) tvar else NoType - } - } - - /** A new constraint which is derived from this constraint by adding or replacing - * the entries corresponding to `pt` with `entries`. - */ - private def updateEntries(pt: PolyType, entries: Array[Type])(implicit ctx: Context) : NaiveConstraint = { - val res = new NaiveConstraint(myMap.updated(pt, entries)) - - //assert(res.domainPolys.filter(pt => - // pt.resultType.resultType.widen.classSymbol.name.toString == "Ensuring").length < 2) //DEBUG - if (Config.checkConstraintsNonCyclic) checkNonCyclic(pt, entries) - ctx.runInfo.recordConstraintSize(res, res.myMap.size) - res - } - - def checkNonCyclic(pt: PolyType, entries: Array[Type])(implicit ctx: Context): Unit = - for ((entry, i) <- entries.zipWithIndex) { - val param = PolyParam(pt, i) - entry match { - case TypeBounds(lo, hi) => - assert(!param.occursIn(lo, fromBelow = true), s"$param occurs below $lo") - assert(!param.occursIn(hi, fromBelow = false), s"$param occurs above $hi") - case _ => - } - } - - def checkNonCyclic()(implicit ctx: Context): Unit = { - for (pt <- domainPolys) checkNonCyclic(pt, myMap(pt)) - } - - /** Check that no constrained parameter contains itself as a bound, - * either directly or indirectly. This should be not a structer criterion - * than checkNonCyclic because transitivity should be eliminated always, - * but it's good to be paranoid. - */ - def checkNonCyclicTrans()(implicit ctx: Context): Unit = { - for (pt <- domainPolys) - checkNonCyclicTrans(pt, myMap(pt)) - } - - private def checkNonCyclicTrans(pt: PolyType, entries: Array[Type])(implicit ctx: Context): Unit = - for ((entry, i) <- entries.zipWithIndex) { - def occursIn(params: Set[PolyParam], bound: Type, fromBelow: Boolean): Boolean = bound.stripTypeVar match { - case bound: PolyParam => - params.contains(bound) || { - at(bound) match { - case TypeBounds(lo, hi) => - occursIn(params + bound, if (fromBelow) lo else hi, fromBelow) - case _ => - false - } - } - case bound: AndOrType => - def occ1 = occursIn(params, bound.tp1, fromBelow) - def occ2 = occursIn(params, bound.tp2, fromBelow) - if (fromBelow == bound.isAnd) occ1 && occ2 else occ1 || occ2 - case _ => false - } - val param = PolyParam(pt, i) - entry match { - case TypeBounds(lo, hi) => - assert(!occursIn(Set(param), lo, fromBelow = true), s"$param occurs below $lo") - assert(!occursIn(Set(param), hi, fromBelow = false), s"$param occurs above $hi") - case _ => - } - } - - def updated(param: PolyParam, tpe: Type)(implicit ctx: Context): This = { - val newEntries = myMap(param.binder).clone - newEntries(param.paramNum) = tpe - updateEntries(param.binder, newEntries) - } - - def order(param: PolyParam, bound: PolyParam, inOrder: Boolean)(implicit ctx: Context): This = - if (related(param, bound, inOrder)) this - else { - val oldBounds = bounds(param) - val newBounds = - if (inOrder) TypeBounds(oldBounds.lo, AndType(oldBounds.hi, bound)) - else TypeBounds(OrType(oldBounds.lo, bound), oldBounds.hi) - updated(param, newBounds) - } - - /** A new constraint with all entries coming from `pt` removed. */ - def remove(pt: PolyType)(implicit ctx: Context): This = - new NaiveConstraint(myMap remove pt) - - def isRemovable(pt: PolyType, removedParam: Int = -1): Boolean = { - val entries = myMap(pt) - var noneLeft = true - var i = paramCount(entries) - while (noneLeft && i > 0) { - i -= 1 - if (i != removedParam && isBounds(entries(i))) noneLeft = false - else typeVar(entries, i) match { - case tv: TypeVar => - if (!tv.inst.exists) noneLeft = false // need to keep line around to compute instType - case _ => - } - } - noneLeft - } - - /** Drop parameter `PolyParam(poly, n)` from `bounds`, - * replacing with Nothing in the lower bound and by `Any` in the upper bound. - */ - private def dropParamIn(bounds: TypeBounds, poly: PolyType, n: Int)(implicit ctx: Context): TypeBounds = { - def drop(tp: Type): Type = tp match { - case tp: AndOrType => - val tp1 = drop(tp.tp1) - val tp2 = drop(tp.tp2) - if (!tp1.exists) tp2 - else if (!tp2.exists) tp1 - else tp - case PolyParam(`poly`, `n`) => NoType - case _ => tp - } - def approx(tp: Type, limit: Type): Type = { - val tp1 = drop(tp) - if (tp1.exists || !tp.exists) tp1 else limit - } - bounds.derivedTypeBounds( - approx(bounds.lo, defn.NothingType), approx(bounds.hi, defn.AnyType)) - } - - /** A new constraint which is derived from this constraint by removing - * the type parameter `param` from the domain and replacing all occurrences - * of the parameter elsewhere in the constraint by type `tp`. - */ - private def uncheckedReplace(param: PolyParam, tp: Type)(implicit ctx: Context): NaiveConstraint = { - - def subst(poly: PolyType, entries: Array[Type]) = { - var result = entries - var i = 0 - while (i < paramCount(entries)) { - entries(i) match { - case oldBounds: TypeBounds => - val newBounds = oldBounds.substParam(param, tp).asInstanceOf[TypeBounds] - if (oldBounds ne newBounds) { - if (result eq entries) result = entries.clone - result(i) = dropParamIn(newBounds, poly, i) - } - case _ => - } - i += 1 - } - result - } - - val pt = param.binder - val constr1 = if (isRemovable(pt, param.paramNum)) remove(pt) else updated(param, tp) - val result = new NaiveConstraint(constr1.myMap mapValues subst) - if (Config.checkConstraintsNonCyclic) result.checkNonCyclic() - result - } - - def replace(param: PolyParam, tp: Type)(implicit ctx: Context): This = { - val tp1 = tp.dealias.stripTypeVar - if (param == tp1) this else uncheckedReplace(param, tp1) - } - - def unify(p1: PolyParam, p2: PolyParam)(implicit ctx: Context): This = { - val p1Bounds = - dropParamIn(bounds(p1), p2.binder, p2.paramNum) & - dropParamIn(bounds(p2), p1.binder, p1.paramNum) - this.updated(p1, p1Bounds).updated(p2, p1) - } - - def add(poly: PolyType, tvars: List[TypeVar])(implicit ctx: Context): This = { - val nparams = poly.paramNames.length - val entries = new Array[Type](nparams * 2) - poly.paramBounds.copyToArray(entries, 0) - tvars.copyToArray(entries, nparams) - updateEntries(poly, entries) - } - - def domainPolys: List[PolyType] = myMap.keys - - def domainParams: List[PolyParam] = - for { - (poly, entries) <- myMap.toList - n <- 0 until paramCount(entries) - if isBounds(entries(n)) - } yield PolyParam(poly, n) - - def forallParams(p: PolyParam => Boolean): Boolean = { - myMap.foreachBinding { (poly, entries) => - for (i <- 0 until paramCount(entries)) - if (isBounds(entries(i)) && !p(PolyParam(poly, i))) return false - } - true - } - - def foreachTypeVar(op: TypeVar => Unit): Unit = - myMap.foreachBinding { (poly, entries) => - for (i <- 0 until paramCount(entries)) { - typeVar(entries, i) match { - case tv: TypeVar if !tv.inst.exists => op(tv) - case _ => - } - } - } - - private var myUninstVars: mutable.ArrayBuffer[TypeVar] = null - - /** The uninstantiated typevars of this constraint */ - def uninstVars: collection.Seq[TypeVar] = { - if (myUninstVars == null) { - myUninstVars = new mutable.ArrayBuffer[TypeVar] - myMap.foreachBinding { (poly, entries) => - for (i <- 0 until paramCount(entries)) { - typeVar(entries, i) match { - case tv: TypeVar if isBounds(entries(i)) => myUninstVars += tv - case _ => - } - } - } - } - myUninstVars - } - - def constrainedTypesText(printer: Printer): Text = - Text(domainPolys map (_.toText(printer)), ", ") - - def constraintText(indent: Int, printer: Printer): Text = { - val assocs = - for (param <- domainParams) - yield (" " * indent) ~ param.toText(printer) ~ entry(param).toText(printer) - Text(assocs, "\n") - } - - override def toText(printer: Printer): Text = { - val header: Text = "Constraint(" - val uninstVarsText = " uninstVars = " ~ - Text(uninstVars map (_.toText(printer)), ", ") ~ ";" - val constrainedText = - " constrained types = " ~ constrainedTypesText(printer) ~ ";" - val constraintsText = - " constraint = " ~ constraintText(3, printer) ~ ")" - Text.lines(List(header, uninstVarsText, constrainedText, constraintsText)) - } -} diff --git a/src/dotty/tools/dotc/core/TrackingConstraint.scala b/src/dotty/tools/dotc/core/TrackingConstraint.scala index 6e9ef5a2b..18e37a73e 100644 --- a/src/dotty/tools/dotc/core/TrackingConstraint.scala +++ b/src/dotty/tools/dotc/core/TrackingConstraint.scala @@ -93,7 +93,7 @@ class TrackingConstraint(private val myMap: ParamInfo, private def typeVar(entries: Array[Type], n: Int): Type = entries(paramCount(entries) + n) - private def entry(param: PolyParam): Type = { + def entry(param: PolyParam): Type = { val entries = myMap(param.binder) if (entries == null) NoType else entries(param.paramNum) @@ -119,55 +119,79 @@ class TrackingConstraint(private val myMap: ParamInfo, // ---------- Dependency handling ---------------------------------------------- - private def upperBits(i: Int): BitSet = less(i) + private def upperBits(less: Array[BitSet], i: Int): BitSet = less(i) - private def lowerBits(i: Int): BitSet = - (BitSet() /: less.indices) ((bits, j) => if (less(i)(j)) bits + j else bits) + private def lowerBits(less: Array[BitSet], i: Int): BitSet = + (BitSet() /: less.indices) ((bits, j) => if (less(j)(i)) bits + j else bits) - private def minUpperBits(i: Int): BitSet = { - val all = upperBits(i) + private def minUpperBits(less: Array[BitSet], i: Int): BitSet = { + val all = upperBits(less, i) all.filterNot(j => all.exists(k => less(k)(j))) } - private def minLowerBits(i: Int): BitSet = { - val all = lowerBits(i) + private def minLowerBits(less: Array[BitSet], i: Int): BitSet = { + val all = lowerBits(less, i) all.filterNot(j => all.exists(k => less(j)(k))) } - private def overParams(op: Int => BitSet): PolyParam => List[PolyParam] = param => - op(paramIndex(param)).toList.map(params).filter(contains) + private def overParams(op: (Array[BitSet], Int) => BitSet): PolyParam => List[PolyParam] = param => + op(less, paramIndex(param)).toList.map(params).filter(contains) - val upper = overParams(upperBits) - val lower = overParams(lowerBits) + val allUpper = overParams(upperBits) + val allLower = overParams(lowerBits) val minUpper = overParams(minUpperBits) val minLower = overParams(minLowerBits) + def upper(param: PolyParam): List[PolyParam] = allUpper(param) + def lower(param: PolyParam): List[PolyParam] = allLower(param) + + def exclusiveLower(param: PolyParam, butNot: PolyParam): List[PolyParam] = { + val excluded = lowerBits(less, paramIndex(butNot)) + overParams(lowerBits(_, _) &~ excluded)(param) + } + + def exclusiveUpper(param: PolyParam, butNot: PolyParam): List[PolyParam] = { + val excluded = upperBits(less, paramIndex(butNot)) + overParams(upperBits(_, _) &~ excluded)(param) + } // ---------- Info related to PolyParams ------------------------------------------- - def related(param1: PolyParam, param2: PolyParam, firstIsLower: Boolean)(implicit ctx: Context): Boolean = { - val i1 = paramIndex(param1) - val i2 = paramIndex(param2) - if (firstIsLower) less(i1)(i2) else less(i2)(i1) - } + def isLess(param1: PolyParam, param2: PolyParam)(implicit ctx: Context): Boolean = + less(paramIndex(param1))(paramIndex(param2)) - def nonParamBounds(param: PolyParam)(implicit ctx: Context): TypeBounds = + def nonParamBounds(param: PolyParam): TypeBounds = entry(param).asInstanceOf[TypeBounds] - def bounds(param: PolyParam)(implicit ctx: Context): TypeBounds = { - val bounds @ TypeBounds(lo, hi) = nonParamBounds(param) - bounds.derivedTypeBounds( - (lo /: minLower(param))(OrType.apply), - (hi /: minUpper(param))(AndType.apply)) - } - - def at(param: PolyParam)(implicit ctx: Context): Type = { - entry(param) match { - case _: TypeBounds => bounds(param) - case e => e + def checkBound(param: PolyParam, bound: Type)(implicit ctx: Context): Type = { + assert(param != bound) + bound match { + case TypeBounds(lo, hi) => + checkBound(param, lo) + checkBound(param, hi) + case bound: TypeVar => + checkBound(param, bound.underlying) + case bound: RefinedType => + checkBound(param, bound.underlying) + case bound: AndOrType => + checkBound(param, bound.tp1) + checkBound(param, bound.tp2) + case _ => } + bound } - + + def fullLowerBound(param: PolyParam)(implicit ctx: Context): Type = { + val lo = checkBound(param, nonParamBounds(param).lo) + checkBound(param, (lo /: minLower(param))(_ | _)) + } + + def fullUpperBound(param: PolyParam)(implicit ctx: Context): Type = + (nonParamBounds(param).hi /: minUpper(param))(_ & _) + + def fullBounds(param: PolyParam)(implicit ctx: Context): TypeBounds = + nonParamBounds(param).derivedTypeBounds(fullLowerBound(param), fullUpperBound(param)) + def typeVarOfParam(param: PolyParam): Type = { val entries = myMap(param.binder) if (entries == null) NoType @@ -177,30 +201,19 @@ class TrackingConstraint(private val myMap: ParamInfo, } } -// ---------- Type splitting -------------------------------------------------- - - /** The set of "dependent" constrained parameters that unconditionally strengthen bound `tp`. - * @param seenFromBelow If true, `bound` is an upper bound, else a lower bound. - */ - private def depParams(tp: Type, seenFromBelow: Boolean): Set[PolyParam] = tp match { - case tp: PolyParam if contains(tp) => - Set(tp) - case tp: AndOrType if seenFromBelow == tp.isAnd => - depParams(tp.tp1, seenFromBelow) | depParams(tp.tp2, seenFromBelow) - case _ => - Set.empty - } +// ---------- Adding PolyTypes -------------------------------------------------- - /** The bound type `tp` without dependent parameters. + /** The bound type `tp` without dependent parameters * NoType if type consists only of dependent parameters. * @param seenFromBelow If true, `bound` is an upper bound, else a lower bound. */ - private def stripParams(tp: Type, seenFromBelow: Boolean)(implicit ctx: Context): Type = tp match { - case tp: PolyParam if contains(tp) => - NoType + private def stripParams(tp: Type, handleParam: (PolyParam, Boolean) => Type, + seenFromBelow: Boolean)(implicit ctx: Context): Type = tp match { + case tp: PolyParam => + handleParam(tp, seenFromBelow) case tp: AndOrType if seenFromBelow == tp.isAnd => - val tp1 = nonParamType(tp.tp1, seenFromBelow) - val tp2 = nonParamType(tp.tp2, seenFromBelow) + val tp1 = stripParams(tp.tp1, handleParam, seenFromBelow) + val tp2 = stripParams(tp.tp2, handleParam, seenFromBelow) if (tp1.exists) if (tp2.exists) tp.derivedAndOrType(tp1, tp2) else tp1 @@ -213,95 +226,94 @@ class TrackingConstraint(private val myMap: ParamInfo, * A top or bottom type if type consists only of dependent parameters. * @param seenFromBelow If true, `bound` is an upper bound, else a lower bound. */ - private def nonParamType(tp: Type, seenFromBelow: Boolean)(implicit ctx: Context): Type = - stripParams(tp, seenFromBelow).orElse(if (seenFromBelow) defn.AnyType else defn.NothingType) + private def nonParamType(tp: Type, handleParam: (PolyParam, Boolean) => Type, + seenFromBelow: Boolean)(implicit ctx: Context): Type = + stripParams(tp, handleParam, seenFromBelow) + .orElse(if (seenFromBelow) defn.AnyType else defn.NothingType) - /** The `tp1 is a TypeBounds type, the bounds without dependent parameters, - * otherwise `tp`. + /** The bounds of `tp1` without dependent parameters. + * @pre `tp` is a TypeBounds type. */ - private def nonParamType(tp: Type)(implicit ctx: Context): Type = tp match { + private def nonParamBounds(tp: Type, handleParam: (PolyParam, Boolean) => Type)(implicit ctx: Context): Type = tp match { case tp @ TypeBounds(lo, hi) => tp.derivedTypeBounds( - nonParamType(lo, seenFromBelow = false), - nonParamType(hi, seenFromBelow = true)) - case _ => - tp + nonParamType(lo, handleParam, seenFromBelow = false), + nonParamType(hi, handleParam, seenFromBelow = true)) } - /** An updated partial order matrix that incorporates `less` and also reflects the new `bounds` - * for parameter `param`. - */ - private def updatedLess(less: Array[BitSet], param: PolyParam, bounds: Type): Array[BitSet] = bounds match { - case TypeBounds(lo, hi) => - updatedLess( - updatedLess(less, param, lo, seenFromBelow = false), - param, hi, seenFromBelow = true) - case _ => - less + def add(poly: PolyType, tvars: List[TypeVar])(implicit ctx: Context): This = { + assert(!contains(poly)) + val nparams = poly.paramNames.length + val entries1 = new Array[Type](nparams * 2) + poly.paramBounds.copyToArray(entries1, 0) + tvars.copyToArray(entries1, nparams) + val is = poly.paramBounds.indices + val newParams = is.map(PolyParam(poly, _)) + val params1 = params ++ newParams + var less1 = less ++ is.map(Function.const(BitSet.empty)) + for (i <- is) { + def handleParam(param: PolyParam, seenFromBelow: Boolean): Type = { + def record(paramIdx: Int): Type = { + less1 = + if (seenFromBelow) updatedLess(less1, nparams + i, paramIdx) + else updatedLess(less1, paramIdx, nparams + i) + NoType + } + if (param.binder eq poly) record(nparams + param.paramNum) + else if (contains(param.binder)) record(paramIndex(param)) + else param + } + entries1(i) = checkBound(newParams(i), nonParamBounds(entries1(i), handleParam)) + } + newConstraint(myMap.updated(poly, entries1), less1, params1) } - /** An updated partial order matrix that incorporates `less` and also reflects that `param` has a new - * `bound`, where `seenFromBelow` is true iff `bound` is an upper bound for `param`. - */ - def updatedLess(less: Array[BitSet], param: PolyParam, bound: Type, seenFromBelow: Boolean): Array[BitSet] = - updatedLess(less, param, depParams(bound, seenFromBelow).iterator, inOrder = seenFromBelow) - - /** An updated partial order matrix that incorporates `less` and also reflects that `param` relates - * to all parameters in `ps2` wrt <:< if `inOrder` is true, `>:>` otherwise. - */ - def updatedLess(less: Array[BitSet], p1: PolyParam, ps2: Iterator[PolyParam], inOrder: Boolean): Array[BitSet] = - if (ps2.hasNext) updatedLess(updatedLess(less, p1, ps2.next, inOrder), p1, ps2, inOrder) - else less +// ---------- Updates ------------------------------------------------------------ /** An updated partial order matrix that incorporates `less` and also reflects that `param` relates * to `p2` wrt <:< if `inOrder` is true, `>:>` otherwise. */ - def updatedLess(less: Array[BitSet], p1: PolyParam, p2: PolyParam, inOrder: Boolean): Array[BitSet] = - if (!inOrder) updatedLess(less, p2, p1, true) - else { - val i1 = paramIndex(p1) - val i2 = paramIndex(p2) + private def updatedLess(less: Array[BitSet], i1: Int, i2: Int): Array[BitSet] = { if (i1 == i2 || less(i1)(i2)) less else { val result = less.clone - result(i1) = result(i1) + i2 | upperBits(i2) - assert(!result(i1)(i1)) - for (j <- lowerBits(i1)) { - result(j) = result(j) + i2 | upperBits(i2) + val newUpper = upperBits(less, i2) + i2 + def update(j: Int) = { + result(j) |= newUpper assert(!result(j)(j)) } + update(i1) + lowerBits(less, i1).foreach(update) result } - } + } -// ---------- Updates ------------------------------------------------------------ - - def order(param: PolyParam, bound: PolyParam, inOrder: Boolean)(implicit ctx: Context): This = { - val less1 = updatedLess(less, param, bound, inOrder) + def addLess(p1: PolyParam, p2: PolyParam)(implicit ctx: Context): This = { + val less1 = updatedLess(less, paramIndex(p1), paramIndex(p2)) if (less1 eq less) this else newConstraint(myMap, less1, params) } - def nonParamUpdated(param: PolyParam, tpe: Type)(implicit ctx: Context): This = { - val entries1 = myMap(param.binder).clone - entries1(param.paramNum) = tpe - newConstraint(myMap.updated(param.binder, entries1), less, params) + def updateEntry(param: PolyParam, tp: Type)(implicit ctx: Context): This = { + val entries = myMap(param.binder) + val entry = entries(param.paramNum) + if (entry eq tp) this + else { + if (!tp.isInstanceOf[TypeBounds]) typr.println(i"inst entry $param to $tp") + val entries1 = entries.clone + entries1(param.paramNum) = checkBound(param, tp) + newConstraint(myMap.updated(param.binder, entries1), less, params) + } } - def updated(param: PolyParam, tpe: Type)(implicit ctx: Context): This = { - val less1 = updatedLess(less, param, tpe) - val entries = myMap(param.binder) - val entry1 = nonParamType(tpe) - val idx = param.paramNum - val entries1 = - if (entry1 eq entries(idx)) entries - else { - val entries1 = entries.clone - entries1(idx) = entry1 - entries1 - } - newConstraint(myMap.updated(param.binder, entries1), less1, params) + def unify(p1: PolyParam, p2: PolyParam)(implicit ctx: Context): This = { + val p1Bounds = + dropParamIn(nonParamBounds(p1), p2.binder, p2.paramNum) & + dropParamIn(nonParamBounds(p2), p1.binder, p1.paramNum) + this.updateEntry(p1, p1Bounds).updateEntry(p2, p1) } - + +// ---------- Removals ------------------------------------------------------------ + /** Drop parameter `PolyParam(poly, n)` from `bounds`, * replacing with Nothing in the lower bound and by `Any` in the upper bound. */ @@ -324,10 +336,6 @@ class TrackingConstraint(private val myMap: ParamInfo, approx(bounds.lo, defn.NothingType), approx(bounds.hi, defn.AnyType)) } - /** A new constraint which is derived from this constraint by removing - * the type parameter `param` from the domain and replacing all occurrences - * of the parameter elsewhere in the constraint by type `tp`. - */ def replace(param: PolyParam, tp: Type)(implicit ctx: Context): TrackingConstraint = { val replacement = tp.dealias.stripTypeVar @@ -340,7 +348,7 @@ class TrackingConstraint(private val myMap: ParamInfo, val newBounds = oldBounds.substParam(param, replacement).asInstanceOf[TypeBounds] if (oldBounds ne newBounds) { if (result eq entries) result = entries.clone - result(i) = dropParamIn(newBounds, poly, i) + result(i) = checkBound(PolyParam(poly, i), dropParamIn(newBounds, poly, i)) } case _ => } @@ -351,39 +359,13 @@ class TrackingConstraint(private val myMap: ParamInfo, if (param == replacement) this else { + assert(replacement.isValueType) val pt = param.binder - val constr1 = if (isRemovable(pt, param.paramNum)) remove(pt) else updated(param, replacement) - val result = new TrackingConstraint(constr1.myMap mapValues subst, constr1.less, constr1.params) - if (Config.checkConstraintsNonCyclic) result.checkNonCyclic() - result + val constr1 = if (isRemovable(pt, param.paramNum)) remove(pt) else updateEntry(param, replacement) + newConstraint(constr1.myMap mapValues subst, constr1.less, constr1.params) } } - def unify(p1: PolyParam, p2: PolyParam)(implicit ctx: Context): This = { - val p1Bounds = - dropParamIn(nonParamBounds(p1), p2.binder, p2.paramNum) & - dropParamIn(nonParamBounds(p2), p1.binder, p1.paramNum) - this.nonParamUpdated(p1, p1Bounds).nonParamUpdated(p2, p1) - } - - def add(poly: PolyType, tvars: List[TypeVar])(implicit ctx: Context): This = { - assert(!contains(poly)) - val nparams = poly.paramNames.length - val entries1 = new Array[Type](nparams * 2) - poly.paramBounds.copyToArray(entries1, 0) - tvars.copyToArray(entries1, nparams) - val is = poly.paramBounds.indices - val newParams = is.map(PolyParam(poly, _)) - val params1 = params ++ newParams - var less1 = less ++ is.map(Function.const(BitSet.empty)) - for (i <- is) { - less1 = updatedLess(less1, newParams(i), entries1(i)) - entries1(i) = nonParamType(entries1(i)) - } - newConstraint(myMap.updated(poly, entries1), less1, params1) - } - - /** A new constraint with all entries coming from `pt` removed. */ def remove(pt: PolyType)(implicit ctx: Context): This = { val start = polyStart(pt) val skipped = pt.paramNames.length @@ -425,7 +407,7 @@ class TrackingConstraint(private val myMap: ParamInfo, def domainPolys: List[PolyType] = polyTypes.toList - def domainParams: List[PolyParam] = params.toList + def domainParams: List[PolyParam] = params.toList.filter(contains) def forallParams(p: PolyParam => Boolean): Boolean = { myMap.foreachBinding { (poly, entries) => @@ -454,7 +436,7 @@ class TrackingConstraint(private val myMap: ParamInfo, myMap.foreachBinding { (poly, entries) => for (i <- 0 until paramCount(entries)) { typeVar(entries, i) match { - case tv: TypeVar if isBounds(entries(i)) => myUninstVars += tv + case tv: TypeVar if !tv.inst.exists && isBounds(entries(i)) => myUninstVars += tv case _ => } } @@ -468,13 +450,8 @@ class TrackingConstraint(private val myMap: ParamInfo, private def checkNonCyclic(idx: Int)(implicit ctx: Context): Unit = assert(!less(idx)(idx), i"cyclic constraint involving ${params(idx)}") - def checkNonCyclic(pt: PolyType, entries: Array[Type])(implicit ctx: Context): Unit = - for (i <- entries.indices) checkNonCyclic(paramIndex(PolyParam(pt, i))) - def checkNonCyclic()(implicit ctx: Context): Unit = for (i <- params.indices) checkNonCyclic(i) - - def checkNonCyclicTrans()(implicit ctx: Context): Unit = checkNonCyclic() // ---------- toText ----------------------------------------------------- diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala index 0d2dc20d3..046424eaf 100644 --- a/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/src/dotty/tools/dotc/core/TypeComparer.scala @@ -85,7 +85,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi assert(isSatisfiable, constraint.show) } - def isSubType(tp1: Type, tp2: Type): Boolean = ctx.traceIndented(s"isSubType ${traceInfo(tp1, tp2)} ${if (Config.verboseExplainSubtype) s" ${tp1.getClass}, ${tp2.getClass}" else ""}", subtyping) /*<|<*/ { + def isSubType(tp1: Type, tp2: Type): Boolean = ctx.traceIndented(s"isSubType ${traceInfo(tp1, tp2)}", subtyping) /*<|<*/ { if (tp2 eq NoType) false else if (tp1 eq tp2) true else { @@ -1118,26 +1118,6 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi false } - /** Constraint `c1` subsumes constraint `c2`, if under `c2` as constraint we have - * for all poly params `p` defined in `c2` as `p >: L2 <: U2`: - * - * c1 defines p with bounds p >: L1 <: U1, and - * L2 <: L1, and - * U1 <: U2 - * - * Both `c1` and `c2` are required to derive from constraint `pre`, possibly - * narrowing it with further bounds. - */ - def subsumes(c1: Constraint, c2: Constraint, pre: Constraint): Boolean = - if (c2 eq pre) true - else if (c1 eq pre) false - else { - val saved = constraint - try - c2.forallParams(p => c1.contains(p) && isSubType(c1.bounds(p), c2.bounds(p))) - finally constraint = saved - } - /** A new type comparer of the same type as this one, using the given context. */ def copyIn(ctx: Context) = new TypeComparer(ctx) @@ -1147,8 +1127,14 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi def traceIndented[T](str: String)(op: => T): T = op private def traceInfo(tp1: Type, tp2: Type) = - s"${tp1.show} <:< ${tp2.show}" + - (if (ctx.settings.verbose.value) s" ${tp1.getClass} ${tp2.getClass}${if (frozenConstraint) " frozen" else ""}" else "") + s"${tp1.show} <:< ${tp2.show}" + { + if (ctx.settings.verbose.value || Config.verboseExplainSubtype) { + s" ${tp1.getClass}, ${tp2.getClass}" + + (if (frozenConstraint) " frozen" else "") + + (if (ctx.mode is Mode.TypevarsMissContext) " tvars-miss-ctx" else "") + } + else "" + } /** Show subtype goal that led to an assertion failure */ def showGoal(tp1: Type, tp2: Type) = { diff --git a/src/dotty/tools/dotc/core/TyperState.scala b/src/dotty/tools/dotc/core/TyperState.scala index cb8538e26..bdba128a9 100644 --- a/src/dotty/tools/dotc/core/TyperState.scala +++ b/src/dotty/tools/dotc/core/TyperState.scala @@ -17,7 +17,7 @@ class TyperState(r: Reporter) extends DotClass with Showable { def reporter = r /** The current constraint set */ - def constraint: Constraint = new NaiveConstraint(SimpleMap.Empty)//new TrackingConstraint(SimpleMap.Empty, Array(), Array()) + def constraint: Constraint = new TrackingConstraint(SimpleMap.Empty, Array(), Array()) def constraint_=(c: Constraint): Unit = {} /** The uninstantiated variables */ @@ -38,7 +38,7 @@ class TyperState(r: Reporter) extends DotClass with Showable { * is done only in a temporary way for contexts that may be retracted * without also retracting the type var as a whole. */ - def instType(tvar: TypeVar)(implicit ctx: Context): Type = constraint.at(tvar.origin) match { + def instType(tvar: TypeVar)(implicit ctx: Context): Type = constraint.entry(tvar.origin) match { case _: TypeBounds => NoType case tp: PolyParam => var tvar1 = constraint.typeVarOfParam(tp) diff --git a/src/dotty/tools/dotc/core/Types.scala b/src/dotty/tools/dotc/core/Types.scala index 8249e5a4c..30e394941 100644 --- a/src/dotty/tools/dotc/core/Types.scala +++ b/src/dotty/tools/dotc/core/Types.scala @@ -2251,7 +2251,7 @@ object Types { * is also a singleton type. */ def instantiate(fromBelow: Boolean)(implicit ctx: Context): Type = { - def upperBound = ctx.typerState.constraint.bounds(origin).hi + def upperBound = ctx.typerState.constraint.fullUpperBound(origin) def isSingleton(tp: Type): Boolean = tp match { case tp: SingletonType => true case AndType(tp1, tp2) => isSingleton(tp1) | isSingleton(tp2) diff --git a/src/dotty/tools/dotc/printing/PlainPrinter.scala b/src/dotty/tools/dotc/printing/PlainPrinter.scala index e86539d6c..1a6cc77b2 100644 --- a/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -145,10 +145,10 @@ class PlainPrinter(_ctx: Context) extends Printer { if (tp.isInstantiated) toTextLocal(tp.instanceOpt) ~ "'" // debug for now, so that we can see where the TypeVars are. else { - val bounds = ctx.typerState.constraint.at(tp.origin) match { - case bounds: TypeBounds => bounds - case _ => TypeBounds.empty - } + val constr = ctx.typerState.constraint + val bounds = + if (constr.contains(tp)) constr.fullBounds(tp.origin) + else TypeBounds.empty "(" ~ toText(tp.origin) ~ "?" ~ toText(bounds) ~ ")" } case _ => diff --git a/src/dotty/tools/dotc/typer/Inferencing.scala b/src/dotty/tools/dotc/typer/Inferencing.scala index 05be46f29..e41b2d194 100644 --- a/src/dotty/tools/dotc/typer/Inferencing.scala +++ b/src/dotty/tools/dotc/typer/Inferencing.scala @@ -203,7 +203,7 @@ trait Inferencing { this: Checking => if (v == 1) tvar.instantiate(fromBelow = false) else if (v == -1) tvar.instantiate(fromBelow = true) else { - val bounds = ctx.typerState.constraint.bounds(tvar.origin) + val bounds = ctx.typerState.constraint.fullBounds(tvar.origin) if (!(bounds.hi <:< bounds.lo)) result = Some(tvar) tvar.instantiate(fromBelow = false) } diff --git a/src/dotty/tools/dotc/typer/ProtoTypes.scala b/src/dotty/tools/dotc/typer/ProtoTypes.scala index e16b83afd..521f0deaa 100644 --- a/src/dotty/tools/dotc/typer/ProtoTypes.scala +++ b/src/dotty/tools/dotc/typer/ProtoTypes.scala @@ -325,6 +325,7 @@ object ProtoTypes { else pt val tvars = if (owningTree.isEmpty) Nil else newTypeVars(added) state.constraint = state.constraint.add(added, tvars) + ctx.typeComparer.initialize(added) (added, tvars) } @@ -376,7 +377,7 @@ object ProtoTypes { case tp: TypeAlias => // default case, inlined for speed tp.derivedTypeAlias(wildApprox(tp.alias, theMap)) case tp @ PolyParam(poly, pnum) => // !!! todo adapt to TrackingConstraint - ctx.typerState.constraint.at(tp) match { + ctx.typerState.constraint.entry(tp) match { case bounds: TypeBounds => wildApprox(WildcardType(bounds)) case NoType => WildcardType(wildApprox(poly.paramBounds(pnum)).bounds) case inst => wildApprox(inst) |