[ty] Reachability constraints: minor documentation fixes (#21774)

This commit is contained in:
David Peter 2025-12-03 16:40:11 +01:00 committed by GitHub
parent 45842cc034
commit d6e472f297
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
3 changed files with 18 additions and 18 deletions

View File

@ -715,7 +715,7 @@ reveal_type(Y) # revealed: Unknown
# The `*` import is not considered a redefinition
# of the global variable `Z` in this module, as the symbol in
# the `a` module is in a branch that is statically known
# the `exporter` module is in a branch that is statically known
# to be dead code given the `python-version` configuration.
# Thus this still reveals `Literal[True]`.
reveal_type(Z) # revealed: Literal[True]

View File

@ -166,10 +166,10 @@ impl<'db> PatternPredicate<'db> {
}
}
/// A "placeholder predicate" that is used to model the fact that the boundness of a
/// (possible) definition or declaration caused by a `*` import cannot be fully determined
/// until type-inference time. This is essentially the same as a standard reachability constraint,
/// so we reuse the [`Predicate`] infrastructure to model it.
/// A "placeholder predicate" that is used to model the fact that the boundness of a (possible)
/// definition or declaration caused by a `*` import cannot be fully determined until type-
/// inference time. This is essentially the same as a standard reachability constraint, so we reuse
/// the [`Predicate`] infrastructure to model it.
///
/// To illustrate, say we have a module `exporter.py` like so:
///
@ -183,14 +183,14 @@ impl<'db> PatternPredicate<'db> {
/// ```py
/// A = 1
///
/// from importer import *
/// from exporter import *
/// ```
///
/// Since we cannot know whether or not <condition> is true at semantic-index time,
/// we record a definition for `A` in `b.py` as a result of the `from a import *`
/// statement, but place a predicate on it to record the fact that we don't yet
/// know whether this definition will be visible from all control-flow paths or not.
/// Essentially, we model `b.py` as something similar to this:
/// Since we cannot know whether or not <condition> is true at semantic-index time, we record
/// a definition for `A` in `importer.py` as a result of the `from exporter import *` statement,
/// but place a predicate on it to record the fact that we don't yet know whether this definition
/// will be visible from all control-flow paths or not. Essentially, we model `importer.py` as
/// something similar to this:
///
/// ```py
/// A = 1
@ -199,8 +199,8 @@ impl<'db> PatternPredicate<'db> {
/// from a import A
/// ```
///
/// At type-check time, the placeholder predicate for the `A` definition is evaluated by
/// attempting to resolve the `A` symbol in `a.py`'s global namespace:
/// At type-check time, the placeholder predicate for the `A` definition is evaluated by attempting
/// to resolve the `A` symbol in `exporter.py`'s global namespace:
/// - If it resolves to a definitely bound symbol, then the predicate resolves to [`Truthiness::AlwaysTrue`]
/// - If it resolves to an unbound symbol, then the predicate resolves to [`Truthiness::AlwaysFalse`]
/// - If it resolves to a possibly bound symbol, then the predicate resolves to [`Truthiness::Ambiguous`]

View File

@ -3,7 +3,7 @@
//! During semantic index building, we record so-called reachability constraints that keep track
//! of a set of conditions that need to apply in order for a certain statement or expression to
//! be reachable from the start of the scope. As an example, consider the following situation where
//! we have just processed two `if`-statements:
//! we have just processed an `if`-statement:
//! ```py
//! if test:
//! <is this reachable?>
@ -101,13 +101,13 @@
//! <is this reachable?>
//! ```
//! If we would not record any constraints at the branching point, we would have an `always-true`
//! reachability for the no-loop branch, and a `always-false` reachability for the branch which enters
//! the loop. Merging those would lead to a reachability of `always-true OR always-false = always-true`,
//! reachability for the no-loop branch, and a `always-true` reachability for the branch which enters
//! the loop. Merging those would lead to a reachability of `always-true OR always-true = always-true`,
//! i.e. we would consider the end of the scope to be unconditionally reachable, which is not correct.
//!
//! Recording an ambiguous constraint at the branching point modifies the constraints in both branches to
//! `always-true AND ambiguous = ambiguous` and `always-false AND ambiguous = always-false`, respectively.
//! Merging these two using OR correctly leads to `ambiguous` for the end-of-scope reachability.
//! `always-true AND ambiguous = ambiguous`. Merging these two using OR correctly leads to `ambiguous` for
//! the end-of-scope reachability.
//!
//!
//! ## Reachability constraints and bindings