aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJonas Schievink <[email protected]>2020-06-14 14:56:02 +0100
committerJonas Schievink <[email protected]>2020-06-14 14:56:02 +0100
commit4ebafb900561babe780e3f3ee06597acff33f885 (patch)
treee69ba146c2d321f770498585ccf4ea77cc3e23f6
parent246c66a7f7fd3f85d7d6e47a36f17bafb0ccb08a (diff)
_match.rs: improve comment formatting
-rw-r--r--crates/ra_hir_ty/src/_match.rs255
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//! ```
190use std::sync::Arc; 219use std::sync::Arc;
191 220
192use smallvec::{smallvec, SmallVec}; 221use smallvec::{smallvec, SmallVec};