@@ -39,7 +39,7 @@ use syntax_pos::{Span, DUMMY_SP};
3939
4040use arena:: TypedArena ;
4141
42- use std:: cmp:: Ordering ;
42+ use std:: cmp:: { self , Ordering } ;
4343use std:: fmt;
4444use std:: iter:: { FromIterator , IntoIterator , repeat} ;
4545
@@ -419,6 +419,99 @@ fn all_constructors(_cx: &mut MatchCheckCtxt, pcx: PatternContext) -> Vec<Constr
419419 }
420420}
421421
422+ fn max_slice_length < ' a , ' tcx , I > (
423+ _cx : & mut MatchCheckCtxt < ' a , ' tcx > ,
424+ patterns : I ) -> usize
425+ where I : Iterator < Item =& ' a Pattern < ' tcx > >
426+ {
427+ // The exhaustiveness-checking paper does not include any details on
428+ // checking variable-length slice patterns. However, they are matched
429+ // by an infinite collection of fixed-length array patterns.
430+ //
431+ // Checking the infinite set directly would take an infinite amount
432+ // of time. However, it turns out that for each finite set of
433+ // patterns `P`, all sufficiently large array lengths are equivalent:
434+ //
435+ // Each slice `s` with a "sufficiently-large" length `l ≥ L` that applies
436+ // to exactly the subset `Pₜ` of `P` can be transformed to a slice
437+ // `sₘ` for each sufficiently-large length `m` that applies to exactly
438+ // the same subset of `P`.
439+ //
440+ // Because of that, each witness for reachability-checking from one
441+ // of the sufficiently-large lengths can be transformed to an
442+ // equally-valid witness from any other length, so we only have
443+ // to check slice lengths from the "minimal sufficiently-large length"
444+ // and below.
445+ //
446+ // Note that the fact that there is a *single* `sₘ` for each `m`
447+ // not depending on the specific pattern in `P` is important: if
448+ // you look at the pair of patterns
449+ // `[true, ..]`
450+ // `[.., false]`
451+ // Then any slice of length ≥1 that matches one of these two
452+ // patterns can be be trivially turned to a slice of any
453+ // other length ≥1 that matches them and vice-versa - for
454+ // but the slice from length 2 `[false, true]` that matches neither
455+ // of these patterns can't be turned to a slice from length 1 that
456+ // matches neither of these patterns, so we have to consider
457+ // slices from length 2 there.
458+ //
459+ // Now, to see that that length exists and find it, observe that slice
460+ // patterns are either "fixed-length" patterns (`[_, _, _]`) or
461+ // "variable-length" patterns (`[_, .., _]`).
462+ //
463+ // For fixed-length patterns, all slices with lengths *longer* than
464+ // the pattern's length have the same outcome (of not matching), so
465+ // as long as `L` is greater than the pattern's length we can pick
466+ // any `sₘ` from that length and get the same result.
467+ //
468+ // For variable-length patterns, the situation is more complicated,
469+ // because as seen above the precise value of `sₘ` matters.
470+ //
471+ // However, for each variable-length pattern `p` with a prefix of length
472+ // `plₚ` and suffix of length `slₚ`, only the first `plₚ` and the last
473+ // `slₚ` elements are examined.
474+ //
475+ // Therefore, as long as `L` is positive (to avoid concerns about empty
476+ // types), all elements after the maximum prefix length and before
477+ // the maximum suffix length are not examined by any variable-length
478+ // pattern, and therefore can be added/removed without affecting
479+ // them - creating equivalent patterns from any sufficiently-large
480+ // length.
481+ //
482+ // Of course, if fixed-length patterns exist, we must be sure
483+ // that our length is large enough to miss them all, so
484+ // we can pick `L = max(FIXED_LEN+1 ∪ {max(PREFIX_LEN) + max(SUFFIX_LEN)})`
485+ //
486+ // for example, with the above pair of patterns, all elements
487+ // but the first and last can be added/removed, so any
488+ // witness of length ≥2 (say, `[false, false, true]`) can be
489+ // turned to a witness from any other length ≥2.
490+
491+ let mut max_prefix_len = 0 ;
492+ let mut max_suffix_len = 0 ;
493+ let mut max_fixed_len = 0 ;
494+
495+ for row in patterns {
496+ match * row. kind {
497+ PatternKind :: Constant { value : ConstVal :: ByteStr ( ref data) } => {
498+ max_fixed_len = cmp:: max ( max_fixed_len, data. len ( ) ) ;
499+ }
500+ PatternKind :: Slice { ref prefix, slice : None , ref suffix } => {
501+ let fixed_len = prefix. len ( ) + suffix. len ( ) ;
502+ max_fixed_len = cmp:: max ( max_fixed_len, fixed_len) ;
503+ }
504+ PatternKind :: Slice { ref prefix, slice : Some ( _) , ref suffix } => {
505+ max_prefix_len = cmp:: max ( max_prefix_len, prefix. len ( ) ) ;
506+ max_suffix_len = cmp:: max ( max_suffix_len, suffix. len ( ) ) ;
507+ }
508+ _ => { }
509+ }
510+ }
511+
512+ cmp:: max ( max_fixed_len + 1 , max_prefix_len + max_suffix_len)
513+ }
514+
422515/// Algorithm from http://moscova.inria.fr/~maranget/papers/warn/index.html
423516///
424517/// Whether a vector `v` of patterns is 'useful' in relation to a set of such
@@ -453,16 +546,12 @@ pub fn is_useful<'a, 'tcx>(cx: &mut MatchCheckCtxt<'a, 'tcx>,
453546
454547 let & Matrix ( ref rows) = matrix;
455548 assert ! ( rows. iter( ) . all( |r| r. len( ) == v. len( ) ) ) ;
549+
550+
456551 let pcx = PatternContext {
457552 ty : rows. iter ( ) . map ( |r| r[ 0 ] . ty ) . find ( |ty| !ty. references_error ( ) )
458553 . unwrap_or ( v[ 0 ] . ty ) ,
459- max_slice_length : rows. iter ( ) . filter_map ( |row| match * row[ 0 ] . kind {
460- PatternKind :: Slice { ref prefix, slice : _, ref suffix } =>
461- Some ( prefix. len ( ) + suffix. len ( ) ) ,
462- PatternKind :: Constant { value : ConstVal :: ByteStr ( ref data) } =>
463- Some ( data. len ( ) ) ,
464- _ => None
465- } ) . max ( ) . map_or ( 0 , |v| v + 1 )
554+ max_slice_length : max_slice_length ( cx, rows. iter ( ) . map ( |r| r[ 0 ] ) . chain ( Some ( v[ 0 ] ) ) )
466555 } ;
467556
468557 debug ! ( "is_useful_expand_first_col: pcx={:?}, expanding {:?}" , pcx, v[ 0 ] ) ;
0 commit comments