|
1 | | -# Region constraint collection |
2 | | - |
3 | | -> WARNING: This README is obsolete and will be removed soon! For |
4 | | -> more info on how the current borrowck works, see the [rustc guide]. |
| 1 | +For info on how the current borrowck works, see the [rustc guide]. |
5 | 2 |
|
6 | 3 | [rustc guide]: https://rust-lang.github.io/rustc-guide/mir/borrowck.html |
7 | | - |
8 | | -## Terminology |
9 | | - |
10 | | -Note that we use the terms region and lifetime interchangeably. |
11 | | - |
12 | | -## Introduction |
13 | | - |
14 | | -As described in the rustc guide [chapter on type inference][ti], and unlike |
15 | | -normal type inference, which is similar in spirit to H-M and thus |
16 | | -works progressively, the region type inference works by accumulating |
17 | | -constraints over the course of a function. Finally, at the end of |
18 | | -processing a function, we process and solve the constraints all at |
19 | | -once. |
20 | | - |
21 | | -[ti]: https://rust-lang.github.io/rustc-guide/type-inference.html |
22 | | - |
23 | | -The constraints are always of one of three possible forms: |
24 | | - |
25 | | -- `ConstrainVarSubVar(Ri, Rj)` states that region variable Ri must be |
26 | | - a subregion of Rj |
27 | | -- `ConstrainRegSubVar(R, Ri)` states that the concrete region R (which |
28 | | - must not be a variable) must be a subregion of the variable Ri |
29 | | -- `ConstrainVarSubReg(Ri, R)` states the variable Ri should be less |
30 | | - than the concrete region R. This is kind of deprecated and ought to |
31 | | - be replaced with a verify (they essentially play the same role). |
32 | | - |
33 | | -In addition to constraints, we also gather up a set of "verifys" |
34 | | -(what, you don't think Verify is a noun? Get used to it my |
35 | | -friend!). These represent relations that must hold but which don't |
36 | | -influence inference proper. These take the form of: |
37 | | - |
38 | | -- `VerifyRegSubReg(Ri, Rj)` indicates that Ri <= Rj must hold, |
39 | | - where Rj is not an inference variable (and Ri may or may not contain |
40 | | - one). This doesn't influence inference because we will already have |
41 | | - inferred Ri to be as small as possible, so then we just test whether |
42 | | - that result was less than Rj or not. |
43 | | -- `VerifyGenericBound(R, Vb)` is a more complex expression which tests |
44 | | - that the region R must satisfy the bound `Vb`. The bounds themselves |
45 | | - may have structure like "must outlive one of the following regions" |
46 | | - or "must outlive ALL of the following regions. These bounds arise |
47 | | - from constraints like `T: 'a` -- if we know that `T: 'b` and `T: 'c` |
48 | | - (say, from where clauses), then we can conclude that `T: 'a` if `'b: |
49 | | - 'a` *or* `'c: 'a`. |
50 | | - |
51 | | -## Building up the constraints |
52 | | - |
53 | | -Variables and constraints are created using the following methods: |
54 | | - |
55 | | -- `new_region_var()` creates a new, unconstrained region variable; |
56 | | -- `make_subregion(Ri, Rj)` states that Ri is a subregion of Rj |
57 | | -- `lub_regions(Ri, Rj) -> Rk` returns a region Rk which is |
58 | | - the smallest region that is greater than both Ri and Rj |
59 | | -- `glb_regions(Ri, Rj) -> Rk` returns a region Rk which is |
60 | | - the greatest region that is smaller than both Ri and Rj |
61 | | - |
62 | | -The actual region resolution algorithm is not entirely |
63 | | -obvious, though it is also not overly complex. |
64 | | - |
65 | | -## Snapshotting |
66 | | - |
67 | | -It is also permitted to try (and rollback) changes to the graph. This |
68 | | -is done by invoking `start_snapshot()`, which returns a value. Then |
69 | | -later you can call `rollback_to()` which undoes the work. |
70 | | -Alternatively, you can call `commit()` which ends all snapshots. |
71 | | -Snapshots can be recursive---so you can start a snapshot when another |
72 | | -is in progress, but only the root snapshot can "commit". |
73 | | - |
74 | | -## Skolemization |
75 | | - |
76 | | -For a discussion on skolemization and higher-ranked subtyping, please |
77 | | -see the module `middle::infer::higher_ranked::doc`. |
0 commit comments