package dotty.tools.dotc
package transform
package patmat
import core.Types._
import core.Contexts._
import core.Flags._
import ast.Trees._
import ast.tpd
import core.Decorators._
import core.Symbols._
import core.StdNames._
import core.NameOps._
import core.Constants._
import reporting.diagnostic.messages._
import config.Printers.{ exhaustivity => debug }
/** Space logic for checking exhaustivity and unreachability of pattern matching
*
* Space can be thought of as a set of possible values. A type or a pattern
* both refer to spaces. The space of a type is the values that inhabit the
* type. The space of a pattern is the values that can be covered by the
* pattern.
*
* Space is recursively defined as follows:
*
* 1. `Empty` is a space
* 2. For a type T, `Typ(T)` is a space
* 3. A union of spaces `S1 | S2 | ...` is a space
* 4. For a case class Kon(x1: T1, x2: T2, .., xn: Tn), if S1, S2, ..., Sn
* are spaces, then `Kon(S1, S2, ..., Sn)` is a space.
*
* For the problem of exhaustivity check, its formulation in terms of space is as follows:
*
* Is the space Typ(T) a subspace of the union of space covered by all the patterns?
*
* The problem of unreachable patterns can be formulated as follows:
*
* Is the space covered by a pattern a subspace of the space covered by previous patterns?
*
* Assumption:
* (1) One case class cannot be inherited directly or indirectly by another
* case class.
* (2) Inheritance of a case class cannot be well handled by the algorithm.
*
*/
/** space definition */
sealed trait Space
/** Empty space */
case object Empty extends Space
/** Space representing the set of all values of a type
*
* @param tp: the type this space represents
* @param decomposed: does the space result from decomposition? Used for pretty print
*
*/
case class Typ(tp: Type, decomposed: Boolean) extends Space
/** Space representing a constructor pattern */
case class Kon(tp: Type, params: List[Space]) extends Space
/** Union of spaces */
case class Or(spaces: List[Space]) extends Space
/** abstract space logic */
trait SpaceLogic {
/** Is `tp1` a subtype of `tp2`? */
def isSubType(tp1: Type, tp2: Type): Boolean
/** Is `tp1` the same type as `tp2`? */
def isEqualType(tp1: Type, tp2: Type): Boolean
/** Is the type `tp` decomposable? i.e. all values of the type can be covered
* by its decomposed types.
*
* Abstract sealed class, OrType, Boolean and Java enums can be decomposed.
*/
def canDecompose(tp: Type): Boolean
/** Return term parameter types of the case class `tp` */
def signature(tp: Type): List[Type]
/** Get components of decomposable types */
def decompose(tp: Type): List[Space]
/** Display space in string format */
def show(sp: Space): String
/** Simplify space using the laws, there's no nested union after simplify */
def simplify(space: Space): Space = space match {
case Kon(tp, spaces) =>
val sp = Kon(tp, spaces.map(simplify _))
if (sp.params.contains(Empty)) Empty
else sp
case Or(spaces) =>
val set = spaces.map(simplify _).flatMap {
case Or(ss) => ss
case s => Seq(s)
} filter (_ != Empty)
if (set.isEmpty) Empty
else if (set.size == 1) set.toList(0)
else Or(set)
case Typ(tp, _) =>
if (canDecompose(tp) && decompose(tp).isEmpty) Empty
else space
case _ => space
}
/** Flatten space to get rid of `Or` for pretty print */
def flatten(space: Space): List[Space] = space match {
case Kon(tp, spaces) =>
val flats = spaces.map(flatten _)
flats.foldLeft(List[Kon]()) { (acc, flat) =>
if (acc.isEmpty) flat.map(s => Kon(tp, Nil :+ s))
else for (Kon(tp, ss) <- acc; s <- flat) yield Kon(tp, ss :+ s)
}
case Or(spaces) =>
spaces.flatMap(flatten _)
case _ => List(space)
}
/** Is `a` a subspace of `b`? Equivalent to `a - b == Empty`, but faster */
def isSubspace(a: Space, b: Space): Boolean = {
def tryDecompose1(tp: Type) = canDecompose(tp) && isSubspace(Or(decompose(tp)), b)
def tryDecompose2(tp: Type) = canDecompose(tp) && isSubspace(a, Or(decompose(tp)))
val res = (a, b) match {
case (Empty, _) => true
case (_, Empty) => false
case (Or(ss), _) => ss.forall(isSubspace(_, b))
case (Typ(tp1, _), Typ(tp2, _)) =>
isSubType(tp1, tp2) || tryDecompose1(tp1) || tryDecompose2(tp2)
case (Typ(tp1, _), Or(ss)) =>
ss.exists(isSubspace(a, _)) || tryDecompose1(tp1)
case (Typ(tp1, _), Kon(tp2, ss)) =>
isSubType(tp1, tp2) && isSubspace(Kon(tp2, signature(tp2).map(Typ(_, false))), b) ||
tryDecompose1(tp1)
case (Kon(tp1, ss), Typ(tp2, _)) =>
isSubType(tp1, tp2) ||
simplify(a) == Empty ||
(isSubType(tp2, tp1) && tryDecompose1(tp1)) ||
tryDecompose2(tp2)
case (Kon(_, _), Or(_)) =>
simplify(minus(a, b)) == Empty
case (Kon(tp1, ss1), Kon(tp2, ss2)) =>
isEqualType(tp1, tp2) && ss1.zip(ss2).forall((isSubspace _).tupled)
}
debug.println(s"${show(a)} < ${show(b)} = $res")
res
}
/** Intersection of two spaces */
def intersect(a: Space, b: Space): Space = {
def tryDecompose1(tp: Type) = intersect(Or(decompose(tp)), b)
def tryDecompose2(tp: Type) = intersect(a, Or(decompose(tp)))
val res = (a, b) match {
case (Empty, _) | (_, Empty) => Empty
case (_, Or(ss)) => Or(ss.map(intersect(a, _)).filterConserve(_ ne Empty))
case (Or(ss), _) => Or(ss.map(intersect(_, b)).filterConserve(_ ne Empty))
case (Typ(tp1, _), Typ(tp2, _)) =>
if (isSubType(tp1, tp2)) a
else if (isSubType(tp2, tp1)) b
else if (canDecompose(tp1)) tryDecompose1(tp1)
else if (canDecompose(tp2)) tryDecompose2(tp2)
else Empty
case (Typ(tp1, _), Kon(tp2, ss)) =>
if (isSubType(tp2, tp1)) b
else if (isSubType(tp1, tp2)) a // problematic corner case: inheriting a case class
else if (canDecompose(tp1)) tryDecompose1(tp1)
else Empty
case (Kon(tp1, ss), Typ(tp2, _)) =>
if (isSubType(tp1, tp2)) a
else if (isSubType(tp2, tp1)) a // problematic corner case: inheriting a case class
else if (canDecompose(tp2)) tryDecompose2(tp2)
else Empty
case (Kon(tp1, ss1), Kon(tp2, ss2)) =>
if (!isEqualType(tp1, tp2)) Empty
else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty)) Empty
else Kon(tp1, ss1.zip(ss2).map((intersect _).tupled))
}
debug.println(s"${show(a)} & ${show(b)} = ${show(res)}")
res
}
/** The space of a not covered by b */
def minus(a: Space, b: Space): Space = {
def tryDecompose1(tp: Type) = minus(Or(decompose(tp)), b)
def tryDecompose2(tp: Type) = minus(a, Or(decompose(tp)))
val res = (a, b) match {
case (Empty, _) => Empty
case (_, Empty) => a
case (Typ(tp1, _), Typ(tp2, _)) =>
if (isSubType(tp1, tp2)) Empty
else if (canDecompose(tp1)) tryDecompose1(tp1)
else if (canDecompose(tp2)) tryDecompose2(tp2)
else a
case (Typ(tp1, _), Kon(tp2, ss)) =>
// corner case: inheriting a case class
// rationale: every instance of `tp1` is covered by `tp2(_)`
if (isSubType(tp1, tp2)) minus(Kon(tp2, signature(tp2).map(Typ(_, false))), b)
else if (canDecompose(tp1)) tryDecompose1(tp1)
else a
case (_, Or(ss)) =>
ss.foldLeft(a)(minus)
case (Or(ss), _) =>
Or(ss.map(minus(_, b)))
case (Kon(tp1, ss), Typ(tp2, _)) =>
// uncovered corner case: tp2 :< tp1
if (isSubType(tp1, tp2)) Empty
else if (simplify(a) == Empty) Empty
else if (canDecompose(tp2)) tryDecompose2(tp2)
else a
case (Kon(tp1, ss1), Kon(tp2, ss2)) =>
if (!isEqualType(tp1, tp2)) a
else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty)) a
else if (ss1.zip(ss2).forall((isSubspace _).tupled)) Empty
else
// `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
Or(ss1.zip(ss2).map((minus _).tupled).zip(0 to ss2.length - 1).map {
case (ri, i) => Kon(tp1, ss1.updated(i, ri))
})
}
debug.println(s"${show(a)} - ${show(b)} = ${show(res)}")
res
}
}
/** Scala implementation of space logic */
class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
import tpd._
/** Return the space that represents the pattern `pat`
*
* If roundUp is true, approximate extractors to its type,
* otherwise approximate extractors to Empty
*/
def project(pat: Tree, roundUp: Boolean = true)(implicit ctx: Context): Space = pat match {
case Literal(c) =>
if (c.value.isInstanceOf[Symbol])
Typ(c.value.asInstanceOf[Symbol].termRef, false)
else
Typ(ConstantType(c), false)
case _: BackquotedIdent => Typ(pat.tpe, false)
case Ident(_) | Select(_, _) =>
Typ(pat.tpe.stripAnnots, false)
case Alternative(trees) => Or(trees.map(project(_, roundUp)))
case Bind(_, pat) => project(pat)
case UnApply(_, _, pats) =>
if (pat.tpe.classSymbol.is(CaseClass))
Kon(pat.tpe.stripAnnots, pats.map(pat => project(pat, roundUp)))
else if (roundUp) Typ(pat.tpe.stripAnnots, false)
else Empty
case Typed(pat @ UnApply(_, _, _), _) => project(pat)
case Typed(expr, _) => Typ(expr.tpe.stripAnnots, true)
case _ =>
Empty
}
/* Erase a type binding according to erasure semantics in pattern matching */
def erase(tp: Type): Type = {
def doErase(tp: Type): Type = tp match {
case tp: HKApply => erase(tp.superType)
case tp: RefinedType => erase(tp.parent)
case _ => tp
}
tp match {
case OrType(tp1, tp2) =>
OrType(erase(tp1), erase(tp2))
case AndType(tp1, tp2) =>
AndType(erase(tp1), erase(tp2))
case _ =>
val origin = doErase(tp)
if (origin =:= defn.ArrayType) tp else origin
}
}
/** Is `tp1` a subtype of `tp2`? */
def isSubType(tp1: Type, tp2: Type): Boolean = {
// check SI-9657 and tests/patmat/gadt.scala
val res = erase(tp1) <:< erase(tp2)
debug.println(s"${tp1.show} <:< ${tp2.show} = $res")
res
}
def isEqualType(tp1: Type, tp2: Type): Boolean = tp1 =:= tp2
/** Parameter types of the case class type `tp` */
def signature(tp: Type): List[Type] = {
val ktor = tp.classSymbol.primaryConstructor.info
val meth = ktor match {
case ktor: PolyType =>
ktor.instantiate(tp.classSymbol.typeParams.map(_.typeRef)).asSeenFrom(tp, tp.classSymbol)
case _ => ktor
}
// refine path-dependent type in params. refer to t9672
meth.firstParamTypes.map(_.asSeenFrom(tp, tp.classSymbol))
}
/** Decompose a type into subspaces -- assume the type can be decomposed */
def decompose(tp: Type): List[Space] = {
val children = tp.classSymbol.annotations.filter(_.symbol == ctx.definitions.ChildAnnot).map { annot =>
// refer to definition of Annotation.makeChild
annot.tree match {
case Apply(TypeApply(_, List(tpTree)), _) => tpTree.symbol
}
}
debug.println(s"candidates for ${tp.show} : [${children.map(_.show).mkString(", ")}]")
tp.dealias match {
case OrType(tp1, tp2) => List(Typ(tp1, true), Typ(tp2, true))
case _ if tp =:= ctx.definitions.BooleanType =>
List(
Typ(ConstantType(Constant(true)), true),
Typ(ConstantType(Constant(false)), true)
)
case _ if tp.classSymbol.is(Enum) =>
children.map(sym => Typ(sym.termRef, true))
case _ =>
val parts = children.map { sym =>
if (sym.is(ModuleClass))
refine(tp, sym.sourceModule.termRef)
else if (sym.isTerm)
refine(tp, sym.termRef)
else if (sym.info.typeParams.length > 0 || tp.isInstanceOf[TypeRef])
refine(tp, sym.typeRef)
else
sym.typeRef
} filter { tpe =>
// Child class may not always be subtype of parent:
// GADT & path-dependent types
val res = tpe <:< expose(tp)
if (!res) debug.println(s"unqualified child ousted: ${tpe.show} !< ${tp.show}")
res
}
debug.println(s"${tp.show} decomposes to [${parts.map(_.show).mkString(", ")}]")
parts.map(Typ(_, true))
}
}
/** Refine tp2 based on tp1
*
* E.g. if `tp1` is `Option[Int]`, `tp2` is `Some`, then return
* `Some[Int]`.
*
* If `tp1` is `path1.A`, `tp2` is `path2.B`, and `path1` is subtype of
* `path2`, then return `path1.B`.
*/
def refine(tp1: Type, tp2: Type): Type = (tp1, tp2) match {
case (tp1: RefinedType, _: TypeRef) => tp1.wrapIfMember(refine(tp1.parent, tp2))
case (tp1: HKApply, _) => refine(tp1.superType, tp2)
case (TypeRef(ref1: TypeProxy, _), tp2 @ TypeRef(ref2: TypeProxy, _)) =>
if (ref1.underlying <:< ref2.underlying) tp2.derivedSelect(ref1) else tp2
case (TypeRef(ref1: TypeProxy, _), tp2 @ TermRef(ref2: TypeProxy, _)) =>
if (ref1.underlying <:< ref2.underlying) tp2.derivedSelect(ref1) else tp2
case _ => tp2
}
/** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
def canDecompose(tp: Type): Boolean = {
val res = tp.classSymbol.is(allOf(Abstract, Sealed)) ||
tp.classSymbol.is(allOf(Trait, Sealed)) ||
tp.dealias.isInstanceOf[OrType] ||
tp =:= ctx.definitions.BooleanType ||
tp.classSymbol.is(allOf(Enum, Sealed)) // Enum value doesn't have Sealed flag
debug.println(s"decomposable: ${tp.show} = $res")
res
}
/** Show friendly type name with current scope in mind
*
* E.g. C.this.B --> B if current owner is C
* C.this.x.T --> x.T if current owner is C
* X[T] --> X
* C --> C if current owner is C !!!
*
*/
def showType(tp: Type): String = {
val enclosingCls = ctx.owner.enclosingClass.asClass.classInfo.symbolicTypeRef
def isOmittable(sym: Symbol) =
sym.isEffectiveRoot || sym.isAnonymousClass || sym.name.isReplWrapperName ||
ctx.definitions.UnqualifiedOwnerTypes.exists(_.symbol == sym) ||
sym.showFullName.startsWith("scala.") ||
sym == enclosingCls.typeSymbol
def refinePrefix(tp: Type): String = tp match {
case NoPrefix => ""
case tp: NamedType if isOmittable(tp.symbol) => ""
case tp: ThisType => refinePrefix(tp.tref)
case tp: RefinedType => refinePrefix(tp.parent)
case tp: NamedType => tp.name.show.stripSuffix("$")
}
def refine(tp: Type): String = tp match {
case tp: RefinedType => refine(tp.parent)
case tp: ThisType => refine(tp.tref)
case tp: NamedType =>
val pre = refinePrefix(tp.prefix)
if (tp.name == tpnme.higherKinds) pre
else if (pre.isEmpty) tp.name.show.stripSuffix("$")
else pre + "." + tp.name.show.stripSuffix("$")
case _ => tp.show.stripSuffix("$")
}
val text = tp.stripAnnots match {
case tp: OrType => showType(tp.tp1) + " | " + showType(tp.tp2)
case tp => refine(tp)
}
if (text.isEmpty) enclosingCls.show.stripSuffix("$")
else text
}
/** Display spaces */
def show(s: Space): String = {
def doShow(s: Space, mergeList: Boolean = false): String = s match {
case Empty => ""
case Typ(c: ConstantType, _) => c.value.show
case Typ(tp: TermRef, _) => tp.symbol.showName
case Typ(tp, decomposed) =>
val sym = tp.widen.classSymbol
if (ctx.definitions.isTupleType(tp))
signature(tp).map(_ => "_").mkString("(", ", ", ")")
else if (sym.showFullName == "scala.collection.immutable.::")
if (mergeList) "_" else "List(_)"
else if (tp.classSymbol.is(CaseClass))
// use constructor syntax for case class
showType(tp) + signature(tp).map(_ => "_").mkString("(", ", ", ")")
else if (signature(tp).nonEmpty)
tp.classSymbol.name + signature(tp).map(_ => "_").mkString("(", ", ", ")")
else if (decomposed) "_: " + showType(tp)
else "_"
case Kon(tp, params) =>
if (ctx.definitions.isTupleType(tp))
"(" + params.map(doShow(_)).mkString(", ") + ")"
else if (tp.widen.classSymbol.showFullName == "scala.collection.immutable.::")
if (mergeList) params.map(doShow(_, mergeList)).mkString(", ")
else params.map(doShow(_, true)).filter(_ != "Nil").mkString("List(", ", ", ")")
else
showType(tp) + params.map(doShow(_)).mkString("(", ", ", ")")
case Or(_) =>
throw new Exception("incorrect flatten result " + s)
}
flatten(s).map(doShow(_, false)).distinct.mkString(", ")
}
def checkable(tree: Match): Boolean = {
def isCheckable(tp: Type): Boolean = tp match {
case AnnotatedType(tp, annot) =>
(ctx.definitions.UncheckedAnnot != annot.symbol) && isCheckable(tp)
case _ =>
// Possible to check everything, but be compatible with scalac by default
ctx.settings.YcheckAllPatmat.value ||
tp.typeSymbol.is(Sealed) ||
tp.isInstanceOf[OrType] ||
tp.typeSymbol == ctx.definitions.BooleanType.typeSymbol ||
tp.typeSymbol.is(Enum) ||
canDecompose(tp) ||
(defn.isTupleType(tp) && tp.dealias.argInfos.exists(isCheckable(_)))
}
val Match(sel, cases) = tree
val res = isCheckable(sel.tpe.widen.deAnonymize.dealiasKeepAnnots)
debug.println(s"checkable: ${sel.show} = $res")
res
}
/** Expose refined type to eliminate reference to type variables
*
* A = B M { type T = A } ~~> M { type T = B }
*
* A <: X :> Y M { type T = A } ~~> M { type T <: X :> Y }
*
* A <: X :> Y B <: U :> V M { type T <: A :> B } ~~> M { type T <: X :> V }
*
* A = X B = Y M { type T <: A :> B } ~~> M { type T <: X :> Y }
*/
def expose(tp: Type): Type = {
def follow(tp: Type, up: Boolean): Type = tp match {
case tp: TypeProxy =>
tp.underlying match {
case TypeBounds(lo, hi) =>
follow(if (up) hi else lo, up)
case _ =>
tp
}
case OrType(tp1, tp2) =>
OrType(follow(tp1, up), follow(tp2, up))
case AndType(tp1, tp2) =>
AndType(follow(tp1, up), follow(tp2, up))
}
tp match {
case tp: RefinedType =>
tp.refinedInfo match {
case tpa : TypeAlias =>
val hi = follow(tpa.alias, true)
val lo = follow(tpa.alias, false)
val refined = if (hi =:= lo)
tpa.derivedTypeAlias(hi)
else
tpa.derivedTypeBounds(lo, hi)
tp.derivedRefinedType(
expose(tp.parent),
tp.refinedName,
refined
)
case tpb @ TypeBounds(lo, hi) =>
tp.derivedRefinedType(
expose(tp.parent),
tp.refinedName,
tpb.derivedTypeBounds(follow(lo, false), follow(hi, true))
)
case tp => tp
}
case _ => tp
}
}
def checkExhaustivity(_match: Match): Unit = {
val Match(sel, cases) = _match
val selTyp = sel.tpe.widen.deAnonymize.dealias
val patternSpace = cases.map({ x =>
val space = project(x.pat)
debug.println(s"${x.pat.show} projects to ${show(space)}")
space
}).reduce((a, b) => Or(List(a, b)))
val uncovered = simplify(minus(Typ(selTyp, true), patternSpace))
if (uncovered != Empty)
ctx.warning(PatternMatchExhaustivity(show(uncovered)), _match.pos)
}
def checkRedundancy(_match: Match): Unit = {
val Match(sel, cases) = _match
// ignore selector type for now
// val selTyp = sel.tpe.widen.deAnonymize.dealias
// starts from the second, the first can't be redundant
(1 until cases.length).foreach { i =>
// in redundancy check, take guard as false, take extractor as match
// nothing in order to soundly approximate
val prevs = cases.take(i).map { x =>
if (x.guard.isEmpty) project(x.pat, false)
else Empty
}.reduce((a, b) => Or(List(a, b)))
val curr = project(cases(i).pat)
if (isSubspace(curr, prevs)) {
ctx.warning(MatchCaseUnreachable(), cases(i).body.pos)
}
}
}
}
