Expand description

super::usefulness explains most of what is happening in this file. As explained there, values and patterns are made from constructors applied to fields. This file defines a Constructor enum, a Fields struct, and various operations to manipulate them and convert them from/to patterns.

There’s one idea that is not detailed in super::usefulness because the details are not needed there: constructor splitting.

Constructor splitting

The idea is as follows: given a constructor c and a matrix, we want to specialize in turn with all the value constructors that are covered by c, and compute usefulness for each. Instead of listing all those constructors (which is intractable), we group those value constructors together as much as possible. Example:

match (0, false) {
    (0 ..=100, true) => {} // `p_1`
    (50..=150, false) => {} // `p_2`
    (0 ..=200, _) => {} // `q`
}

The naive approach would try all numbers in the range 0..=200. But we can be a lot more clever: 0 and 1 for example will match the exact same rows, and return equivalent witnesses. In fact all of 0..50 would. We can thus restrict our exploration to 4 constructors: 0..50, 50..=100, 101..=150 and 151..=200. That is enough and infinitely more tractable.

We capture this idea in a function split(p_1 ... p_n, c) which returns a list of constructors c' covered by c. Given such a c', we require that all value ctors c'' covered by c' return an equivalent set of witnesses after specializing and computing usefulness. In the example above, witnesses for specializing by c'' covered by 0..50 will only differ in their first element.

We usually also ask that the c' together cover all of the original c. However we allow skipping some constructors as long as it doesn’t change whether the resulting list of witnesses is empty of not. We use this in the wildcard _ case.

Splitting is implemented in the Constructor::split function. We don’t do splitting for or-patterns; instead we just try the alternatives one-by-one. For details on splitting wildcards, see SplitWildcard; for integer ranges, see SplitIntRange; for slices, see SplitVarLenSlice.

Structs

  • Values and patterns can be represented as a constructor applied to some fields. This represents a pattern in this form. This also keeps track of whether the pattern has been found reachable during analysis. For this reason we should be careful not to clone patterns for which we care about that. Use clone_and_forget_reachability if you’re sure.
  • Fields 🔒
    A value can be decomposed into a constructor applied to some fields. This struct represents those fields, generalized to allow patterns in each field. See also Constructor.
  • IntRange 🔒
    An inclusive interval, used for precise integer exhaustiveness checking. IntRanges always store a contiguous range. This means that values are encoded such that 0 encodes the minimum value for the integer, regardless of the signedness. For example, the pattern -128..=127i8 is encoded as 0..=255. This makes comparisons and arithmetic on interval endpoints much more straightforward. See signed_bias for details.
  • Slice 🔒
    A constructor for array and slice patterns.
  • A range of integers that is partitioned into disjoint subranges. This does constructor splitting for integer ranges as explained at the top of the file.
  • This computes constructor splitting for variable-length slices, as explained at the top of the file.
  • A wildcard constructor that we split relative to the constructors in the matrix, as explained at the top of the file.

Enums

  • A value can be decomposed into a constructor applied to some fields. This struct represents the constructor. See also Fields.
  • IntBorder 🔒
    Represents a border between 2 integers. Because the intervals spanning borders must be able to cover every integer, we need to be able to represent 2^128 + 1 such borders.
  • SliceKind 🔒

Functions

  • Recursively expand this pattern into its subpatterns. Only useful for or-patterns.