When checking for control flow falling off a function after a `match`, determine whether it's possible for no case to have matched. Using the same implementation, also detect whether `case`s in a `match` are unreachable.
For now, the implementation never considers a match against specific values for any type other than tuples, alternatives, and `bool` to be exhaustive. In particular, matching against the sole value `{}` of type `{}` is not considered exhaustive. This is probably best left until explorer supports matching on struct and maybe class types more generally.
This implementation closely follows the algorithm described in the paper [Warnings for pattern matching](http://moscova.inria.fr/~maranget/papers/warn/warn.pdf) by Luc Maranget. Various optimizations are possible, such as reducing the amount of copying done, but for the purposes of explorer, comprehensibility is being favored over efficiency.
The problem is, perhaps surprisingly, co-NP-hard (by reduction to the tautology problem for disjunctive normal form, which is in turn dual to the satisfaction problem for conjunctive normal form, which is well-known to be NP-hard). The algorithm is therefore exponential-time in the worst case, but seems to be well-studied and performs well enough on non-pathological examples. Nonetheless, a depth limit has been imposed to prevent pathological examples such as those generated by a fuzzer from causing long runtimes.
Co-authored-by: Jon Ross-Perkins <jperkins@google.com>
The most significant change here is that explorer now uses the chosen spelling
rather than the old `Bool` spelling. Also update a few documentation examples
and some skeletal design docs to use the chosen spelling.
Support is added for all of the non-type expression contexts where we currently accept built-in conversions, such as reordering the fields in a struct.
In order for this to work, we need to always use the argument deduction code path for function calls, instead of only using it when there is a `[...]` list, which means that argument deduction now needs to support implicit conversion.
Co-authored-by: Jon Meow <jperkins@google.com>
Use FileCheck's `[[@LINE+n]]` mechanism to refer to the next line.
This is made awkward by a couple of things:
* We want to keep the `CHECK` lines in the original order.
* Errors are sometimes more than one line long.
The approach we use is to interleave the original lines and the check lines, putting each check line as early as possible subject to two rules:
1) Check lines never precede the 'AUTOUPDATE' line
2) Except when required by rule (1), a check line that refers to a source line by line number is never placed earlier than a source line that precedes that source line.
The actual `[[@LINE+n]]` annotations are created in a second pass after we've interleaved the lines so that we can work out the correct offsets.
Co-authored-by: Jon Meow <jperkins@google.com>
Richard SmithandJon Ross-Perkins
pk19604014