@@ -985,7 +985,6 @@ pub enum WitnessPreference {
985985#[ derive( Copy , Clone , Debug ) ]
986986struct PatCtxt < ' tcx > {
987987 ty : Ty < ' tcx > ,
988- max_slice_length : u64 ,
989988 span : Span ,
990989}
991990
@@ -1143,108 +1142,6 @@ fn all_constructors<'a, 'tcx>(
11431142 ctors
11441143}
11451144
1146- fn max_slice_length < ' p , ' a , ' tcx , I > ( cx : & mut MatchCheckCtxt < ' a , ' tcx > , patterns : I ) -> u64
1147- where
1148- I : Iterator < Item = & ' p Pat < ' tcx > > ,
1149- ' tcx : ' p ,
1150- {
1151- // The exhaustiveness-checking paper does not include any details on
1152- // checking variable-length slice patterns. However, they are matched
1153- // by an infinite collection of fixed-length array patterns.
1154- //
1155- // Checking the infinite set directly would take an infinite amount
1156- // of time. However, it turns out that for each finite set of
1157- // patterns `P`, all sufficiently large array lengths are equivalent:
1158- //
1159- // Each slice `s` with a "sufficiently-large" length `l ≥ L` that applies
1160- // to exactly the subset `Pₜ` of `P` can be transformed to a slice
1161- // `sₘ` for each sufficiently-large length `m` that applies to exactly
1162- // the same subset of `P`.
1163- //
1164- // Because of that, each witness for reachability-checking from one
1165- // of the sufficiently-large lengths can be transformed to an
1166- // equally-valid witness from any other length, so we only have
1167- // to check slice lengths from the "minimal sufficiently-large length"
1168- // and below.
1169- //
1170- // Note that the fact that there is a *single* `sₘ` for each `m`
1171- // not depending on the specific pattern in `P` is important: if
1172- // you look at the pair of patterns
1173- // `[true, ..]`
1174- // `[.., false]`
1175- // Then any slice of length ≥1 that matches one of these two
1176- // patterns can be trivially turned to a slice of any
1177- // other length ≥1 that matches them and vice-versa - for
1178- // but the slice from length 2 `[false, true]` that matches neither
1179- // of these patterns can't be turned to a slice from length 1 that
1180- // matches neither of these patterns, so we have to consider
1181- // slices from length 2 there.
1182- //
1183- // Now, to see that that length exists and find it, observe that slice
1184- // patterns are either "fixed-length" patterns (`[_, _, _]`) or
1185- // "variable-length" patterns (`[_, .., _]`).
1186- //
1187- // For fixed-length patterns, all slices with lengths *longer* than
1188- // the pattern's length have the same outcome (of not matching), so
1189- // as long as `L` is greater than the pattern's length we can pick
1190- // any `sₘ` from that length and get the same result.
1191- //
1192- // For variable-length patterns, the situation is more complicated,
1193- // because as seen above the precise value of `sₘ` matters.
1194- //
1195- // However, for each variable-length pattern `p` with a prefix of length
1196- // `plₚ` and suffix of length `slₚ`, only the first `plₚ` and the last
1197- // `slₚ` elements are examined.
1198- //
1199- // Therefore, as long as `L` is positive (to avoid concerns about empty
1200- // types), all elements after the maximum prefix length and before
1201- // the maximum suffix length are not examined by any variable-length
1202- // pattern, and therefore can be added/removed without affecting
1203- // them - creating equivalent patterns from any sufficiently-large
1204- // length.
1205- //
1206- // Of course, if fixed-length patterns exist, we must be sure
1207- // that our length is large enough to miss them all, so
1208- // we can pick `L = max(FIXED_LEN+1 ∪ {max(PREFIX_LEN) + max(SUFFIX_LEN)})`
1209- //
1210- // for example, with the above pair of patterns, all elements
1211- // but the first and last can be added/removed, so any
1212- // witness of length ≥2 (say, `[false, false, true]`) can be
1213- // turned to a witness from any other length ≥2.
1214-
1215- let mut max_prefix_len = 0 ;
1216- let mut max_suffix_len = 0 ;
1217- let mut max_fixed_len = 0 ;
1218-
1219- for row in patterns {
1220- match * row. kind {
1221- PatKind :: Constant { value } => {
1222- // extract the length of an array/slice from a constant
1223- match ( value. val , & value. ty . kind ) {
1224- ( _, ty:: Array ( _, n) ) => {
1225- max_fixed_len = cmp:: max ( max_fixed_len, n. eval_usize ( cx. tcx , cx. param_env ) )
1226- }
1227- ( ConstValue :: Slice { start, end, .. } , ty:: Slice ( _) ) => {
1228- max_fixed_len = cmp:: max ( max_fixed_len, ( end - start) as u64 )
1229- }
1230- _ => { }
1231- }
1232- }
1233- PatKind :: Slice { ref prefix, slice : None , ref suffix } => {
1234- let fixed_len = prefix. len ( ) as u64 + suffix. len ( ) as u64 ;
1235- max_fixed_len = cmp:: max ( max_fixed_len, fixed_len) ;
1236- }
1237- PatKind :: Slice { ref prefix, slice : Some ( _) , ref suffix } => {
1238- max_prefix_len = cmp:: max ( max_prefix_len, prefix. len ( ) as u64 ) ;
1239- max_suffix_len = cmp:: max ( max_suffix_len, suffix. len ( ) as u64 ) ;
1240- }
1241- _ => { }
1242- }
1243- }
1244-
1245- cmp:: max ( max_fixed_len + 1 , max_prefix_len + max_suffix_len)
1246- }
1247-
12481145/// An inclusive interval, used for precise integer exhaustiveness checking.
12491146/// `IntRange`s always store a contiguous range. This means that values are
12501147/// encoded such that `0` encodes the minimum value for the integer,
@@ -1609,7 +1506,6 @@ pub fn is_useful<'p, 'a, 'tcx>(
16091506 // introducing uninhabited patterns for inaccessible fields. We
16101507 // need to figure out how to model that.
16111508 ty,
1612- max_slice_length : max_slice_length ( cx, matrix. heads ( ) . chain ( Some ( v. head ( ) ) ) ) ,
16131509 span,
16141510 } ;
16151511
@@ -2088,8 +1984,105 @@ fn split_grouped_constructors<'p, 'tcx>(
20881984 split_ctors. push ( IntRange :: range_to_ctor ( tcx, ty, range, span) ) ;
20891985 }
20901986 }
2091- VarLenSlice ( prefix, suffix) => {
2092- split_ctors. extend ( ( prefix + suffix..pcx. max_slice_length + 1 ) . map ( FixedLenSlice ) )
1987+ VarLenSlice ( self_prefix, self_suffix) => {
1988+ // The exhaustiveness-checking paper does not include any details on
1989+ // checking variable-length slice patterns. However, they are matched
1990+ // by an infinite collection of fixed-length array patterns.
1991+ //
1992+ // Checking the infinite set directly would take an infinite amount
1993+ // of time. However, it turns out that for each finite set of
1994+ // patterns `P`, all sufficiently large array lengths are equivalent:
1995+ //
1996+ // Each slice `s` with a "sufficiently-large" length `l ≥ L` that applies
1997+ // to exactly the subset `Pₜ` of `P` can be transformed to a slice
1998+ // `sₘ` for each sufficiently-large length `m` that applies to exactly
1999+ // the same subset of `P`.
2000+ //
2001+ // Because of that, each witness for reachability-checking from one
2002+ // of the sufficiently-large lengths can be transformed to an
2003+ // equally-valid witness from any other length, so we only have
2004+ // to check slice lengths from the "minimal sufficiently-large length"
2005+ // and below.
2006+ //
2007+ // Note that the fact that there is a *single* `sₘ` for each `m`
2008+ // not depending on the specific pattern in `P` is important: if
2009+ // you look at the pair of patterns
2010+ // `[true, ..]`
2011+ // `[.., false]`
2012+ // Then any slice of length ≥1 that matches one of these two
2013+ // patterns can be trivially turned to a slice of any
2014+ // other length ≥1 that matches them and vice-versa - for
2015+ // but the slice from length 2 `[false, true]` that matches neither
2016+ // of these patterns can't be turned to a slice from length 1 that
2017+ // matches neither of these patterns, so we have to consider
2018+ // slices from length 2 there.
2019+ //
2020+ // Now, to see that that length exists and find it, observe that slice
2021+ // patterns are either "fixed-length" patterns (`[_, _, _]`) or
2022+ // "variable-length" patterns (`[_, .., _]`).
2023+ //
2024+ // For fixed-length patterns, all slices with lengths *longer* than
2025+ // the pattern's length have the same outcome (of not matching), so
2026+ // as long as `L` is greater than the pattern's length we can pick
2027+ // any `sₘ` from that length and get the same result.
2028+ //
2029+ // For variable-length patterns, the situation is more complicated,
2030+ // because as seen above the precise value of `sₘ` matters.
2031+ //
2032+ // However, for each variable-length pattern `p` with a prefix of length
2033+ // `plₚ` and suffix of length `slₚ`, only the first `plₚ` and the last
2034+ // `slₚ` elements are examined.
2035+ //
2036+ // Therefore, as long as `L` is positive (to avoid concerns about empty
2037+ // types), all elements after the maximum prefix length and before
2038+ // the maximum suffix length are not examined by any variable-length
2039+ // pattern, and therefore can be added/removed without affecting
2040+ // them - creating equivalent patterns from any sufficiently-large
2041+ // length.
2042+ //
2043+ // Of course, if fixed-length patterns exist, we must be sure
2044+ // that our length is large enough to miss them all, so
2045+ // we can pick `L = max(FIXED_LEN+1 ∪ {max(PREFIX_LEN) + max(SUFFIX_LEN)})`
2046+ //
2047+ // for example, with the above pair of patterns, all elements
2048+ // but the first and last can be added/removed, so any
2049+ // witness of length ≥2 (say, `[false, false, true]`) can be
2050+ // turned to a witness from any other length ≥2.
2051+
2052+ let mut max_prefix_len = self_prefix;
2053+ let mut max_suffix_len = self_suffix;
2054+ let mut max_fixed_len = 0 ;
2055+
2056+ for row in matrix. heads ( ) {
2057+ match * row. kind {
2058+ PatKind :: Constant { value } => {
2059+ // extract the length of an array/slice from a constant
2060+ match ( value. val , & value. ty . kind ) {
2061+ ( _, ty:: Array ( _, n) ) => {
2062+ max_fixed_len =
2063+ cmp:: max ( max_fixed_len, n. eval_usize ( tcx, param_env) )
2064+ }
2065+ ( ConstValue :: Slice { start, end, .. } , ty:: Slice ( _) ) => {
2066+ max_fixed_len = cmp:: max ( max_fixed_len, ( end - start) as u64 )
2067+ }
2068+ _ => { }
2069+ }
2070+ }
2071+ PatKind :: Slice { ref prefix, slice : None , ref suffix } => {
2072+ let fixed_len = prefix. len ( ) as u64 + suffix. len ( ) as u64 ;
2073+ max_fixed_len = cmp:: max ( max_fixed_len, fixed_len) ;
2074+ }
2075+ PatKind :: Slice { ref prefix, slice : Some ( _) , ref suffix } => {
2076+ max_prefix_len = cmp:: max ( max_prefix_len, prefix. len ( ) as u64 ) ;
2077+ max_suffix_len = cmp:: max ( max_suffix_len, suffix. len ( ) as u64 ) ;
2078+ }
2079+ _ => { }
2080+ }
2081+ }
2082+
2083+ let max_slice_length = cmp:: max ( max_fixed_len + 1 , max_prefix_len + max_suffix_len) ;
2084+ split_ctors
2085+ . extend ( ( self_prefix + self_suffix..=max_slice_length) . map ( FixedLenSlice ) )
20932086 }
20942087 // Any other constructor can be used unchanged.
20952088 _ => split_ctors. push ( ctor) ,
0 commit comments