|
|
# Exhaustiveness/Redundancy check implementation \[THE PAGE IS CURRENTLY UNDER CONSTRUCTION\]
|
|
|
# Exhaustiveness/Redundancy Check Implementation \[THE PAGE IS CURRENTLY UNDER CONSTRUCTION\]
|
|
|
|
|
|
|
|
|
This page describes how the exhaustiveness and redundancy cheker is implemented
|
|
|
in GHC. If you are looking for a general description of the problem and an
|
|
|
overview of our approach see [PatternMatchCheck](pattern-match-check).
|
|
|
|
|
|
|
|
|
The most relevant modules are:
|
|
|
|
|
|
- `deSugar/PmExpr.hs`: The expression type (`PmExpr`) and the term equalities (`SimpleEq`s and `ComplexEq`s) used by the checker (and the term oracle).
|
|
|
- `deSugar/TmOracle.hs`: The (incremental) term oracle and other relevant utilities. The interface to the solver is function `tmOracle`.
|
|
|
- `deSugar/Check.hs`: The main algorithm. Main exports are functions `checkSingle` (check a single binding -- let),
|
|
|
`checkMatches` (check a `MatchGroup` -- case expressions and functions) and `dsPmWarn` (print the results if the respective flags are enabled).
|
|
|
|
|
|
|
|
|
We explain each one separately below.
|
|
|
|
|
|
## The `PmExpr` Datatype and Friends
|
|
|
|
|
|
|
|
|
The module exports the following data types:
|
|
|
|
|
|
```wiki
|
|
|
data PmExpr = PmExprVar Id
|
|
|
| PmExprCon DataCon [PmExpr]
|
|
|
| PmExprLit PmLit
|
|
|
| PmExprEq PmExpr PmExpr -- Syntactic equality
|
|
|
| PmExprOther (HsExpr Id) -- NOTE [PmExprOther in PmExpr]
|
|
|
|
|
|
data PmLit = PmSLit HsLit -- simple
|
|
|
| PmOLit Bool {- is it negated? -} (HsOverLit Id) -- overloaded
|
|
|
|
|
|
type SimpleEq = (Id, PmExpr) -- We always use this orientation
|
|
|
type ComplexEq = (PmExpr, PmExpr)
|
|
|
```
|
|
|
|
|
|
|
|
|
Type `PmExpr` represents Haskell expressions. Since the term oracle is minimal at the moment, only specific forms are supported
|
|
|
and the rest are wrapped in a `PmExprOther`. Note that `PmExprEq` is not function `(==)` but represents structural equality and
|
|
|
is used for non-overloaded literals. E.g. the constraint \*x is not equal to 5\* is represented as (False \~ (x \~ 5)):
|
|
|
|
|
|
```wiki
|
|
|
PmExprEq (PmExprCon <False> []) (PmExprEq (PmExprVar <x>) (PmExprLit (PmSLit <5>)))
|
|
|
```
|
|
|
|
|
|
|
|
|
Literals `PmLit` are separately defined because (as we explain below) appear in the pattern language as well. Equality check for
|
|
|
`PmLit` is exported too, with signature:
|
|
|
|
|
|
```wiki
|
|
|
eqPmLit :: PmLit -> PmLit -> Maybe Bool
|
|
|
```
|
|
|
|
|
|
|
|
|
Instead of `Bool` we return `Maybe Bool` because if two overloaded literals look different it does not mean they actually are. Hence
|
|
|
equality in this case is inconclusive, unless we unfold the `from`-function (like `fromInteger`). E.g. syntactic equality 5 \~ 6 is
|
|
|
not necessarily inconsistent, since it actually represents `fromInteger 5 ~ fromInteger 6` which depends on the implementation of
|
|
|
function `fromInteger`. On the other hand, `fromInteger 5 ~ fromInteger 5` is always true, since `fromInteger` is a pure function.
|
|
|
We could have treated overloaded literals as function applications (e.g. `fromInteger 5`) but since the term oracle cannot handle
|
|
|
function applications, we would get poor error messages for overloaded literals. Instead, we took this \*syntactic\* approach (which
|
|
|
looks a bit hackish though).
|
|
|
|
|
|
|
|
|
Term equalities take two forms: `SimpleEq` and `ComplexEq`. `SimpleEq`s are generated by the algorithm and are the input to the term
|
|
|
oracle, as we show in the paper. Yet, the oracle returns residual constraints which may be complex so we need a type for them as well.
|
|
|
E.g. { x \~ False, x \~ (y \~ 5) } gets simplified to { False \~ (y \~ 5) } which cannot progress unless we get more information about y.
|
|
|
|
|
|
## The Term Oracle
|
|
|
|
|
|
|
|
|
The term oracle lives in `deSugar/TmOracle.hs` and has the following signature:
|
|
|
|
|
|
```wiki
|
|
|
tmOracle :: TmState -> [SimpleEq] -> Maybe TmState
|
|
|
```
|
|
|
|
|
|
|
|
|
The state of the oracle `TmState` is represented as follows:
|
|
|
|
|
|
```wiki
|
|
|
type PmVarEnv = Map.Map Id PmExpr
|
|
|
type TmOracleEnv = (Bool, PmVarEnv)
|
|
|
type TmState = ([ComplexEq], TmOracleEnv)
|
|
|
```
|
|
|
|
|
|
`TmState` contains the following components:
|
|
|
|
|
|
1. A list of complex constraints
|
|
|
|
|
|
**--FINISH THE TERM ORACLE--**
|
|
|
|
|
|
## The `PmPat` datatype and friends
|
|
|
|
|
|
|
... | ... | |