Skip to content

Refactor inhabited in exhaustivness check #3888

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jan 29, 2018
Merged

Refactor inhabited in exhaustivness check #3888

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a913f77
refactor inhabited in exhaustivness check
liufengyun Jan 23, 2018
7799da6
address review: simplify CNF conversion
liufengyun Jan 26, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
182 changes: 90 additions & 92 deletions compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -278,21 +278,8 @@ trait SpaceLogic {
}
}

object SpaceEngine {
private sealed trait Implementability {
def show(implicit ctx: Context) = this match {
case SubclassOf(classSyms) => s"SubclassOf(${classSyms.map(_.show)})"
case other => other.toString
}
}
private case object ClassOrTrait extends Implementability
private case class SubclassOf(classSyms: List[Symbol]) extends Implementability
private case object Unimplementable extends Implementability
}

/** Scala implementation of space logic */
class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
import SpaceEngine._
import tpd._

private val scalaSomeClass = ctx.requiredClass("scala.Some")
Expand All @@ -301,77 +288,15 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
private val scalaNilType = ctx.requiredModuleRef("scala.collection.immutable.Nil")
private val scalaConsType = ctx.requiredClassRef("scala.collection.immutable.::")

/** Checks if it's possible to create a trait/class which is a subtype of `tp`.
*
* - doesn't handle member collisions (will not declare a type unimplementable because of one)
* - expects that neither Any nor Object reach it
* (this is currently true due to both isSubType and and/or type simplification)
*
* See [[intersectUnrelatedAtomicTypes]].
*/
private def implementability(tp: Type): Implementability = tp.dealias match {
case AndType(tp1, tp2) =>
(implementability(tp1), implementability(tp2)) match {
case (Unimplementable, _) | (_, Unimplementable) => Unimplementable
case (SubclassOf(classSyms1), SubclassOf(classSyms2)) =>
(for {
sym1 <- classSyms1
sym2 <- classSyms2
result <-
if (sym1 isSubClass sym2) List(sym1)
else if (sym2 isSubClass sym1) List(sym2)
else Nil
} yield result) match {
case Nil => Unimplementable
case lst => SubclassOf(lst)
}
case (ClassOrTrait, ClassOrTrait) => ClassOrTrait
case (SubclassOf(clss), _) => SubclassOf(clss)
case (_, SubclassOf(clss)) => SubclassOf(clss)
}
case OrType(tp1, tp2) =>
(implementability(tp1), implementability(tp2)) match {
case (ClassOrTrait, _) | (_, ClassOrTrait) => ClassOrTrait
case (SubclassOf(classSyms1), SubclassOf(classSyms2)) =>
SubclassOf(classSyms1 ::: classSyms2)
case (SubclassOf(classSyms), _) => SubclassOf(classSyms)
case (_, SubclassOf(classSyms)) => SubclassOf(classSyms)
case _ => Unimplementable
}
case _: SingletonType =>
// singleton types have no instantiable subtypes
Unimplementable
case tp: RefinedType =>
// refinement itself is not considered - it would at most make
// a type unimplementable because of a member collision
implementability(tp.parent)
case other =>
val classSym = other.classSymbol
if (classSym.exists) {
if (classSym is Final) Unimplementable
else if (classSym is Trait) ClassOrTrait
else SubclassOf(List(classSym))
} else {
// if no class symbol exists, conservatively say that anything
// can implement `tp`
ClassOrTrait
}
}

override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
val and = AndType(tp1, tp2)
// Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
// Then, no leaf of the and-type tree `and` is a subtype of `and`.
// Then, to create a value of type `and` you must instantiate a trait (class/module)
// which is a subtype of all the leaves of `and`.
val imp = implementability(and)
val res = inhabited(and)

debug.println(s"atomic intersection: ${and.show} ~ ${imp.show}")
debug.println(s"atomic intersection: ${and.show} = ${res}")

imp match {
case Unimplementable => Empty
case _ => Typ(and, true)
}
if (res) Typ(and, true) else Empty
}

/* Whether the extractor is irrefutable */
Expand Down Expand Up @@ -574,21 +499,94 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {

/** Can this type be inhabited by a value?
*
* Intersection between singleton types and other types is always empty
* the singleton type is not a subtype of the other type.
* See patmat/i3573.scala for an example.
* Check is based on the following facts:
*
* - single inheritance of classes
* - final class cannot be extended
* - intersection of a singleton type with another irrelevant type (patmat/i3574.scala)
*
*/
def inhabited(tpe: Type)(implicit ctx: Context): Boolean = {
val emptySingletonIntersection = new ExistsAccumulator({
case AndType(s: SingletonType, t) =>
!(s <:< t)
case AndType(t, s: SingletonType) =>
!(s <:< t)
case x =>
false
})

!emptySingletonIntersection(false, tpe)
def inhabited(tp: Type)(implicit ctx: Context): Boolean = {
// convert top-level type shape into "conjunctive normal form"
def cnf(tp: Type): Type = tp match {
case AndType(OrType(l, r), tp) =>
OrType(cnf(AndType(l, tp)), cnf(AndType(r, tp)))
case AndType(tp, o: OrType) =>
cnf(AndType(o, tp))
case AndType(l, r) =>
val l1 = cnf(l)
val r1 = cnf(r)
if (l1.ne(l) || r1.ne(r)) cnf(AndType(l1, r1))
else AndType(l1, r1)
case OrType(l, r) =>
OrType(cnf(l), cnf(r))
case tp @ RefinedType(OrType(tp1, tp2), _, _) =>
OrType(
cnf(tp.derivedRefinedType(tp1, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo)),
cnf(tp.derivedRefinedType(tp2, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo))
)
case tp: RefinedType =>
val parent1 = cnf(tp.parent)
val tp1 = tp.derivedRefinedType(parent1, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo)

if (parent1.ne(tp.parent)) cnf(tp1) else tp1
case tp: TypeAlias =>
cnf(tp.alias)
case _ =>
tp
}

def isSingleton(tp: Type): Boolean = tp.dealias match {
case AndType(l, r) => isSingleton(l) || isSingleton(r)
case OrType(l, r) => isSingleton(l) && isSingleton(r)
case tp => tp.isSingleton
}

def superType(tp: Type): Type = tp match {
case tp: TypeProxy => tp.superType
case OrType(tp1, tp2) => OrType(superType(tp1), superType(tp2))
case AndType(tp1, tp2) => AndType(superType(tp1), superType(tp2))
case _ => tp
}

def recur(tp: Type): Boolean = tp.dealias match {
case AndType(tp1, tp2) =>
recur(tp1) && recur(tp2) && {
val bases1 = tp1.widenDealias.classSymbols
val bases2 = tp2.widenDealias.classSymbols

debug.println(s"bases of ${tp1.show}: " + bases1)
debug.println(s"bases of ${tp2.show}: " + bases2)

val noClassConflict =
bases1.forall(sym1 => sym1.is(Trait) || bases2.forall(sym2 => sym2.is(Trait) || sym1.isSubClass(sym2))) ||
bases1.forall(sym1 => sym1.is(Trait) || bases2.forall(sym2 => sym2.is(Trait) || sym2.isSubClass(sym1)))

debug.println(s"class conflict for ${tp.show}? " + !noClassConflict)

noClassConflict &&
(!isSingleton(tp1) || tp1 <:< tp2) &&
(!isSingleton(tp2) || tp2 <:< tp1) &&
(!bases1.exists(_ is Final) || tp1 <:< superType(tp2)) &&
(!bases2.exists(_ is Final) || tp2 <:< superType(tp1))
}
case OrType(tp1, tp2) =>
recur(tp1) || recur(tp2)
case tp: RefinedType =>
recur(tp.parent)
case tp: TypeRef =>
recur(tp.prefix) &&
!(tp.classSymbol.is(Sealed) && tp.classSymbol.is(AbstractOrTrait) && tp.classSymbol.children.isEmpty) &&
!(tp.classSymbol.is(AbstractFinal))
case _ =>
true
}

val res = recur(cnf(tp))

debug.println(s"${tp.show} inhabited? " + res)

res
}

/** Instantiate type `tp1` to be a subtype of `tp2`
Expand Down