Skip to content

Commit

Permalink
[red-knot] Migrate is_gradual_equivalent_to unit tests to Markdown …
Browse files Browse the repository at this point in the history
…tests (#15563)

## Summary

Part of #15397 and #15516.

## Test Plan

Markdown tests.
  • Loading branch information
InSyncWithFoo authored Jan 18, 2025
1 parent 98ef564 commit 9d845ec
Show file tree
Hide file tree
Showing 4 changed files with 95 additions and 86 deletions.
Original file line number Diff line number Diff line change
@@ -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
101 changes: 15 additions & 86 deletions crates/red_knot_python_semantic/src/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)));
Expand Down Expand Up @@ -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`
Expand Down Expand Up @@ -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,
Expand All @@ -3466,6 +3478,7 @@ impl KnownFunction {
Self::IsAssignableTo
| Self::IsDisjointFrom
| Self::IsEquivalentTo
| Self::IsGradualEquivalentTo
| Self::IsFullyStatic
| Self::IsSingleValued
| Self::IsSingleton
Expand All @@ -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,
Expand Down Expand Up @@ -4323,7 +4337,6 @@ pub(crate) mod tests {
Unknown,
None,
Any,
Todo,
IntLiteral(i64),
BooleanLiteral(bool),
StringLiteral(&'static str),
Expand All @@ -4347,7 +4360,6 @@ pub(crate) mod tests {
SubclassOfAny,
SubclassOfBuiltinClass(&'static str),
SubclassOfAbcClass(&'static str),
SliceLiteral(i32, i32, i32),
AlwaysTruthy,
AlwaysFalsy,
}
Expand All @@ -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),
Expand Down Expand Up @@ -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,
}
Expand Down Expand Up @@ -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()
Expand Down
13 changes: 13 additions & 0 deletions crates/red_knot_python_semantic/src/types/property_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
);
}
Original file line number Diff line number Diff line change
Expand Up @@ -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: ...

0 comments on commit 9d845ec

Please sign in to comment.