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

Whole-module lifting w/ fixed eta-wrapping for eliminators #76

Closed nateyazdani closed 4 years ago

nateyazdani commented 4 years ago

This all works now, after I got carried away chasing my bug :-) The main test used for validation is coq/examples/ListToVect.v, modified to use the whole-module lifting command (Lift Module $base $orn in $mod as $id). The general test script passes successfully as well.

The changes here directly related to mapping ornamental lifting over a module involve simply creating some module utilities (seemodutils.ml) and applying them in the frontend.

However, a bug in the "eta-wrapping" process for eliminators of lifted inductive types would cause many/most module elements involving lifted inductive predicates to fail (e.g., Forall, In, NoDup from the pre-processed List module). (We had seen this previously and suspected a bug in module processing.) Strangely, skipping the eliminator wrapping (Eta.eta_extern, called from Lift.define_lifted_eliminator) would cause more such module elements to succeed, at the cost of failing tests in coq/Indtype.v.

Printing out intermediate terms revealed that the eliminators generated by Eta.eta_extern were frequently ill-typed. The strategy of the Eta module had been simply to eta-expand any sigT-typed variable in sight, but as it turns out, only the eliminator motive really needs an eta-expanding wrapper, given DEVOID's general eta-expansion policy. This strategy is implemented as Lift.eta_guard_eliminator (especially eta_guard_motive), replacing the Eta module. I've attached a file, Sample.v, to demonstrate the pattern of eliminator wrapping.

There are a handful of helper functions (e.g., pr_global_as_constr, with_suffix), plus the module utilities, that might be better placed in the plugin library. Also, if you think they'd have use in other contexts, the local helper functions in eta_guard_eliminator could be factored out without too much mess.

Once merged, this PR will close issue #27.

nateyazdani commented 4 years ago

Postscript: I realized just now that this eliminator wrapping is pretty much exactly dependent elimination specialized for sigma-typed indices. Not sure it's worth renaming stuff, but that does nicely explain the pattern of motive wrapping.

tlringer commented 4 years ago

Sorry I'm getting to this late! POPL and all. I'll take a look now. Looks exciting.

tlringer commented 4 years ago

Related to #32 also

nateyazdani commented 4 years ago

All feedback should now be addressed.

This PR now depends on PR 27 to coq-plugin-lib: https://github.com/uwplse/coq-plugin-lib/pull/27. The git submodule should now point to the appropriate commit, at the head of the module_utilities branch.

nateyazdani commented 4 years ago

Also, I should add that I have indeed rebuilt and rerun the testsuite successfully.

nateyazdani commented 4 years ago

Great, thanks for the quick turn-around!

Assuming the extra test in ListToVect.v is actually what was requested, this should be good to go :-)