From 9d845ec8f585ecd61964c8bfa45440e237423f8a Mon Sep 17 00:00:00 2001 From: InSync Date: Sat, 18 Jan 2025 07:48:01 +0700 Subject: [PATCH] [red-knot] Migrate `is_gradual_equivalent_to` unit tests to Markdown tests (#15563) ## Summary Part of #15397 and #15516. ## Test Plan Markdown tests. --- .../is_gradual_equivalent_to.md | 66 ++++++++++++ crates/red_knot_python_semantic/src/types.rs | 101 +++--------------- .../src/types/property_tests.rs | 13 +++ .../knot_extensions/knot_extensions.pyi | 1 + 4 files changed, 95 insertions(+), 86 deletions(-) create mode 100644 crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md diff --git a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md new file mode 100644 index 0000000000..e215033a83 --- /dev/null +++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_gradual_equivalent_to.md @@ -0,0 +1,66 @@ +# Gradual equivalence relation + +Two gradual types `A` and `B` are equivalent if all [materializations] of `A` are also +materializations of `B`, and all materializations of `B` are also materializations of `A`. + +## Basic + +```py +from typing import Any +from typing_extensions import Literal, LiteralString, Never +from knot_extensions import AlwaysFalsy, AlwaysTruthy, TypeOf, Unknown, is_gradual_equivalent_to, static_assert + +static_assert(is_gradual_equivalent_to(Any, Any)) +static_assert(is_gradual_equivalent_to(Unknown, Unknown)) +static_assert(is_gradual_equivalent_to(Any, Unknown)) + +static_assert(is_gradual_equivalent_to(Never, Never)) +static_assert(is_gradual_equivalent_to(AlwaysTruthy, AlwaysTruthy)) +static_assert(is_gradual_equivalent_to(AlwaysFalsy, AlwaysFalsy)) +static_assert(is_gradual_equivalent_to(LiteralString, LiteralString)) + +static_assert(is_gradual_equivalent_to(Literal[True], Literal[True])) +static_assert(is_gradual_equivalent_to(Literal[False], Literal[False])) +static_assert(is_gradual_equivalent_to(TypeOf[0:1:2], TypeOf[0:1:2])) + +static_assert(is_gradual_equivalent_to(TypeOf[str], TypeOf[str])) +static_assert(is_gradual_equivalent_to(type, type[object])) + +static_assert(not is_gradual_equivalent_to(type, type[Any])) +static_assert(not is_gradual_equivalent_to(type[object], type[Any])) +``` + +## Unions and intersections + +```py +from typing import Any +from knot_extensions import Intersection, Not, Unknown, is_gradual_equivalent_to, static_assert + +static_assert(is_gradual_equivalent_to(str | int, str | int)) +static_assert(is_gradual_equivalent_to(str | int | Any, str | int | Unknown)) + +# TODO: These should pass +static_assert(is_gradual_equivalent_to(str | int, int | str)) # error: [static-assert-error] +# error: [static-assert-error] +static_assert( + is_gradual_equivalent_to(Intersection[str, int, Not[bytes], Not[None]], Intersection[int, str, Not[None], Not[bytes]]) +) +# error: [static-assert-error] +static_assert(is_gradual_equivalent_to(Intersection[str | int, Not[type[Any]]], Intersection[int | str, Not[type[Unknown]]])) + +static_assert(not is_gradual_equivalent_to(str | int, int | str | bytes)) +static_assert(not is_gradual_equivalent_to(str | int | bytes, int | str | dict)) +``` + +## Tuples + +```py +from knot_extensions import Unknown, is_gradual_equivalent_to, static_assert + +static_assert(is_gradual_equivalent_to(tuple[str, Any], tuple[str, Unknown])) + +static_assert(not is_gradual_equivalent_to(tuple[str, int], tuple[str, int, bytes])) +static_assert(not is_gradual_equivalent_to(tuple[str, int], tuple[int, str])) +``` + +[materializations]: https://typing.readthedocs.io/en/latest/spec/glossary.html#term-materialize diff --git a/crates/red_knot_python_semantic/src/types.rs b/crates/red_knot_python_semantic/src/types.rs index 031ad5ab45..0c3998976c 100644 --- a/crates/red_knot_python_semantic/src/types.rs +++ b/crates/red_knot_python_semantic/src/types.rs @@ -1955,6 +1955,15 @@ impl<'db> Type<'db> { .set_return_ty(Type::BooleanLiteral(ty_a.is_disjoint_from(db, ty_b))); CallOutcome::callable(binding) } + Some(KnownFunction::IsGradualEquivalentTo) => { + let (ty_a, ty_b) = binding + .two_parameter_tys() + .unwrap_or((Type::unknown(), Type::unknown())); + binding.set_return_ty(Type::BooleanLiteral( + ty_a.is_gradual_equivalent_to(db, ty_b), + )); + CallOutcome::callable(binding) + } Some(KnownFunction::IsFullyStatic) => { let ty = binding.one_parameter_ty().unwrap_or(Type::unknown()); binding.set_return_ty(Type::BooleanLiteral(ty.is_fully_static(db))); @@ -3404,6 +3413,8 @@ pub enum KnownFunction { IsAssignableTo, /// `knot_extensions.is_disjoint_from` IsDisjointFrom, + /// `knot_extensions.is_gradual_equivalent_to` + IsGradualEquivalentTo, /// `knot_extensions.is_fully_static` IsFullyStatic, /// `knot_extensions.is_singleton` @@ -3440,6 +3451,7 @@ impl KnownFunction { "is_disjoint_from" => Self::IsDisjointFrom, "is_equivalent_to" => Self::IsEquivalentTo, "is_assignable_to" => Self::IsAssignableTo, + "is_gradual_equivalent_to" => Self::IsGradualEquivalentTo, "is_fully_static" => Self::IsFullyStatic, "is_singleton" => Self::IsSingleton, "is_single_valued" => Self::IsSingleValued, @@ -3466,6 +3478,7 @@ impl KnownFunction { Self::IsAssignableTo | Self::IsDisjointFrom | Self::IsEquivalentTo + | Self::IsGradualEquivalentTo | Self::IsFullyStatic | Self::IsSingleValued | Self::IsSingleton @@ -3484,7 +3497,8 @@ impl KnownFunction { Self::IsEquivalentTo | Self::IsSubtypeOf | Self::IsAssignableTo - | Self::IsDisjointFrom => ParameterExpectations::TwoTypeExpressions, + | Self::IsDisjointFrom + | Self::IsGradualEquivalentTo => ParameterExpectations::TwoTypeExpressions, Self::AssertType => ParameterExpectations::ValueExpressionAndTypeExpression, Self::Cast => ParameterExpectations::TypeExpressionAndValueExpression, @@ -4323,7 +4337,6 @@ pub(crate) mod tests { Unknown, None, Any, - Todo, IntLiteral(i64), BooleanLiteral(bool), StringLiteral(&'static str), @@ -4347,7 +4360,6 @@ pub(crate) mod tests { SubclassOfAny, SubclassOfBuiltinClass(&'static str), SubclassOfAbcClass(&'static str), - SliceLiteral(i32, i32, i32), AlwaysTruthy, AlwaysFalsy, } @@ -4359,7 +4371,6 @@ pub(crate) mod tests { Ty::Unknown => Type::unknown(), Ty::None => Type::none(db), Ty::Any => Type::any(), - Ty::Todo => todo_type!("Ty::Todo"), Ty::IntLiteral(n) => Type::IntLiteral(n), Ty::StringLiteral(s) => Type::string_literal(db, s), Ty::BooleanLiteral(b) => Type::BooleanLiteral(b), @@ -4407,12 +4418,6 @@ pub(crate) mod tests { .expect_class_literal() .class, ), - Ty::SliceLiteral(start, stop, step) => Type::SliceLiteral(SliceLiteralType::new( - db, - Some(start), - Some(stop), - Some(step), - )), Ty::AlwaysTruthy => Type::AlwaysTruthy, Ty::AlwaysFalsy => Type::AlwaysFalsy, } @@ -4625,82 +4630,6 @@ pub(crate) mod tests { assert!(no_default.is_singleton(&db)); } - #[test_case(Ty::Todo, Ty::Todo)] - #[test_case(Ty::Any, Ty::Any)] - #[test_case(Ty::Unknown, Ty::Unknown)] - #[test_case(Ty::Any, Ty::Unknown)] - #[test_case(Ty::Todo, Ty::Unknown)] - #[test_case(Ty::Todo, Ty::Any)] - #[test_case(Ty::Never, Ty::Never)] - #[test_case(Ty::AlwaysTruthy, Ty::AlwaysTruthy)] - #[test_case(Ty::AlwaysFalsy, Ty::AlwaysFalsy)] - #[test_case(Ty::LiteralString, Ty::LiteralString)] - #[test_case(Ty::BooleanLiteral(true), Ty::BooleanLiteral(true))] - #[test_case(Ty::BooleanLiteral(false), Ty::BooleanLiteral(false))] - #[test_case(Ty::SliceLiteral(0, 1, 2), Ty::SliceLiteral(0, 1, 2))] - #[test_case(Ty::BuiltinClassLiteral("str"), Ty::BuiltinClassLiteral("str"))] - #[test_case(Ty::BuiltinInstance("type"), Ty::SubclassOfBuiltinClass("object"))] - // TODO: Compare unions/intersections with different orders - // #[test_case( - // Ty::Union(vec![Ty::BuiltinInstance("str"), Ty::BuiltinInstance("int")]), - // Ty::Union(vec![Ty::BuiltinInstance("int"), Ty::BuiltinInstance("str")]) - // )] - // #[test_case( - // Ty::Intersection { - // pos: vec![Ty::BuiltinInstance("str"), Ty::BuiltinInstance("int")], - // neg: vec![Ty::BuiltinInstance("bytes"), Ty::None] - // }, - // Ty::Intersection { - // pos: vec![Ty::BuiltinInstance("int"), Ty::BuiltinInstance("str")], - // neg: vec![Ty::None, Ty::BuiltinInstance("bytes")] - // } - // )] - // #[test_case( - // Ty::Intersection { - // pos: vec![Ty::Union(vec![Ty::BuiltinInstance("str"), Ty::BuiltinInstance("int")])], - // neg: vec![Ty::SubclassOfAny] - // }, - // Ty::Intersection { - // pos: vec![Ty::Union(vec![Ty::BuiltinInstance("int"), Ty::BuiltinInstance("str")])], - // neg: vec![Ty::SubclassOfUnknown] - // } - // )] - fn is_gradual_equivalent_to(a: Ty, b: Ty) { - let db = setup_db(); - let a = a.into_type(&db); - let b = b.into_type(&db); - - assert!(a.is_gradual_equivalent_to(&db, b)); - assert!(b.is_gradual_equivalent_to(&db, a)); - } - - #[test_case(Ty::BuiltinInstance("type"), Ty::SubclassOfAny)] - #[test_case(Ty::SubclassOfBuiltinClass("object"), Ty::SubclassOfAny)] - #[test_case( - Ty::Union(vec![Ty::BuiltinInstance("str"), Ty::BuiltinInstance("int")]), - Ty::Union(vec![Ty::BuiltinInstance("int"), Ty::BuiltinInstance("str"), Ty::BuiltinInstance("bytes")]) - )] - #[test_case( - Ty::Union(vec![Ty::BuiltinInstance("str"), Ty::BuiltinInstance("int"), Ty::BuiltinInstance("bytes")]), - Ty::Union(vec![Ty::BuiltinInstance("int"), Ty::BuiltinInstance("str"), Ty::BuiltinInstance("dict")]) - )] - #[test_case( - Ty::Tuple(vec![Ty::BuiltinInstance("str"), Ty::BuiltinInstance("int")]), - Ty::Tuple(vec![Ty::BuiltinInstance("str"), Ty::BuiltinInstance("int"), Ty::BuiltinInstance("bytes")]) - )] - #[test_case( - Ty::Tuple(vec![Ty::BuiltinInstance("str"), Ty::BuiltinInstance("int")]), - Ty::Tuple(vec![Ty::BuiltinInstance("int"), Ty::BuiltinInstance("str")]) - )] - fn is_not_gradual_equivalent_to(a: Ty, b: Ty) { - let db = setup_db(); - let a = a.into_type(&db); - let b = b.into_type(&db); - - assert!(!a.is_gradual_equivalent_to(&db, b)); - assert!(!b.is_gradual_equivalent_to(&db, a)); - } - #[test] fn typing_vs_typeshed_no_default() { let db = TestDbBuilder::new() diff --git a/crates/red_knot_python_semantic/src/types/property_tests.rs b/crates/red_knot_python_semantic/src/types/property_tests.rs index d259ebb916..c8d71a4beb 100644 --- a/crates/red_knot_python_semantic/src/types/property_tests.rs +++ b/crates/red_knot_python_semantic/src/types/property_tests.rs @@ -404,4 +404,17 @@ mod flaky { 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)) ); + + // Symmetry: If `S` is gradual equivalent to `T`, `T` is gradual equivalent to `S`. + type_property_test!( + gradual_equivalent_to_is_symmetric, db, + forall types s, t. s.is_gradual_equivalent_to(db, t) => t.is_gradual_equivalent_to(db, s) + ); + + // A fully static type does not have any materializations. + // Thus, two equivalent (fully static) types are also gradual equivalent. + type_property_test!( + two_equivalent_types_are_also_gradual_equivalent, db, + forall types s, t. s.is_equivalent_to(db, t) => s.is_gradual_equivalent_to(db, t) + ); } diff --git a/crates/red_knot_vendored/knot_extensions/knot_extensions.pyi b/crates/red_knot_vendored/knot_extensions/knot_extensions.pyi index 80d565479b..e78a56d4e6 100644 --- a/crates/red_knot_vendored/knot_extensions/knot_extensions.pyi +++ b/crates/red_knot_vendored/knot_extensions/knot_extensions.pyi @@ -21,6 +21,7 @@ def is_equivalent_to(type_a: Any, type_b: Any) -> bool: ... def is_subtype_of(type_derived: Any, type_base: Any) -> bool: ... def is_assignable_to(type_target: Any, type_source: Any) -> bool: ... def is_disjoint_from(type_a: Any, type_b: Any) -> bool: ... +def is_gradual_equivalent_to(type_a: Any, type_b: Any) -> bool: ... def is_fully_static(type: Any) -> bool: ... def is_singleton(type: Any) -> bool: ... def is_single_valued(type: Any) -> bool: ...