|
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