Skip to content

Commit 96bd9db

Browse files
OlivierBlanvillainOlivierBlanvillain
committed
Refactor intersecting as disjoint
1 parent 0cec095 commit 96bd9db

File tree

2 files changed

+40
-42
lines changed

2 files changed

+40
-42
lines changed

‎compiler/src/dotty/tools/dotc/core/TypeComparer.scala

+36-38
Original file line numberDiff line numberDiff line change
@@ -1895,9 +1895,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
18951895
/** Returns last check's debug mode, if explicitly enabled. */
18961896
def lastTrace(): String = ""
18971897

1898-
/** Do `tp1` and `tp2` share a non-null inhabitant?
1898+
/** Are `tp1` and `tp2` disjoint types?
18991899
*
1900-
* `false` implies that we found a proof; uncertainty default to `true`.
1900+
* `true` implies that we found a proof; uncertainty default to `false`.
19011901
*
19021902
* Proofs rely on the following properties of Scala types:
19031903
*
@@ -1906,8 +1906,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
19061906
* 3. ConstantTypes with distinc values are non intersecting
19071907
* 4. There is no value of type Nothing
19081908
*/
1909-
def intersecting(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
1910-
// println(s"intersecting(${tp1.show}, ${tp2.show})")
1909+
def disjoint(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
1910+
// println(s"disjoint(${tp1.show}, ${tp2.show})")
19111911
/** Can we enumerate all instantiations of this type? */
19121912
def isClosedSum(tp: Symbol): Boolean =
19131913
tp.is(Sealed) && tp.is(AbstractOrTrait) && !tp.hasAnonymousChild
@@ -1921,34 +1921,34 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
19211921

19221922
(tp1.dealias, tp2.dealias) match {
19231923
case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol == defn.SingletonClass || tp2.symbol == defn.SingletonClass =>
1924-
true
1924+
false
19251925
case (tp1: ConstantType, tp2: ConstantType) =>
1926-
tp1 == tp2
1926+
tp1 != tp2
19271927
case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
19281928
val cls1 = tp1.classSymbol
19291929
val cls2 = tp2.classSymbol
19301930
if (cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1)) {
1931-
true
1931+
false
19321932
} else {
19331933
if (cls1.is(Final) || cls2.is(Final))
19341934
// One of these types is final and they are not mutually
19351935
// subtype, so they must be unrelated.
1936-
false
1936+
true
19371937
else if (!cls2.is(Trait) && !cls1.is(Trait))
19381938
// Both of these types are classes and they are not mutually
19391939
// subtype, so they must be unrelated by single inheritance
19401940
// of classes.
1941-
false
1941+
true
19421942
else if (isClosedSum(cls1))
1943-
decompose(cls1, tp1).exists(x => intersecting(x, tp2))
1943+
decompose(cls1, tp1).forall(x => disjoint(x, tp2))
19441944
else if (isClosedSum(cls2))
1945-
decompose(cls2, tp2).exists(x => intersecting(x, tp1))
1945+
decompose(cls2, tp2).forall(x => disjoint(x, tp1))
19461946
else
1947-
true
1947+
false
19481948
}
19491949
case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) if tycon1 == tycon2 =>
1950-
def covariantIntersecting(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = {
1951-
intersecting(tp1, tp2) || {
1950+
def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean = {
1951+
disjoint(tp1, tp2) && {
19521952
// We still need to proof that `Nothing` is not a valid
19531953
// instantiation of this type parameter. We have two ways
19541954
// to get to that conclusion:
@@ -1966,21 +1966,21 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
19661966
case _ =>
19671967
false
19681968
}
1969-
lowerBoundedByNothing && !typeUsedAsField
1969+
!lowerBoundedByNothing || typeUsedAsField
19701970
}
19711971
}
19721972

1973-
(args1, args2, tycon1.typeParams).zipped.forall {
1973+
(args1, args2, tycon1.typeParams).zipped.exists {
19741974
(arg1, arg2, tparam) =>
19751975
val v = tparam.paramVariance
19761976
if (v > 0)
1977-
covariantIntersecting(arg1, arg2, tparam)
1977+
covariantDisjoint(arg1, arg2, tparam)
19781978
else if (v < 0)
19791979
// Contravariant case: a value where this type parameter is
19801980
// instantiated to `Any` belongs to both types.
1981-
true
1981+
false
19821982
else
1983-
covariantIntersecting(arg1, arg2, tparam) && (isSameType(arg1, arg2) || {
1983+
covariantDisjoint(arg1, arg2, tparam) || !isSameType(arg1, arg2) && {
19841984
// We can only trust a "no" from `isSameType` when both
19851985
// `arg1` and `arg2` are fully instantiated.
19861986
def fullyInstantiated(tp: Type): Boolean = new TypeAccumulator[Boolean] {
@@ -1993,37 +1993,35 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
19931993
}
19941994
}
19951995
}.apply(true, tp)
1996-
!(fullyInstantiated(arg1) && fullyInstantiated(arg2))
1997-
})
1996+
fullyInstantiated(arg1) && fullyInstantiated(arg2)
1997+
}
19981998
}
19991999
case (tp1: HKLambda, tp2: HKLambda) =>
2000-
intersecting(tp1.resType, tp2.resType)
2000+
disjoint(tp1.resType, tp2.resType)
20012001
case (_: HKLambda, _) =>
2002-
// The intersection is ill kinded and therefore empty.
2003-
false
2002+
// The intersection of these two types would be ill kinded, they are therefore disjoint.
2003+
true
20042004
case (_, _: HKLambda) =>
2005-
false
2005+
true
20062006
case (tp1: OrType, _) =>
2007-
intersecting(tp1.tp1, tp2) || intersecting(tp1.tp2, tp2)
2007+
disjoint(tp1.tp1, tp2) && disjoint(tp1.tp2, tp2)
20082008
case (_, tp2: OrType) =>
2009-
intersecting(tp1, tp2.tp1) || intersecting(tp1, tp2.tp2)
2009+
disjoint(tp1, tp2.tp1) && disjoint(tp1, tp2.tp2)
20102010
case (tp1: AndType, tp2: AndType) =>
2011-
intersecting(tp1.tp1, tp2.tp1) && intersecting(tp1.tp2, tp2.tp2) ||
2012-
intersecting(tp1.tp1, tp2.tp2) && intersecting(tp1.tp2, tp2.tp1)
2011+
(disjoint(tp1.tp1, tp2.tp1) || disjoint(tp1.tp2, tp2.tp2)) &&
2012+
(disjoint(tp1.tp1, tp2.tp2) || disjoint(tp1.tp2, tp2.tp1))
20132013
case (tp1: AndType, _) =>
2014-
intersecting(tp1.tp1, tp2) && intersecting(tp1.tp2, tp2) ||
2015-
intersecting(tp1.tp2, tp2) && intersecting(tp1.tp1, tp2)
2014+
disjoint(tp1.tp2, tp2) || disjoint(tp1.tp1, tp2)
20162015
case (_, tp2: AndType) =>
2017-
intersecting(tp1, tp2.tp1) && intersecting(tp1, tp2.tp2) ||
2018-
intersecting(tp1, tp2.tp2) && intersecting(tp1, tp2.tp1)
2016+
disjoint(tp1, tp2.tp2) || disjoint(tp1, tp2.tp1)
20192017
case (tp1: TypeProxy, tp2: TypeProxy) =>
2020-
intersecting(tp1.underlying, tp2) && intersecting(tp1, tp2.underlying)
2018+
disjoint(tp1.underlying, tp2) || disjoint(tp1, tp2.underlying)
20212019
case (tp1: TypeProxy, _) =>
2022-
intersecting(tp1.underlying, tp2)
2020+
disjoint(tp1.underlying, tp2)
20232021
case (_, tp2: TypeProxy) =>
2024-
intersecting(tp1, tp2.underlying)
2022+
disjoint(tp1, tp2.underlying)
20252023
case _ =>
2026-
true
2024+
false
20272025
}
20282026
}
20292027
}
@@ -2175,7 +2173,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
21752173
}
21762174
else if (isSubType(widenAbstractTypes(scrut), widenAbstractTypes(pat)))
21772175
Some(NoType)
2178-
else if (!intersecting(scrut, pat))
2176+
else if (disjoint(scrut, pat))
21792177
// We found a proof that `scrut` and `pat` are incompatible.
21802178
// The search continues.
21812179
None

‎compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

+4-4
Original file line numberDiff line numberDiff line change
@@ -299,11 +299,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
299299
// Since projections of types don't include null, intersection with null is empty.
300300
return Empty
301301
}
302-
val res = ctx.typeComparer.intersecting(tp1, tp2)
302+
val res = ctx.typeComparer.disjoint(tp1, tp2)
303303

304-
debug.println(s"atomic intersection: ${AndType(tp1, tp2).show} = ${res}")
304+
debug.println(s"atomic intersection: ${AndType(tp1, tp2).show} = ${!res}")
305305

306-
if (!res) Empty
306+
if (res) Empty
307307
else if (tp1.isSingleton) Typ(tp1, true)
308308
else if (tp2.isSingleton) Typ(tp2, true)
309309
else Typ(AndType(tp1, tp2), true)
@@ -498,7 +498,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
498498

499499
def inhabited(tp: Type): Boolean =
500500
tp.dealias match {
501-
case AndType(tp1, tp2) => ctx.typeComparer.intersecting(tp1, tp2)
501+
case AndType(tp1, tp2) => !ctx.typeComparer.disjoint(tp1, tp2)
502502
case OrType(tp1, tp2) => inhabited(tp1) || inhabited(tp2)
503503
case tp: RefinedType => inhabited(tp.parent)
504504
case tp: TypeRef => inhabited(tp.prefix)

0 commit comments

Comments
 (0)