package dotty.tools
package dotc
package core
import Types._, Contexts._, Symbols._
import Decorators._
import config.Config
import config.Printers._
/** Methods for adding constraints and solving them.
*
* Constraints are required to be in normalized form. This means
* (1) if P <: Q in C then also Q >: P in C
* (2) if P r Q in C and Q r R in C then also P r R in C, where r is <: or :>
*
* "P <: Q in C" means here: There is a constraint P <: H[Q],
* where H is the multi-hole context given by:
*
* H = []
* H & T
* T & H
* H | H
*
* (the idea is that a parameter Q in a H context is guaranteed to be a supertype of P).
*
* "P >: Q in C" means: There is a constraint P >: L[Q],
* where L is the multi-hole context given by:
*
* L = []
* L | T
* T | L
* L & L
*/
trait ConstraintHandling {
implicit val ctx: Context
def isSubType(tp1: Type, tp2: Type): Boolean
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
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 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 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
}
/** Make p2 = p1, transfer all bounds of p2 to p1
* @pre less(p1)(p2)
*/
private def unify(p1: PolyParam, p2: PolyParam): Boolean = {
constr.println(s"unifying $p1 $p2")
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))
}
protected final def isSubTypeWhenFrozen(tp1: Type, tp2: Type): Boolean = {
val saved = frozenConstraint
frozenConstraint = true
try isSubType(tp1, tp2)
finally frozenConstraint = saved
}
/** Test whether the lower bounds of all parameters in this
* constraint are a solution to the constraint.
*/
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
}
}
/** Solve constraint set for given type parameter `param`.
* If `fromBelow` is true the parameter is approximated by its lower bound,
* otherwise it is approximated by its upper bound. However, any occurrences
* of the parameter in a refinement somewhere in the bound are removed.
* (Such occurrences can arise for F-bounded types).
* The constraint is left unchanged.
* @return the instantiating type
* @pre `param` is in the constraint's domain.
*/
final def approximation(param: PolyParam, fromBelow: Boolean): Type = {
val avoidParam = new TypeMap {
override def stopAtStatic = true
def apply(tp: Type) = mapOver {
tp match {
case tp: RefinedType if param occursIn tp.refinedInfo => tp.parent
case _ => tp
}
}
}
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
}
/** 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.
*/
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
}
/** 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 =
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))
}
}
/** Can `param` be constrained with new bounds? */
final def canConstrain(param: PolyParam): Boolean =
!frozenConstraint && (constraint contains param)
/** Add constraint `param <: bond` if `fromBelow` is true, `param >: bound` otherwise.
* `bound` is assumed to be in normalized form, as specified in `firstTry` and
* `secondTry` of `TypeComparer`. In particular, it should not be an alias type,
* lazy ref, typevar, wildcard type, error type. In addition, upper bounds may
* not be AndTypes and lower bounds may not be OrTypes.
*/
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) // DEBUG in case following fails
checkPropagated(s"added $description") {
addConstraintInvocations += 1
try bound match {
case bound: PolyParam if constraint contains bound =>
if (fromBelow) addLess(bound, param) else addLess(param, bound)
case _ =>
if (fromBelow) addLowerBound(param, bound) else addUpperBound(param, bound)
}
finally addConstraintInvocations -= 1
}
}
/** Check that constraint is fully propagated. See comment in Config.checkConstraintsPropagated */
def checkPropagated(msg: => String)(result: Boolean): Boolean = {
if (Config.checkConstraintsPropagated && 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
}
}