search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

Add function to translate match expressions to eliminator applications #16

Closed nateyazdani closed 5 years ago

nateyazdani commented 6 years ago

This PR is to add a function to translate match expressions to eliminator applications in a function/proof before lifting. It does not translate fixed-point expressions, the translation of which would, in general, require complex transformation of the source term. The best user interface for this match "desugaring" would be to run the translation automatically before lifting, but as I recall that you wanted something different, I did not include that integration in this PR.

nateyazdani commented 6 years ago

Are you sure that you want this as a separate command? Again, I strongly feel that a separate command is a bad interface; it's a bit ridiculous to make users explicitly define an intermediate value. At the very least, a configurable option (e.g., Set/Unset Lifting Desugar Matches) would make sense.

I'll open an issue to describe fixed-point support.

tlringer commented 6 years ago

Yes, because the best way to fix lifting is to eventually support lifting match statements instead of rewriting them to induction principles. I don't want anything without guaranteed behavior in the core algorithm. So I want this to be an extra thing that you can run ahead of time so that you can lift, not part of lifting.

nateyazdani commented 6 years ago

Alrighty, I believe that I've addressed all feedback and resolved the merge conflicts. Take a look when you can and let me know if you spot anything else that needs fixing.