Skip to content
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.

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

[red knot] add Type::is_disjoint_from and intersection simplifications #13775

Merged
merged 38 commits into from
Oct 18, 2024
Merged
Show file tree
Hide file tree
Changes from 37 commits
Commits
Show all changes
38 commits
Select commit Hold shift + click to select a range
81157e0
[red-knot] intersection type simplifications
sharkdp Oct 16, 2024
14dee2e
clean up
sharkdp Oct 16, 2024
e06687c
Handle more cases in disjoint_from
sharkdp Oct 16, 2024
5770be6
Handle tuples, intersections
sharkdp Oct 16, 2024
ccb9b1f
Remove commented-out code
sharkdp Oct 16, 2024
d0063ed
Fix tuples
sharkdp Oct 16, 2024
0f9ba92
Fix TODO
sharkdp Oct 16, 2024
68eae7f
Minor improvements
sharkdp Oct 16, 2024
68ab56e
Add new simplification
sharkdp Oct 16, 2024
4b95c65
Add simplification for bools
sharkdp Oct 16, 2024
1917618
Add rule for S & T = S
sharkdp Oct 17, 2024
8d78019
Remove/reduce simplify
sharkdp Oct 17, 2024
1737dd8
Additional rules
sharkdp Oct 17, 2024
98df522
Mirror version of the bool rule
sharkdp Oct 17, 2024
2bd1789
Handle more cases in disjoint_from
sharkdp Oct 17, 2024
8ff474f
Remove TODO
sharkdp Oct 17, 2024
6370969
Improve test coverage
sharkdp Oct 17, 2024
efe64d8
Change test name
sharkdp Oct 17, 2024
bf4af40
Fix instance checks
sharkdp Oct 17, 2024
5dd8ab5
Use matches!(…) for instance checks
sharkdp Oct 17, 2024
08cc4ba
Flatten nested match statements
sharkdp Oct 17, 2024
76787c8
Use Iterator::find
sharkdp Oct 18, 2024
e242909
Fix is_disjoint_from(tuple, other)
sharkdp Oct 18, 2024
28f7b46
Handle None, BooleanLiteral, IntLiteral, StringLiteral, BytesLiteral …
sharkdp Oct 18, 2024
06ecd88
Handle None in a more general way
sharkdp Oct 18, 2024
57b6949
Same for (Boolean|Int|String|Bytes)Literal
sharkdp Oct 18, 2024
599c9d6
Add test for BytesLiteral vs StringLiteral
sharkdp Oct 18, 2024
7992f1d
Add TODO comment
sharkdp Oct 18, 2024
ebd4b6e
Use test_cases instead of loop
sharkdp Oct 18, 2024
8d0ff15
Fix TODO regarding Any/Unknown/Todo
sharkdp Oct 18, 2024
3282c0c
Fix comment regarding tuples
sharkdp Oct 18, 2024
1b66358
Add support for removing multiple elements in one go
sharkdp Oct 18, 2024
9eddcbe
Add 'object' as a third type to the boolean simplification tests
sharkdp Oct 18, 2024
e0cfef4
Add 'third' type to simplification unit tests
sharkdp Oct 18, 2024
34b0383
Fix is_disjoint for function/class/module
sharkdp Oct 18, 2024
eaa3d48
Add test for union of class types
sharkdp Oct 18, 2024
3d4bd52
Add TODO comment regarding KnownClass::Type
sharkdp Oct 18, 2024
b3b0ffb
bool and int are not disjoint
carljm Oct 18, 2024
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
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,7 @@
x = None if flag else 1

if x is None:
# TODO the following should be simplified to 'None'
reveal_type(x) # revealed: None | Literal[1] & None
reveal_type(x) # revealed: None
carljm marked this conversation as resolved.
Show resolved Hide resolved

reveal_type(x) # revealed: None | Literal[1]
```
Expand All @@ -22,8 +21,7 @@ x = A()
y = x if flag else None

if y is x:
# TODO the following should be simplified to 'A'
reveal_type(y) # revealed: A | None & A
reveal_type(y) # revealed: A

reveal_type(y) # revealed: A | None
```
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,7 @@ x = True if flag else False
reveal_type(x) # revealed: bool

if x is not False:
# TODO the following should be `Literal[True]`
reveal_type(x) # revealed: bool & ~Literal[False]
reveal_type(x) # revealed: Literal[True]
```

## `is not` for non-singleton types
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,5 @@ match x:
case None:
y = x

# TODO intersection simplification: should be just Literal[0] | None
reveal_type(y) # revealed: Literal[0] | None | Literal[1] & None
reveal_type(y) # revealed: Literal[0] | None
```
244 changes: 242 additions & 2 deletions crates/red_knot_python_semantic/src/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -471,6 +471,150 @@ impl<'db> Type<'db> {
self == other
}

/// Return true if this type and `other` have no common elements.
///
/// Note: This function aims to have no false positives, but might return
/// wrong `false` answers in some cases.
pub(crate) fn is_disjoint_from(self, db: &'db dyn Db, other: Type<'db>) -> bool {
match (self, other) {
sharkdp marked this conversation as resolved.
Show resolved Hide resolved
carljm marked this conversation as resolved.
Show resolved Hide resolved
(Type::Never, _) | (_, Type::Never) => true,

(Type::Any, _) | (_, Type::Any) => false,
(Type::Unknown, _) | (_, Type::Unknown) => false,
(Type::Unbound, _) | (_, Type::Unbound) => false,
(Type::Todo, _) | (_, Type::Todo) => false,

(Type::Union(union), other) | (other, Type::Union(union)) => union
.elements(db)
.iter()
.all(|e| e.is_disjoint_from(db, other)),

(Type::Intersection(intersection), other)
| (other, Type::Intersection(intersection)) => {
if intersection
.positive(db)
.iter()
.any(|p| p.is_disjoint_from(db, other))
{
true
} else {
// TODO we can do better here. For example:
// X & ~Literal[1] is disjoint from Literal[1]
false
}
}

(
left @ (Type::None
| Type::BooleanLiteral(..)
| Type::IntLiteral(..)
| Type::StringLiteral(..)
| Type::BytesLiteral(..)
| Type::Function(..)
| Type::Module(..)
| Type::Class(..)),
right @ (Type::None
| Type::BooleanLiteral(..)
| Type::IntLiteral(..)
| Type::StringLiteral(..)
| Type::BytesLiteral(..)
| Type::Function(..)
| Type::Module(..)
| Type::Class(..)),
) => left != right,

(Type::None, Type::Instance(class_type)) | (Type::Instance(class_type), Type::None) => {
!matches!(
class_type.known(db),
Some(KnownClass::NoneType | KnownClass::Object)
)
}
sharkdp marked this conversation as resolved.
Show resolved Hide resolved
(Type::None, _) | (_, Type::None) => true,

(Type::BooleanLiteral(..), Type::Instance(class_type))
| (Type::Instance(class_type), Type::BooleanLiteral(..)) => !matches!(
class_type.known(db),
Some(KnownClass::Bool | KnownClass::Object)
Copy link
Contributor

@carljm carljm Oct 18, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because bool is a subtype of int in Python (sadly), we must also include KnownClass::Int here.

There was already a test for this case, but it asserted wrongly that int and a BooleanLiteral were disjoint; I switched it to assert the opposite.

There was also an IntersectionBuilder test relying on this assumption of bool/int disjointness; I fixed it by using a StringLiteral instead of a BooleanLiteral.

),
sharkdp marked this conversation as resolved.
Show resolved Hide resolved
(Type::BooleanLiteral(..), _) | (_, Type::BooleanLiteral(..)) => true,

(Type::IntLiteral(..), Type::Instance(class_type))
| (Type::Instance(class_type), Type::IntLiteral(..)) => !matches!(
class_type.known(db),
Some(KnownClass::Int | KnownClass::Object)
),
sharkdp marked this conversation as resolved.
Show resolved Hide resolved
(Type::IntLiteral(..), _) | (_, Type::IntLiteral(..)) => true,

(Type::StringLiteral(..), Type::LiteralString)
| (Type::LiteralString, Type::StringLiteral(..)) => false,
sharkdp marked this conversation as resolved.
Show resolved Hide resolved
(Type::StringLiteral(..), Type::Instance(class_type))
| (Type::Instance(class_type), Type::StringLiteral(..)) => !matches!(
class_type.known(db),
Some(KnownClass::Str | KnownClass::Object)
),
sharkdp marked this conversation as resolved.
Show resolved Hide resolved
(Type::StringLiteral(..), _) | (_, Type::StringLiteral(..)) => true,

(Type::LiteralString, Type::LiteralString) => false,
sharkdp marked this conversation as resolved.
Show resolved Hide resolved
(Type::LiteralString, Type::Instance(class_type))
| (Type::Instance(class_type), Type::LiteralString) => !matches!(
class_type.known(db),
Some(KnownClass::Str | KnownClass::Object)
),
sharkdp marked this conversation as resolved.
Show resolved Hide resolved
(Type::LiteralString, _) | (_, Type::LiteralString) => true,

(Type::BytesLiteral(..), Type::Instance(class_type))
| (Type::Instance(class_type), Type::BytesLiteral(..)) => !matches!(
class_type.known(db),
Some(KnownClass::Bytes | KnownClass::Object)
),
(Type::BytesLiteral(..), _) | (_, Type::BytesLiteral(..)) => true,

(
Type::Function(..) | Type::Module(..) | Type::Class(..),
Type::Instance(class_type),
)
| (
Type::Instance(class_type),
Type::Function(..) | Type::Module(..) | Type::Class(..),
) => !class_type.is_known(db, KnownClass::Object),

(Type::Instance(..), Type::Instance(..)) => {
// TODO: once we have support for `final`, there might be some cases where
// we can determine that two types are disjoint. For non-final classes, we
// return false (multiple inheritance).

// TODO: is there anything specific to do for instances of KnownClass::Type?

false
}

(Type::Tuple(tuple), other) | (other, Type::Tuple(tuple)) => {
if let Type::Tuple(other_tuple) = other {
if tuple.len(db) == other_tuple.len(db) {
tuple
.elements(db)
.iter()
.zip(other_tuple.elements(db).iter())
.any(|(e1, e2)| e1.is_disjoint_from(db, *e2))
} else {
true
}
} else {
// We can not be sure if the tuple is disjoint from 'other' because:
// - 'other' might be the homogeneous arbitrary-length tuple type
// tuple[T, ...] (which we don't have support for yet); if all of
// our element types are not disjoint with T, this is not disjoint
// - 'other' might be a user subtype of tuple, which, if generic
// over the same or compatible *Ts, would overlap with tuple.
//
// TODO: add checks for the above cases once we support them

false
}
}
}
}

/// Return true if there is just a single inhabitant for this type.
///
/// Note: This function aims to have no false positives, but might return `false`
Expand Down Expand Up @@ -1548,8 +1692,8 @@ impl<'db> TupleType<'db> {
#[cfg(test)]
mod tests {
use super::{
builtins_symbol_ty, BytesLiteralType, StringLiteralType, Truthiness, TupleType, Type,
UnionType,
builtins_symbol_ty, BytesLiteralType, IntersectionBuilder, StringLiteralType, Truthiness,
TupleType, Type, UnionType,
};
use crate::db::tests::TestDb;
use crate::program::{Program, SearchPathSettings};
Expand Down Expand Up @@ -1593,6 +1737,7 @@ mod tests {
BytesLiteral(&'static str),
BuiltinInstance(&'static str),
Union(Vec<Ty>),
Intersection { pos: Vec<Ty>, neg: Vec<Ty> },
Tuple(Vec<Ty>),
}

Expand All @@ -1612,6 +1757,16 @@ mod tests {
Ty::Union(tys) => {
UnionType::from_elements(db, tys.into_iter().map(|ty| ty.into_type(db)))
}
Ty::Intersection { pos, neg } => {
let mut builder = IntersectionBuilder::new(db);
for p in pos {
builder = builder.add_positive(p.into_type(db));
}
for n in neg {
builder = builder.add_negative(n.into_type(db));
}
builder.build()
}
Ty::Tuple(tys) => {
let elements: Box<_> = tys.into_iter().map(|ty| ty.into_type(db)).collect();
Type::Tuple(TupleType::new(db, elements))
Expand Down Expand Up @@ -1687,6 +1842,91 @@ mod tests {
assert!(from.into_type(&db).is_equivalent_to(&db, to.into_type(&db)));
}

#[test_case(Ty::Never, Ty::Never)]
#[test_case(Ty::Never, Ty::None)]
#[test_case(Ty::Never, Ty::BuiltinInstance("int"))]
#[test_case(Ty::None, Ty::BoolLiteral(true))]
#[test_case(Ty::None, Ty::IntLiteral(1))]
#[test_case(Ty::None, Ty::StringLiteral("test"))]
#[test_case(Ty::None, Ty::BytesLiteral("test"))]
#[test_case(Ty::None, Ty::LiteralString)]
#[test_case(Ty::None, Ty::BuiltinInstance("int"))]
#[test_case(Ty::None, Ty::Tuple(vec![Ty::None]))]
#[test_case(Ty::BoolLiteral(true), Ty::BuiltinInstance("int"))]
#[test_case(Ty::BoolLiteral(true), Ty::BoolLiteral(false))]
#[test_case(Ty::BoolLiteral(true), Ty::Tuple(vec![Ty::None]))]
#[test_case(Ty::IntLiteral(1), Ty::IntLiteral(2))]
#[test_case(Ty::IntLiteral(1), Ty::Tuple(vec![Ty::None]))]
#[test_case(Ty::StringLiteral("a"), Ty::StringLiteral("b"))]
#[test_case(Ty::StringLiteral("a"), Ty::Tuple(vec![Ty::None]))]
#[test_case(Ty::LiteralString, Ty::BytesLiteral("a"))]
#[test_case(Ty::BytesLiteral("a"), Ty::BytesLiteral("b"))]
#[test_case(Ty::BytesLiteral("a"), Ty::Tuple(vec![Ty::None]))]
#[test_case(Ty::BytesLiteral("a"), Ty::StringLiteral("a"))]
#[test_case(Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::IntLiteral(3))]
#[test_case(Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::Union(vec![Ty::IntLiteral(3), Ty::IntLiteral(4)]))]
#[test_case(Ty::Intersection{pos: vec![Ty::BuiltinInstance("int"), Ty::IntLiteral(1)], neg: vec![]}, Ty::IntLiteral(2))]
#[test_case(Ty::Tuple(vec![Ty::IntLiteral(1)]), Ty::Tuple(vec![Ty::IntLiteral(2)]))]
#[test_case(Ty::Tuple(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::Tuple(vec![Ty::IntLiteral(1)]))]
#[test_case(Ty::Tuple(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::Tuple(vec![Ty::IntLiteral(1), Ty::IntLiteral(3)]))]
fn is_disjoint_from(a: Ty, b: Ty) {
let db = setup_db();
let a = a.into_type(&db);
let b = b.into_type(&db);

assert!(a.is_disjoint_from(&db, b));
assert!(b.is_disjoint_from(&db, a));
}

#[test_case(Ty::Any, Ty::BuiltinInstance("int"))]
#[test_case(Ty::None, Ty::None)]
#[test_case(Ty::None, Ty::BuiltinInstance("object"))]
#[test_case(Ty::BuiltinInstance("int"), Ty::BuiltinInstance("int"))]
#[test_case(Ty::BuiltinInstance("str"), Ty::LiteralString)]
#[test_case(Ty::BoolLiteral(true), Ty::BoolLiteral(true))]
#[test_case(Ty::BoolLiteral(false), Ty::BoolLiteral(false))]
#[test_case(Ty::BoolLiteral(true), Ty::BuiltinInstance("bool"))]
#[test_case(Ty::IntLiteral(1), Ty::IntLiteral(1))]
#[test_case(Ty::StringLiteral("a"), Ty::StringLiteral("a"))]
#[test_case(Ty::StringLiteral("a"), Ty::LiteralString)]
#[test_case(Ty::StringLiteral("a"), Ty::BuiltinInstance("str"))]
#[test_case(Ty::LiteralString, Ty::LiteralString)]
#[test_case(Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::IntLiteral(2))]
#[test_case(Ty::Union(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::Union(vec![Ty::IntLiteral(2), Ty::IntLiteral(3)]))]
#[test_case(Ty::Intersection{pos: vec![Ty::BuiltinInstance("int"), Ty::IntLiteral(2)], neg: vec![]}, Ty::IntLiteral(2))]
#[test_case(Ty::Tuple(vec![Ty::IntLiteral(1), Ty::IntLiteral(2)]), Ty::Tuple(vec![Ty::IntLiteral(1), Ty::BuiltinInstance("int")]))]
fn is_not_disjoint_from(a: Ty, b: Ty) {
let db = setup_db();
let a = a.into_type(&db);
let b = b.into_type(&db);

assert!(!a.is_disjoint_from(&db, b));
assert!(!b.is_disjoint_from(&db, a));
}

#[test]
fn is_disjoint_from_union_of_class_types() {
let mut db = setup_db();
db.write_dedented(
"/src/module.py",
"
class A: ...
class B: ...
x = A if flag else B
",
)
.unwrap();
let module = ruff_db::files::system_path_to_file(&db, "/src/module.py").unwrap();

let type_a = super::global_symbol_ty(&db, module, "A");
let type_x = super::global_symbol_ty(&db, module, "x");

assert!(matches!(type_a, Type::Class(_)));
assert!(matches!(type_x, Type::Union(_)));

assert!(!type_a.is_disjoint_from(&db, type_x));
}

#[test_case(Ty::None)]
#[test_case(Ty::BoolLiteral(true))]
#[test_case(Ty::BoolLiteral(false))]
Expand Down
Loading
Loading