|
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