|
8 | 8 | //! This file includes the logic for exhaustiveness and usefulness checking for
|
9 | 9 | //! pattern-matching. Specifically, given a list of patterns for a type, we can
|
10 | 10 | //! tell whether:
|
11 |
| -//! (a) the patterns cover every possible constructor for the type [exhaustiveness] |
12 |
| -//! (b) each pattern is necessary [usefulness] |
| 11 | +//! - (a) the patterns cover every possible constructor for the type (exhaustiveness). |
| 12 | +//! - (b) each pattern is necessary (usefulness). |
13 | 13 | //!
|
14 |
| -//! The algorithm implemented here is a modified version of the one described in: |
15 |
| -//! http://moscova.inria.fr/~maranget/papers/warn/index.html |
| 14 | +//! The algorithm implemented here is a modified version of the one described in |
| 15 | +//! <http://moscova.inria.fr/~maranget/papers/warn/index.html>. |
16 | 16 | //! However, to save future implementors from reading the original paper, we
|
17 | 17 | //! summarise the algorithm here to hopefully save time and be a little clearer
|
18 | 18 | //! (without being so rigorous).
|
|
37 | 37 | //! new pattern `p`.
|
38 | 38 | //!
|
39 | 39 | //! For example, say we have the following:
|
| 40 | +//! |
| 41 | +//! ```ignore |
| 42 | +//! // x: (Option<bool>, Result<()>) |
| 43 | +//! match x { |
| 44 | +//! (Some(true), _) => {} |
| 45 | +//! (None, Err(())) => {} |
| 46 | +//! (None, Err(_)) => {} |
| 47 | +//! } |
40 | 48 | //! ```
|
41 |
| -//! // x: (Option<bool>, Result<()>) |
42 |
| -//! match x { |
43 |
| -//! (Some(true), _) => {} |
44 |
| -//! (None, Err(())) => {} |
45 |
| -//! (None, Err(_)) => {} |
46 |
| -//! } |
47 |
| -//! ``` |
| 49 | +//! |
48 | 50 | //! Here, the matrix `P` starts as:
|
| 51 | +//! |
| 52 | +//! ```text |
49 | 53 | //! [
|
50 | 54 | //! [(Some(true), _)],
|
51 | 55 | //! [(None, Err(()))],
|
52 | 56 | //! [(None, Err(_))],
|
53 | 57 | //! ]
|
| 58 | +//! ``` |
| 59 | +//! |
54 | 60 | //! We can tell it's not exhaustive, because `U(P, _)` is true (we're not covering
|
55 | 61 | //! `[(Some(false), _)]`, for instance). In addition, row 3 is not useful, because
|
56 | 62 | //! all the values it covers are already covered by row 2.
|
|
60 | 66 | //! To match the paper, the top of the stack is at the beginning / on the left.
|
61 | 67 | //!
|
62 | 68 | //! There are two important operations on pattern-stacks necessary to understand the algorithm:
|
63 |
| -//! 1. We can pop a given constructor off the top of a stack. This operation is called |
64 |
| -//! `specialize`, and is denoted `S(c, p)` where `c` is a constructor (like `Some` or |
65 |
| -//! `None`) and `p` a pattern-stack. |
66 |
| -//! If the pattern on top of the stack can cover `c`, this removes the constructor and |
67 |
| -//! pushes its arguments onto the stack. It also expands OR-patterns into distinct patterns. |
68 |
| -//! Otherwise the pattern-stack is discarded. |
69 |
| -//! This essentially filters those pattern-stacks whose top covers the constructor `c` and |
70 |
| -//! discards the others. |
71 | 69 | //!
|
72 |
| -//! For example, the first pattern above initially gives a stack `[(Some(true), _)]`. If we |
73 |
| -//! pop the tuple constructor, we are left with `[Some(true), _]`, and if we then pop the |
74 |
| -//! `Some` constructor we get `[true, _]`. If we had popped `None` instead, we would get |
75 |
| -//! nothing back. |
| 70 | +//! 1. We can pop a given constructor off the top of a stack. This operation is called |
| 71 | +//! `specialize`, and is denoted `S(c, p)` where `c` is a constructor (like `Some` or |
| 72 | +//! `None`) and `p` a pattern-stack. |
| 73 | +//! If the pattern on top of the stack can cover `c`, this removes the constructor and |
| 74 | +//! pushes its arguments onto the stack. It also expands OR-patterns into distinct patterns. |
| 75 | +//! Otherwise the pattern-stack is discarded. |
| 76 | +//! This essentially filters those pattern-stacks whose top covers the constructor `c` and |
| 77 | +//! discards the others. |
| 78 | +//! |
| 79 | +//! For example, the first pattern above initially gives a stack `[(Some(true), _)]`. If we |
| 80 | +//! pop the tuple constructor, we are left with `[Some(true), _]`, and if we then pop the |
| 81 | +//! `Some` constructor we get `[true, _]`. If we had popped `None` instead, we would get |
| 82 | +//! nothing back. |
| 83 | +//! |
| 84 | +//! This returns zero or more new pattern-stacks, as follows. We look at the pattern `p_1` |
| 85 | +//! on top of the stack, and we have four cases: |
| 86 | +//! |
| 87 | +//! * 1.1. `p_1 = c(r_1, .., r_a)`, i.e. the top of the stack has constructor `c`. We push onto |
| 88 | +//! the stack the arguments of this constructor, and return the result: |
| 89 | +//! |
| 90 | +//! r_1, .., r_a, p_2, .., p_n |
| 91 | +//! |
| 92 | +//! * 1.2. `p_1 = c'(r_1, .., r_a')` where `c ≠ c'`. We discard the current stack and return |
| 93 | +//! nothing. |
| 94 | +//! * 1.3. `p_1 = _`. We push onto the stack as many wildcards as the constructor `c` has |
| 95 | +//! arguments (its arity), and return the resulting stack: |
76 | 96 | //!
|
77 |
| -//! This returns zero or more new pattern-stacks, as follows. We look at the pattern `p_1` |
78 |
| -//! on top of the stack, and we have four cases: |
79 |
| -//! 1.1. `p_1 = c(r_1, .., r_a)`, i.e. the top of the stack has constructor `c`. We |
80 |
| -//! push onto the stack the arguments of this constructor, and return the result: |
81 |
| -//! r_1, .., r_a, p_2, .., p_n |
82 |
| -//! 1.2. `p_1 = c'(r_1, .., r_a')` where `c ≠ c'`. We discard the current stack and |
83 |
| -//! return nothing. |
84 |
| -//! 1.3. `p_1 = _`. We push onto the stack as many wildcards as the constructor `c` has |
85 |
| -//! arguments (its arity), and return the resulting stack: |
86 |
| -//! _, .., _, p_2, .., p_n |
87 |
| -//! 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting |
88 |
| -//! stack: |
89 |
| -//! S(c, (r_1, p_2, .., p_n)) |
90 |
| -//! S(c, (r_2, p_2, .., p_n)) |
| 97 | +//! _, .., _, p_2, .., p_n |
91 | 98 | //!
|
92 |
| -//! 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is |
93 |
| -//! a pattern-stack. |
94 |
| -//! This is used when we know there are missing constructor cases, but there might be |
95 |
| -//! existing wildcard patterns, so to check the usefulness of the matrix, we have to check |
96 |
| -//! all its *other* components. |
| 99 | +//! * 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting stack: |
97 | 100 | //!
|
98 |
| -//! It is computed as follows. We look at the pattern `p_1` on top of the stack, |
99 |
| -//! and we have three cases: |
100 |
| -//! 1.1. `p_1 = c(r_1, .., r_a)`. We discard the current stack and return nothing. |
101 |
| -//! 1.2. `p_1 = _`. We return the rest of the stack: |
102 |
| -//! p_2, .., p_n |
103 |
| -//! 1.3. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting |
104 |
| -//! stack. |
105 |
| -//! D((r_1, p_2, .., p_n)) |
106 |
| -//! D((r_2, p_2, .., p_n)) |
| 101 | +//! S(c, (r_1, p_2, .., p_n)) |
| 102 | +//! S(c, (r_2, p_2, .., p_n)) |
107 | 103 | //!
|
108 |
| -//! Note that the OR-patterns are not always used directly in Rust, but are used to derive the |
109 |
| -//! exhaustive integer matching rules, so they're written here for posterity. |
| 104 | +//! 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is |
| 105 | +//! a pattern-stack. |
| 106 | +//! This is used when we know there are missing constructor cases, but there might be |
| 107 | +//! existing wildcard patterns, so to check the usefulness of the matrix, we have to check |
| 108 | +//! all its *other* components. |
| 109 | +//! |
| 110 | +//! It is computed as follows. We look at the pattern `p_1` on top of the stack, |
| 111 | +//! and we have three cases: |
| 112 | +//! * 1.1. `p_1 = c(r_1, .., r_a)`. We discard the current stack and return nothing. |
| 113 | +//! * 1.2. `p_1 = _`. We return the rest of the stack: |
| 114 | +//! |
| 115 | +//! p_2, .., p_n |
| 116 | +//! |
| 117 | +//! * 1.3. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting stack: |
| 118 | +//! |
| 119 | +//! D((r_1, p_2, .., p_n)) |
| 120 | +//! D((r_2, p_2, .., p_n)) |
| 121 | +//! |
| 122 | +//! Note that the OR-patterns are not always used directly in Rust, but are used to derive the |
| 123 | +//! exhaustive integer matching rules, so they're written here for posterity. |
110 | 124 | //!
|
111 | 125 | //! Both those operations extend straightforwardly to a list or pattern-stacks, i.e. a matrix, by
|
112 | 126 | //! working row-by-row. Popping a constructor ends up keeping only the matrix rows that start with
|
|
120 | 134 | //! operates principally on the first component of the matrix and new pattern-stack `p`.
|
121 | 135 | //! This algorithm is realised in the `is_useful` function.
|
122 | 136 | //!
|
123 |
| -//! Base case. (`n = 0`, i.e., an empty tuple pattern) |
124 |
| -//! - If `P` already contains an empty pattern (i.e., if the number of patterns `m > 0`), |
125 |
| -//! then `U(P, p)` is false. |
126 |
| -//! - Otherwise, `P` must be empty, so `U(P, p)` is true. |
| 137 | +//! Base case (`n = 0`, i.e., an empty tuple pattern): |
| 138 | +//! - If `P` already contains an empty pattern (i.e., if the number of patterns `m > 0`), then |
| 139 | +//! `U(P, p)` is false. |
| 140 | +//! - Otherwise, `P` must be empty, so `U(P, p)` is true. |
| 141 | +//! |
| 142 | +//! Inductive step (`n > 0`, i.e., whether there's at least one column [which may then be expanded |
| 143 | +//! into further columns later]). We're going to match on the top of the new pattern-stack, `p_1`: |
| 144 | +//! |
| 145 | +//! - If `p_1 == c(r_1, .., r_a)`, i.e. we have a constructor pattern. |
| 146 | +//! Then, the usefulness of `p_1` can be reduced to whether it is useful when |
| 147 | +//! we ignore all the patterns in the first column of `P` that involve other constructors. |
| 148 | +//! This is where `S(c, P)` comes in: |
| 149 | +//! |
| 150 | +//! ```text |
| 151 | +//! U(P, p) := U(S(c, P), S(c, p)) |
| 152 | +//! ``` |
| 153 | +//! |
| 154 | +//! This special case is handled in `is_useful_specialized`. |
| 155 | +//! |
| 156 | +//! For example, if `P` is: |
| 157 | +//! |
| 158 | +//! ```text |
| 159 | +//! [ |
| 160 | +//! [Some(true), _], |
| 161 | +//! [None, 0], |
| 162 | +//! ] |
| 163 | +//! ``` |
127 | 164 | //!
|
128 |
| -//! Inductive step. (`n > 0`, i.e., whether there's at least one column |
129 |
| -//! [which may then be expanded into further columns later]) |
130 |
| -//! We're going to match on the top of the new pattern-stack, `p_1`. |
131 |
| -//! - If `p_1 == c(r_1, .., r_a)`, i.e. we have a constructor pattern. |
132 |
| -//! Then, the usefulness of `p_1` can be reduced to whether it is useful when |
133 |
| -//! we ignore all the patterns in the first column of `P` that involve other constructors. |
134 |
| -//! This is where `S(c, P)` comes in: |
135 |
| -//! `U(P, p) := U(S(c, P), S(c, p))` |
136 |
| -//! This special case is handled in `is_useful_specialized`. |
| 165 | +//! and `p` is `[Some(false), 0]`, then we don't care about row 2 since we know `p` only |
| 166 | +//! matches values that row 2 doesn't. For row 1 however, we need to dig into the |
| 167 | +//! arguments of `Some` to know whether some new value is covered. So we compute |
| 168 | +//! `U([[true, _]], [false, 0])`. |
137 | 169 | //!
|
138 |
| -//! For example, if `P` is: |
139 |
| -//! [ |
140 |
| -//! [Some(true), _], |
141 |
| -//! [None, 0], |
142 |
| -//! ] |
143 |
| -//! and `p` is [Some(false), 0], then we don't care about row 2 since we know `p` only |
144 |
| -//! matches values that row 2 doesn't. For row 1 however, we need to dig into the |
145 |
| -//! arguments of `Some` to know whether some new value is covered. So we compute |
146 |
| -//! `U([[true, _]], [false, 0])`. |
| 170 | +//! - If `p_1 == _`, then we look at the list of constructors that appear in the first component of |
| 171 | +//! the rows of `P`: |
| 172 | +//! - If there are some constructors that aren't present, then we might think that the |
| 173 | +//! wildcard `_` is useful, since it covers those constructors that weren't covered |
| 174 | +//! before. |
| 175 | +//! That's almost correct, but only works if there were no wildcards in those first |
| 176 | +//! components. So we need to check that `p` is useful with respect to the rows that |
| 177 | +//! start with a wildcard, if there are any. This is where `D` comes in: |
| 178 | +//! `U(P, p) := U(D(P), D(p))` |
147 | 179 | //!
|
148 |
| -//! - If `p_1 == _`, then we look at the list of constructors that appear in the first |
149 |
| -//! component of the rows of `P`: |
150 |
| -//! + If there are some constructors that aren't present, then we might think that the |
151 |
| -//! wildcard `_` is useful, since it covers those constructors that weren't covered |
152 |
| -//! before. |
153 |
| -//! That's almost correct, but only works if there were no wildcards in those first |
154 |
| -//! components. So we need to check that `p` is useful with respect to the rows that |
155 |
| -//! start with a wildcard, if there are any. This is where `D` comes in: |
156 |
| -//! `U(P, p) := U(D(P), D(p))` |
| 180 | +//! For example, if `P` is: |
| 181 | +//! ```text |
| 182 | +//! [ |
| 183 | +//! [_, true, _], |
| 184 | +//! [None, false, 1], |
| 185 | +//! ] |
| 186 | +//! ``` |
| 187 | +//! and `p` is `[_, false, _]`, the `Some` constructor doesn't appear in `P`. So if we |
| 188 | +//! only had row 2, we'd know that `p` is useful. However row 1 starts with a |
| 189 | +//! wildcard, so we need to check whether `U([[true, _]], [false, 1])`. |
157 | 190 | //!
|
158 |
| -//! For example, if `P` is: |
159 |
| -//! [ |
160 |
| -//! [_, true, _], |
161 |
| -//! [None, false, 1], |
162 |
| -//! ] |
163 |
| -//! and `p` is [_, false, _], the `Some` constructor doesn't appear in `P`. So if we |
164 |
| -//! only had row 2, we'd know that `p` is useful. However row 1 starts with a |
165 |
| -//! wildcard, so we need to check whether `U([[true, _]], [false, 1])`. |
| 191 | +//! - Otherwise, all possible constructors (for the relevant type) are present. In this |
| 192 | +//! case we must check whether the wildcard pattern covers any unmatched value. For |
| 193 | +//! that, we can think of the `_` pattern as a big OR-pattern that covers all |
| 194 | +//! possible constructors. For `Option`, that would mean `_ = None | Some(_)` for |
| 195 | +//! example. The wildcard pattern is useful in this case if it is useful when |
| 196 | +//! specialized to one of the possible constructors. So we compute: |
| 197 | +//! `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` |
166 | 198 | //!
|
167 |
| -//! + Otherwise, all possible constructors (for the relevant type) are present. In this |
168 |
| -//! case we must check whether the wildcard pattern covers any unmatched value. For |
169 |
| -//! that, we can think of the `_` pattern as a big OR-pattern that covers all |
170 |
| -//! possible constructors. For `Option`, that would mean `_ = None | Some(_)` for |
171 |
| -//! example. The wildcard pattern is useful in this case if it is useful when |
172 |
| -//! specialized to one of the possible constructors. So we compute: |
173 |
| -//! `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` |
| 199 | +//! For example, if `P` is: |
| 200 | +//! ```text |
| 201 | +//! [ |
| 202 | +//! [Some(true), _], |
| 203 | +//! [None, false], |
| 204 | +//! ] |
| 205 | +//! ``` |
| 206 | +//! and `p` is `[_, false]`, both `None` and `Some` constructors appear in the first |
| 207 | +//! components of `P`. We will therefore try popping both constructors in turn: we |
| 208 | +//! compute `U([[true, _]], [_, false])` for the `Some` constructor, and `U([[false]], |
| 209 | +//! [false])` for the `None` constructor. The first case returns true, so we know that |
| 210 | +//! `p` is useful for `P`. Indeed, it matches `[Some(false), _]` that wasn't matched |
| 211 | +//! before. |
174 | 212 | //!
|
175 |
| -//! For example, if `P` is: |
176 |
| -//! [ |
177 |
| -//! [Some(true), _], |
178 |
| -//! [None, false], |
179 |
| -//! ] |
180 |
| -//! and `p` is [_, false], both `None` and `Some` constructors appear in the first |
181 |
| -//! components of `P`. We will therefore try popping both constructors in turn: we |
182 |
| -//! compute U([[true, _]], [_, false]) for the `Some` constructor, and U([[false]], |
183 |
| -//! [false]) for the `None` constructor. The first case returns true, so we know that |
184 |
| -//! `p` is useful for `P`. Indeed, it matches `[Some(false), _]` that wasn't matched |
185 |
| -//! before. |
| 213 | +//! - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: |
186 | 214 | //!
|
187 |
| -//! - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: |
188 |
| -//! `U(P, p) := U(P, (r_1, p_2, .., p_n)) |
189 |
| -//! || U(P, (r_2, p_2, .., p_n))` |
| 215 | +//! ```text |
| 216 | +//! U(P, p) := U(P, (r_1, p_2, .., p_n)) |
| 217 | +//! || U(P, (r_2, p_2, .., p_n)) |
| 218 | +//! ``` |
190 | 219 | use std::sync::Arc;
|
191 | 220 |
|
192 | 221 | use smallvec::{smallvec, SmallVec};
|
|
0 commit comments