Compare commits
5 Commits
david/allo
...
alex/truth
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
1ef2f73820 | ||
|
|
91784bbe93 | ||
|
|
80136d81f6 | ||
|
|
2851098c36 | ||
|
|
84fdb04049 |
@@ -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]
|
||||
|
||||
@@ -11,37 +11,37 @@ x = foo()
|
||||
if x:
|
||||
reveal_type(x) # revealed: Literal[-1, True, "foo", b"bar"]
|
||||
else:
|
||||
reveal_type(x) # revealed: Literal[0, False, "", b""] | None | tuple[()]
|
||||
reveal_type(x) # revealed: Literal[0, False, "", b""] | tuple[()] | None
|
||||
|
||||
if not x:
|
||||
reveal_type(x) # revealed: Literal[0, False, "", b""] | None | tuple[()]
|
||||
reveal_type(x) # revealed: Literal[0, False, "", b""] | tuple[()] | None
|
||||
else:
|
||||
reveal_type(x) # revealed: Literal[-1, True, "foo", b"bar"]
|
||||
|
||||
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, b"bar", "", "foo", b""] | 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, b"bar", "", "foo", b""] | 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, b"bar", "", "foo", b""] | 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, b"bar", "", "foo", b""] | bool | tuple[()] | None
|
||||
|
||||
if (isinstance(x, int) or isinstance(x, str)) and x:
|
||||
reveal_type(x) # revealed: Literal[-1, True, "foo"]
|
||||
else:
|
||||
reveal_type(x) # revealed: Literal[b"", b"bar", 0, False, ""] | None | tuple[()]
|
||||
reveal_type(x) # revealed: tuple[()] | None | Literal[b"", b"bar", 0, False, ""]
|
||||
```
|
||||
|
||||
## Function Literals
|
||||
|
||||
@@ -346,4 +346,24 @@ 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))
|
||||
```
|
||||
|
||||
### `bool` is assignable to `AlwaysTruthy | AlwaysFalsy`
|
||||
|
||||
```py
|
||||
from knot_extensions import static_assert, is_assignable_to, AlwaysTruthy, AlwaysFalsy
|
||||
|
||||
static_assert(is_assignable_to(bool, AlwaysTruthy | AlwaysFalsy))
|
||||
```
|
||||
|
||||
[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
|
||||
|
||||
@@ -881,6 +881,15 @@ impl<'db> Type<'db> {
|
||||
(Type::Never, _) => true,
|
||||
(_, Type::Never) => false,
|
||||
|
||||
(Type::Instance(InstanceType { class }), _) if class.is_known(db, KnownClass::Bool) => {
|
||||
Type::BooleanLiteral(true).is_subtype_of(db, target)
|
||||
&& Type::BooleanLiteral(false).is_subtype_of(db, target)
|
||||
}
|
||||
(_, Type::Instance(InstanceType { class })) if class.is_known(db, KnownClass::Bool) => {
|
||||
self.is_subtype_of(db, Type::BooleanLiteral(true))
|
||||
|| self.is_subtype_of(db, Type::BooleanLiteral(false))
|
||||
}
|
||||
|
||||
(Type::Union(union), _) => union
|
||||
.elements(db)
|
||||
.iter()
|
||||
@@ -961,7 +970,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(_), _) => {
|
||||
@@ -1077,6 +1086,7 @@ impl<'db> Type<'db> {
|
||||
if self.is_gradual_equivalent_to(db, target) {
|
||||
return true;
|
||||
}
|
||||
|
||||
match (self, target) {
|
||||
// Never can be assigned to any type.
|
||||
(Type::Never, _) => true,
|
||||
@@ -1093,6 +1103,15 @@ impl<'db> Type<'db> {
|
||||
true
|
||||
}
|
||||
|
||||
(Type::Instance(InstanceType { class }), _) if class.is_known(db, KnownClass::Bool) => {
|
||||
Type::BooleanLiteral(true).is_assignable_to(db, target)
|
||||
&& Type::BooleanLiteral(false).is_assignable_to(db, target)
|
||||
}
|
||||
(_, Type::Instance(InstanceType { class })) if class.is_known(db, KnownClass::Bool) => {
|
||||
self.is_assignable_to(db, Type::BooleanLiteral(false))
|
||||
|| self.is_assignable_to(db, Type::BooleanLiteral(true))
|
||||
}
|
||||
|
||||
// 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)
|
||||
|
||||
@@ -33,6 +33,7 @@ use smallvec::SmallVec;
|
||||
pub(crate) struct UnionBuilder<'db> {
|
||||
elements: Vec<Type<'db>>,
|
||||
db: &'db dyn Db,
|
||||
bool_literals_present: BoolLiteralsPresent,
|
||||
}
|
||||
|
||||
impl<'db> UnionBuilder<'db> {
|
||||
@@ -40,6 +41,7 @@ impl<'db> UnionBuilder<'db> {
|
||||
Self {
|
||||
db,
|
||||
elements: vec![],
|
||||
bool_literals_present: BoolLiteralsPresent::Zero,
|
||||
}
|
||||
}
|
||||
|
||||
@@ -54,28 +56,16 @@ impl<'db> UnionBuilder<'db> {
|
||||
}
|
||||
}
|
||||
Type::Never => {}
|
||||
Type::Instance(InstanceType { class }) if class.is_known(self.db, KnownClass::Bool) => {
|
||||
self = self
|
||||
.add(Type::BooleanLiteral(false))
|
||||
.add(Type::BooleanLiteral(true));
|
||||
}
|
||||
_ => {
|
||||
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) {
|
||||
@@ -93,9 +83,14 @@ impl<'db> UnionBuilder<'db> {
|
||||
return self;
|
||||
}
|
||||
}
|
||||
|
||||
if ty.is_boolean_literal() {
|
||||
self.bool_literals_present.increment();
|
||||
}
|
||||
|
||||
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 +105,7 @@ impl<'db> UnionBuilder<'db> {
|
||||
current_index += 1;
|
||||
retain
|
||||
});
|
||||
self.elements.push(to_add);
|
||||
self.elements.push(ty);
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -119,14 +114,56 @@ impl<'db> UnionBuilder<'db> {
|
||||
}
|
||||
|
||||
pub(crate) fn build(self) -> Type<'db> {
|
||||
match self.elements.len() {
|
||||
let UnionBuilder {
|
||||
mut elements,
|
||||
db,
|
||||
bool_literals_present,
|
||||
} = self;
|
||||
|
||||
match elements.len() {
|
||||
0 => Type::Never,
|
||||
1 => self.elements[0],
|
||||
_ => Type::Union(UnionType::new(self.db, self.elements.into_boxed_slice())),
|
||||
1 => elements[0],
|
||||
_ => {
|
||||
if bool_literals_present.is_two() {
|
||||
let mut element_iter = elements.iter();
|
||||
if let Some(first_pos) = element_iter.position(Type::is_boolean_literal) {
|
||||
if let Some(second_pos) = element_iter.position(Type::is_boolean_literal) {
|
||||
let bool_instance = KnownClass::Bool.to_instance(db);
|
||||
if elements.len() == 2 {
|
||||
return bool_instance;
|
||||
}
|
||||
elements.swap_remove(first_pos + second_pos + 1);
|
||||
elements[first_pos] = bool_instance;
|
||||
}
|
||||
}
|
||||
}
|
||||
Type::Union(UnionType::new(db, elements.into_boxed_slice()))
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Debug, Copy, Clone, PartialEq, Eq)]
|
||||
enum BoolLiteralsPresent {
|
||||
Zero,
|
||||
One,
|
||||
Two,
|
||||
}
|
||||
|
||||
impl BoolLiteralsPresent {
|
||||
fn increment(&mut self) {
|
||||
*self = match self {
|
||||
BoolLiteralsPresent::Zero => BoolLiteralsPresent::One,
|
||||
BoolLiteralsPresent::One => BoolLiteralsPresent::Two,
|
||||
BoolLiteralsPresent::Two => BoolLiteralsPresent::Two,
|
||||
};
|
||||
}
|
||||
|
||||
const fn is_two(self) -> bool {
|
||||
matches!(self, BoolLiteralsPresent::Two)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
pub(crate) struct IntersectionBuilder<'db> {
|
||||
// Really this builds a union-of-intersections, because we always keep our set-theoretic types
|
||||
@@ -154,7 +191,18 @@ impl<'db> IntersectionBuilder<'db> {
|
||||
}
|
||||
|
||||
pub(crate) fn add_positive(mut self, ty: Type<'db>) -> Self {
|
||||
if let Type::Union(union) = ty {
|
||||
const BOOL_LITERALS: &[Type] = &[Type::BooleanLiteral(false), Type::BooleanLiteral(true)];
|
||||
|
||||
// Treat `bool` as `Literal[True] | Literal[False]`
|
||||
let union_elements = match ty {
|
||||
Type::Union(union) => Some(union.elements(self.db)),
|
||||
Type::Instance(InstanceType { class }) if class.is_known(self.db, KnownClass::Bool) => {
|
||||
Some(BOOL_LITERALS)
|
||||
}
|
||||
_ => None,
|
||||
};
|
||||
|
||||
if let Some(elements) = union_elements {
|
||||
// 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
|
||||
// of those sub-intersections in it. E.g. if `self` is a simple intersection `T1 & T2`
|
||||
@@ -163,8 +211,7 @@ impl<'db> IntersectionBuilder<'db> {
|
||||
// (T2 & T4)`. If `self` is already a union-of-intersections `(T1 & T2) | (T3 & T4)`
|
||||
// and we add `T5 | T6` to it, that flattens all the way out to `(T1 & T2 & T5) | (T1 &
|
||||
// T2 & T6) | (T3 & T4 & T5) ...` -- you get the idea.
|
||||
union
|
||||
.elements(self.db)
|
||||
elements
|
||||
.iter()
|
||||
.map(|elem| self.clone().add_positive(*elem))
|
||||
.fold(IntersectionBuilder::empty(self.db), |mut builder, sub| {
|
||||
@@ -183,43 +230,52 @@ 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.
|
||||
if let Type::Union(union) = ty {
|
||||
for elem in union.elements(self.db) {
|
||||
self = self.add_negative(*elem);
|
||||
|
||||
match ty {
|
||||
Type::Union(union) => {
|
||||
for elem in union.elements(self.db) {
|
||||
self = self.add_negative(*elem);
|
||||
}
|
||||
self
|
||||
}
|
||||
self
|
||||
} else if let Type::Intersection(intersection) = ty {
|
||||
// (A | B) & ~(C & ~D)
|
||||
// -> (A | B) & (~C | D)
|
||||
// -> ((A | B) & ~C) | ((A | B) & D)
|
||||
// i.e. if we have an intersection of positive constraints C
|
||||
// and negative constraints D, then our new intersection
|
||||
// is (existing & ~C) | (existing & D)
|
||||
|
||||
let positive_side = intersection
|
||||
.positive(self.db)
|
||||
.iter()
|
||||
// we negate all the positive constraints while distributing
|
||||
.map(|elem| self.clone().add_negative(*elem));
|
||||
|
||||
let negative_side = intersection
|
||||
.negative(self.db)
|
||||
.iter()
|
||||
// all negative constraints end up becoming positive constraints
|
||||
.map(|elem| self.clone().add_positive(*elem));
|
||||
|
||||
positive_side.chain(negative_side).fold(
|
||||
IntersectionBuilder::empty(self.db),
|
||||
|mut builder, sub| {
|
||||
builder.intersections.extend(sub.intersections);
|
||||
builder
|
||||
},
|
||||
)
|
||||
} else {
|
||||
for inner in &mut self.intersections {
|
||||
inner.add_negative(self.db, ty);
|
||||
Type::Instance(InstanceType { class }) if class.is_known(self.db, KnownClass::Bool) => {
|
||||
self.add_negative(Type::BooleanLiteral(false))
|
||||
.add_negative(Type::BooleanLiteral(true))
|
||||
}
|
||||
Type::Intersection(intersection) => {
|
||||
// (A | B) & ~(C & ~D)
|
||||
// -> (A | B) & (~C | D)
|
||||
// -> ((A | B) & ~C) | ((A | B) & D)
|
||||
// i.e. if we have an intersection of positive constraints C
|
||||
// and negative constraints D, then our new intersection
|
||||
// is (existing & ~C) | (existing & D)
|
||||
|
||||
let positive_side = intersection
|
||||
.positive(self.db)
|
||||
.iter()
|
||||
// we negate all the positive constraints while distributing
|
||||
.map(|elem| self.clone().add_negative(*elem));
|
||||
|
||||
let negative_side = intersection
|
||||
.negative(self.db)
|
||||
.iter()
|
||||
// all negative constraints end up becoming positive constraints
|
||||
.map(|elem| self.clone().add_positive(*elem));
|
||||
|
||||
positive_side.chain(negative_side).fold(
|
||||
IntersectionBuilder::empty(self.db),
|
||||
|mut builder, sub| {
|
||||
builder.intersections.extend(sub.intersections);
|
||||
builder
|
||||
},
|
||||
)
|
||||
}
|
||||
_ => {
|
||||
for inner in &mut self.intersections {
|
||||
inner.add_negative(self.db, ty);
|
||||
}
|
||||
self
|
||||
}
|
||||
self
|
||||
}
|
||||
}
|
||||
|
||||
@@ -246,7 +302,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 +349,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 +396,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 +419,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, ""));
|
||||
|
||||
@@ -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