diff options
author | Martin Odersky <odersky@gmail.com> | 2014-04-29 16:14:42 +0200 |
---|---|---|
committer | Dmitry Petrashko <dmitry.petrashko@gmail.com> | 2014-05-08 21:51:46 +0200 |
commit | ef8f24203f4a3ef75d0b8e45a9dd9470bd474e7d (patch) | |
tree | e568b66eb7d8c33bc0770c0fb3b043d007a93078 /src | |
parent | f84a49d4502c9a1ad328c1f5a3a558afade63848 (diff) | |
download | dotty-ef8f24203f4a3ef75d0b8e45a9dd9470bd474e7d.tar.gz dotty-ef8f24203f4a3ef75d0b8e45a9dd9470bd474e7d.tar.bz2 dotty-ef8f24203f4a3ef75d0b8e45a9dd9470bd474e7d.zip |
Tightened satisfiablity checks.
Satisfiability was too loose before. It is noww tightened. We check that the lower bounds
of all constrained parameters represent a solution to the constraint. To make the check pass
we have to first propagate the constraint by re-verifying all bounds.
Diffstat (limited to 'src')
-rw-r--r-- | src/dotty/tools/dotc/core/Constraint.scala | 12 | ||||
-rw-r--r-- | src/dotty/tools/dotc/core/TypeComparer.scala | 48 |
2 files changed, 55 insertions, 5 deletions
diff --git a/src/dotty/tools/dotc/core/Constraint.scala b/src/dotty/tools/dotc/core/Constraint.scala index d3d19ec30..a16c85316 100644 --- a/src/dotty/tools/dotc/core/Constraint.scala +++ b/src/dotty/tools/dotc/core/Constraint.scala @@ -77,6 +77,8 @@ class Constraint(val myMap: SimpleMap[PolyType, Array[Type]]) extends Showable { */ private def updateEntries(pt: PolyType, entries: Array[Type])(implicit ctx: Context) : Constraint = { val res = new Constraint(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 @@ -246,6 +248,16 @@ class Constraint(val myMap: SimpleMap[PolyType, Array[Type]]) extends Showable { if isBounds(entries(n)) } yield PolyParam(poly, n) + /** Check whether predicate holds for all parameters in constraint + */ + 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 + } + /** Perform operation `op` on all typevars, or only on uninstantiated * typevars, depending on whether `uninstOnly` is set or not. */ diff --git a/src/dotty/tools/dotc/core/TypeComparer.scala b/src/dotty/tools/dotc/core/TypeComparer.scala index cab09826b..319b9957e 100644 --- a/src/dotty/tools/dotc/core/TypeComparer.scala +++ b/src/dotty/tools/dotc/core/TypeComparer.scala @@ -79,13 +79,50 @@ class TypeComparer(initctx: Context) extends DotClass { myAnyType } + /** Map that approximates each param in constraint by its lower bound */ + val approxParams = new TypeMap { + def apply(tp: Type): Type = tp.stripTypeVar match { + case tp: PolyParam if constraint contains tp => + this(constraint.bounds(tp).lo) + case tp => + mapOver(tp) + } + } + + /** Propagate new constraint by comparing all bounds */ + def propagate: Boolean = + constraint.forallParams { poly => + val TypeBounds(lo, hi) = constraint.bounds(poly) + isSubType(lo, hi) + } + + /** Check whether the lower bounds of all parameters in this + * constraint are a solution to the constraint. + */ + def isSatisfiable: Boolean = + constraint.forallParams { poly => + val TypeBounds(lo, hi) = constraint.bounds(poly) + isSubType(approxParams(lo), approxParams(hi)) || + { ctx.log(i"sub fail $lo <:< $hi") + ctx.log(i"approximated = ${approxParams(lo)} <:< ${approxParams(hi)}") + ctx.log(TypeComparer.explained(implicit ctx => isSubType(approxParams(lo), approxParams(hi)))) + false + } + } + /** Update constraint for `param` to `bounds`, check that * new constraint is still satisfiable. */ private def updateConstraint(param: PolyParam, bounds: TypeBounds): Boolean = { val saved = constraint constraint = constraint.updated(param, bounds) - isSubType(bounds.lo, bounds.hi) || + + propagate && + { isSatisfiable || { + ctx.log(i"SAT $constraint produced by $param $bounds is not satisfiable") + false + } + } || { constraint = saved; false } // don't leave the constraint in unsatisfiable state } @@ -101,7 +138,7 @@ class TypeComparer(initctx: Context) extends DotClass { finally ignoreConstraint = saved val res = (param == bound) || (oldBounds eq newBounds) || updateConstraint(param, newBounds) - constr.println(s"add constraint $param ${if (fromBelow) ">:" else "<:"} $bound = $res") + constr.println(s"added1 constraint $param ${if (fromBelow) ">:" else "<:"} $bound = $res") if (res) constr.println(constraint.show) res } @@ -127,7 +164,8 @@ class TypeComparer(initctx: Context) extends DotClass { def addConstraint(param: PolyParam, bound0: Type, fromBelow: Boolean): Boolean = { assert(!frozenConstraint) val bound = bound0.dealias.stripTypeVar - constr.println(s"adding ${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show} (${bound.getClass}) to ${constraint.show}") + def description = s"${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show} (${bound.getClass}) to ${constraint.show}" + constr.println(s"adding $description") val res = bound match { case bound: PolyParam if constraint contains bound => val TypeBounds(lo, hi) = constraint.bounds(bound) @@ -150,7 +188,7 @@ class TypeComparer(initctx: Context) extends DotClass { case bound => // !!! remove to keep the originals addConstraint1(param, bound, fromBelow) } - constr.println(s"added ${param.show} ${if (fromBelow) ">:>" else "<:<"} ${bound.show} = ${constraint.show}") + constr.println(s"added $description = ${constraint.show}") res } @@ -656,7 +694,7 @@ class TypeComparer(initctx: Context) extends DotClass { v == 0 || tparam.variance == v } hk.println(s"isSubTypeHK: args1 = $args1, hk-bounds = $hkBounds $boundsOK $variancesOK") - boundsOK && variancesOK + boundsOK && variancesOK || fourthTry(tp1, tp2) } def trySetType(tr: NamedType, bounds: TypeBounds): Boolean = |