The Coq mailing list

[Talia Ringer <tringer AT cs.washington.edu>]

Hi coq-club,

I've implemented some simple refactoring support in PUMPKIN PATCH for a user. Even though it is preliminary (I started implementing it yesterday), I want to share in case it is useful for anyone else, and also so that I can think more about good interfaces.

The functionality that I implemented is just a way to replace terms with convertible terms systematically, either in a definition or across an entire module. The idea being that sometimes people have automatically generated specifications or just handwritten specifications that are kind of ugly, but they would prefer to reason about cleaned up versions, or at least present those to the user.

Using this

You just write:

Replace Convertible t1 t2 t3 in ugly as pretty.

To define a new term "pretty" that is "ugly" with all occurrences of subterms convertible with t1, t2, or t3 replaced with t1, t2, and t3 themselves. To do this across an entire module, you write:

Replace Convertible t1 t2 t3 in Ugly as Pretty.

And this gives you back a new module "Pretty" that is "Ugly," but with all subterms convertible to t1, t2, and t3 in all terms of Ugly replaced with t1, t2, and t3 themselves.

OK, now what?

After using this you'll get back a new definition or module. This is nice for some users who just want a way to deal with automatically generated, not very pretty specifications.

But probably a lot of you want this sort of functionality to directly change your existing definitions or modules. Right now you have to copy and paste the result back in if you want that, and that's kind of annoying, especially since the module will give you back proof terms and you might need to tweak proof scripts (say, to unfold the definition you just replaced).

I'd like to make an interface that is good for this!  And of course we want to support this across files! I don't know the best way to do this. So, for now I've just built some basic infrastructure.

I really want your input! This is why I'm sharing this early. So, if you have an idea for what you'd like the user experience to be for a tool like this, please let me know by cutting an issue inside of the PUMPKIN PATCH repository with the ideal user experience you imagine.

Correctness

If you do plan to keep the old definitions around, or if you want a certificate, you will eventually be able to get this by setting the option "PUMPKIN Prove Replace." This is a WIP (I just started implementing it today) but will eventually generate correctness proofs for all of the replacements. Right now it generates the correctness proofs that are reflexivity, and soon it will generate correctness proofs for inductive types (equivalence), but correctness proofs about theorems that use those inductive types will take longer (transport along the equivalence).

Other refactoring support

Implementing some more basic refactoring is on my roadmap, so if you would like any kind of basic refactor in Coq, please also cut an issue in the PUMPKIN PATCH repository so I have things that people want documented. One that is on my roadmap is renaming definitions (I still want to hear from you if you want this, so I know how to build a good interface for it). The same holds for renaming modules. Just like with repairs, if you encounter annoying refactors during development, please do think of me and cut an issue as a wish so I can eventually support it, if I don't support it yet.

Talia