Commit Graph
6 Commits
Author SHA1 Message Date
Richard SmithandJon Ross-Perkins 0191e2e41e implement checking for pattern match exhaustiveness and for unreachable cases (#2164)
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>
2022-09-13 13:40:25 -07:00
Richard Smith 7a67715ac5 Error: track message and prefix/location separately. (#1529)
This allows us to combine multiple Errors together without repeating the prefix
information. Also fixes several cases where two "COMPILATION ERROR" prefixes
would be prepended to the same message when errors with prefixes and locations
were produced by the lexer and parser.
2022-07-26 15:08:19 -07:00
Jonathan Ross-Perkins a97276bcf7 TODO -> FIXME (#1316)
This is for https://google.github.io/styleguide/cppguide.html#TODO_Comments; FIXME seems to be getting used for the same purpose, and we should probably only have one so that it's easier to scan for.
2022-06-07 10:49:17 -07:00
Richard Smith 96a663766c Remove support for nesting blocks within blocks. (#1309)
This is not part of the approved design and gets in the way of
supporting `where` expressions, which are part of the approved design.
2022-06-03 18:46:46 -07:00
Richard Smith 8dd398807d Support user-defined implicit conversions via ImplicitAs (#1273)
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.
2022-05-20 17:10:30 -07:00
Jon Meow 309ec35f95 Rename executable_semantics to explorer (#1188)
Change generated with:

```
#!/usr/bin/bash -eux

# Helper script for renaming pending work.
# Run from the repo root.

# Rename executable_semantics in code.
sed -i 's/executable_semantics/explorer/g' \
  $(git grep -l 'executable_semantics' . | grep -v proposals)
sed -i 's/executable semantics/explorer/g' \
  $(git grep -l 'executable semantics' . | grep -v proposals)
sed -i 's/Executable semantics/Explorer/g' \
  $(git grep -l 'Executable semantics' . |  grep -v proposals)
sed -i 's/Executable Semantics/Explorer/g' \
  $(git grep -l 'Executable Semantics' . |  grep -v proposals)
sed -i 's/EXECUTABLE_SEMANTICS/EXPLORER/g' \
  $(git grep -l 'EXECUTABLE_SEMANTICS' . | grep -v proposals)
sed -i 's/ExecutableSemantics/Explorer/g' \
  $(git grep -l 'ExecutableSemantics' . | grep -v proposals)
sed -i 's/executable-semantics/explorer/g' \
  $(git grep -l 'executable-semantics' . | grep -v proposals)

# This is only needed for the initial move.
mv executable_semantics explorer
mv explorer/fuzzing/executable_semantics_fuzzer.cpp explorer/fuzzing/explorer_fuzzer.cpp
```

Verified with `bazel test ...`
2022-04-29 13:20:25 -07:00