nordic-dev.net/rust
nordic-dev.net/rust
2
0
Fork 0
mirror of https://github.com/rust-lang/rust.git synced 2025-05-14 02:49:40 +00:00
Code Issues Packages Projects Releases Wiki Activity

_match.rs: fix module doc comment

Browse Source 
It was applied to a `use` item, not to the module
This commit is contained in:
Jonas Schievink 2020-06-14 14:53:36 +02:00
parent 06e47688bf
commit c7ad3ad991
1 changed files with 271 additions and 271 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

542
src/librustc_mir_build/hair/pattern/_match.rs
View File

@ -1,274 +1,274 @@
/// Note: most of the tests relevant to this file can be found (at the time of writing) in //! Note: most of the tests relevant to this file can be found (at the time of writing) in
/// src/tests/ui/pattern/usefulness. //! src/tests/ui/pattern/usefulness.
/// //!
/// This file includes the logic for exhaustiveness and usefulness checking for //! This file includes the logic for exhaustiveness and usefulness checking for
/// pattern-matching. Specifically, given a list of patterns for a type, we can //! pattern-matching. Specifically, given a list of patterns for a type, we can
/// tell whether: //! tell whether:
/// (a) the patterns cover every possible constructor for the type [exhaustiveness] //! (a) the patterns cover every possible constructor for the type [exhaustiveness]
/// (b) each pattern is necessary [usefulness] //! (b) each pattern is necessary [usefulness]
/// //!
/// The algorithm implemented here is a modified version of the one described in: //! The algorithm implemented here is a modified version of the one described in:
/// http://moscova.inria.fr/~maranget/papers/warn/index.html //! http://moscova.inria.fr/~maranget/papers/warn/index.html
/// However, to save future implementors from reading the original paper, we //! However, to save future implementors from reading the original paper, we
/// summarise the algorithm here to hopefully save time and be a little clearer //! summarise the algorithm here to hopefully save time and be a little clearer
/// (without being so rigorous). //! (without being so rigorous).
/// //!
/// # Premise //! # Premise
/// //!
/// The core of the algorithm revolves about a "usefulness" check. In particular, we //! 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 //! 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 //! 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- //! `P_1 ..= P_m`, adding a new pattern `p` will be "useful" (that is, cover previously-
/// uncovered values of the type). //! uncovered values of the type).
/// //!
/// If we have this predicate, then we can easily compute both exhaustiveness of an //! 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. //! 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 //! (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) //! 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 //! (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 //! pattern to those that have come before it doesn't increase the number of values
/// we're matching). //! we're matching).
/// //!
/// # Core concept //! # Core concept
/// //!
/// The idea that powers everything that is done in this file is the following: a value is made //! 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`, `(,)` //! 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 //! (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. //! 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 //! 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 //! 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 //! 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 //! 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: //! 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. //! `(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 //! 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 //! describe this set using constructors. For example, `Err(_)` captures all values of the type
/// `Result<T, E>` that start with the `Err` constructor (for some choice of `T` and `E`). The //! `Result<T, E>` 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 //! wildcard `_` captures all values of the given type starting with any of the constructors for
/// that type. //! that type.
/// //!
/// We use this to compute whether different patterns might capture a same value. Do the patterns //! 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 //! `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 //! 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, //! 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 //! 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 //! `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 //! 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 //! figure out if some new pattern might capture a value that hadn't been captured by previous
/// patterns. //! patterns.
/// //!
/// Constructors are represented by the `Constructor` enum, and its fields by the `Fields` enum. //! 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 //! Most of the complexity of this file resides in transforming between patterns and
/// (`Constructor`, `Fields`) pairs, handling all the special cases correctly. //! (`Constructor`, `Fields`) pairs, handling all the special cases correctly.
/// //!
/// Caveat: this constructors/fields distinction doesn't quite cover every Rust value. For example //! Caveat: this constructors/fields distinction doesn't quite cover every Rust value. For example
/// a value of type `Rc<u64>` doesn't fit this idea very well, nor do various other things. //! a value of type `Rc<u64>` 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. //! However, this idea covers most of the cases that are relevant to exhaustiveness checking.
/// //!
/// //!
/// # Algorithm //! # Algorithm
/// //!
/// Recall that `U(P, p)` represents whether, given an existing list of patterns (aka matrix) `P`, //! 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. //! 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, //! 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 //! 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 //! calls those pattern-vectors, and we will call them pattern-stacks. The same holds for the
/// new pattern `p`. //! new pattern `p`.
/// //!
/// For example, say we have the following: //! For example, say we have the following:
/// ``` //! ```
/// // x: (Option<bool>, Result<()>) //! // x: (Option<bool>, Result<()>)
/// match x { //! match x {
/// (Some(true), _) => {} //! (Some(true), _) => {}
/// (None, Err(())) => {} //! (None, Err(())) => {}
/// (None, Err(_)) => {} //! (None, Err(_)) => {}
/// } //! }
/// ``` //! ```
/// Here, the matrix `P` starts as: //! Here, the matrix `P` starts as:
/// [ //! [
/// [(Some(true), _)], //! [(Some(true), _)],
/// [(None, Err(()))], //! [(None, Err(()))],
/// [(None, Err(_))], //! [(None, Err(_))],
/// ] //! ]
/// We can tell it's not exhaustive, because `U(P, _)` is true (we're not covering //! 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 //! `[(Some(false), _)]`, for instance). In addition, row 3 is not useful, because
/// all the values it covers are already covered by row 2. //! 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 //! 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. //! 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. //! 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: //! 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 //! 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 //! `specialize`, and is denoted `S(c, p)` where `c` is a constructor (like `Some` or
/// `None`) and `p` a pattern-stack. //! `None`) and `p` a pattern-stack.
/// If the pattern on top of the stack can cover `c`, this removes the constructor and //! 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. //! pushes its arguments onto the stack. It also expands OR-patterns into distinct patterns.
/// Otherwise the pattern-stack is discarded. //! Otherwise the pattern-stack is discarded.
/// This essentially filters those pattern-stacks whose top covers the constructor `c` and //! This essentially filters those pattern-stacks whose top covers the constructor `c` and
/// discards the others. //! discards the others.
/// //!
/// For example, the first pattern above initially gives a stack `[(Some(true), _)]`. If we //! 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 //! 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 //! `Some` constructor we get `[true, _]`. If we had popped `None` instead, we would get
/// nothing back. //! nothing back.
/// //!
/// This returns zero or more new pattern-stacks, as follows. We look at the pattern `p_1` //! 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: //! 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 //! 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: //! push onto the stack the arguments of this constructor, and return the result:
/// r_1, .., r_a, p_2, .., p_n //! 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 //! 1.2. `p_1 = c'(r_1, .., r_a')` where `c ≠ c'`. We discard the current stack and
/// return nothing. //! return nothing.
/// 1.3. `p_1 = _`. We push onto the stack as many wildcards as the constructor `c` has //! 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: //! arguments (its arity), and return the resulting stack:
/// _, .., _, p_2, .., p_n //! _, .., _, p_2, .., p_n
/// 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting //! 1.4. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting
/// stack: //! stack:
/// S(c, (r_1, p_2, .., p_n)) //! S(c, (r_1, p_2, .., p_n))
/// S(c, (r_2, 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 //! 2. We can pop a wildcard off the top of the stack. This is called `D(p)`, where `p` is
/// a pattern-stack. //! a pattern-stack.
/// This is used when we know there are missing constructor cases, but there might be //! 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 //! existing wildcard patterns, so to check the usefulness of the matrix, we have to check
/// all its *other* components. //! all its *other* components.
/// //!
/// It is computed as follows. We look at the pattern `p_1` on top of the stack, //! It is computed as follows. We look at the pattern `p_1` on top of the stack,
/// and we have three cases: //! and we have three cases:
/// 1.1. `p_1 = c(r_1, .., r_a)`. We discard the current stack and return nothing. //! 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: //! 1.2. `p_1 = _`. We return the rest of the stack:
/// p_2, .., p_n //! p_2, .., p_n
/// 1.3. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting //! 1.3. `p_1 = r_1 | r_2`. We expand the OR-pattern and then recurse on each resulting
/// stack. //! stack.
/// D((r_1, p_2, .., p_n)) //! D((r_1, p_2, .., p_n))
/// D((r_2, 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 //! 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. //! 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 //! 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 //! 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 given constructor, and popping a wildcard keeps those rows that start with a wildcard.
/// //!
/// //!
/// The algorithm for computing `U` //! The algorithm for computing `U`
/// ------------------------------- //! -------------------------------
/// The algorithm is inductive (on the number of columns: i.e., components of tuple patterns). //! 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 //! 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`. //! operates principally on the first component of the matrix and new pattern-stack `p`.
/// This algorithm is realised in the `is_useful` function. //! This algorithm is realised in the `is_useful` function.
/// //!
/// Base case. (`n = 0`, i.e., an empty tuple pattern) //! 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`), //! - If `P` already contains an empty pattern (i.e., if the number of patterns `m > 0`),
/// then `U(P, p)` is false. //! then `U(P, p)` is false.
/// - Otherwise, `P` must be empty, so `U(P, p)` is true. //! - Otherwise, `P` must be empty, so `U(P, p)` is true.
/// //!
/// Inductive step. (`n > 0`, i.e., whether there's at least one column //! Inductive step. (`n > 0`, i.e., whether there's at least one column
/// [which may then be expanded into further columns later]) //! [which may then be expanded into further columns later])
/// We're going to match on the top of the new pattern-stack, `p_1`. //! 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. //! - 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 //! 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. //! we ignore all the patterns in the first column of `P` that involve other constructors.
/// This is where `S(c, P)` comes in: //! This is where `S(c, P)` comes in:
/// `U(P, p) := U(S(c, P), S(c, p))` //! `U(P, p) := U(S(c, P), S(c, p))`
/// This special case is handled in `is_useful_specialized`. //! This special case is handled in `is_useful_specialized`.
/// //!
/// For example, if `P` is: //! For example, if `P` is:
/// [ //! [
/// [Some(true), _], //! [Some(true), _],
/// [None, 0], //! [None, 0],
/// ] //! ]
/// and `p` is [Some(false), 0], then we don't care about row 2 since we know `p` only //! 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 //! 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 //! arguments of `Some` to know whether some new value is covered. So we compute
/// `U([[true, _]], [false, 0])`. //! `U([[true, _]], [false, 0])`.
/// //!
/// - If `p_1 == _`, then we look at the list of constructors that appear in the first //! - If `p_1 == _`, then we look at the list of constructors that appear in the first
/// component of the rows of `P`: //! component of the rows of `P`:
/// + If there are some constructors that aren't present, then we might think that the //! + 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 //! wildcard `_` is useful, since it covers those constructors that weren't covered
/// before. //! before.
/// That's almost correct, but only works if there were no wildcards in those first //! 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 //! 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: //! start with a wildcard, if there are any. This is where `D` comes in:
/// `U(P, p) := U(D(P), D(p))` //! `U(P, p) := U(D(P), D(p))`
/// //!
/// For example, if `P` is: //! For example, if `P` is:
/// [ //! [
/// [_, true, _], //! [_, true, _],
/// [None, false, 1], //! [None, false, 1],
/// ] //! ]
/// and `p` is [_, false, _], the `Some` constructor doesn't appear in `P`. So if we //! 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 //! 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])`. //! wildcard, so we need to check whether `U([[true, _]], [false, 1])`.
/// //!
/// + Otherwise, all possible constructors (for the relevant type) are present. In this //! + 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 //! 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 //! 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 //! possible constructors. For `Option`, that would mean `_ = None | Some(_)` for
/// example. The wildcard pattern is useful in this case if it is useful when //! example. The wildcard pattern is useful in this case if it is useful when
/// specialized to one of the possible constructors. So we compute: //! specialized to one of the possible constructors. So we compute:
/// `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))` //! `U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))`
/// //!
/// For example, if `P` is: //! For example, if `P` is:
/// [ //! [
/// [Some(true), _], //! [Some(true), _],
/// [None, false], //! [None, false],
/// ] //! ]
/// and `p` is [_, false], both `None` and `Some` constructors appear in the first //! 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 //! components of `P`. We will therefore try popping both constructors in turn: we
/// compute U([[true, _]], [_, false]) for the `Some` constructor, and U([[false]], //! 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 //! [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 //! `p` is useful for `P`. Indeed, it matches `[Some(false), _]` that wasn't matched
/// before. //! before.
/// //!
/// - If `p_1 == r_1 | r_2`, then the usefulness depends on each `r_i` separately: //! - 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, p) := U(P, (r_1, p_2, .., p_n))
/// || U(P, (r_2, p_2, .., p_n))` //! || U(P, (r_2, p_2, .., p_n))`
/// //!
/// Modifications to the algorithm //! Modifications to the algorithm
/// ------------------------------ //! ------------------------------
/// The algorithm in the paper doesn't cover some of the special cases that arise in Rust, for //! 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 //! 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 //! throughout the code below. I'll make a quick note here about how exhaustive integer matching is
/// accounted for, though. //! accounted for, though.
/// //!
/// Exhaustive integer matching //! Exhaustive integer matching
/// --------------------------- //! ---------------------------
/// An integer type can be thought of as a (huge) sum type: 1 | 2 | 3 | ... //! 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 //! 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 //! 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 //! 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 //! 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 //! 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. //! 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: //! 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 //! - When we match on a constructor that's actually a range, we have to treat it as if we would
/// an OR-pattern. //! an OR-pattern.
/// + It turns out that we can simply extend the case for single-value patterns in //! + 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 //! `specialize` to either be *equal* to a value constructor, or *contained within* a range
/// constructor. //! constructor.
/// + When the pattern itself is a range, you just want to tell whether any of the values in //! + 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 //! the pattern range coincide with values in the constructor range, which is precisely
/// intersection. //! intersection.
/// Since when encountering a range pattern for a value constructor, we also use inclusion, it //! 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, //! 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. //! 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 //! - When we're testing for usefulness of a pattern and the pattern's first component is a
/// wildcard. //! wildcard.
/// + If all the constructors appear in the matrix, we have a slight complication. By default, //! + 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 //! 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 //! 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 //! 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 //! 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 //! of the matrix `P` and new pattern `p` are the same. This is described in more
/// detail in `split_grouped_constructors`. //! detail in `split_grouped_constructors`.
/// + If some constructors are missing from the matrix, it turns out we don't need to do //! + 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 //! anything special (because we know none of the integers are actually wildcards: i.e., we
/// can't span wildcards using ranges). //! can't span wildcards using ranges).
use self::Constructor::*; use self::Constructor::*;
use self::SliceKind::*; use self::SliceKind::*;
use self::Usefulness::*; use self::Usefulness::*;