@@ -403,129 +403,141 @@ impl Slice {
403403 self . kind . arity ( )
404404 }
405405
406- /// The exhaustiveness-checking paper does not include any details on
407- /// checking variable-length slice patterns. However, they may be
408- /// matched by an infinite collection of fixed-length array patterns.
409- ///
410- /// Checking the infinite set directly would take an infinite amount
411- /// of time. However, it turns out that for each finite set of
412- /// patterns `P`, all sufficiently large array lengths are equivalent:
413- ///
414- /// Each slice `s` with a "sufficiently-large" length `l ≥ L` that applies
415- /// to exactly the subset `Pₜ` of `P` can be transformed to a slice
416- /// `sₘ` for each sufficiently-large length `m` that applies to exactly
417- /// the same subset of `P`.
418- ///
419- /// Because of that, each witness for reachability-checking of one
420- /// of the sufficiently-large lengths can be transformed to an
421- /// equally-valid witness of any other length, so we only have
422- /// to check slices of the "minimal sufficiently-large length"
423- /// and less.
424- ///
425- /// Note that the fact that there is a *single* `sₘ` for each `m`
426- /// not depending on the specific pattern in `P` is important: if
427- /// you look at the pair of patterns
428- /// `[true, ..]`
429- /// `[.., false]`
430- /// Then any slice of length ≥1 that matches one of these two
431- /// patterns can be trivially turned to a slice of any
432- /// other length ≥1 that matches them and vice-versa,
433- /// but the slice of length 2 `[false, true]` that matches neither
434- /// of these patterns can't be turned to a slice from length 1 that
435- /// matches neither of these patterns, so we have to consider
436- /// slices from length 2 there.
437- ///
438- /// Now, to see that that length exists and find it, observe that slice
439- /// patterns are either "fixed-length" patterns (`[_, _, _]`) or
440- /// "variable-length" patterns (`[_, .., _]`).
441- ///
442- /// For fixed-length patterns, all slices with lengths *longer* than
443- /// the pattern's length have the same outcome (of not matching), so
444- /// as long as `L` is greater than the pattern's length we can pick
445- /// any `sₘ` from that length and get the same result.
446- ///
447- /// For variable-length patterns, the situation is more complicated,
448- /// because as seen above the precise value of `sₘ` matters.
449- ///
450- /// However, for each variable-length pattern `p` with a prefix of length
451- /// `plₚ` and suffix of length `slₚ`, only the first `plₚ` and the last
452- /// `slₚ` elements are examined.
453- ///
454- /// Therefore, as long as `L` is positive (to avoid concerns about empty
455- /// types), all elements after the maximum prefix length and before
456- /// the maximum suffix length are not examined by any variable-length
457- /// pattern, and therefore can be added/removed without affecting
458- /// them - creating equivalent patterns from any sufficiently-large
459- /// length.
460- ///
461- /// Of course, if fixed-length patterns exist, we must be sure
462- /// that our length is large enough to miss them all, so
463- /// we can pick `L = max(max(FIXED_LEN)+1, max(PREFIX_LEN) + max(SUFFIX_LEN))`
464- ///
465- /// for example, with the above pair of patterns, all elements
466- /// but the first and last can be added/removed, so any
467- /// witness of length ≥2 (say, `[false, false, true]`) can be
468- /// turned to a witness from any other length ≥2.
406+ /// Split this slice, as described at the top of the file.
469407 fn split < ' p , ' tcx > ( self , pcx : PatCtxt < ' _ , ' p , ' tcx > ) -> SmallVec < [ Constructor < ' tcx > ; 1 ] > {
470408 let ( self_prefix, self_suffix) = match self . kind {
471409 VarLen ( self_prefix, self_suffix) => ( self_prefix, self_suffix) ,
472410 _ => return smallvec ! [ Slice ( self ) ] ,
473411 } ;
474412
475- let head_ctors = pcx. matrix . head_ctors ( pcx. cx ) . filter ( |c| !c. is_wildcard ( ) ) ;
413+ let mut split_self = SplitVarLenSlice :: new ( self_prefix, self_suffix, self . array_len ) ;
414+ let slices = pcx. matrix . head_ctors ( pcx. cx ) . filter_map ( |c| c. as_slice ( ) ) . map ( |s| s. kind ) ;
415+ split_self. split ( slices) ;
416+ split_self. iter ( ) . map ( Slice ) . collect ( )
417+ }
476418
477- let mut max_prefix_len = self_prefix;
478- let mut max_suffix_len = self_suffix;
479- let mut max_fixed_len = 0 ;
419+ /// See `Constructor::is_covered_by`
420+ fn is_covered_by ( self , other : Self ) -> bool {
421+ other. kind . covers_length ( self . arity ( ) )
422+ }
423+ }
480424
481- for ctor in head_ctors {
482- if let Slice ( slice) = ctor {
483- match slice. kind {
484- FixedLen ( len) => {
485- max_fixed_len = cmp:: max ( max_fixed_len, len) ;
486- }
487- VarLen ( prefix, suffix) => {
488- max_prefix_len = cmp:: max ( max_prefix_len, prefix) ;
489- max_suffix_len = cmp:: max ( max_suffix_len, suffix) ;
490- }
425+ /// The exhaustiveness-checking paper does not include any details on checking variable-length
426+ /// slice patterns. However, they may be matched by an infinite collection of fixed-length array
427+ /// patterns.
428+ ///
429+ /// Checking the infinite set directly would take an infinite amount of time. However, it turns out
430+ /// that for each finite set of patterns `P`, all sufficiently large array lengths are equivalent:
431+ ///
432+ /// Each slice `s` with a "sufficiently-large" length `l ≥ L` that applies to exactly the subset
433+ /// `Pₜ` of `P` can be transformed to a slice `sₘ` for each sufficiently-large length `m` that
434+ /// applies to exactly the same subset of `P`.
435+ ///
436+ /// Because of that, each witness for reachability-checking of one of the sufficiently-large
437+ /// lengths can be transformed to an equally-valid witness of any other length, so we only have to
438+ /// check slices of the "minimal sufficiently-large length" and less.
439+ ///
440+ /// Note that the fact that there is a *single* `sₘ` for each `m` not depending on the specific
441+ /// pattern in `P` is important: if you look at the pair of patterns `[true, ..]` `[.., false]`
442+ /// Then any slice of length ≥1 that matches one of these two patterns can be trivially turned to a
443+ /// slice of any other length ≥1 that matches them and vice-versa, but the slice of length 2
444+ /// `[false, true]` that matches neither of these patterns can't be turned to a slice from length 1
445+ /// that matches neither of these patterns, so we have to consider slices from length 2 there.
446+ ///
447+ /// Now, to see that that length exists and find it, observe that slice patterns are either
448+ /// "fixed-length" patterns (`[_, _, _]`) or "variable-length" patterns (`[_, .., _]`).
449+ ///
450+ /// For fixed-length patterns, all slices with lengths *longer* than the pattern's length have the
451+ /// same outcome (of not matching), so as long as `L` is greater than the pattern's length we can
452+ /// pick any `sₘ` from that length and get the same result.
453+ ///
454+ /// For variable-length patterns, the situation is more complicated, because as seen above the
455+ /// precise value of `sₘ` matters.
456+ ///
457+ /// However, for each variable-length pattern `p` with a prefix of length `plₚ` and suffix of
458+ /// length `slₚ`, only the first `plₚ` and the last `slₚ` elements are examined.
459+ ///
460+ /// Therefore, as long as `L` is positive (to avoid concerns about empty types), all elements after
461+ /// the maximum prefix length and before the maximum suffix length are not examined by any
462+ /// variable-length pattern, and therefore can be added/removed without affecting them - creating
463+ /// equivalent patterns from any sufficiently-large length.
464+ ///
465+ /// Of course, if fixed-length patterns exist, we must be sure that our length is large enough to
466+ /// miss them all, so we can pick `L = max(max(FIXED_LEN)+1, max(PREFIX_LEN) + max(SUFFIX_LEN))`
467+ ///
468+ /// `max_slice` below will be made to have arity `L`.
469+ ///
470+ /// For example, with the above pair of patterns, all elements but the first and last can be
471+ /// added/removed, so any witness of length ≥2 (say, `[false, false, true]`) can be turned to a
472+ /// witness from any other length ≥2.
473+ #[ derive( Debug ) ]
474+ struct SplitVarLenSlice {
475+ /// If the type is an array, this is its size.
476+ array_len : Option < u64 > ,
477+ /// The arity of the input slice.
478+ arity : u64 ,
479+ /// The smallest slice bigger than any slice seen. `max_slice.arity()` is the length `L`
480+ /// described above.
481+ max_slice : SliceKind ,
482+ }
483+
484+ impl SplitVarLenSlice {
485+ fn new ( prefix : u64 , suffix : u64 , array_len : Option < u64 > ) -> Self {
486+ SplitVarLenSlice { array_len, arity : prefix + suffix, max_slice : VarLen ( prefix, suffix) }
487+ }
488+
489+ /// Pass a set of slices relative to which to split this one.
490+ fn split ( & mut self , slices : impl Iterator < Item = SliceKind > ) {
491+ let ( max_prefix_len, max_suffix_len) = match & mut self . max_slice {
492+ VarLen ( prefix, suffix) => ( prefix, suffix) ,
493+ FixedLen ( _) => return , // No need to split
494+ } ;
495+ // We grow `self.max_slice` to be larger than all slices encountered, as described above.
496+ // For diagnostics, we keep the prefix and suffix lengths separate, but grow them so that
497+ // `L = max_prefix_len + max_suffix_len`.
498+ let mut max_fixed_len = 0 ;
499+ for slice in slices {
500+ match slice {
501+ FixedLen ( len) => {
502+ max_fixed_len = cmp:: max ( max_fixed_len, len) ;
503+ }
504+ VarLen ( prefix, suffix) => {
505+ * max_prefix_len = cmp:: max ( * max_prefix_len, prefix) ;
506+ * max_suffix_len = cmp:: max ( * max_suffix_len, suffix) ;
491507 }
492- } else {
493- bug ! ( "unexpected ctor for slice type: {:?}" , ctor) ;
494508 }
495509 }
496-
497- // For diagnostics, we keep the prefix and suffix lengths separate, so in the case
498- // where `max_fixed_len + 1` is the largest, we adapt `max_prefix_len` accordingly,
499- // so that `L = max_prefix_len + max_suffix_len`.
500- if max_fixed_len + 1 >= max_prefix_len + max_suffix_len {
510+ // We want `L = max(L, max_fixed_len + 1)`, modulo the fact that we keep prefix and
511+ // suffix separate.
512+ if max_fixed_len + 1 >= * max_prefix_len + * max_suffix_len {
501513 // The subtraction can't overflow thanks to the above check.
502- // The new `max_prefix_len` is also guaranteed to be larger than its previous
503- // value.
504- max_prefix_len = max_fixed_len + 1 - max_suffix_len;
514+ // The new `max_prefix_len` is larger than its previous value.
515+ * max_prefix_len = max_fixed_len + 1 - * max_suffix_len;
505516 }
506517
507- let final_slice = VarLen ( max_prefix_len, max_suffix_len) ;
508- let final_slice = Slice :: new ( self . array_len , final_slice) ;
518+ // We cap the arity of `max_slice` at the array size.
509519 match self . array_len {
510- Some ( _) => smallvec ! [ Slice ( final_slice) ] ,
511- None => {
512- // `self` originally covered the range `(self.arity()..infinity)`. We split that
513- // range into two: lengths smaller than `final_slice.arity()` are treated
514- // independently as fixed-lengths slices, and lengths above are captured by
515- // `final_slice`.
516- let smaller_lengths = ( self . arity ( ) ..final_slice. arity ( ) ) . map ( FixedLen ) ;
517- smaller_lengths
518- . map ( |kind| Slice :: new ( self . array_len , kind) )
519- . chain ( Some ( final_slice) )
520- . map ( Slice )
521- . collect ( )
522- }
520+ Some ( len) if self . max_slice . arity ( ) >= len => self . max_slice = FixedLen ( len) ,
521+ _ => { }
523522 }
524523 }
525524
526- /// See `Constructor::is_covered_by`
527- fn is_covered_by ( self , other : Self ) -> bool {
528- other. kind . covers_length ( self . arity ( ) )
525+ /// Iterate over the partition of this slice.
526+ fn iter < ' a > ( & ' a self ) -> impl Iterator < Item = Slice > + Captures < ' a > {
527+ let smaller_lengths = match self . array_len {
528+ // The only admissible fixed-length slice is one of the array size. Whether `max_slice`
529+ // is fixed-length or variable-length, it will be the only relevant slice to output
530+ // here.
531+ Some ( _) => ( 0 ..0 ) , // empty range
532+ // We cover all arities in the range `(self.arity..infinity)`. We split that range into
533+ // two: lengths smaller than `max_slice.arity()` are treated independently as
534+ // fixed-lengths slices, and lengths above are captured by `max_slice`.
535+ None => self . arity ..self . max_slice . arity ( ) ,
536+ } ;
537+ smaller_lengths
538+ . map ( FixedLen )
539+ . chain ( once ( self . max_slice ) )
540+ . map ( move |kind| Slice :: new ( self . array_len , kind) )
529541 }
530542}
531543
0 commit comments