Pattern match compilation

[brendanzab]

Core languages like PiSigma and MiniTT have simple constructs for pattern matching, allowing for easier verification of type checking.

I'm not sure where this should be done, however. MLton seems to do it during its defunctorise pass.

We can do it in a naive way for now, but there is an interesting paper showing how to do it well: Compiling Pattern Matching to Good Decision Trees. Do note that we have the added complication of perhaps wanting to add dependent patterns etc.

Compiling non-dependent pattern matching to case trees is described in chapter 5 of The Implementation of Functional Programming Languages. This is what Sixten currently uses, "with some dependent pattern matching hacked in".

Compiling dependent pattern matching to case trees has been described by Jesper Cockx in:

• Dependent pattern matching and proof-relevant unification
• Elaborating dependent (co)pattern matching