From c7ad3ad99128b904fafb17ee8ee8889bfcaf5170 Mon Sep 17 00:00:00 2001 From: Jonas Schievink Date: Sun, 14 Jun 2020 14:53:36 +0200 Subject: [PATCH] _match.rs: fix module doc comment It was applied to a `use` item, not to the module --- src/librustc_mir_build/hair/pattern/_match.rs | 542 +++++++++--------- 1 file changed, 271 insertions(+), 271 deletions(-) diff --git a/src/librustc_mir_build/hair/pattern/_match.rs b/src/librustc_mir_build/hair/pattern/_match.rs index dc7d8098e55..4a4de6c420b 100644 --- a/src/librustc_mir_build/hair/pattern/_match.rs +++ b/src/librustc_mir_build/hair/pattern/_match.rs @@ -1,274 +1,274 @@ -/// Note: most of the tests relevant to this file can be found (at the time of writing) in -/// src/tests/ui/pattern/usefulness. -/// -/// This file includes the logic for exhaustiveness and usefulness checking for -/// pattern-matching. Specifically, given a list of patterns for a type, we can -/// tell whether: -/// (a) the patterns cover every possible constructor for the type [exhaustiveness] -/// (b) each pattern is necessary [usefulness] -/// -/// The algorithm implemented here is a modified version of the one described in: -/// http://moscova.inria.fr/~maranget/papers/warn/index.html -/// However, to save future implementors from reading the original paper, we -/// summarise the algorithm here to hopefully save time and be a little clearer -/// (without being so rigorous). -/// -/// # Premise -/// -/// The core of the algorithm revolves about a "usefulness" check. In particular, we -/// are trying to compute a predicate `U(P, p)` where `P` is a list of patterns (we refer to this as -/// a matrix). `U(P, p)` represents whether, given an existing list of patterns -/// `P_1 ..= P_m`, adding a new pattern `p` will be "useful" (that is, cover previously- -/// uncovered values of the type). -/// -/// If we have this predicate, then we can easily compute both exhaustiveness of an -/// entire set of patterns and the individual usefulness of each one. -/// (a) the set of patterns is exhaustive iff `U(P, _)` is false (i.e., adding a wildcard -/// match doesn't increase the number of values we're matching) -/// (b) a pattern `P_i` is not useful if `U(P[0..=(i-1), P_i)` is false (i.e., adding a -/// pattern to those that have come before it doesn't increase the number of values -/// we're matching). -/// -/// # Core concept -/// -/// The idea that powers everything that is done in this file is the following: a value is made -/// from a constructor applied to some fields. Examples of constructors are `Some`, `None`, `(,)` -/// (the 2-tuple constructor), `Foo {..}` (the constructor for a struct `Foo`), and `2` (the -/// constructor for the number `2`). Fields are just a (possibly empty) list of values. -/// -/// Some of the constructors listed above might feel weird: `None` and `2` don't take any -/// arguments. This is part of what makes constructors so general: we will consider plain values -/// like numbers and string literals to be constructors that take no arguments, also called "0-ary -/// constructors"; they are the simplest case of constructors. This allows us to see any value as -/// made up from a tree of constructors, each having a given number of children. For example: -/// `(None, Ok(0))` is made from 4 different constructors. -/// -/// This idea can be extended to patterns: a pattern captures a set of possible values, and we can -/// describe this set using constructors. For example, `Err(_)` captures all values of the type -/// `Result` that start with the `Err` constructor (for some choice of `T` and `E`). The -/// wildcard `_` captures all values of the given type starting with any of the constructors for -/// that type. -/// -/// We use this to compute whether different patterns might capture a same value. Do the patterns -/// `Ok("foo")` and `Err(_)` capture a common value? The answer is no, because the first pattern -/// captures only values starting with the `Ok` constructor and the second only values starting -/// with the `Err` constructor. Do the patterns `Some(42)` and `Some(1..10)` intersect? They might, -/// since they both capture values starting with `Some`. To be certain, we need to dig under the -/// `Some` constructor and continue asking the question. This is the main idea behind the -/// exhaustiveness algorithm: by looking at patterns constructor-by-constructor, we can efficiently -/// figure out if some new pattern might capture a value that hadn't been captured by previous -/// patterns. -/// -/// Constructors are represented by the `Constructor` enum, and its fields by the `Fields` enum. -/// Most of the complexity of this file resides in transforming between patterns and -/// (`Constructor`, `Fields`) pairs, handling all the special cases correctly. -/// -/// Caveat: this constructors/fields distinction doesn't quite cover every Rust value. For example -/// a value of type `Rc` doesn't fit this idea very well, nor do various other things. -/// However, this idea covers most of the cases that are relevant to exhaustiveness checking. -/// -/// -/// # Algorithm -/// -/// Recall that `U(P, p)` represents whether, given an existing list of patterns (aka matrix) `P`, -/// adding a new pattern `p` will cover previously-uncovered values of the type. -/// During the course of the algorithm, the rows of the matrix won't just be individual patterns, -/// but rather partially-deconstructed patterns in the form of a list of fields. The paper -/// calls those pattern-vectors, and we will call them pattern-stacks. The same holds for the -/// new pattern `p`. -/// -/// For example, say we have the following: -/// ``` -/// // x: (Option, Result<()>) -/// match x { -/// (Some(true), _) => {} -/// (None, Err(())) => {} -/// (None, Err(_)) => {} -/// } -/// ``` -/// Here, the matrix `P` starts as: -/// [ -/// [(Some(true), _)], -/// [(None, Err(()))], -/// [(None, Err(_))], -/// ] -/// We can tell it's not exhaustive, because `U(P, _)` is true (we're not covering -/// `[(Some(false), _)]`, for instance). In addition, row 3 is not useful, because -/// all the values it covers are already covered by row 2. -/// -/// A list of patterns can be thought of as a stack, because we are mainly interested in the top of -/// the stack at any given point, and we can pop or apply constructors to get new pattern-stacks. -/// To match the paper, the top of the stack is at the beginning / on the left. -/// -/// There are two important operations on pattern-stacks necessary to understand the algorithm: -/// 1. We can pop a given constructor off the top of a stack. This operation is called -/// `specialize`, and is denoted `S(c, p)` where `c` is a constructor (like `Some` or -/// `None`) and `p` a pattern-stack. -/// If the pattern on top of the stack can cover `c`, this removes the constructor and -/// pushes its arguments onto the stack. It also expands OR-patterns into distinct patterns. -/// Otherwise the pattern-stack is discarded. -/// This essentially filters those pattern-stacks whose top covers the constructor `c` and -/// discards the others. -/// -/// For example, the first pattern above initially gives a stack `[(Some(true), _)]`. If we -/// pop the tuple constructor, we are left with `[Some(true), _]`, and if we then pop the -/// `Some` constructor we get `[true, _]`. If we had popped `None` instead, we would get -/// nothing back. -/// -/// This returns zero or more new pattern-stacks, as follows. We look at the pattern `p_1` -/// on top of the stack, and we have four cases: -/// 1.1. `p_1 = c(r_1, .., r_a)`, i.e. the top of the stack has constructor `c`. We -/// push onto the stack the arguments of this constructor, and return the result: -/// r_1, .., r_a, p_2, .., p_n -/// 1.2. `p_1 = c'(r_1, .., r_a')` where `c ≠ c'`. We discard the current stack and -/// return nothing. -/// 1.3. `p_1 = _`. We push onto the stack as many wildcards as the constructor `c` has -/// arguments (its arity), and return the resulting stack: -/// _, .., _, p_2, .., p_n -/// 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting -/// stack: -/// S(c, (r_1, p_2, .., p_n)) -/// S(c, (r_2, p_2, .., p_n)) -/// -/// 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is -/// a pattern-stack. -/// This is used when we know there are missing constructor cases, but there might be -/// existing wildcard patterns, so to check the usefulness of the matrix, we have to check -/// all its *other* components. -/// -/// It is computed as follows. We look at the pattern `p_1` on top of the stack, -/// and we have three cases: -/// 1.1. `p_1 = c(r_1, .., r_a)`. We discard the current stack and return nothing. -/// 1.2. `p_1 = _`. We return the rest of the stack: -/// p_2, .., p_n -/// 1.3. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting -/// stack. -/// D((r_1, p_2, .., p_n)) -/// D((r_2, p_2, .., p_n)) -/// -/// Note that the OR-patterns are not always used directly in Rust, but are used to derive the -/// exhaustive integer matching rules, so they're written here for posterity. -/// -/// Both those operations extend straightforwardly to a list or pattern-stacks, i.e. a matrix, by -/// working row-by-row. Popping a constructor ends up keeping only the matrix rows that start with -/// the given constructor, and popping a wildcard keeps those rows that start with a wildcard. -/// -/// -/// The algorithm for computing `U` -/// ------------------------------- -/// The algorithm is inductive (on the number of columns: i.e., components of tuple patterns). -/// That means we're going to check the components from left-to-right, so the algorithm -/// operates principally on the first component of the matrix and new pattern-stack `p`. -/// This algorithm is realised in the `is_useful` function. -/// -/// Base case. (`n = 0`, i.e., an empty tuple pattern) -/// - If `P` already contains an empty pattern (i.e., if the number of patterns `m > 0`), -/// then `U(P, p)` is false. -/// - Otherwise, `P` must be empty, so `U(P, p)` is true. -/// -/// Inductive step. (`n > 0`, i.e., whether there's at least one column -/// [which may then be expanded into further columns later]) -/// We're going to match on the top of the new pattern-stack, `p_1`. -/// - If `p_1 == c(r_1, .., r_a)`, i.e. we have a constructor pattern. -/// Then, the usefulness of `p_1` can be reduced to whether it is useful when -/// we ignore all the patterns in the first column of `P` that involve other constructors. -/// This is where `S(c, P)` comes in: -/// `U(P, p) := U(S(c, P), S(c, p))` -/// This special case is handled in `is_useful_specialized`. -/// -/// For example, if `P` is: -/// [ -/// [Some(true), _], -/// [None, 0], -/// ] -/// and `p` is [Some(false), 0], then we don't care about row 2 since we know `p` only -/// matches values that row 2 doesn't. For row 1 however, we need to dig into the -/// arguments of `Some` to know whether some new value is covered. So we compute -/// `U([[true, _]], [false, 0])`. -/// -/// - If `p_1 == _`, then we look at the list of constructors that appear in the first -/// component of the rows of `P`: -/// + If there are some constructors that aren't present, then we might think that the -/// wildcard `_` is useful, since it covers those constructors that weren't covered -/// before. -/// That's almost correct, but only works if there were no wildcards in those first -/// components. So we need to check that `p` is useful with respect to the rows that -/// start with a wildcard, if there are any. This is where `D` comes in: -/// `U(P, p) := U(D(P), D(p))` -/// -/// For example, if `P` is: -/// [ -/// [_, true, _], -/// [None, false, 1], -/// ] -/// and `p` is [_, false, _], the `Some` constructor doesn't appear in `P`. So if we -/// only had row 2, we'd know that `p` is useful. However row 1 starts with a -/// wildcard, so we need to check whether `U([[true, _]], [false, 1])`. -/// -/// + Otherwise, all possible constructors (for the relevant type) are present. In this -/// case we must check whether the wildcard pattern covers any unmatched value. For -/// that, we can think of the `_` pattern as a big OR-pattern that covers all -/// possible constructors. For `Option`, that would mean `_ = None | Some(_)` for -/// example. The wildcard pattern is useful in this case if it is useful when -/// specialized to one of the possible constructors. So we compute: -/// `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` -/// -/// For example, if `P` is: -/// [ -/// [Some(true), _], -/// [None, false], -/// ] -/// and `p` is [_, false], both `None` and `Some` constructors appear in the first -/// components of `P`. We will therefore try popping both constructors in turn: we -/// compute U([[true, _]], [_, false]) for the `Some` constructor, and U([[false]], -/// [false]) for the `None` constructor. The first case returns true, so we know that -/// `p` is useful for `P`. Indeed, it matches `[Some(false), _]` that wasn't matched -/// before. -/// -/// - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: -/// `U(P, p) := U(P, (r_1, p_2, .., p_n)) -/// || U(P, (r_2, p_2, .., p_n))` -/// -/// Modifications to the algorithm -/// ------------------------------ -/// The algorithm in the paper doesn't cover some of the special cases that arise in Rust, for -/// example uninhabited types and variable-length slice patterns. These are drawn attention to -/// throughout the code below. I'll make a quick note here about how exhaustive integer matching is -/// accounted for, though. -/// -/// Exhaustive integer matching -/// --------------------------- -/// An integer type can be thought of as a (huge) sum type: 1 | 2 | 3 | ... -/// So to support exhaustive integer matching, we can make use of the logic in the paper for -/// OR-patterns. However, we obviously can't just treat ranges x..=y as individual sums, because -/// they are likely gigantic. So we instead treat ranges as constructors of the integers. This means -/// that we have a constructor *of* constructors (the integers themselves). We then need to work -/// through all the inductive step rules above, deriving how the ranges would be treated as -/// OR-patterns, and making sure that they're treated in the same way even when they're ranges. -/// There are really only four special cases here: -/// - When we match on a constructor that's actually a range, we have to treat it as if we would -/// an OR-pattern. -/// + It turns out that we can simply extend the case for single-value patterns in -/// `specialize` to either be *equal* to a value constructor, or *contained within* a range -/// constructor. -/// + When the pattern itself is a range, you just want to tell whether any of the values in -/// the pattern range coincide with values in the constructor range, which is precisely -/// intersection. -/// Since when encountering a range pattern for a value constructor, we also use inclusion, it -/// means that whenever the constructor is a value/range and the pattern is also a value/range, -/// we can simply use intersection to test usefulness. -/// - When we're testing for usefulness of a pattern and the pattern's first component is a -/// wildcard. -/// + If all the constructors appear in the matrix, we have a slight complication. By default, -/// the behaviour (i.e., a disjunction over specialised matrices for each constructor) is -/// invalid, because we want a disjunction over every *integer* in each range, not just a -/// disjunction over every range. This is a bit more tricky to deal with: essentially we need -/// to form equivalence classes of subranges of the constructor range for which the behaviour -/// of the matrix `P` and new pattern `p` are the same. This is described in more -/// detail in `split_grouped_constructors`. -/// + If some constructors are missing from the matrix, it turns out we don't need to do -/// anything special (because we know none of the integers are actually wildcards: i.e., we -/// can't span wildcards using ranges). +//! Note: most of the tests relevant to this file can be found (at the time of writing) in +//! src/tests/ui/pattern/usefulness. +//! +//! This file includes the logic for exhaustiveness and usefulness checking for +//! pattern-matching. Specifically, given a list of patterns for a type, we can +//! tell whether: +//! (a) the patterns cover every possible constructor for the type [exhaustiveness] +//! (b) each pattern is necessary [usefulness] +//! +//! The algorithm implemented here is a modified version of the one described in: +//! http://moscova.inria.fr/~maranget/papers/warn/index.html +//! However, to save future implementors from reading the original paper, we +//! summarise the algorithm here to hopefully save time and be a little clearer +//! (without being so rigorous). +//! +//! # Premise +//! +//! The core of the algorithm revolves about a "usefulness" check. In particular, we +//! are trying to compute a predicate `U(P, p)` where `P` is a list of patterns (we refer to this as +//! a matrix). `U(P, p)` represents whether, given an existing list of patterns +//! `P_1 ..= P_m`, adding a new pattern `p` will be "useful" (that is, cover previously- +//! uncovered values of the type). +//! +//! If we have this predicate, then we can easily compute both exhaustiveness of an +//! entire set of patterns and the individual usefulness of each one. +//! (a) the set of patterns is exhaustive iff `U(P, _)` is false (i.e., adding a wildcard +//! match doesn't increase the number of values we're matching) +//! (b) a pattern `P_i` is not useful if `U(P[0..=(i-1), P_i)` is false (i.e., adding a +//! pattern to those that have come before it doesn't increase the number of values +//! we're matching). +//! +//! # Core concept +//! +//! The idea that powers everything that is done in this file is the following: a value is made +//! from a constructor applied to some fields. Examples of constructors are `Some`, `None`, `(,)` +//! (the 2-tuple constructor), `Foo {..}` (the constructor for a struct `Foo`), and `2` (the +//! constructor for the number `2`). Fields are just a (possibly empty) list of values. +//! +//! Some of the constructors listed above might feel weird: `None` and `2` don't take any +//! arguments. This is part of what makes constructors so general: we will consider plain values +//! like numbers and string literals to be constructors that take no arguments, also called "0-ary +//! constructors"; they are the simplest case of constructors. This allows us to see any value as +//! made up from a tree of constructors, each having a given number of children. For example: +//! `(None, Ok(0))` is made from 4 different constructors. +//! +//! This idea can be extended to patterns: a pattern captures a set of possible values, and we can +//! describe this set using constructors. For example, `Err(_)` captures all values of the type +//! `Result` that start with the `Err` constructor (for some choice of `T` and `E`). The +//! wildcard `_` captures all values of the given type starting with any of the constructors for +//! that type. +//! +//! We use this to compute whether different patterns might capture a same value. Do the patterns +//! `Ok("foo")` and `Err(_)` capture a common value? The answer is no, because the first pattern +//! captures only values starting with the `Ok` constructor and the second only values starting +//! with the `Err` constructor. Do the patterns `Some(42)` and `Some(1..10)` intersect? They might, +//! since they both capture values starting with `Some`. To be certain, we need to dig under the +//! `Some` constructor and continue asking the question. This is the main idea behind the +//! exhaustiveness algorithm: by looking at patterns constructor-by-constructor, we can efficiently +//! figure out if some new pattern might capture a value that hadn't been captured by previous +//! patterns. +//! +//! Constructors are represented by the `Constructor` enum, and its fields by the `Fields` enum. +//! Most of the complexity of this file resides in transforming between patterns and +//! (`Constructor`, `Fields`) pairs, handling all the special cases correctly. +//! +//! Caveat: this constructors/fields distinction doesn't quite cover every Rust value. For example +//! a value of type `Rc` doesn't fit this idea very well, nor do various other things. +//! However, this idea covers most of the cases that are relevant to exhaustiveness checking. +//! +//! +//! # Algorithm +//! +//! Recall that `U(P, p)` represents whether, given an existing list of patterns (aka matrix) `P`, +//! adding a new pattern `p` will cover previously-uncovered values of the type. +//! During the course of the algorithm, the rows of the matrix won't just be individual patterns, +//! but rather partially-deconstructed patterns in the form of a list of fields. The paper +//! calls those pattern-vectors, and we will call them pattern-stacks. The same holds for the +//! new pattern `p`. +//! +//! For example, say we have the following: +//! ``` +//! // x: (Option, Result<()>) +//! match x { +//! (Some(true), _) => {} +//! (None, Err(())) => {} +//! (None, Err(_)) => {} +//! } +//! ``` +//! Here, the matrix `P` starts as: +//! [ +//! [(Some(true), _)], +//! [(None, Err(()))], +//! [(None, Err(_))], +//! ] +//! We can tell it's not exhaustive, because `U(P, _)` is true (we're not covering +//! `[(Some(false), _)]`, for instance). In addition, row 3 is not useful, because +//! all the values it covers are already covered by row 2. +//! +//! A list of patterns can be thought of as a stack, because we are mainly interested in the top of +//! the stack at any given point, and we can pop or apply constructors to get new pattern-stacks. +//! To match the paper, the top of the stack is at the beginning / on the left. +//! +//! There are two important operations on pattern-stacks necessary to understand the algorithm: +//! 1. We can pop a given constructor off the top of a stack. This operation is called +//! `specialize`, and is denoted `S(c, p)` where `c` is a constructor (like `Some` or +//! `None`) and `p` a pattern-stack. +//! If the pattern on top of the stack can cover `c`, this removes the constructor and +//! pushes its arguments onto the stack. It also expands OR-patterns into distinct patterns. +//! Otherwise the pattern-stack is discarded. +//! This essentially filters those pattern-stacks whose top covers the constructor `c` and +//! discards the others. +//! +//! For example, the first pattern above initially gives a stack `[(Some(true), _)]`. If we +//! pop the tuple constructor, we are left with `[Some(true), _]`, and if we then pop the +//! `Some` constructor we get `[true, _]`. If we had popped `None` instead, we would get +//! nothing back. +//! +//! This returns zero or more new pattern-stacks, as follows. We look at the pattern `p_1` +//! on top of the stack, and we have four cases: +//! 1.1. `p_1 = c(r_1, .., r_a)`, i.e. the top of the stack has constructor `c`. We +//! push onto the stack the arguments of this constructor, and return the result: +//! r_1, .., r_a, p_2, .., p_n +//! 1.2. `p_1 = c'(r_1, .., r_a')` where `c ≠ c'`. We discard the current stack and +//! return nothing. +//! 1.3. `p_1 = _`. We push onto the stack as many wildcards as the constructor `c` has +//! arguments (its arity), and return the resulting stack: +//! _, .., _, p_2, .., p_n +//! 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting +//! stack: +//! S(c, (r_1, p_2, .., p_n)) +//! S(c, (r_2, p_2, .., p_n)) +//! +//! 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is +//! a pattern-stack. +//! This is used when we know there are missing constructor cases, but there might be +//! existing wildcard patterns, so to check the usefulness of the matrix, we have to check +//! all its *other* components. +//! +//! It is computed as follows. We look at the pattern `p_1` on top of the stack, +//! and we have three cases: +//! 1.1. `p_1 = c(r_1, .., r_a)`. We discard the current stack and return nothing. +//! 1.2. `p_1 = _`. We return the rest of the stack: +//! p_2, .., p_n +//! 1.3. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting +//! stack. +//! D((r_1, p_2, .., p_n)) +//! D((r_2, p_2, .., p_n)) +//! +//! Note that the OR-patterns are not always used directly in Rust, but are used to derive the +//! exhaustive integer matching rules, so they're written here for posterity. +//! +//! Both those operations extend straightforwardly to a list or pattern-stacks, i.e. a matrix, by +//! working row-by-row. Popping a constructor ends up keeping only the matrix rows that start with +//! the given constructor, and popping a wildcard keeps those rows that start with a wildcard. +//! +//! +//! The algorithm for computing `U` +//! ------------------------------- +//! The algorithm is inductive (on the number of columns: i.e., components of tuple patterns). +//! That means we're going to check the components from left-to-right, so the algorithm +//! operates principally on the first component of the matrix and new pattern-stack `p`. +//! This algorithm is realised in the `is_useful` function. +//! +//! Base case. (`n = 0`, i.e., an empty tuple pattern) +//! - If `P` already contains an empty pattern (i.e., if the number of patterns `m > 0`), +//! then `U(P, p)` is false. +//! - Otherwise, `P` must be empty, so `U(P, p)` is true. +//! +//! Inductive step. (`n > 0`, i.e., whether there's at least one column +//! [which may then be expanded into further columns later]) +//! We're going to match on the top of the new pattern-stack, `p_1`. +//! - If `p_1 == c(r_1, .., r_a)`, i.e. we have a constructor pattern. +//! Then, the usefulness of `p_1` can be reduced to whether it is useful when +//! we ignore all the patterns in the first column of `P` that involve other constructors. +//! This is where `S(c, P)` comes in: +//! `U(P, p) := U(S(c, P), S(c, p))` +//! This special case is handled in `is_useful_specialized`. +//! +//! For example, if `P` is: +//! [ +//! [Some(true), _], +//! [None, 0], +//! ] +//! and `p` is [Some(false), 0], then we don't care about row 2 since we know `p` only +//! matches values that row 2 doesn't. For row 1 however, we need to dig into the +//! arguments of `Some` to know whether some new value is covered. So we compute +//! `U([[true, _]], [false, 0])`. +//! +//! - If `p_1 == _`, then we look at the list of constructors that appear in the first +//! component of the rows of `P`: +//! + If there are some constructors that aren't present, then we might think that the +//! wildcard `_` is useful, since it covers those constructors that weren't covered +//! before. +//! That's almost correct, but only works if there were no wildcards in those first +//! components. So we need to check that `p` is useful with respect to the rows that +//! start with a wildcard, if there are any. This is where `D` comes in: +//! `U(P, p) := U(D(P), D(p))` +//! +//! For example, if `P` is: +//! [ +//! [_, true, _], +//! [None, false, 1], +//! ] +//! and `p` is [_, false, _], the `Some` constructor doesn't appear in `P`. So if we +//! only had row 2, we'd know that `p` is useful. However row 1 starts with a +//! wildcard, so we need to check whether `U([[true, _]], [false, 1])`. +//! +//! + Otherwise, all possible constructors (for the relevant type) are present. In this +//! case we must check whether the wildcard pattern covers any unmatched value. For +//! that, we can think of the `_` pattern as a big OR-pattern that covers all +//! possible constructors. For `Option`, that would mean `_ = None | Some(_)` for +//! example. The wildcard pattern is useful in this case if it is useful when +//! specialized to one of the possible constructors. So we compute: +//! `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` +//! +//! For example, if `P` is: +//! [ +//! [Some(true), _], +//! [None, false], +//! ] +//! and `p` is [_, false], both `None` and `Some` constructors appear in the first +//! components of `P`. We will therefore try popping both constructors in turn: we +//! compute U([[true, _]], [_, false]) for the `Some` constructor, and U([[false]], +//! [false]) for the `None` constructor. The first case returns true, so we know that +//! `p` is useful for `P`. Indeed, it matches `[Some(false), _]` that wasn't matched +//! before. +//! +//! - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: +//! `U(P, p) := U(P, (r_1, p_2, .., p_n)) +//! || U(P, (r_2, p_2, .., p_n))` +//! +//! Modifications to the algorithm +//! ------------------------------ +//! The algorithm in the paper doesn't cover some of the special cases that arise in Rust, for +//! example uninhabited types and variable-length slice patterns. These are drawn attention to +//! throughout the code below. I'll make a quick note here about how exhaustive integer matching is +//! accounted for, though. +//! +//! Exhaustive integer matching +//! --------------------------- +//! An integer type can be thought of as a (huge) sum type: 1 | 2 | 3 | ... +//! So to support exhaustive integer matching, we can make use of the logic in the paper for +//! OR-patterns. However, we obviously can't just treat ranges x..=y as individual sums, because +//! they are likely gigantic. So we instead treat ranges as constructors of the integers. This means +//! that we have a constructor *of* constructors (the integers themselves). We then need to work +//! through all the inductive step rules above, deriving how the ranges would be treated as +//! OR-patterns, and making sure that they're treated in the same way even when they're ranges. +//! There are really only four special cases here: +//! - When we match on a constructor that's actually a range, we have to treat it as if we would +//! an OR-pattern. +//! + It turns out that we can simply extend the case for single-value patterns in +//! `specialize` to either be *equal* to a value constructor, or *contained within* a range +//! constructor. +//! + When the pattern itself is a range, you just want to tell whether any of the values in +//! the pattern range coincide with values in the constructor range, which is precisely +//! intersection. +//! Since when encountering a range pattern for a value constructor, we also use inclusion, it +//! means that whenever the constructor is a value/range and the pattern is also a value/range, +//! we can simply use intersection to test usefulness. +//! - When we're testing for usefulness of a pattern and the pattern's first component is a +//! wildcard. +//! + If all the constructors appear in the matrix, we have a slight complication. By default, +//! the behaviour (i.e., a disjunction over specialised matrices for each constructor) is +//! invalid, because we want a disjunction over every *integer* in each range, not just a +//! disjunction over every range. This is a bit more tricky to deal with: essentially we need +//! to form equivalence classes of subranges of the constructor range for which the behaviour +//! of the matrix `P` and new pattern `p` are the same. This is described in more +//! detail in `split_grouped_constructors`. +//! + If some constructors are missing from the matrix, it turns out we don't need to do +//! anything special (because we know none of the integers are actually wildcards: i.e., we +//! can't span wildcards using ranges). use self::Constructor::*; use self::SliceKind::*; use self::Usefulness::*;