|
40 | 40 | //! Splitting is implemented in the [`Constructor::split`] function. We don't do splitting for
|
41 | 41 | //! or-patterns; instead we just try the alternatives one-by-one. For details on splitting
|
42 | 42 | //! wildcards, see [`SplitWildcard`]; for integer ranges, see [`IntRange::split`]; for slices, see
|
43 |
| -//! [`SplitVarLenSlice`]. |
| 43 | +//! [`Slice::split`]. |
44 | 44 |
|
45 | 45 | use std::cell::Cell;
|
46 | 46 | use std::cmp::{self, max, min, Ordering};
|
@@ -410,141 +410,130 @@ impl Slice {
|
410 | 410 | fn is_covered_by(self, other: Self) -> bool {
|
411 | 411 | other.kind.covers_length(self.arity())
|
412 | 412 | }
|
413 |
| -} |
414 | 413 |
|
415 |
| -/// This computes constructor splitting for variable-length slices, as explained at the top of the |
416 |
| -/// file. |
417 |
| -/// |
418 |
| -/// A slice pattern `[x, .., y]` behaves like the infinite or-pattern `[x, y] | [x, _, y] | [x, _, |
419 |
| -/// _, y] | ...`. The corresponding value constructors are fixed-length array constructors above a |
420 |
| -/// given minimum length. We obviously can't list this infinitude of constructors. Thankfully, |
421 |
| -/// it turns out that for each finite set of slice patterns, all sufficiently large array lengths |
422 |
| -/// are equivalent. |
423 |
| -/// |
424 |
| -/// Let's look at an example, where we are trying to split the last pattern: |
425 |
| -/// ``` |
426 |
| -/// # fn foo(x: &[bool]) { |
427 |
| -/// match x { |
428 |
| -/// [true, true, ..] => {} |
429 |
| -/// [.., false, false] => {} |
430 |
| -/// [..] => {} |
431 |
| -/// } |
432 |
| -/// # } |
433 |
| -/// ``` |
434 |
| -/// Here are the results of specialization for the first few lengths: |
435 |
| -/// ``` |
436 |
| -/// # fn foo(x: &[bool]) { match x { |
437 |
| -/// // length 0 |
438 |
| -/// [] => {} |
439 |
| -/// // length 1 |
440 |
| -/// [_] => {} |
441 |
| -/// // length 2 |
442 |
| -/// [true, true] => {} |
443 |
| -/// [false, false] => {} |
444 |
| -/// [_, _] => {} |
445 |
| -/// // length 3 |
446 |
| -/// [true, true, _ ] => {} |
447 |
| -/// [_, false, false] => {} |
448 |
| -/// [_, _, _ ] => {} |
449 |
| -/// // length 4 |
450 |
| -/// [true, true, _, _ ] => {} |
451 |
| -/// [_, _, false, false] => {} |
452 |
| -/// [_, _, _, _ ] => {} |
453 |
| -/// // length 5 |
454 |
| -/// [true, true, _, _, _ ] => {} |
455 |
| -/// [_, _, _, false, false] => {} |
456 |
| -/// [_, _, _, _, _ ] => {} |
457 |
| -/// # _ => {} |
458 |
| -/// # }} |
459 |
| -/// ``` |
460 |
| -/// |
461 |
| -/// If we went above length 5, we would simply be inserting more columns full of wildcards in the |
462 |
| -/// middle. This means that the set of witnesses for length `l >= 5` if equivalent to the set for |
463 |
| -/// any other `l' >= 5`: simply add or remove wildcards in the middle to convert between them. |
464 |
| -/// |
465 |
| -/// This applies to any set of slice patterns: there will be a length `L` above which all lengths |
466 |
| -/// behave the same. This is exactly what we need for constructor splitting. Therefore a |
467 |
| -/// variable-length slice can be split into a variable-length slice of minimal length `L`, and many |
468 |
| -/// fixed-length slices of lengths `< L`. |
469 |
| -/// |
470 |
| -/// For each variable-length pattern `p` with a prefix of length `plₚ` and suffix of length `slₚ`, |
471 |
| -/// only the first `plₚ` and the last `slₚ` elements are examined. Therefore, as long as `L` is |
472 |
| -/// positive (to avoid concerns about empty types), all elements after the maximum prefix length |
473 |
| -/// and before the maximum suffix length are not examined by any variable-length pattern, and |
474 |
| -/// therefore can be added/removed without affecting them - creating equivalent patterns from any |
475 |
| -/// sufficiently-large length. |
476 |
| -/// |
477 |
| -/// Of course, if fixed-length patterns exist, we must be sure that our length is large enough to |
478 |
| -/// miss them all, so we can pick `L = max(max(FIXED_LEN)+1, max(PREFIX_LEN) + max(SUFFIX_LEN))` |
479 |
| -/// |
480 |
| -/// `max_slice` below will be made to have arity `L`. |
481 |
| -#[derive(Debug)] |
482 |
| -struct SplitVarLenSlice { |
483 |
| - /// If the type is an array, this is its size. |
484 |
| - array_len: Option<usize>, |
485 |
| - /// The arity of the input slice. |
486 |
| - arity: usize, |
487 |
| - /// The smallest slice bigger than any slice seen. `max_slice.arity()` is the length `L` |
488 |
| - /// described above. |
489 |
| - max_slice: SliceKind, |
490 |
| -} |
491 |
| - |
492 |
| -impl SplitVarLenSlice { |
493 |
| - fn new(prefix: usize, suffix: usize, array_len: Option<usize>) -> Self { |
494 |
| - SplitVarLenSlice { array_len, arity: prefix + suffix, max_slice: VarLen(prefix, suffix) } |
495 |
| - } |
496 |
| - |
497 |
| - /// Pass a set of slices relative to which to split this one. |
498 |
| - fn split(&mut self, slices: impl Iterator<Item = SliceKind>) { |
499 |
| - let VarLen(max_prefix_len, max_suffix_len) = &mut self.max_slice else { |
500 |
| - // No need to split |
501 |
| - return; |
502 |
| - }; |
503 |
| - // We grow `self.max_slice` to be larger than all slices encountered, as described above. |
504 |
| - // For diagnostics, we keep the prefix and suffix lengths separate, but grow them so that |
505 |
| - // `L = max_prefix_len + max_suffix_len`. |
506 |
| - let mut max_fixed_len = 0; |
507 |
| - for slice in slices { |
508 |
| - match slice { |
509 |
| - FixedLen(len) => { |
510 |
| - max_fixed_len = cmp::max(max_fixed_len, len); |
| 414 | + /// This computes constructor splitting for variable-length slices, as explained at the top of |
| 415 | + /// the file. |
| 416 | + /// |
| 417 | + /// A slice pattern `[x, .., y]` behaves like the infinite or-pattern `[x, y] | [x, _, y] | [x, |
| 418 | + /// _, _, y] | etc`. The corresponding value constructors are fixed-length array constructors of |
| 419 | + /// corresponding lengths. We obviously can't list this infinitude of constructors. |
| 420 | + /// Thankfully, it turns out that for each finite set of slice patterns, all sufficiently large |
| 421 | + /// array lengths are equivalent. |
| 422 | + /// |
| 423 | + /// Let's look at an example, where we are trying to split the last pattern: |
| 424 | + /// ``` |
| 425 | + /// # fn foo(x: &[bool]) { |
| 426 | + /// match x { |
| 427 | + /// [true, true, ..] => {} |
| 428 | + /// [.., false, false] => {} |
| 429 | + /// [..] => {} // `self` |
| 430 | + /// } |
| 431 | + /// # } |
| 432 | + /// ``` |
| 433 | + /// Here are the results of specialization for the first few lengths: |
| 434 | + /// ``` |
| 435 | + /// # fn foo(x: &[bool]) { match x { |
| 436 | + /// // length 0 |
| 437 | + /// [] => {} |
| 438 | + /// // length 1 |
| 439 | + /// [_] => {} |
| 440 | + /// // length 2 |
| 441 | + /// [true, true] => {} |
| 442 | + /// [false, false] => {} |
| 443 | + /// [_, _] => {} |
| 444 | + /// // length 3 |
| 445 | + /// [true, true, _ ] => {} |
| 446 | + /// [_, false, false] => {} |
| 447 | + /// [_, _, _ ] => {} |
| 448 | + /// // length 4 |
| 449 | + /// [true, true, _, _ ] => {} |
| 450 | + /// [_, _, false, false] => {} |
| 451 | + /// [_, _, _, _ ] => {} |
| 452 | + /// // length 5 |
| 453 | + /// [true, true, _, _, _ ] => {} |
| 454 | + /// [_, _, _, false, false] => {} |
| 455 | + /// [_, _, _, _, _ ] => {} |
| 456 | + /// # _ => {} |
| 457 | + /// # }} |
| 458 | + /// ``` |
| 459 | + /// |
| 460 | + /// We see that above length 4, we are simply inserting columns full of wildcards in the middle. |
| 461 | + /// This means that specialization and witness computation with slices of length `l >= 4` will |
| 462 | + /// give equivalent results independently of `l`. This applies to any set of slice patterns: |
| 463 | + /// there will be a length `L` above which all lengths behave the same. This is exactly what we |
| 464 | + /// need for constructor splitting. |
| 465 | + /// |
| 466 | + /// A variable-length slice pattern covers all lengths from its arity up to infinity. As we just |
| 467 | + /// saw, we can split this in two: lengths below `L` are treated individually with a |
| 468 | + /// fixed-length slice each; lengths above `L` are grouped into a single variable-length slice |
| 469 | + /// constructor. |
| 470 | + /// |
| 471 | + /// For each variable-length slice pattern `p` with a prefix of length `plₚ` and suffix of |
| 472 | + /// length `slₚ`, only the first `plₚ` and the last `slₚ` elements are examined. Therefore, as |
| 473 | + /// long as `L` is positive (to avoid concerns about empty types), all elements after the |
| 474 | + /// maximum prefix length and before the maximum suffix length are not examined by any |
| 475 | + /// variable-length pattern, and therefore can be ignored. This gives us a way to compute `L`. |
| 476 | + /// |
| 477 | + /// Additionally, if fixed-length patterns exist, we must pick an `L` large enough to miss them, |
| 478 | + /// so we can pick `L = max(max(FIXED_LEN)+1, max(PREFIX_LEN) + max(SUFFIX_LEN))`. |
| 479 | + /// `max_slice` below will be made to have this arity `L`. |
| 480 | + /// |
| 481 | + /// If `self` is fixed-length, it is returned as-is. |
| 482 | + fn split(self, column_slices: impl Iterator<Item = Slice>) -> impl Iterator<Item = Slice> { |
| 483 | + // Range of lengths below `L`. |
| 484 | + let smaller_lengths; |
| 485 | + let mut max_slice = self.kind; |
| 486 | + match &mut max_slice { |
| 487 | + VarLen(max_prefix_len, max_suffix_len) => { |
| 488 | + // We grow `max_slice` to be larger than all slices encountered, as described above. |
| 489 | + // For diagnostics, we keep the prefix and suffix lengths separate, but grow them so that |
| 490 | + // `L = max_prefix_len + max_suffix_len`. |
| 491 | + let mut max_fixed_len = 0; |
| 492 | + for slice in column_slices { |
| 493 | + match slice.kind { |
| 494 | + FixedLen(len) => { |
| 495 | + max_fixed_len = cmp::max(max_fixed_len, len); |
| 496 | + } |
| 497 | + VarLen(prefix, suffix) => { |
| 498 | + *max_prefix_len = cmp::max(*max_prefix_len, prefix); |
| 499 | + *max_suffix_len = cmp::max(*max_suffix_len, suffix); |
| 500 | + } |
| 501 | + } |
511 | 502 | }
|
512 |
| - VarLen(prefix, suffix) => { |
513 |
| - *max_prefix_len = cmp::max(*max_prefix_len, prefix); |
514 |
| - *max_suffix_len = cmp::max(*max_suffix_len, suffix); |
| 503 | + // We want `L = max(L, max_fixed_len + 1)`, modulo the fact that we keep prefix and |
| 504 | + // suffix separate. |
| 505 | + if max_fixed_len + 1 >= *max_prefix_len + *max_suffix_len { |
| 506 | + // The subtraction can't overflow thanks to the above check. |
| 507 | + // The new `max_prefix_len` is larger than its previous value. |
| 508 | + *max_prefix_len = max_fixed_len + 1 - *max_suffix_len; |
515 | 509 | }
|
516 |
| - } |
517 |
| - } |
518 |
| - // We want `L = max(L, max_fixed_len + 1)`, modulo the fact that we keep prefix and |
519 |
| - // suffix separate. |
520 |
| - if max_fixed_len + 1 >= *max_prefix_len + *max_suffix_len { |
521 |
| - // The subtraction can't overflow thanks to the above check. |
522 |
| - // The new `max_prefix_len` is larger than its previous value. |
523 |
| - *max_prefix_len = max_fixed_len + 1 - *max_suffix_len; |
524 |
| - } |
525 | 510 |
|
526 |
| - // We cap the arity of `max_slice` at the array size. |
527 |
| - match self.array_len { |
528 |
| - Some(len) if self.max_slice.arity() >= len => self.max_slice = FixedLen(len), |
529 |
| - _ => {} |
530 |
| - } |
531 |
| - } |
| 511 | + // We cap the arity of `max_slice` at the array size. |
| 512 | + match self.array_len { |
| 513 | + Some(len) if max_slice.arity() >= len => max_slice = FixedLen(len), |
| 514 | + _ => {} |
| 515 | + } |
532 | 516 |
|
533 |
| - /// Iterate over the partition of this slice. |
534 |
| - fn iter(&self) -> impl Iterator<Item = Slice> + Captures<'_> { |
535 |
| - let smaller_lengths = match self.array_len { |
536 |
| - // The only admissible fixed-length slice is one of the array size. Whether `max_slice` |
537 |
| - // is fixed-length or variable-length, it will be the only relevant slice to output |
538 |
| - // here. |
539 |
| - Some(_) => 0..0, // empty range |
540 |
| - // We cover all arities in the range `(self.arity..infinity)`. We split that range into |
541 |
| - // two: lengths smaller than `max_slice.arity()` are treated independently as |
542 |
| - // fixed-lengths slices, and lengths above are captured by `max_slice`. |
543 |
| - None => self.arity..self.max_slice.arity(), |
| 517 | + smaller_lengths = match self.array_len { |
| 518 | + // The only admissible fixed-length slice is one of the array size. Whether `max_slice` |
| 519 | + // is fixed-length or variable-length, it will be the only relevant slice to output |
| 520 | + // here. |
| 521 | + Some(_) => 0..0, // empty range |
| 522 | + // We need to cover all arities in the range `(arity..infinity)`. We split that |
| 523 | + // range into two: lengths smaller than `max_slice.arity()` are treated |
| 524 | + // independently as fixed-lengths slices, and lengths above are captured by |
| 525 | + // `max_slice`. |
| 526 | + None => self.arity()..max_slice.arity(), |
| 527 | + }; |
| 528 | + } |
| 529 | + FixedLen(_) => { |
| 530 | + // No need to split. |
| 531 | + smaller_lengths = 0..0; |
| 532 | + } |
544 | 533 | };
|
545 | 534 | smaller_lengths
|
546 | 535 | .map(FixedLen)
|
547 |
| - .chain(once(self.max_slice)) |
| 536 | + .chain(once(max_slice)) |
548 | 537 | .map(move |kind| Slice::new(self.array_len, kind))
|
549 | 538 | }
|
550 | 539 | }
|
@@ -716,11 +705,9 @@ impl<'tcx> Constructor<'tcx> {
|
716 | 705 | let int_ranges = ctors.filter_map(|ctor| ctor.as_int_range()).cloned();
|
717 | 706 | ctor_range.split(int_ranges).map(IntRange).collect()
|
718 | 707 | }
|
719 |
| - &Slice(Slice { kind: VarLen(self_prefix, self_suffix), array_len }) => { |
720 |
| - let mut split_self = SplitVarLenSlice::new(self_prefix, self_suffix, array_len); |
721 |
| - let slices = ctors.filter_map(|c| c.as_slice()).map(|s| s.kind); |
722 |
| - split_self.split(slices); |
723 |
| - split_self.iter().map(Slice).collect() |
| 708 | + &Slice(slice @ Slice { kind: VarLen(..), .. }) => { |
| 709 | + let slices = ctors.filter_map(|c| c.as_slice()); |
| 710 | + slice.split(slices).map(Slice).collect() |
724 | 711 | }
|
725 | 712 | // Any other constructor can be used unchanged.
|
726 | 713 | _ => smallvec![self.clone()],
|
|
0 commit comments