CakeML / CakeML/cakeml

Verify a more sophisticated pattern-match compiler

Open
#667 4 comments 0 reactions 1 assignee Assigned to @aceawan View on GitHub
enhancement
Dominant language
Standard ML
Stars
1.2k
Forks
104
Avg merge
2d 21h
Merged PRs (30d)
16

Description

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](https://www.researchgate.net/profile/Fabrice_Le_Fessant/publication/2840783_Optimizing_Pattern_Matching/links/553666bd0cf268fd0018281b.pdf)
- Decision trees : Maranget, 2008, [Compiling Pattern Matching to Good Decisions Trees](https://www.cs.tufts.edu/~nr/cs257/archive/luc-maranget/jun08.pdf)

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](http://moscova.inria.fr/~maranget/papers/warn/warn.pdf)) 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

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.