update/remove some old readmes
This commit is contained in:
parent
14ea6e50c1
commit
a6294b7628
4 changed files with 85 additions and 161 deletions
|
|
@ -2,8 +2,12 @@
|
|||
|
||||
> WARNING: This README is obsolete and will be removed soon! For
|
||||
> more info on how the current borrowck works, see the [rustc guide].
|
||||
>
|
||||
> As of edition 2018, region inference is done using Non-lexical lifetimes,
|
||||
> which is described in the guide and [this RFC].
|
||||
|
||||
[rustc guide]: https://rust-lang.github.io/rustc-guide/mir/borrowck.html
|
||||
[this RFC]: https://github.com/rust-lang/rfcs/blob/master/text/2094-nll.md
|
||||
|
||||
## Terminology
|
||||
|
||||
|
|
|
|||
|
|
@ -1,77 +1,3 @@
|
|||
# Region constraint collection
|
||||
|
||||
> WARNING: This README is obsolete and will be removed soon! For
|
||||
> more info on how the current borrowck works, see the [rustc guide].
|
||||
For info on how the current borrowck works, see the [rustc guide].
|
||||
|
||||
[rustc guide]: https://rust-lang.github.io/rustc-guide/mir/borrowck.html
|
||||
|
||||
## Terminology
|
||||
|
||||
Note that we use the terms region and lifetime interchangeably.
|
||||
|
||||
## Introduction
|
||||
|
||||
As described in the rustc guide [chapter on type inference][ti], and unlike
|
||||
normal type inference, which is similar in spirit to H-M and thus
|
||||
works progressively, the region type inference works by accumulating
|
||||
constraints over the course of a function. Finally, at the end of
|
||||
processing a function, we process and solve the constraints all at
|
||||
once.
|
||||
|
||||
[ti]: https://rust-lang.github.io/rustc-guide/type-inference.html
|
||||
|
||||
The constraints are always of one of three possible forms:
|
||||
|
||||
- `ConstrainVarSubVar(Ri, Rj)` states that region variable Ri must be
|
||||
a subregion of Rj
|
||||
- `ConstrainRegSubVar(R, Ri)` states that the concrete region R (which
|
||||
must not be a variable) must be a subregion of the variable Ri
|
||||
- `ConstrainVarSubReg(Ri, R)` states the variable Ri should be less
|
||||
than the concrete region R. This is kind of deprecated and ought to
|
||||
be replaced with a verify (they essentially play the same role).
|
||||
|
||||
In addition to constraints, we also gather up a set of "verifys"
|
||||
(what, you don't think Verify is a noun? Get used to it my
|
||||
friend!). These represent relations that must hold but which don't
|
||||
influence inference proper. These take the form of:
|
||||
|
||||
- `VerifyRegSubReg(Ri, Rj)` indicates that Ri <= Rj must hold,
|
||||
where Rj is not an inference variable (and Ri may or may not contain
|
||||
one). This doesn't influence inference because we will already have
|
||||
inferred Ri to be as small as possible, so then we just test whether
|
||||
that result was less than Rj or not.
|
||||
- `VerifyGenericBound(R, Vb)` is a more complex expression which tests
|
||||
that the region R must satisfy the bound `Vb`. The bounds themselves
|
||||
may have structure like "must outlive one of the following regions"
|
||||
or "must outlive ALL of the following regions. These bounds arise
|
||||
from constraints like `T: 'a` -- if we know that `T: 'b` and `T: 'c`
|
||||
(say, from where clauses), then we can conclude that `T: 'a` if `'b:
|
||||
'a` *or* `'c: 'a`.
|
||||
|
||||
## Building up the constraints
|
||||
|
||||
Variables and constraints are created using the following methods:
|
||||
|
||||
- `new_region_var()` creates a new, unconstrained region variable;
|
||||
- `make_subregion(Ri, Rj)` states that Ri is a subregion of Rj
|
||||
- `lub_regions(Ri, Rj) -> Rk` returns a region Rk which is
|
||||
the smallest region that is greater than both Ri and Rj
|
||||
- `glb_regions(Ri, Rj) -> Rk` returns a region Rk which is
|
||||
the greatest region that is smaller than both Ri and Rj
|
||||
|
||||
The actual region resolution algorithm is not entirely
|
||||
obvious, though it is also not overly complex.
|
||||
|
||||
## Snapshotting
|
||||
|
||||
It is also permitted to try (and rollback) changes to the graph. This
|
||||
is done by invoking `start_snapshot()`, which returns a value. Then
|
||||
later you can call `rollback_to()` which undoes the work.
|
||||
Alternatively, you can call `commit()` which ends all snapshots.
|
||||
Snapshots can be recursive---so you can start a snapshot when another
|
||||
is in progress, but only the root snapshot can "commit".
|
||||
|
||||
## Skolemization
|
||||
|
||||
For a discussion on skolemization and higher-ranked subtyping, please
|
||||
see the module `middle::infer::higher_ranked::doc`.
|
||||
|
|
|
|||
|
|
@ -1,81 +0,0 @@
|
|||
The `ObligationForest` is a utility data structure used in trait
|
||||
matching to track the set of outstanding obligations (those not yet
|
||||
resolved to success or error). It also tracks the "backtrace" of each
|
||||
pending obligation (why we are trying to figure this out in the first
|
||||
place).
|
||||
|
||||
### External view
|
||||
|
||||
`ObligationForest` supports two main public operations (there are a
|
||||
few others not discussed here):
|
||||
|
||||
1. Add a new root obligations (`push_tree`).
|
||||
2. Process the pending obligations (`process_obligations`).
|
||||
|
||||
When a new obligation `N` is added, it becomes the root of an
|
||||
obligation tree. This tree can also carry some per-tree state `T`,
|
||||
which is given at the same time. This tree is a singleton to start, so
|
||||
`N` is both the root and the only leaf. Each time the
|
||||
`process_obligations` method is called, it will invoke its callback
|
||||
with every pending obligation (so that will include `N`, the first
|
||||
time). The callback also receives a (mutable) reference to the
|
||||
per-tree state `T`. The callback should process the obligation `O`
|
||||
that it is given and return one of three results:
|
||||
|
||||
- `Ok(None)` -> ambiguous result. Obligation was neither a success
|
||||
nor a failure. It is assumed that further attempts to process the
|
||||
obligation will yield the same result unless something in the
|
||||
surrounding environment changes.
|
||||
- `Ok(Some(C))` - the obligation was *shallowly successful*. The
|
||||
vector `C` is a list of subobligations. The meaning of this is that
|
||||
`O` was successful on the assumption that all the obligations in `C`
|
||||
are also successful. Therefore, `O` is only considered a "true"
|
||||
success if `C` is empty. Otherwise, `O` is put into a suspended
|
||||
state and the obligations in `C` become the new pending
|
||||
obligations. They will be processed the next time you call
|
||||
`process_obligations`.
|
||||
- `Err(E)` -> obligation failed with error `E`. We will collect this
|
||||
error and return it from `process_obligations`, along with the
|
||||
"backtrace" of obligations (that is, the list of obligations up to
|
||||
and including the root of the failed obligation). No further
|
||||
obligations from that same tree will be processed, since the tree is
|
||||
now considered to be in error.
|
||||
|
||||
When the call to `process_obligations` completes, you get back an `Outcome`,
|
||||
which includes three bits of information:
|
||||
|
||||
- `completed`: a list of obligations where processing was fully
|
||||
completed without error (meaning that all transitive subobligations
|
||||
have also been completed). So, for example, if the callback from
|
||||
`process_obligations` returns `Ok(Some(C))` for some obligation `O`,
|
||||
then `O` will be considered completed right away if `C` is the
|
||||
empty vector. Otherwise it will only be considered completed once
|
||||
all the obligations in `C` have been found completed.
|
||||
- `errors`: a list of errors that occurred and associated backtraces
|
||||
at the time of error, which can be used to give context to the user.
|
||||
- `stalled`: if true, then none of the existing obligations were
|
||||
*shallowly successful* (that is, no callback returned `Ok(Some(_))`).
|
||||
This implies that all obligations were either errors or returned an
|
||||
ambiguous result, which means that any further calls to
|
||||
`process_obligations` would simply yield back further ambiguous
|
||||
results. This is used by the `FulfillmentContext` to decide when it
|
||||
has reached a steady state.
|
||||
|
||||
#### Snapshots
|
||||
|
||||
The `ObligationForest` supports a limited form of snapshots; see
|
||||
`start_snapshot`; `commit_snapshot`; and `rollback_snapshot`. In
|
||||
particular, you can use a snapshot to roll back new root
|
||||
obligations. However, it is an error to attempt to
|
||||
`process_obligations` during a snapshot.
|
||||
|
||||
### Implementation details
|
||||
|
||||
For the most part, comments specific to the implementation are in the
|
||||
code. This file only contains a very high-level overview. Basically,
|
||||
the forest is stored in a vector. Each element of the vector is a node
|
||||
in some tree. Each node in the vector has the index of an (optional)
|
||||
parent and (for convenience) its root (which may be itself). It also
|
||||
has a current state, described by `NodeState`. After each
|
||||
processing step, we compress the vector to remove completed and error
|
||||
nodes, which aren't needed anymore.
|
||||
|
|
@ -1,9 +1,84 @@
|
|||
//! The `ObligationForest` is a utility data structure used in trait
|
||||
//! matching to track the set of outstanding obligations (those not
|
||||
//! yet resolved to success or error). It also tracks the "backtrace"
|
||||
//! of each pending obligation (why we are trying to figure this out
|
||||
//! in the first place). See README.md for a general overview of how
|
||||
//! to use this class.
|
||||
//! matching to track the set of outstanding obligations (those not yet
|
||||
//! resolved to success or error). It also tracks the "backtrace" of each
|
||||
//! pending obligation (why we are trying to figure this out in the first
|
||||
//! place).
|
||||
//!
|
||||
//! ### External view
|
||||
//!
|
||||
//! `ObligationForest` supports two main public operations (there are a
|
||||
//! few others not discussed here):
|
||||
//!
|
||||
//! 1. Add a new root obligations (`push_tree`).
|
||||
//! 2. Process the pending obligations (`process_obligations`).
|
||||
//!
|
||||
//! When a new obligation `N` is added, it becomes the root of an
|
||||
//! obligation tree. This tree can also carry some per-tree state `T`,
|
||||
//! which is given at the same time. This tree is a singleton to start, so
|
||||
//! `N` is both the root and the only leaf. Each time the
|
||||
//! `process_obligations` method is called, it will invoke its callback
|
||||
//! with every pending obligation (so that will include `N`, the first
|
||||
//! time). The callback also receives a (mutable) reference to the
|
||||
//! per-tree state `T`. The callback should process the obligation `O`
|
||||
//! that it is given and return one of three results:
|
||||
//!
|
||||
//! - `Ok(None)` -> ambiguous result. Obligation was neither a success
|
||||
//! nor a failure. It is assumed that further attempts to process the
|
||||
//! obligation will yield the same result unless something in the
|
||||
//! surrounding environment changes.
|
||||
//! - `Ok(Some(C))` - the obligation was *shallowly successful*. The
|
||||
//! vector `C` is a list of subobligations. The meaning of this is that
|
||||
//! `O` was successful on the assumption that all the obligations in `C`
|
||||
//! are also successful. Therefore, `O` is only considered a "true"
|
||||
//! success if `C` is empty. Otherwise, `O` is put into a suspended
|
||||
//! state and the obligations in `C` become the new pending
|
||||
//! obligations. They will be processed the next time you call
|
||||
//! `process_obligations`.
|
||||
//! - `Err(E)` -> obligation failed with error `E`. We will collect this
|
||||
//! error and return it from `process_obligations`, along with the
|
||||
//! "backtrace" of obligations (that is, the list of obligations up to
|
||||
//! and including the root of the failed obligation). No further
|
||||
//! obligations from that same tree will be processed, since the tree is
|
||||
//! now considered to be in error.
|
||||
//!
|
||||
//! When the call to `process_obligations` completes, you get back an `Outcome`,
|
||||
//! which includes three bits of information:
|
||||
//!
|
||||
//! - `completed`: a list of obligations where processing was fully
|
||||
//! completed without error (meaning that all transitive subobligations
|
||||
//! have also been completed). So, for example, if the callback from
|
||||
//! `process_obligations` returns `Ok(Some(C))` for some obligation `O`,
|
||||
//! then `O` will be considered completed right away if `C` is the
|
||||
//! empty vector. Otherwise it will only be considered completed once
|
||||
//! all the obligations in `C` have been found completed.
|
||||
//! - `errors`: a list of errors that occurred and associated backtraces
|
||||
//! at the time of error, which can be used to give context to the user.
|
||||
//! - `stalled`: if true, then none of the existing obligations were
|
||||
//! *shallowly successful* (that is, no callback returned `Ok(Some(_))`).
|
||||
//! This implies that all obligations were either errors or returned an
|
||||
//! ambiguous result, which means that any further calls to
|
||||
//! `process_obligations` would simply yield back further ambiguous
|
||||
//! results. This is used by the `FulfillmentContext` to decide when it
|
||||
//! has reached a steady state.
|
||||
//!
|
||||
//! #### Snapshots
|
||||
//!
|
||||
//! The `ObligationForest` supports a limited form of snapshots; see
|
||||
//! `start_snapshot`; `commit_snapshot`; and `rollback_snapshot`. In
|
||||
//! particular, you can use a snapshot to roll back new root
|
||||
//! obligations. However, it is an error to attempt to
|
||||
//! `process_obligations` during a snapshot.
|
||||
//!
|
||||
//! ### Implementation details
|
||||
//!
|
||||
//! For the most part, comments specific to the implementation are in the
|
||||
//! code. This file only contains a very high-level overview. Basically,
|
||||
//! the forest is stored in a vector. Each element of the vector is a node
|
||||
//! in some tree. Each node in the vector has the index of an (optional)
|
||||
//! parent and (for convenience) its root (which may be itself). It also
|
||||
//! has a current state, described by `NodeState`. After each
|
||||
//! processing step, we compress the vector to remove completed and error
|
||||
//! nodes, which aren't needed anymore.
|
||||
|
||||
use fx::{FxHashMap, FxHashSet};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue