|
4 | 4 | //! This file includes the logic for exhaustiveness and usefulness checking for
|
5 | 5 | //! pattern-matching. Specifically, given a list of patterns for a type, we can
|
6 | 6 | //! tell whether:
|
7 |
| -//! (a) the patterns cover every possible constructor for the type [exhaustiveness] |
8 |
| -//! (b) each pattern is necessary [usefulness] |
| 7 | +//! (a) the patterns cover every possible constructor for the type (exhaustiveness) |
| 8 | +//! (b) each pattern is necessary (usefulness) |
9 | 9 | //!
|
10 | 10 | //! The algorithm implemented here is a modified version of the one described in:
|
11 | 11 | //! http://moscova.inria.fr/~maranget/papers/warn/index.html
|
|
101 | 101 | //! To match the paper, the top of the stack is at the beginning / on the left.
|
102 | 102 | //!
|
103 | 103 | //! There are two important operations on pattern-stacks necessary to understand the algorithm:
|
104 |
| -//! 1. We can pop a given constructor off the top of a stack. This operation is called |
105 |
| -//! `specialize`, and is denoted `S(c, p)` where `c` is a constructor (like `Some` or |
106 |
| -//! `None`) and `p` a pattern-stack. |
107 |
| -//! If the pattern on top of the stack can cover `c`, this removes the constructor and |
108 |
| -//! pushes its arguments onto the stack. It also expands OR-patterns into distinct patterns. |
109 |
| -//! Otherwise the pattern-stack is discarded. |
110 |
| -//! This essentially filters those pattern-stacks whose top covers the constructor `c` and |
111 |
| -//! discards the others. |
112 | 104 | //!
|
113 |
| -//! For example, the first pattern above initially gives a stack `[(Some(true), _)]`. If we |
114 |
| -//! pop the tuple constructor, we are left with `[Some(true), _]`, and if we then pop the |
115 |
| -//! `Some` constructor we get `[true, _]`. If we had popped `None` instead, we would get |
116 |
| -//! nothing back. |
| 105 | +//! 1. We can pop a given constructor off the top of a stack. This operation is called |
| 106 | +//! `specialize`, and is denoted `S(c, p)` where `c` is a constructor (like `Some` or |
| 107 | +//! `None`) and `p` a pattern-stack. |
| 108 | +//! If the pattern on top of the stack can cover `c`, this removes the constructor and |
| 109 | +//! pushes its arguments onto the stack. It also expands OR-patterns into distinct patterns. |
| 110 | +//! Otherwise the pattern-stack is discarded. |
| 111 | +//! This essentially filters those pattern-stacks whose top covers the constructor `c` and |
| 112 | +//! discards the others. |
117 | 113 | //!
|
118 |
| -//! This returns zero or more new pattern-stacks, as follows. We look at the pattern `p_1` |
119 |
| -//! on top of the stack, and we have four cases: |
120 |
| -//! 1.1. `p_1 = c(r_1, .., r_a)`, i.e. the top of the stack has constructor `c`. We |
121 |
| -//! push onto the stack the arguments of this constructor, and return the result: |
122 |
| -//! r_1, .., r_a, p_2, .., p_n |
123 |
| -//! 1.2. `p_1 = c'(r_1, .., r_a')` where `c ≠ c'`. We discard the current stack and |
124 |
| -//! return nothing. |
125 |
| -//! 1.3. `p_1 = _`. We push onto the stack as many wildcards as the constructor `c` has |
126 |
| -//! arguments (its arity), and return the resulting stack: |
127 |
| -//! _, .., _, p_2, .., p_n |
128 |
| -//! 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting |
129 |
| -//! stack: |
130 |
| -//! S(c, (r_1, p_2, .., p_n)) |
131 |
| -//! S(c, (r_2, p_2, .., p_n)) |
| 114 | +//! For example, the first pattern above initially gives a stack `[(Some(true), _)]`. If we |
| 115 | +//! pop the tuple constructor, we are left with `[Some(true), _]`, and if we then pop the |
| 116 | +//! `Some` constructor we get `[true, _]`. If we had popped `None` instead, we would get |
| 117 | +//! nothing back. |
132 | 118 | //!
|
133 |
| -//! 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is |
134 |
| -//! a pattern-stack. |
135 |
| -//! This is used when we know there are missing constructor cases, but there might be |
136 |
| -//! existing wildcard patterns, so to check the usefulness of the matrix, we have to check |
137 |
| -//! all its *other* components. |
| 119 | +//! This returns zero or more new pattern-stacks, as follows. We look at the pattern `p_1` |
| 120 | +//! on top of the stack, and we have four cases: |
| 121 | +//! 1.1. `p_1 = c(r_1, .., r_a)`, i.e. the top of the stack has constructor `c`. We |
| 122 | +//! push onto the stack the arguments of this constructor, and return the result: |
| 123 | +//! r_1, .., r_a, p_2, .., p_n |
| 124 | +//! 1.2. `p_1 = c'(r_1, .., r_a')` where `c ≠ c'`. We discard the current stack and |
| 125 | +//! return nothing. |
| 126 | +//! 1.3. `p_1 = _`. We push onto the stack as many wildcards as the constructor `c` has |
| 127 | +//! arguments (its arity), and return the resulting stack: |
| 128 | +//! _, .., _, p_2, .., p_n |
| 129 | +//! 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting |
| 130 | +//! stack: |
| 131 | +//! S(c, (r_1, p_2, .., p_n)) |
| 132 | +//! S(c, (r_2, p_2, .., p_n)) |
138 | 133 | //!
|
139 |
| -//! It is computed as follows. We look at the pattern `p_1` on top of the stack, |
140 |
| -//! and we have three cases: |
141 |
| -//! 1.1. `p_1 = c(r_1, .., r_a)`. We discard the current stack and return nothing. |
142 |
| -//! 1.2. `p_1 = _`. We return the rest of the stack: |
143 |
| -//! p_2, .., p_n |
144 |
| -//! 1.3. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting |
145 |
| -//! stack. |
146 |
| -//! D((r_1, p_2, .., p_n)) |
147 |
| -//! D((r_2, p_2, .., p_n)) |
| 134 | +//! 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is |
| 135 | +//! a pattern-stack. |
| 136 | +//! This is used when we know there are missing constructor cases, but there might be |
| 137 | +//! existing wildcard patterns, so to check the usefulness of the matrix, we have to check |
| 138 | +//! all its *other* components. |
148 | 139 | //!
|
149 |
| -//! Note that the OR-patterns are not always used directly in Rust, but are used to derive the |
150 |
| -//! exhaustive integer matching rules, so they're written here for posterity. |
| 140 | +//! It is computed as follows. We look at the pattern `p_1` on top of the stack, |
| 141 | +//! and we have three cases: |
| 142 | +//! 1.1. `p_1 = c(r_1, .., r_a)`. We discard the current stack and return nothing. |
| 143 | +//! 1.2. `p_1 = _`. We return the rest of the stack: |
| 144 | +//! p_2, .., p_n |
| 145 | +//! 1.3. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting |
| 146 | +//! stack. |
| 147 | +//! D((r_1, p_2, .., p_n)) |
| 148 | +//! D((r_2, p_2, .., p_n)) |
| 149 | +//! |
| 150 | +//! Note that the OR-patterns are not always used directly in Rust, but are used to derive the |
| 151 | +//! exhaustive integer matching rules, so they're written here for posterity. |
151 | 152 | //!
|
152 | 153 | //! Both those operations extend straightforwardly to a list or pattern-stacks, i.e. a matrix, by
|
153 | 154 | //! working row-by-row. Popping a constructor ends up keeping only the matrix rows that start with
|
|
168 | 169 | //!
|
169 | 170 | //! Inductive step. (`n > 0`, i.e., whether there's at least one column
|
170 | 171 | //! [which may then be expanded into further columns later])
|
171 |
| -//! We're going to match on the top of the new pattern-stack, `p_1`. |
172 |
| -//! - If `p_1 == c(r_1, .., r_a)`, i.e. we have a constructor pattern. |
173 |
| -//! Then, the usefulness of `p_1` can be reduced to whether it is useful when |
174 |
| -//! we ignore all the patterns in the first column of `P` that involve other constructors. |
175 |
| -//! This is where `S(c, P)` comes in: |
176 |
| -//! `U(P, p) := U(S(c, P), S(c, p))` |
177 |
| -//! This special case is handled in `is_useful_specialized`. |
| 172 | +//! We're going to match on the top of the new pattern-stack, `p_1`. |
| 173 | +//! - If `p_1 == c(r_1, .., r_a)`, i.e. we have a constructor pattern. |
| 174 | +//! Then, the usefulness of `p_1` can be reduced to whether it is useful when |
| 175 | +//! we ignore all the patterns in the first column of `P` that involve other constructors. |
| 176 | +//! This is where `S(c, P)` comes in: |
| 177 | +//! `U(P, p) := U(S(c, P), S(c, p))` |
| 178 | +//! This special case is handled in `is_useful_specialized`. |
178 | 179 | //!
|
179 |
| -//! For example, if `P` is: |
180 |
| -//! [ |
181 |
| -//! [Some(true), _], |
182 |
| -//! [None, 0], |
183 |
| -//! ] |
184 |
| -//! and `p` is [Some(false), 0], then we don't care about row 2 since we know `p` only |
185 |
| -//! matches values that row 2 doesn't. For row 1 however, we need to dig into the |
186 |
| -//! arguments of `Some` to know whether some new value is covered. So we compute |
187 |
| -//! `U([[true, _]], [false, 0])`. |
| 180 | +//! For example, if `P` is: |
| 181 | +//! [ |
| 182 | +//! [Some(true), _], |
| 183 | +//! [None, 0], |
| 184 | +//! ] |
| 185 | +//! and `p` is [Some(false), 0], then we don't care about row 2 since we know `p` only |
| 186 | +//! matches values that row 2 doesn't. For row 1 however, we need to dig into the |
| 187 | +//! arguments of `Some` to know whether some new value is covered. So we compute |
| 188 | +//! `U([[true, _]], [false, 0])`. |
188 | 189 | //!
|
189 |
| -//! - If `p_1 == _`, then we look at the list of constructors that appear in the first |
190 |
| -//! component of the rows of `P`: |
191 |
| -//! + If there are some constructors that aren't present, then we might think that the |
192 |
| -//! wildcard `_` is useful, since it covers those constructors that weren't covered |
193 |
| -//! before. |
194 |
| -//! That's almost correct, but only works if there were no wildcards in those first |
195 |
| -//! components. So we need to check that `p` is useful with respect to the rows that |
196 |
| -//! start with a wildcard, if there are any. This is where `D` comes in: |
197 |
| -//! `U(P, p) := U(D(P), D(p))` |
| 190 | +//! - If `p_1 == _`, then we look at the list of constructors that appear in the first |
| 191 | +//! component of the rows of `P`: |
| 192 | +//! + If there are some constructors that aren't present, then we might think that the |
| 193 | +//! wildcard `_` is useful, since it covers those constructors that weren't covered |
| 194 | +//! before. |
| 195 | +//! That's almost correct, but only works if there were no wildcards in those first |
| 196 | +//! components. So we need to check that `p` is useful with respect to the rows that |
| 197 | +//! start with a wildcard, if there are any. This is where `D` comes in: |
| 198 | +//! `U(P, p) := U(D(P), D(p))` |
198 | 199 | //!
|
199 |
| -//! For example, if `P` is: |
200 |
| -//! [ |
201 |
| -//! [_, true, _], |
202 |
| -//! [None, false, 1], |
203 |
| -//! ] |
204 |
| -//! and `p` is [_, false, _], the `Some` constructor doesn't appear in `P`. So if we |
205 |
| -//! only had row 2, we'd know that `p` is useful. However row 1 starts with a |
206 |
| -//! wildcard, so we need to check whether `U([[true, _]], [false, 1])`. |
| 200 | +//! For example, if `P` is: |
| 201 | +//! [ |
| 202 | +//! [_, true, _], |
| 203 | +//! [None, false, 1], |
| 204 | +//! ] |
| 205 | +//! and `p` is [_, false, _], the `Some` constructor doesn't appear in `P`. So if we |
| 206 | +//! only had row 2, we'd know that `p` is useful. However row 1 starts with a |
| 207 | +//! wildcard, so we need to check whether `U([[true, _]], [false, 1])`. |
207 | 208 | //!
|
208 |
| -//! + Otherwise, all possible constructors (for the relevant type) are present. In this |
209 |
| -//! case we must check whether the wildcard pattern covers any unmatched value. For |
210 |
| -//! that, we can think of the `_` pattern as a big OR-pattern that covers all |
211 |
| -//! possible constructors. For `Option`, that would mean `_ = None | Some(_)` for |
212 |
| -//! example. The wildcard pattern is useful in this case if it is useful when |
213 |
| -//! specialized to one of the possible constructors. So we compute: |
214 |
| -//! `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` |
| 209 | +//! + Otherwise, all possible constructors (for the relevant type) are present. In this |
| 210 | +//! case we must check whether the wildcard pattern covers any unmatched value. For |
| 211 | +//! that, we can think of the `_` pattern as a big OR-pattern that covers all |
| 212 | +//! possible constructors. For `Option`, that would mean `_ = None | Some(_)` for |
| 213 | +//! example. The wildcard pattern is useful in this case if it is useful when |
| 214 | +//! specialized to one of the possible constructors. So we compute: |
| 215 | +//! `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` |
215 | 216 | //!
|
216 |
| -//! For example, if `P` is: |
217 |
| -//! [ |
218 |
| -//! [Some(true), _], |
219 |
| -//! [None, false], |
220 |
| -//! ] |
221 |
| -//! and `p` is [_, false], both `None` and `Some` constructors appear in the first |
222 |
| -//! components of `P`. We will therefore try popping both constructors in turn: we |
223 |
| -//! compute U([[true, _]], [_, false]) for the `Some` constructor, and U([[false]], |
224 |
| -//! [false]) for the `None` constructor. The first case returns true, so we know that |
225 |
| -//! `p` is useful for `P`. Indeed, it matches `[Some(false), _]` that wasn't matched |
226 |
| -//! before. |
| 217 | +//! For example, if `P` is: |
| 218 | +//! [ |
| 219 | +//! [Some(true), _], |
| 220 | +//! [None, false], |
| 221 | +//! ] |
| 222 | +//! and `p` is [_, false], both `None` and `Some` constructors appear in the first |
| 223 | +//! components of `P`. We will therefore try popping both constructors in turn: we |
| 224 | +//! compute `U([[true, _]], [_, false])` for the `Some` constructor, and `U([[false]], |
| 225 | +//! [false])` for the `None` constructor. The first case returns true, so we know that |
| 226 | +//! `p` is useful for `P`. Indeed, it matches `[Some(false), _]` that wasn't matched |
| 227 | +//! before. |
227 | 228 | //!
|
228 |
| -//! - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: |
229 |
| -//! `U(P, p) := U(P, (r_1, p_2, .., p_n)) |
230 |
| -//! || U(P, (r_2, p_2, .., p_n))` |
| 229 | +//! - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: |
| 230 | +//! `U(P, p) := U(P, (r_1, p_2, .., p_n)) |
| 231 | +//! || U(P, (r_2, p_2, .., p_n))` |
231 | 232 | //!
|
232 | 233 | //! Modifications to the algorithm
|
233 | 234 | //! ------------------------------
|
|
0 commit comments