Skip to content

WIP: Pattern match complex expressions by GVN

Sebastian Graf requested to merge wip/gvn-pmcheck into master

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 PmExprOthers 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.

Merge request reports