WIP: Pattern match complex expressions by GVN
By referential transparency, multiple syntactic occurrences of the same
expression evaluate to the same value. Global value numbering (GVN)
assigns each such expression the same unique number (a Name
in our
case). Two expressions trivially have the same value if they are
assigned the same value number.
The term oracle TmOracle
of the pattern match checker couldn't handle
any complex expression before this patch. It would just give up on
anything involving a function application whose head was not a
constructor, by falling back to PmExprOther
. This means it could not
determine completeness of the following example:
foo
| True <- id True
= 1
| False <- id True
= 2
This is simply because TmOracle
couldn't figure out that id True
always evaluates to the same Bool
.
In this patch, we desugar such PmExprOther
s in pattern guards to
CoreExpr
. We do so in order to utilise CoreMap Name
for a
light-weight GVN pass without concern for subexpressions. TmOracle
only sees the representing variables, like so:
x = id True
foo
| True <- x
= 1
| False <- x
= 2
So TmOracle
still doesn't need to decide equality of complex
expressions, which allows it to stay dead simple.
This is still a proof of concept, there probably are a number of regressions and further bugs to be resolved.