|
7 | 7 | //! have the same type, and that they only overlap if they are the identical.
|
8 | 8 | //!
|
9 | 9 | //! For example, if we are comparing these:
|
| 10 | +//! ```text |
10 | 11 | //! BORROW: (*x1[2].y).z.a
|
11 | 12 | //! ACCESS: (*x1[i].y).w.b
|
| 13 | +//! ``` |
12 | 14 | //!
|
13 | 15 | //! Then our steps are:
|
| 16 | +//! ```text |
14 | 17 | //! x1 | x1 -- places are the same
|
15 | 18 | //! x1[2] | x1[i] -- equal or disjoint (disjoint if indexes differ)
|
16 | 19 | //! x1[2].y | x1[i].y -- equal or disjoint
|
17 | 20 | //! *x1[2].y | *x1[i].y -- equal or disjoint
|
18 | 21 | //! (*x1[2].y).z | (*x1[i].y).w -- we are disjoint and don't need to check more!
|
| 22 | +//! ``` |
19 | 23 | //!
|
20 | 24 | //! Because `zip` does potentially bad things to the iterator inside, this loop
|
21 | 25 | //! also handles the case where the access might be a *prefix* of the borrow, e.g.
|
22 | 26 | //!
|
| 27 | +//! ```text |
23 | 28 | //! BORROW: (*x1[2].y).z.a
|
24 | 29 | //! ACCESS: x1[i].y
|
| 30 | +//! ``` |
25 | 31 | //!
|
26 | 32 | //! Then our steps are:
|
| 33 | +//! ```text |
27 | 34 | //! x1 | x1 -- places are the same
|
28 | 35 | //! x1[2] | x1[i] -- equal or disjoint (disjoint if indexes differ)
|
29 | 36 | //! x1[2].y | x1[i].y -- equal or disjoint
|
| 37 | +//! ``` |
30 | 38 | //!
|
31 | 39 | //! -- here we run out of access - the borrow can access a part of it. If this
|
32 | 40 | //! is a full deep access, then we *know* the borrow conflicts with it. However,
|
33 | 41 | //! if the access is shallow, then we can proceed:
|
34 | 42 | //!
|
| 43 | +//! ```text |
35 | 44 | //! x1[2].y | (*x1[i].y) -- a deref! the access can't get past this, so we
|
36 | 45 | //! are disjoint
|
| 46 | +//! ``` |
37 | 47 | //!
|
38 | 48 | //! Our invariant is, that at each step of the iteration:
|
39 | 49 | //! - If we didn't run out of access to match, our borrow and access are comparable
|
|
0 commit comments