|
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