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

Support lifting for refinements #41

Open tlringer opened 5 years ago

tlringer commented 5 years ago

Lifting currently assumes that the new index is not A itself, and does not refer to A. That means that we can't handle refinement types like is_positive and is_even. There are some conceptual difficulties to handling this, but they are an interesting set of types worth handling. Essentially, the issue is that lifting needs to prevent itself from infinitely recursing once it lifts.

I believe this assumption was also accidentally omitted in the paper submission, so it should either be fixed before publication, or the paper should add the assumption to address it.

tlringer commented 4 years ago

Does this work with the current termination workflow? Give it a shot