Verify a more sophisticated pattern-match compiler

[aceawan]

This issue is about optimizing the compilation of pattern-matching expressions and improving the exhaustiveness checking for patterns. Two strategies for pattern-matching compilation backtracking and decision trees, described :

• Backtracking automata : Le Fessant & Maranget, 2001, Optimizing Pattern Matching
• Decision trees : Maranget, 2008, Compiling Pattern Matching to Good Decisions Trees

As mentioned in the conclusion of the second article, when correctly implemented, compilation to decision trees can match the performance of backtracking automata and sometimes perform better. It is also simpler to implement.

After discussion with @myreen , we think decisions trees could be the right way to go, but insights on both these techniques are welcome.

Another related paper is (Maranget, 2007, Warnings for pattern matching) that describes pattern exhaustiveness checking separately from their compilation, which would be needed with the backtracking method.

Related existing issues are :

• #664 support for or-patterns : both papers describe how to support or-patterns compilation
• #663 support for when clause in patterns : none of the papers mention when clauses and it isn't clear how their support could be added. I currently don't plan to add support for when
• Not a referenced issue, but supporting as-clauses in patterns. Papers don't mention it, but it may not be too difficult to add, it is planned to try to support them

[thtuerk]

Hi,

not sure whether this is useful, but HOL's pattern compilation implementation in src/1/Pmatch is using ideas from "Compiling Pattern Matching to Good Decisions Trees". Perhaps one can salvage some of the existing HOL code or a look at this implementation might be useful. The pattern compilation in src/pattern_matches uses this unverified code and checks that the result is correct afterwards. In any case, it is pretty straightforward to implement own heuristics in src/1/Pmatch and it might be a quite simple way to experiment with different heuristics at a very early stage.

Thomas

[aceawan]

Hi @thtuerk ,

Thanks for the advice ! It is definitely a good reference. I am not sure we can re-use any of the code though. @myreen advised me to try to build an abstract theory of pattern matching, and we will worry about connecting it to FlatLang later.