Skip to content

Commit

Permalink
[red-knot] 'is_equivalent_to' is an equivalence relation (#15488)
Browse files Browse the repository at this point in the history
## Summary

Adds two additional tests for `is_equivalent_to` so that we cover all
properties of an [equivalence relation].

## Test Plan

```
while cargo test --release -p red_knot_python_semantic -- --ignored types::property_tests::stable; do :; done
```

[equivalence relation]:
https://en.wikipedia.org/wiki/Equivalence_relation
  • Loading branch information
sharkdp authored Jan 15, 2025
1 parent 96c2d09 commit d486284
Showing 1 changed file with 15 additions and 2 deletions.
17 changes: 15 additions & 2 deletions crates/red_knot_python_semantic/src/types/property_tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -234,12 +234,25 @@ mod stable {
use super::union;
use crate::types::{KnownClass, Type};

// `T` is equivalent to itself.
// Reflexivity: `T` is equivalent to itself.
type_property_test!(
equivalent_to_is_reflexive, db,
forall types t. t.is_fully_static(db) => t.is_equivalent_to(db, t)
);

// Symmetry: If `S` is equivalent to `T`, then `T` must be equivalent to `S`.
// Note that this (trivially) holds true for gradual types as well.
type_property_test!(
equivalent_to_is_symmetric, db,
forall types s, t. s.is_equivalent_to(db, t) => t.is_equivalent_to(db, s)
);

// Transitivity: If `S` is equivalent to `T` and `T` is equivalent to `U`, then `S` must be equivalent to `U`.
type_property_test!(
equivalent_to_is_transitive, db,
forall types s, t, u. s.is_equivalent_to(db, t) && t.is_equivalent_to(db, u) => s.is_equivalent_to(db, u)
);

// A fully static type `T` is a subtype of itself.
type_property_test!(
subtype_of_is_reflexive, db,
Expand Down Expand Up @@ -365,7 +378,7 @@ mod flaky {

// For two fully static types, their intersection must be a subtype of each type in the pair.
type_property_test!(
all_fully_static_type_pairs_are_supertypes_of_their_union, db,
all_fully_static_type_pairs_are_supertypes_of_their_intersection, db,
forall types s, t.
s.is_fully_static(db) && t.is_fully_static(db)
=> intersection(db, s, t).is_subtype_of(db, s) && intersection(db, s, t).is_subtype_of(db, t)
Expand Down

0 comments on commit d486284

Please sign in to comment.