|
19 | 19 | //!
|
20 | 20 | //! The algorithm implemented here is a modified version of the one described in [this
|
21 | 21 | //! paper](http://moscova.inria.fr/~maranget/papers/warn/index.html). We have however generalized
|
22 |
| -//! it to accomodate the variety of patterns that rust supports. We thus explain our version here, |
| 22 | +//! it to accommodate the variety of patterns that Rust supports. We thus explain our version here, |
23 | 23 | //! without being as rigorous.
|
24 | 24 | //!
|
25 | 25 | //!
|
26 | 26 | //! # Summary
|
27 | 27 | //!
|
28 | 28 | //! The core of the algorithm is the notion of "usefulness". A pattern `q` is said to be *useful*
|
29 | 29 | //! relative to another pattern `p` of the same type if there is a value that is matched by `q` and
|
30 |
| -//! not matched by `p`. This generalizes to many `p`s: `q` is useful wrt a list of patterns `p_1 .. |
31 |
| -//! p_n` if there is a value that is matched by `q` and by none of the `p_i`. We write |
| 30 | +//! not matched by `p`. This generalizes to many `p`s: `q` is useful w.r.t. a list of patterns |
| 31 | +//! `p_1 .. p_n` if there is a value that is matched by `q` and by none of the `p_i`. We write |
32 | 32 | //! `usefulness(p_1 .. p_n, q)` for a function that returns a list of such values. The aim of this
|
33 | 33 | //! file is to compute it efficiently.
|
34 | 34 | //!
|
35 | 35 | //! This is enough to compute reachability: a pattern in a `match` expression is reachable iff it
|
36 |
| -//! is useful wrt the patterns above it: |
| 36 | +//! is useful w.r.t. the patterns above it: |
37 | 37 | //! ```rust
|
38 | 38 | //! match x {
|
39 | 39 | //! Some(_) => ...,
|
|
44 | 44 | //! ```
|
45 | 45 | //!
|
46 | 46 | //! This is also enough to compute exhaustiveness: a match is exhaustive iff the wildcard `_`
|
47 |
| -//! pattern is _not_ useful wrt the patterns in the match. The values returned by `usefulness` are |
48 |
| -//! used to tell the user which values are missing. |
| 47 | +//! pattern is _not_ useful w.r.t. the patterns in the match. The values returned by `usefulness` |
| 48 | +//! are used to tell the user which values are missing. |
49 | 49 | //! ```rust
|
50 | 50 | //! match x {
|
51 | 51 | //! Some(0) => ...,
|
|
102 | 102 | //!
|
103 | 103 | //! Note: this constructors/fields distinction may not straightforwardly apply to every Rust type.
|
104 | 104 | //! For example a value of type `Rc<u64>` can't be deconstructed that way, and `&str` has an
|
105 |
| -//! infinity of constructors. There are also subtleties with visibility of fields and |
| 105 | +//! infinitude of constructors. There are also subtleties with visibility of fields and |
106 | 106 | //! uninhabitedness and various other things. The constructors idea can be extended to handle most
|
107 | 107 | //! of these subtleties though; caveats are documented where relevant throughout the code.
|
108 | 108 | //!
|
|
184 | 184 | //!
|
185 | 185 | //! `specialize(c, p0 | p1) := specialize(c, p0) ++ specialize(c, p1)`
|
186 | 186 | //!
|
187 |
| -//! - We treat the other pattern constructors lik big or-patterns of all the possibilities: |
| 187 | +//! - We treat the other pattern constructors as if they were a large or-pattern of all the |
| 188 | +//! possibilities: |
188 | 189 | //!
|
189 | 190 | //! `specialize(c, _) := specialize(c, Variant1(_) | Variant2(_, _) | ...)`
|
190 | 191 | //!
|
|
193 | 194 | //! `specialize(c, [p0, .., p1]) := specialize(c, [p0, p1] | [p0, _, p1] | [p0, _, _, p1] | ...)`
|
194 | 195 | //!
|
195 | 196 | //! - If `c` is a pattern-only constructor, `specialize` is defined on a case-by-case basis. See
|
196 |
| -//! the discussion abount constructor splitting in [`super::deconstruct_pat`]. |
| 197 | +//! the discussion about constructor splitting in [`super::deconstruct_pat`]. |
197 | 198 | //!
|
198 | 199 | //!
|
199 | 200 | //! We then extend this function to work with pattern-stacks as input, by acting on the first
|
|
0 commit comments