New Representation for Pattern Matches

[thtuerk]

As a follow-up on the ITP talk Pattern Matches in HOL: A New Representation and Improved Code Generation (slides, paper) there was a discussion moving the new pattern matching representation from examples/pattern_matches to somewhere in the src directory, so it is easier to use. It should be as early as possible and definitely be loaded by bossLib.

There are a few issues that need addressing, though. Most importantly, we need to come up with a new syntax for it and adapt the parsing and pretty printing. Then one needs to analyse dependencies and remove unnecessary ones in order to get it working early up in the build-process. Then tools need integrating in the standard tools like std_ss. Finally, we might want to add extra features and reimplement existing ones with the help of the new pattern matches. I will create separate issues for these points.

• syntax of pattern matches (issue New Representation for Pattern Matches - Syntax #286)
• move to src (issue New Representation for Pattern Matches - Moving to src #287)
• integrate with existing tools (issue New Representation for Pattern Matches - Integration #288)
• extra features (issue New Representation for Pattern Matches - Extra Features #289 )

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[thtuerk]

I just created a branch pattern_matches. The idea is to use that for performing the changes. I thought of roughly the following workflow:

1. move pattern match example in src
   2a. adapt the parser ( @mn200 )
   2b. integrate with existing tools
2. make sure that at least the src build works, better the examples as well
3. merge with master
4. add extra features

Points 2a and 2b are independent. I will start working on 1 and 2b now.

@mn200 is that plan OK?

[mn200]

Looks great.

[thtuerk]

I believe this issue can be closed. The pmatch patterns are now integrated and documented. However, one could always add extra features. Therefore issue #289 is still open.

@mn200 please close this issue, if you agree.

[thtuerk]

Since there was no disagreement, I'm closing this issue now.