diff options
author | Jonas Schievink <[email protected]> | 2020-06-14 14:56:02 +0100 |
---|---|---|
committer | Jonas Schievink <[email protected]> | 2020-06-14 14:56:02 +0100 |
commit | 4ebafb900561babe780e3f3ee06597acff33f885 (patch) | |
tree | e69ba146c2d321f770498585ccf4ea77cc3e23f6 | |
parent | 246c66a7f7fd3f85d7d6e47a36f17bafb0ccb08a (diff) |
_match.rs: improve comment formatting
-rw-r--r-- | crates/ra_hir_ty/src/_match.rs | 255 |
1 files changed, 142 insertions, 113 deletions
diff --git a/crates/ra_hir_ty/src/_match.rs b/crates/ra_hir_ty/src/_match.rs index 3e6e1e333..fff257193 100644 --- a/crates/ra_hir_ty/src/_match.rs +++ b/crates/ra_hir_ty/src/_match.rs | |||
@@ -8,11 +8,11 @@ | |||
8 | //! This file includes the logic for exhaustiveness and usefulness checking for | 8 | //! This file includes the logic for exhaustiveness and usefulness checking for |
9 | //! pattern-matching. Specifically, given a list of patterns for a type, we can | 9 | //! pattern-matching. Specifically, given a list of patterns for a type, we can |
10 | //! tell whether: | 10 | //! tell whether: |
11 | //! (a) the patterns cover every possible constructor for the type [exhaustiveness] | 11 | //! - (a) the patterns cover every possible constructor for the type (exhaustiveness). |
12 | //! (b) each pattern is necessary [usefulness] | 12 | //! - (b) each pattern is necessary (usefulness). |
13 | //! | 13 | //! |
14 | //! The algorithm implemented here is a modified version of the one described in: | 14 | //! The algorithm implemented here is a modified version of the one described in |
15 | //! http://moscova.inria.fr/~maranget/papers/warn/index.html | 15 | //! <http://moscova.inria.fr/~maranget/papers/warn/index.html>. |
16 | //! However, to save future implementors from reading the original paper, we | 16 | //! However, to save future implementors from reading the original paper, we |
17 | //! summarise the algorithm here to hopefully save time and be a little clearer | 17 | //! summarise the algorithm here to hopefully save time and be a little clearer |
18 | //! (without being so rigorous). | 18 | //! (without being so rigorous). |
@@ -37,20 +37,26 @@ | |||
37 | //! new pattern `p`. | 37 | //! new pattern `p`. |
38 | //! | 38 | //! |
39 | //! For example, say we have the following: | 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<()>) | 49 | //! |
42 | //! match x { | ||
43 | //! (Some(true), _) => {} | ||
44 | //! (None, Err(())) => {} | ||
45 | //! (None, Err(_)) => {} | ||
46 | //! } | ||
47 | //! ``` | ||
48 | //! Here, the matrix `P` starts as: | 50 | //! Here, the matrix `P` starts as: |
51 | //! | ||
52 | //! ```text | ||
49 | //! [ | 53 | //! [ |
50 | //! [(Some(true), _)], | 54 | //! [(Some(true), _)], |
51 | //! [(None, Err(()))], | 55 | //! [(None, Err(()))], |
52 | //! [(None, Err(_))], | 56 | //! [(None, Err(_))], |
53 | //! ] | 57 | //! ] |
58 | //! ``` | ||
59 | //! | ||
54 | //! We can tell it's not exhaustive, because `U(P, _)` is true (we're not covering | 60 | //! We can tell it's not exhaustive, because `U(P, _)` is true (we're not covering |
55 | //! `[(Some(false), _)]`, for instance). In addition, row 3 is not useful, because | 61 | //! `[(Some(false), _)]`, for instance). In addition, row 3 is not useful, because |
56 | //! all the values it covers are already covered by row 2. | 62 | //! all the values it covers are already covered by row 2. |
@@ -60,53 +66,61 @@ | |||
60 | //! To match the paper, the top of the stack is at the beginning / on the left. | 66 | //! To match the paper, the top of the stack is at the beginning / on the left. |
61 | //! | 67 | //! |
62 | //! There are two important operations on pattern-stacks necessary to understand the algorithm: | 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 | 70 | //! 1. We can pop a given constructor off the top of a stack. This operation is called |
73 | //! pop the tuple constructor, we are left with `[Some(true), _]`, and if we then pop the | 71 | //! `specialize`, and is denoted `S(c, p)` where `c` is a constructor (like `Some` or |
74 | //! `Some` constructor we get `[true, _]`. If we had popped `None` instead, we would get | 72 | //! `None`) and `p` a pattern-stack. |
75 | //! nothing back. | 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` | 97 | //! _, .., _, p_2, .., p_n |
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)) | ||
91 | //! | 98 | //! |
92 | //! 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is | 99 | //! * 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting stack: |
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. | ||
97 | //! | 100 | //! |
98 | //! It is computed as follows. We look at the pattern `p_1` on top of the stack, | 101 | //! S(c, (r_1, p_2, .., p_n)) |
99 | //! and we have three cases: | 102 | //! S(c, (r_2, p_2, .., p_n)) |
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)) | ||
107 | //! | 103 | //! |
108 | //! Note that the OR-patterns are not always used directly in Rust, but are used to derive the | 104 | //! 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is |
109 | //! exhaustive integer matching rules, so they're written here for posterity. | 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 | //! Both those operations extend straightforwardly to a list or pattern-stacks, i.e. a matrix, by | 125 | //! Both those operations extend straightforwardly to a list or pattern-stacks, i.e. a matrix, by |
112 | //! working row-by-row. Popping a constructor ends up keeping only the matrix rows that start with | 126 | //! working row-by-row. Popping a constructor ends up keeping only the matrix rows that start with |
@@ -120,73 +134,88 @@ | |||
120 | //! operates principally on the first component of the matrix and new pattern-stack `p`. | 134 | //! operates principally on the first component of the matrix and new pattern-stack `p`. |
121 | //! This algorithm is realised in the `is_useful` function. | 135 | //! This algorithm is realised in the `is_useful` function. |
122 | //! | 136 | //! |
123 | //! Base case. (`n = 0`, i.e., an empty tuple pattern) | 137 | //! 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`), | 138 | //! - If `P` already contains an empty pattern (i.e., if the number of patterns `m > 0`), then |
125 | //! then `U(P, p)` is false. | 139 | //! `U(P, p)` is false. |
126 | //! - Otherwise, `P` must be empty, so `U(P, p)` is true. | 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 | 165 | //! and `p` is `[Some(false), 0]`, then we don't care about row 2 since we know `p` only |
129 | //! [which may then be expanded into further columns later]) | 166 | //! matches values that row 2 doesn't. For row 1 however, we need to dig into the |
130 | //! We're going to match on the top of the new pattern-stack, `p_1`. | 167 | //! arguments of `Some` to know whether some new value is covered. So we compute |
131 | //! - If `p_1 == c(r_1, .., r_a)`, i.e. we have a constructor pattern. | 168 | //! `U([[true, _]], [false, 0])`. |
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`. | ||
137 | //! | 169 | //! |
138 | //! For example, if `P` is: | 170 | //! - If `p_1 == _`, then we look at the list of constructors that appear in the first component of |
139 | //! [ | 171 | //! the rows of `P`: |
140 | //! [Some(true), _], | 172 | //! - If there are some constructors that aren't present, then we might think that the |
141 | //! [None, 0], | 173 | //! wildcard `_` is useful, since it covers those constructors that weren't covered |
142 | //! ] | 174 | //! before. |
143 | //! and `p` is [Some(false), 0], then we don't care about row 2 since we know `p` only | 175 | //! That's almost correct, but only works if there were no wildcards in those first |
144 | //! matches values that row 2 doesn't. For row 1 however, we need to dig into the | 176 | //! components. So we need to check that `p` is useful with respect to the rows that |
145 | //! arguments of `Some` to know whether some new value is covered. So we compute | 177 | //! start with a wildcard, if there are any. This is where `D` comes in: |
146 | //! `U([[true, _]], [false, 0])`. | 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 | 180 | //! For example, if `P` is: |
149 | //! component of the rows of `P`: | 181 | //! ```text |
150 | //! + If there are some constructors that aren't present, then we might think that the | 182 | //! [ |
151 | //! wildcard `_` is useful, since it covers those constructors that weren't covered | 183 | //! [_, true, _], |
152 | //! before. | 184 | //! [None, false, 1], |
153 | //! That's almost correct, but only works if there were no wildcards in those first | 185 | //! ] |
154 | //! components. So we need to check that `p` is useful with respect to the rows that | 186 | //! ``` |
155 | //! start with a wildcard, if there are any. This is where `D` comes in: | 187 | //! and `p` is `[_, false, _]`, the `Some` constructor doesn't appear in `P`. So if we |
156 | //! `U(P, p) := U(D(P), D(p))` | 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: | 191 | //! - Otherwise, all possible constructors (for the relevant type) are present. In this |
159 | //! [ | 192 | //! case we must check whether the wildcard pattern covers any unmatched value. For |
160 | //! [_, true, _], | 193 | //! that, we can think of the `_` pattern as a big OR-pattern that covers all |
161 | //! [None, false, 1], | 194 | //! possible constructors. For `Option`, that would mean `_ = None | Some(_)` for |
162 | //! ] | 195 | //! example. The wildcard pattern is useful in this case if it is useful when |
163 | //! and `p` is [_, false, _], the `Some` constructor doesn't appear in `P`. So if we | 196 | //! specialized to one of the possible constructors. So we compute: |
164 | //! only had row 2, we'd know that `p` is useful. However row 1 starts with a | 197 | //! `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` |
165 | //! wildcard, so we need to check whether `U([[true, _]], [false, 1])`. | ||
166 | //! | 198 | //! |
167 | //! + Otherwise, all possible constructors (for the relevant type) are present. In this | 199 | //! For example, if `P` is: |
168 | //! case we must check whether the wildcard pattern covers any unmatched value. For | 200 | //! ```text |
169 | //! that, we can think of the `_` pattern as a big OR-pattern that covers all | 201 | //! [ |
170 | //! possible constructors. For `Option`, that would mean `_ = None | Some(_)` for | 202 | //! [Some(true), _], |
171 | //! example. The wildcard pattern is useful in this case if it is useful when | 203 | //! [None, false], |
172 | //! specialized to one of the possible constructors. So we compute: | 204 | //! ] |
173 | //! `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` | 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: | 213 | //! - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: |
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. | ||
186 | //! | 214 | //! |
187 | //! - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: | 215 | //! ```text |
188 | //! `U(P, p) := U(P, (r_1, p_2, .., p_n)) | 216 | //! U(P, p) := U(P, (r_1, p_2, .., p_n)) |
189 | //! || U(P, (r_2, p_2, .., p_n))` | 217 | //! || U(P, (r_2, p_2, .., p_n)) |
218 | //! ``` | ||
190 | use std::sync::Arc; | 219 | use std::sync::Arc; |
191 | 220 | ||
192 | use smallvec::{smallvec, SmallVec}; | 221 | use smallvec::{smallvec, SmallVec}; |