|
3 | 3 | //! `Constructor` enum, a `Fields` struct, and various operations to manipulate them and convert |
4 | 4 | //! them from/to patterns. |
5 | 5 | //! |
6 | | -//! There's one idea that is not detailed in [`super::usefulness`] because the details are not |
7 | | -//! needed there: _constructor splitting_. |
| 6 | +//! The one idea that is not detailed in [`super::usefulness`] is _constructor splitting_. |
8 | 7 | //! |
9 | | -//! # Constructor splitting |
| 8 | +//! # Constructor grouping and splitting |
10 | 9 | //! |
11 | | -//! The idea is as follows: given a constructor `c` and a matrix, we want to specialize in turn |
12 | | -//! with all the value constructors that are covered by `c`, and compute usefulness for each. |
13 | | -//! Instead of listing all those constructors (which is intractable), we group those value |
14 | | -//! constructors together as much as possible. Example: |
| 10 | +//! As explained in the corresponding section in [`super::usefulness`], to make usefulness tractable |
| 11 | +//! we need to group together constructors that have the same effect when they are used to |
| 12 | +//! specialize the matrix. |
15 | 13 | //! |
| 14 | +//! Example: |
16 | 15 | //! ```compile_fail,E0004 |
17 | 16 | //! match (0, false) { |
18 | | -//! (0 ..=100, true) => {} // `p_1` |
19 | | -//! (50..=150, false) => {} // `p_2` |
20 | | -//! (0 ..=200, _) => {} // `q` |
| 17 | +//! (0 ..=100, true) => {} |
| 18 | +//! (50..=150, false) => {} |
| 19 | +//! (0 ..=200, _) => {} |
21 | 20 | //! } |
22 | 21 | //! ``` |
23 | 22 | //! |
24 | | -//! The naive approach would try all numbers in the range `0..=200`. But we can be a lot more |
25 | | -//! clever: `0` and `1` for example will match the exact same rows, and return equivalent |
26 | | -//! witnesses. In fact all of `0..50` would. We can thus restrict our exploration to 4 |
27 | | -//! constructors: `0..50`, `50..=100`, `101..=150` and `151..=200`. That is enough and infinitely |
28 | | -//! more tractable. |
| 23 | +//! Here we can restrict specialization to 5 cases: `0..50`, `50..=100`, `101..=150`, `151..=200` |
| 24 | +//! and `200..`. |
29 | 25 | //! |
30 | | -//! We capture this idea in a function `split(p_1 ... p_n, c)` which returns a list of constructors |
31 | | -//! `c'` covered by `c`. Given such a `c'`, we require that all value ctors `c''` covered by `c'` |
32 | | -//! return an equivalent set of witnesses after specializing and computing usefulness. |
33 | | -//! In the example above, witnesses for specializing by `c''` covered by `0..50` will only differ |
34 | | -//! in their first element. |
| 26 | +//! In [`super::usefulness`], we had said that `specialize` only takes value-only constructors. We |
| 27 | +//! relax this restriction: we allow `specialize` to take constructors like `0..50` as long as we're |
| 28 | +//! careful to only do that with constructors that make sense. |
35 | 29 | //! |
36 | | -//! We usually also ask that the `c'` together cover all of the original `c`. However we allow |
37 | | -//! skipping some constructors as long as it doesn't change whether the resulting list of witnesses |
38 | | -//! is empty of not. We use this in the wildcard `_` case. |
| 30 | +//! For example, `specialize(0..50, (0..=100, true))` is sensible, but `specialize(50..=200, |
| 31 | +//! (0..=100, true))` is not. The rule is that we must only use a constructor that is a subset of |
| 32 | +//! constructors in the column (as computed by [`Constructor::is_covered_by`]). No non-trivial |
| 33 | +//! intersections are allowed. |
| 34 | +//! |
| 35 | +//! Note how we only consider the first column of the match. In fact we take as input only the list |
| 36 | +//! of the constructors of that column. We must return a set of constructors that cover the whole |
| 37 | +//! type and is grouped as much as possible, without breaking the "must be included" rule above. The |
| 38 | +//! precise set of invariants is described in [`SplitConstructorSet`]. |
| 39 | +//! |
| 40 | +//! We compute this in two steps: first [`ConstructorSet::for_ty`] computes a representation of the |
| 41 | +//! set of all possible constructors for the type. Then [`ConstructorSet::split`] looks at the |
| 42 | +//! column of constructors and splits the set into groups accordingly. |
| 43 | +//! |
| 44 | +//! Constructor splitting has two interesting special cases: integer range splitting (see |
| 45 | +//! [`IntRange::split`]) and slice splitting (see [`Slice::split`]). |
39 | 46 | //! |
40 | | -//! Splitting is implemented in the [`ConstructorSet::split`] function. We don't do splitting for |
41 | | -//! or-patterns; instead we just try the alternatives one-by-one. For details on splitting |
42 | | -//! wildcards, see [`ConstructorSet::split`]; for integer ranges, see [`IntRange::split`]; for |
43 | | -//! slices, see [`Slice::split`]. |
44 | 47 | //! |
45 | 48 | //! ## Opaque patterns |
46 | 49 | //! |
47 | | -//! Some patterns, such as TODO, cannot be inspected, which we handle with `Constructor::Opaque`. |
48 | | -//! Since we know nothing of these patterns, we assume they never cover each other. In order to |
49 | | -//! respect the invariants of [`SplitConstructorSet`], we give each `Opaque` constructor a unique id |
50 | | -//! so we can recognize it. |
| 50 | +//! Some patterns, such as constants that are not allowed to be matched structurally, cannot be |
| 51 | +//! inspected, which we handle with `Constructor::Opaque`. Since we know nothing of these patterns, |
| 52 | +//! we assume they never cover each other. In order to respect the invariants of |
| 53 | +//! [`SplitConstructorSet`], we give each `Opaque` constructor a unique id so we can recognize it. |
51 | 54 |
|
52 | 55 | use std::cell::Cell; |
53 | 56 | use std::cmp::{self, max, min, Ordering}; |
@@ -645,8 +648,8 @@ impl OpaqueId { |
645 | 648 | /// `Fields`. |
646 | 649 | #[derive(Clone, Debug, PartialEq)] |
647 | 650 | pub(super) enum Constructor<'tcx> { |
648 | | - /// The constructor for patterns that have a single constructor, like tuples, struct patterns |
649 | | - /// and fixed-length arrays. |
| 651 | + /// The constructor for patterns that have a single constructor, like tuples, struct patterns, |
| 652 | + /// and references. Fixed-length arrays are treated separately with `Slice`. |
650 | 653 | Single, |
651 | 654 | /// Enum variants. |
652 | 655 | Variant(VariantIdx), |
@@ -851,16 +854,16 @@ pub(super) enum ConstructorSet { |
851 | 854 | /// `present` is morally the set of constructors present in the column, and `missing` is the set of |
852 | 855 | /// constructors that exist in the type but are not present in the column. |
853 | 856 | /// |
854 | | -/// More formally, they respect the following constraints: |
855 | | -/// - the union of `present` and `missing` covers the whole type |
856 | | -/// - `present` and `missing` are disjoint |
857 | | -/// - neither contains wildcards |
858 | | -/// - each constructor in `present` is covered by some non-wildcard constructor in the column |
859 | | -/// - together, the constructors in `present` cover all the non-wildcard constructor in the column |
860 | | -/// - non-wildcards in the column do no cover anything in `missing` |
861 | | -/// - constructors in `present` and `missing` are split for the column; in other words, they are |
862 | | -/// either fully included in or disjoint from each constructor in the column. This avoids |
863 | | -/// non-trivial intersections like between `0..10` and `5..15`. |
| 857 | +/// More formally, if we discard wildcards from the column, this respects the following constraints: |
| 858 | +/// 1. the union of `present` and `missing` covers the whole type |
| 859 | +/// 2. each constructor in `present` is covered by something in the column |
| 860 | +/// 3. no constructor in `missing` is covered by anything in the column |
| 861 | +/// 4. each constructor in the column is equal to the union of one or more constructors in `present` |
| 862 | +/// 5. `missing` does not contain empty constructors (see discussion about emptiness at the top of |
| 863 | +/// the file); |
| 864 | +/// 6. constructors in `present` and `missing` are split for the column; in other words, they are |
| 865 | +/// either fully included in or fully disjoint from each constructor in the column. In other |
| 866 | +/// words, there are no non-trivial intersections like between `0..10` and `5..15`. |
864 | 867 | #[derive(Debug)] |
865 | 868 | pub(super) struct SplitConstructorSet<'tcx> { |
866 | 869 | pub(super) present: SmallVec<[Constructor<'tcx>; 1]>, |
|
0 commit comments