Compare commits
3 Commits
dcreager/s
...
alex/truth
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
8ce17f30c6 | ||
|
|
7318ff9d63 | ||
|
|
6991676a9d |
@@ -58,7 +58,22 @@ reveal_type(c >= d) # revealed: Literal[True]
|
||||
#### Results with Ambiguity
|
||||
|
||||
```py
|
||||
def _(x: bool, y: int):
|
||||
class P:
|
||||
def __lt__(self, other: "P") -> bool:
|
||||
return True
|
||||
|
||||
def __le__(self, other: "P") -> bool:
|
||||
return True
|
||||
|
||||
def __gt__(self, other: "P") -> bool:
|
||||
return True
|
||||
|
||||
def __ge__(self, other: "P") -> bool:
|
||||
return True
|
||||
|
||||
class Q(P): ...
|
||||
|
||||
def _(x: P, y: Q):
|
||||
a = (x,)
|
||||
b = (y,)
|
||||
|
||||
|
||||
@@ -455,9 +455,9 @@ else:
|
||||
reveal_type(x) # revealed: slice
|
||||
finally:
|
||||
# TODO: should be `Literal[1] | str | bytes | bool | memoryview | float | range | slice`
|
||||
reveal_type(x) # revealed: bool | float | slice
|
||||
reveal_type(x) # revealed: bool | slice | float
|
||||
|
||||
reveal_type(x) # revealed: bool | float | slice
|
||||
reveal_type(x) # revealed: bool | slice | float
|
||||
```
|
||||
|
||||
## Nested `try`/`except` blocks
|
||||
@@ -534,7 +534,7 @@ try:
|
||||
reveal_type(x) # revealed: slice
|
||||
finally:
|
||||
# TODO: should be `Literal[1] | str | bytes | bool | memoryview | float | range | slice`
|
||||
reveal_type(x) # revealed: bool | float | slice
|
||||
reveal_type(x) # revealed: bool | slice | float
|
||||
x = 2
|
||||
reveal_type(x) # revealed: Literal[2]
|
||||
reveal_type(x) # revealed: Literal[2]
|
||||
|
||||
@@ -21,22 +21,22 @@ else:
|
||||
if x and not x:
|
||||
reveal_type(x) # revealed: Never
|
||||
else:
|
||||
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]
|
||||
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | tuple[()] | None
|
||||
|
||||
if not (x and not x):
|
||||
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]
|
||||
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | tuple[()] | None
|
||||
else:
|
||||
reveal_type(x) # revealed: Never
|
||||
|
||||
if x or not x:
|
||||
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]
|
||||
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | tuple[()] | None
|
||||
else:
|
||||
reveal_type(x) # revealed: Never
|
||||
|
||||
if not (x or not x):
|
||||
reveal_type(x) # revealed: Never
|
||||
else:
|
||||
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | None | tuple[()]
|
||||
reveal_type(x) # revealed: Literal[0, -1, "", "foo", b"", b"bar"] | bool | tuple[()] | None
|
||||
|
||||
if (isinstance(x, int) or isinstance(x, str)) and x:
|
||||
reveal_type(x) # revealed: Literal[-1, True, "foo"]
|
||||
|
||||
@@ -346,4 +346,16 @@ static_assert(is_assignable_to(Never, type[str]))
|
||||
static_assert(is_assignable_to(Never, type[Any]))
|
||||
```
|
||||
|
||||
### `bool` is assignable to unions that include `bool`
|
||||
|
||||
Since we decompose `bool` to `Literal[True, False]` in unions, it would be surprisingly easy to get
|
||||
this wrong if we forgot to normalize `bool` to `Literal[True, False]` when it appeared on the
|
||||
left-hand side in `Type::is_assignable_to()`.
|
||||
|
||||
```py
|
||||
from knot_extensions import is_assignable_to, static_assert
|
||||
|
||||
static_assert(is_assignable_to(bool, str | bool))
|
||||
```
|
||||
|
||||
[typing documentation]: https://typing.readthedocs.io/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation
|
||||
|
||||
@@ -118,4 +118,48 @@ class R: ...
|
||||
static_assert(is_equivalent_to(Intersection[tuple[P | Q], R], Intersection[tuple[Q | P], R]))
|
||||
```
|
||||
|
||||
## Unions containing tuples containing `bool`
|
||||
|
||||
```py
|
||||
from knot_extensions import is_equivalent_to, static_assert
|
||||
from typing_extensions import Literal
|
||||
|
||||
class P: ...
|
||||
|
||||
static_assert(is_equivalent_to(tuple[Literal[True, False]] | P, tuple[bool] | P))
|
||||
static_assert(is_equivalent_to(P | tuple[bool], P | tuple[Literal[True, False]]))
|
||||
```
|
||||
|
||||
## Unions and intersections involving `AlwaysTruthy`, `bool` and `AlwaysFalsy`
|
||||
|
||||
```py
|
||||
from knot_extensions import AlwaysTruthy, AlwaysFalsy, static_assert, is_equivalent_to, Not
|
||||
from typing_extensions import Literal
|
||||
|
||||
static_assert(is_equivalent_to(AlwaysTruthy | bool, Literal[False] | AlwaysTruthy))
|
||||
static_assert(is_equivalent_to(AlwaysFalsy | bool, Literal[True] | AlwaysFalsy))
|
||||
static_assert(is_equivalent_to(Not[AlwaysTruthy] | bool, Not[AlwaysTruthy] | Literal[True]))
|
||||
static_assert(is_equivalent_to(Not[AlwaysFalsy] | bool, Literal[False] | Not[AlwaysFalsy]))
|
||||
```
|
||||
|
||||
## Unions and intersections involving `AlwaysTruthy`, `LiteralString` and `AlwaysFalsy`
|
||||
|
||||
```py
|
||||
from knot_extensions import AlwaysTruthy, AlwaysFalsy, static_assert, is_equivalent_to, Not, Intersection
|
||||
from typing_extensions import Literal, LiteralString
|
||||
|
||||
# TODO: these should all pass!
|
||||
|
||||
# error: [static-assert-error]
|
||||
static_assert(is_equivalent_to(AlwaysTruthy | LiteralString, Literal[""] | AlwaysTruthy))
|
||||
# error: [static-assert-error]
|
||||
static_assert(is_equivalent_to(AlwaysFalsy | LiteralString, Intersection[LiteralString, Not[Literal[""]]] | AlwaysFalsy))
|
||||
# error: [static-assert-error]
|
||||
static_assert(is_equivalent_to(Not[AlwaysFalsy] | LiteralString, Literal[""] | Not[AlwaysFalsy]))
|
||||
# error: [static-assert-error]
|
||||
static_assert(
|
||||
is_equivalent_to(Not[AlwaysTruthy] | LiteralString, Not[AlwaysTruthy] | Intersection[LiteralString, Not[Literal[""]]])
|
||||
)
|
||||
```
|
||||
|
||||
[the equivalence relation]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-equivalent
|
||||
|
||||
@@ -449,5 +449,31 @@ static_assert(not is_subtype_of(Intersection[Unknown, int], int))
|
||||
static_assert(not is_subtype_of(tuple[int, int], tuple[int, Unknown]))
|
||||
```
|
||||
|
||||
## `bool` is a subtype of `AlwaysTruthy | AlwaysFalsy`
|
||||
|
||||
`bool` is equivalent to `Literal[True] | Literal[False]`. `Literal[True]` is a subtype of
|
||||
`AlwaysTruthy` and `Literal[False]` is a subtype of `AlwaysFalsy`; it therefore stands to reason
|
||||
that `bool` is a subtype of `AlwaysTruthy | AlwaysFalsy`.
|
||||
|
||||
```py
|
||||
from knot_extensions import AlwaysTruthy, AlwaysFalsy, is_subtype_of, static_assert, Not, is_disjoint_from
|
||||
from typing_extensions import Literal
|
||||
|
||||
static_assert(is_subtype_of(bool, AlwaysTruthy | AlwaysFalsy))
|
||||
|
||||
# the inverse also applies -- TODO: this should pass!
|
||||
# See the TODO comments in the `Type::Intersection` branch of `Type::is_disjoint_from()`.
|
||||
static_assert(is_disjoint_from(bool, Not[AlwaysTruthy | AlwaysFalsy])) # error: [static-assert-error]
|
||||
|
||||
# `Type::is_subtype_of` delegates many questions of `bool` subtyping to `int`,
|
||||
# but set-theoretic types like intersections and unions are still handled differently to `int`
|
||||
static_assert(is_subtype_of(Literal[True], Not[Literal[2]]))
|
||||
static_assert(is_subtype_of(bool, Not[Literal[2]]))
|
||||
static_assert(is_subtype_of(Literal[True], bool | None))
|
||||
static_assert(is_subtype_of(bool, bool | None))
|
||||
|
||||
static_assert(not is_subtype_of(int, Not[Literal[2]]))
|
||||
```
|
||||
|
||||
[special case for float and complex]: https://typing.readthedocs.io/en/latest/spec/special-types.html#special-cases-for-float-and-complex
|
||||
[typing documentation]: https://typing.readthedocs.io/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence
|
||||
|
||||
@@ -811,6 +811,29 @@ impl<'db> Type<'db> {
|
||||
}
|
||||
}
|
||||
|
||||
/// Normalize the type `bool` -> `Literal[True, False]`.
|
||||
///
|
||||
/// Using this method in various type-relational methods
|
||||
/// ensures that the following invariants hold true:
|
||||
///
|
||||
/// - bool ≡ Literal[True, False]
|
||||
/// - bool | T ≡ Literal[True, False] | T
|
||||
/// - bool <: Literal[True, False]
|
||||
/// - bool | T <: Literal[True, False] | T
|
||||
/// - Literal[True, False] <: bool
|
||||
/// - Literal[True, False] | T <: bool | T
|
||||
#[must_use]
|
||||
pub fn with_normalized_bools(self, db: &'db dyn Db) -> Self {
|
||||
match self {
|
||||
Type::Instance(InstanceType { class }) if class.is_known(db, KnownClass::Bool) => {
|
||||
Type::normalized_bool(db)
|
||||
}
|
||||
// TODO: decompose `LiteralString` into `Literal[""] | TruthyLiteralString`?
|
||||
// We'd need to rename this method... --Alex
|
||||
_ => self,
|
||||
}
|
||||
}
|
||||
|
||||
/// Return a normalized version of `self` in which all unions and intersections are sorted
|
||||
/// according to a canonical order, no matter how "deeply" a union/intersection may be nested.
|
||||
#[must_use]
|
||||
@@ -881,6 +904,13 @@ impl<'db> Type<'db> {
|
||||
(Type::Never, _) => true,
|
||||
(_, Type::Never) => false,
|
||||
|
||||
(Type::Instance(InstanceType { class }), _) if class.is_known(db, KnownClass::Bool) => {
|
||||
Type::normalized_bool(db).is_subtype_of(db, target)
|
||||
}
|
||||
(_, Type::Instance(InstanceType { class })) if class.is_known(db, KnownClass::Bool) => {
|
||||
self.is_subtype_of(db, Type::normalized_bool(db))
|
||||
}
|
||||
|
||||
(Type::Union(union), _) => union
|
||||
.elements(db)
|
||||
.iter()
|
||||
@@ -961,7 +991,7 @@ impl<'db> Type<'db> {
|
||||
KnownClass::Str.to_instance(db).is_subtype_of(db, target)
|
||||
}
|
||||
(Type::BooleanLiteral(_), _) => {
|
||||
KnownClass::Bool.to_instance(db).is_subtype_of(db, target)
|
||||
KnownClass::Int.to_instance(db).is_subtype_of(db, target)
|
||||
}
|
||||
(Type::IntLiteral(_), _) => KnownClass::Int.to_instance(db).is_subtype_of(db, target),
|
||||
(Type::BytesLiteral(_), _) => {
|
||||
@@ -1093,6 +1123,13 @@ impl<'db> Type<'db> {
|
||||
true
|
||||
}
|
||||
|
||||
(Type::Instance(InstanceType { class }), _) if class.is_known(db, KnownClass::Bool) => {
|
||||
Type::normalized_bool(db).is_assignable_to(db, target)
|
||||
}
|
||||
(_, Type::Instance(InstanceType { class })) if class.is_known(db, KnownClass::Bool) => {
|
||||
self.is_assignable_to(db, Type::normalized_bool(db))
|
||||
}
|
||||
|
||||
// A union is assignable to a type T iff every element of the union is assignable to T.
|
||||
(Type::Union(union), ty) => union
|
||||
.elements(db)
|
||||
@@ -1183,6 +1220,12 @@ impl<'db> Type<'db> {
|
||||
left.is_equivalent_to(db, right)
|
||||
}
|
||||
(Type::Tuple(left), Type::Tuple(right)) => left.is_equivalent_to(db, right),
|
||||
(Type::Instance(InstanceType { class }), _) if class.is_known(db, KnownClass::Bool) => {
|
||||
Type::normalized_bool(db).is_equivalent_to(db, other)
|
||||
}
|
||||
(_, Type::Instance(InstanceType { class })) if class.is_known(db, KnownClass::Bool) => {
|
||||
self.is_equivalent_to(db, Type::normalized_bool(db))
|
||||
}
|
||||
_ => self == other && self.is_fully_static(db) && other.is_fully_static(db),
|
||||
}
|
||||
}
|
||||
@@ -1241,6 +1284,13 @@ impl<'db> Type<'db> {
|
||||
first.is_gradual_equivalent_to(db, second)
|
||||
}
|
||||
|
||||
(Type::Instance(InstanceType { class }), _) if class.is_known(db, KnownClass::Bool) => {
|
||||
Type::normalized_bool(db).is_gradual_equivalent_to(db, other)
|
||||
}
|
||||
(_, Type::Instance(InstanceType { class })) if class.is_known(db, KnownClass::Bool) => {
|
||||
self.is_gradual_equivalent_to(db, Type::normalized_bool(db))
|
||||
}
|
||||
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
@@ -1255,6 +1305,13 @@ impl<'db> Type<'db> {
|
||||
|
||||
(Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => false,
|
||||
|
||||
(Type::Instance(InstanceType { class }), ty)
|
||||
| (ty, Type::Instance(InstanceType { class }))
|
||||
if class.is_known(db, KnownClass::Bool) =>
|
||||
{
|
||||
Type::normalized_bool(db).is_disjoint_from(db, ty)
|
||||
}
|
||||
|
||||
(Type::Union(union), other) | (other, Type::Union(union)) => union
|
||||
.elements(db)
|
||||
.iter()
|
||||
@@ -2371,6 +2428,13 @@ impl<'db> Type<'db> {
|
||||
KnownClass::NoneType.to_instance(db)
|
||||
}
|
||||
|
||||
/// The type `Literal[True, False]`, which is exactly equivalent to `bool`
|
||||
/// (and which `bool` is eagerly normalized to in several situations)
|
||||
pub fn normalized_bool(db: &'db dyn Db) -> Type<'db> {
|
||||
const LITERAL_BOOLS: [Type; 2] = [Type::BooleanLiteral(false), Type::BooleanLiteral(true)];
|
||||
Type::Union(UnionType::new(db, Box::from(LITERAL_BOOLS)))
|
||||
}
|
||||
|
||||
/// Return the type of `tuple(sys.version_info)`.
|
||||
///
|
||||
/// This is not exactly the type that `sys.version_info` has at runtime,
|
||||
@@ -4642,18 +4706,19 @@ pub struct TupleType<'db> {
|
||||
}
|
||||
|
||||
impl<'db> TupleType<'db> {
|
||||
pub fn from_elements<T: Into<Type<'db>>>(
|
||||
db: &'db dyn Db,
|
||||
types: impl IntoIterator<Item = T>,
|
||||
) -> Type<'db> {
|
||||
pub fn from_elements<I, T>(db: &'db dyn Db, types: I) -> Type<'db>
|
||||
where
|
||||
I: IntoIterator<Item = T>,
|
||||
T: Into<Type<'db>>,
|
||||
{
|
||||
let mut elements = vec![];
|
||||
|
||||
for ty in types {
|
||||
let ty = ty.into();
|
||||
let ty: Type<'db> = ty.into();
|
||||
if ty.is_never() {
|
||||
return Type::Never;
|
||||
}
|
||||
elements.push(ty);
|
||||
elements.push(ty.with_normalized_bools(db));
|
||||
}
|
||||
|
||||
Type::Tuple(Self::new(db, elements.into_boxed_slice()))
|
||||
|
||||
@@ -26,7 +26,7 @@
|
||||
//! eliminate the supertype from the intersection).
|
||||
//! * An intersection containing two non-overlapping types should simplify to [`Type::Never`].
|
||||
|
||||
use crate::types::{InstanceType, IntersectionType, KnownClass, Type, UnionType};
|
||||
use crate::types::{IntersectionType, KnownClass, Type, UnionType};
|
||||
use crate::{Db, FxOrderSet};
|
||||
use smallvec::SmallVec;
|
||||
|
||||
@@ -45,6 +45,7 @@ impl<'db> UnionBuilder<'db> {
|
||||
|
||||
/// Adds a type to this union.
|
||||
pub(crate) fn add(mut self, ty: Type<'db>) -> Self {
|
||||
let ty = ty.with_normalized_bools(self.db);
|
||||
match ty {
|
||||
Type::Union(union) => {
|
||||
let new_elements = union.elements(self.db);
|
||||
@@ -55,27 +56,10 @@ impl<'db> UnionBuilder<'db> {
|
||||
}
|
||||
Type::Never => {}
|
||||
_ => {
|
||||
let bool_pair = if let Type::BooleanLiteral(b) = ty {
|
||||
Some(Type::BooleanLiteral(!b))
|
||||
} else {
|
||||
None
|
||||
};
|
||||
|
||||
let mut to_add = ty;
|
||||
let mut to_remove = SmallVec::<[usize; 2]>::new();
|
||||
let ty_negated = ty.negate(self.db);
|
||||
|
||||
for (index, element) in self.elements.iter().enumerate() {
|
||||
if Some(*element) == bool_pair {
|
||||
to_add = KnownClass::Bool.to_instance(self.db);
|
||||
to_remove.push(index);
|
||||
// The type we are adding is a BooleanLiteral, which doesn't have any
|
||||
// subtypes. And we just found that the union already contained our
|
||||
// mirror-image BooleanLiteral, so it can't also contain bool or any
|
||||
// supertype of bool. Therefore, we are done.
|
||||
break;
|
||||
}
|
||||
|
||||
if ty.is_same_gradual_form(*element) || ty.is_subtype_of(self.db, *element) {
|
||||
return self;
|
||||
} else if element.is_subtype_of(self.db, ty) {
|
||||
@@ -94,8 +78,8 @@ impl<'db> UnionBuilder<'db> {
|
||||
}
|
||||
}
|
||||
match to_remove[..] {
|
||||
[] => self.elements.push(to_add),
|
||||
[index] => self.elements[index] = to_add,
|
||||
[] => self.elements.push(ty),
|
||||
[index] => self.elements[index] = ty,
|
||||
_ => {
|
||||
let mut current_index = 0;
|
||||
let mut to_remove = to_remove.into_iter();
|
||||
@@ -110,7 +94,7 @@ impl<'db> UnionBuilder<'db> {
|
||||
current_index += 1;
|
||||
retain
|
||||
});
|
||||
self.elements.push(to_add);
|
||||
self.elements.push(ty);
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -154,6 +138,7 @@ impl<'db> IntersectionBuilder<'db> {
|
||||
}
|
||||
|
||||
pub(crate) fn add_positive(mut self, ty: Type<'db>) -> Self {
|
||||
let ty = ty.with_normalized_bools(self.db);
|
||||
if let Type::Union(union) = ty {
|
||||
// Distribute ourself over this union: for each union element, clone ourself and
|
||||
// intersect with that union element, then create a new union-of-intersections with all
|
||||
@@ -183,6 +168,9 @@ impl<'db> IntersectionBuilder<'db> {
|
||||
|
||||
pub(crate) fn add_negative(mut self, ty: Type<'db>) -> Self {
|
||||
// See comments above in `add_positive`; this is just the negated version.
|
||||
|
||||
let ty = ty.with_normalized_bools(self.db);
|
||||
|
||||
if let Type::Union(union) = ty {
|
||||
for elem in union.elements(self.db) {
|
||||
self = self.add_negative(*elem);
|
||||
@@ -246,7 +234,7 @@ struct InnerIntersectionBuilder<'db> {
|
||||
|
||||
impl<'db> InnerIntersectionBuilder<'db> {
|
||||
/// Adds a positive type to this intersection.
|
||||
fn add_positive(&mut self, db: &'db dyn Db, mut new_positive: Type<'db>) {
|
||||
fn add_positive(&mut self, db: &'db dyn Db, new_positive: Type<'db>) {
|
||||
match new_positive {
|
||||
// `LiteralString & AlwaysTruthy` -> `LiteralString & ~Literal[""]`
|
||||
Type::AlwaysTruthy if self.positive.contains(&Type::LiteralString) => {
|
||||
@@ -293,62 +281,6 @@ impl<'db> InnerIntersectionBuilder<'db> {
|
||||
return;
|
||||
}
|
||||
|
||||
let addition_is_bool_instance = known_instance == Some(KnownClass::Bool);
|
||||
|
||||
for (index, existing_positive) in self.positive.iter().enumerate() {
|
||||
match existing_positive {
|
||||
// `AlwaysTruthy & bool` -> `Literal[True]`
|
||||
Type::AlwaysTruthy if addition_is_bool_instance => {
|
||||
new_positive = Type::BooleanLiteral(true);
|
||||
}
|
||||
// `AlwaysFalsy & bool` -> `Literal[False]`
|
||||
Type::AlwaysFalsy if addition_is_bool_instance => {
|
||||
new_positive = Type::BooleanLiteral(false);
|
||||
}
|
||||
Type::Instance(InstanceType { class })
|
||||
if class.is_known(db, KnownClass::Bool) =>
|
||||
{
|
||||
match new_positive {
|
||||
// `bool & AlwaysTruthy` -> `Literal[True]`
|
||||
Type::AlwaysTruthy => {
|
||||
new_positive = Type::BooleanLiteral(true);
|
||||
}
|
||||
// `bool & AlwaysFalsy` -> `Literal[False]`
|
||||
Type::AlwaysFalsy => {
|
||||
new_positive = Type::BooleanLiteral(false);
|
||||
}
|
||||
_ => continue,
|
||||
}
|
||||
}
|
||||
_ => continue,
|
||||
}
|
||||
self.positive.swap_remove_index(index);
|
||||
break;
|
||||
}
|
||||
|
||||
if addition_is_bool_instance {
|
||||
for (index, existing_negative) in self.negative.iter().enumerate() {
|
||||
match existing_negative {
|
||||
// `bool & ~Literal[False]` -> `Literal[True]`
|
||||
// `bool & ~Literal[True]` -> `Literal[False]`
|
||||
Type::BooleanLiteral(bool_value) => {
|
||||
new_positive = Type::BooleanLiteral(!bool_value);
|
||||
}
|
||||
// `bool & ~AlwaysTruthy` -> `Literal[False]`
|
||||
Type::AlwaysTruthy => {
|
||||
new_positive = Type::BooleanLiteral(false);
|
||||
}
|
||||
// `bool & ~AlwaysFalsy` -> `Literal[True]`
|
||||
Type::AlwaysFalsy => {
|
||||
new_positive = Type::BooleanLiteral(true);
|
||||
}
|
||||
_ => continue,
|
||||
}
|
||||
self.negative.swap_remove_index(index);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
let mut to_remove = SmallVec::<[usize; 1]>::new();
|
||||
for (index, existing_positive) in self.positive.iter().enumerate() {
|
||||
// S & T = S if S <: T
|
||||
@@ -396,14 +328,6 @@ impl<'db> InnerIntersectionBuilder<'db> {
|
||||
|
||||
/// Adds a negative type to this intersection.
|
||||
fn add_negative(&mut self, db: &'db dyn Db, new_negative: Type<'db>) {
|
||||
let contains_bool = || {
|
||||
self.positive
|
||||
.iter()
|
||||
.filter_map(|ty| ty.into_instance())
|
||||
.filter_map(|instance| instance.class.known(db))
|
||||
.any(KnownClass::is_bool)
|
||||
};
|
||||
|
||||
match new_negative {
|
||||
Type::Intersection(inter) => {
|
||||
for pos in inter.positive(db) {
|
||||
@@ -427,20 +351,10 @@ impl<'db> InnerIntersectionBuilder<'db> {
|
||||
// simplify the representation.
|
||||
self.add_positive(db, ty);
|
||||
}
|
||||
// `bool & ~AlwaysTruthy` -> `bool & Literal[False]`
|
||||
// `bool & ~Literal[True]` -> `bool & Literal[False]`
|
||||
Type::AlwaysTruthy | Type::BooleanLiteral(true) if contains_bool() => {
|
||||
self.add_positive(db, Type::BooleanLiteral(false));
|
||||
}
|
||||
// `LiteralString & ~AlwaysTruthy` -> `LiteralString & Literal[""]`
|
||||
Type::AlwaysTruthy if self.positive.contains(&Type::LiteralString) => {
|
||||
self.add_positive(db, Type::string_literal(db, ""));
|
||||
}
|
||||
// `bool & ~AlwaysFalsy` -> `bool & Literal[True]`
|
||||
// `bool & ~Literal[False]` -> `bool & Literal[True]`
|
||||
Type::AlwaysFalsy | Type::BooleanLiteral(false) if contains_bool() => {
|
||||
self.add_positive(db, Type::BooleanLiteral(true));
|
||||
}
|
||||
// `LiteralString & ~AlwaysFalsy` -> `LiteralString & ~Literal[""]`
|
||||
Type::AlwaysFalsy if self.positive.contains(&Type::LiteralString) => {
|
||||
self.add_negative(db, Type::string_literal(db, ""));
|
||||
|
||||
@@ -1,5 +1,6 @@
|
||||
//! Display implementations for types.
|
||||
|
||||
use std::borrow::Cow;
|
||||
use std::fmt::{self, Display, Formatter, Write};
|
||||
|
||||
use ruff_db::display::FormatterJoinExtension;
|
||||
@@ -151,12 +152,31 @@ struct DisplayUnionType<'db> {
|
||||
|
||||
impl Display for DisplayUnionType<'_> {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
|
||||
let elements = self.ty.elements(self.db);
|
||||
let mut elements = Cow::Borrowed(self.ty.elements(self.db));
|
||||
|
||||
if let Some(literal_false_pos) = elements
|
||||
.iter()
|
||||
.position(|ty| matches!(ty, Type::BooleanLiteral(false)))
|
||||
{
|
||||
if let Some(literal_true_pos) = elements
|
||||
.iter()
|
||||
.position(|ty| matches!(ty, Type::BooleanLiteral(true)))
|
||||
{
|
||||
let (min, max) = if literal_false_pos < literal_true_pos {
|
||||
(literal_false_pos, literal_true_pos)
|
||||
} else {
|
||||
(literal_true_pos, literal_false_pos)
|
||||
};
|
||||
let mutable_elements = elements.to_mut();
|
||||
mutable_elements.swap_remove(max);
|
||||
mutable_elements[min] = KnownClass::Bool.to_instance(self.db);
|
||||
}
|
||||
}
|
||||
|
||||
// Group condensed-display types by kind.
|
||||
let mut grouped_condensed_kinds = FxHashMap::default();
|
||||
|
||||
for element in elements {
|
||||
for element in &*elements {
|
||||
if let Ok(kind) = CondensedDisplayTypeKind::try_from(*element) {
|
||||
grouped_condensed_kinds
|
||||
.entry(kind)
|
||||
@@ -167,7 +187,7 @@ impl Display for DisplayUnionType<'_> {
|
||||
|
||||
let mut join = f.join(" | ");
|
||||
|
||||
for element in elements {
|
||||
for element in &*elements {
|
||||
if let Ok(kind) = CondensedDisplayTypeKind::try_from(*element) {
|
||||
let Some(condensed_kind) = grouped_condensed_kinds.remove(&kind) else {
|
||||
continue;
|
||||
|
||||
@@ -328,8 +328,9 @@ fn union<'db>(db: &'db TestDb, tys: impl IntoIterator<Item = Type<'db>>) -> Type
|
||||
}
|
||||
|
||||
mod stable {
|
||||
use super::union;
|
||||
use super::{intersection, union};
|
||||
use crate::types::{KnownClass, Type};
|
||||
use itertools::Itertools;
|
||||
|
||||
// Reflexivity: `T` is equivalent to itself.
|
||||
type_property_test!(
|
||||
@@ -474,6 +475,32 @@ mod stable {
|
||||
all_type_pairs_are_assignable_to_their_union, db,
|
||||
forall types s, t. s.is_assignable_to(db, union(db, [s, t])) && t.is_assignable_to(db, union(db, [s, t]))
|
||||
);
|
||||
|
||||
// Equal element sets of intersections implies equivalence
|
||||
type_property_test!(
|
||||
intersection_equivalence_not_order_dependent, db,
|
||||
forall types s, t, u.
|
||||
s.is_fully_static(db) && t.is_fully_static(db) && u.is_fully_static(db)
|
||||
=> [s, t, u]
|
||||
.into_iter()
|
||||
.permutations(3)
|
||||
.map(|trio_of_types| intersection(db, trio_of_types))
|
||||
.permutations(2)
|
||||
.all(|vec_of_intersections| vec_of_intersections[0].is_equivalent_to(db, vec_of_intersections[1]))
|
||||
);
|
||||
|
||||
// Equal element sets of unions implies equivalence
|
||||
type_property_test!(
|
||||
union_equivalence_not_order_dependent, db,
|
||||
forall types s, t, u.
|
||||
s.is_fully_static(db) && t.is_fully_static(db) && u.is_fully_static(db)
|
||||
=> [s, t, u]
|
||||
.into_iter()
|
||||
.permutations(3)
|
||||
.map(|trio_of_types| union(db, trio_of_types))
|
||||
.permutations(2)
|
||||
.all(|vec_of_unions| vec_of_unions[0].is_equivalent_to(db, vec_of_unions[1]))
|
||||
);
|
||||
}
|
||||
|
||||
/// This module contains property tests that currently lead to many false positives.
|
||||
@@ -484,8 +511,6 @@ mod stable {
|
||||
/// tests to the `stable` section. In the meantime, it can still be useful to run these
|
||||
/// tests (using [`types::property_tests::flaky`]), to see if there are any new obvious bugs.
|
||||
mod flaky {
|
||||
use itertools::Itertools;
|
||||
|
||||
use super::{intersection, union};
|
||||
|
||||
// Negating `T` twice is equivalent to `T`.
|
||||
@@ -522,34 +547,6 @@ mod flaky {
|
||||
forall types s, t. intersection(db, [s, t]).is_assignable_to(db, s) && intersection(db, [s, t]).is_assignable_to(db, t)
|
||||
);
|
||||
|
||||
// Equal element sets of intersections implies equivalence
|
||||
// flaky at least in part because of https://github.com/astral-sh/ruff/issues/15513
|
||||
type_property_test!(
|
||||
intersection_equivalence_not_order_dependent, db,
|
||||
forall types s, t, u.
|
||||
s.is_fully_static(db) && t.is_fully_static(db) && u.is_fully_static(db)
|
||||
=> [s, t, u]
|
||||
.into_iter()
|
||||
.permutations(3)
|
||||
.map(|trio_of_types| intersection(db, trio_of_types))
|
||||
.permutations(2)
|
||||
.all(|vec_of_intersections| vec_of_intersections[0].is_equivalent_to(db, vec_of_intersections[1]))
|
||||
);
|
||||
|
||||
// Equal element sets of unions implies equivalence
|
||||
// flaky at laest in part because of https://github.com/astral-sh/ruff/issues/15513
|
||||
type_property_test!(
|
||||
union_equivalence_not_order_dependent, db,
|
||||
forall types s, t, u.
|
||||
s.is_fully_static(db) && t.is_fully_static(db) && u.is_fully_static(db)
|
||||
=> [s, t, u]
|
||||
.into_iter()
|
||||
.permutations(3)
|
||||
.map(|trio_of_types| union(db, trio_of_types))
|
||||
.permutations(2)
|
||||
.all(|vec_of_unions| vec_of_unions[0].is_equivalent_to(db, vec_of_unions[1]))
|
||||
);
|
||||
|
||||
// `S | T` is always a supertype of `S`.
|
||||
// Thus, `S` is never disjoint from `S | T`.
|
||||
type_property_test!(
|
||||
|
||||
Reference in New Issue
Block a user