VerCors as a round-trip source transformer

[pieter-bos]

The normal functionality of VerCors is to take a source file and compile it down until it fits into viper. We've been gaining modes that take a source file, parse and resolve it, apply some transformations to it, and then render it back out to a source file. We've gone through some effort to make it so the pretty-printer is more correct than it was and better at making the output look pretty, but in the end this is not quite what we want: really we should be able to take a source file, parse and resolve it, and then output it back character-for-character identical.

Applying transformations should then interact with this in some sensible way (e.g.: applying simplifications would destroy the whitespace information we carry around those nodes and revert to pretty-printing).

The current VerCors functionalities that depend on round-trip source transforming are:

• Vesuv: takes an xml file in some format and then pretty-prints pvl for it
• Veymont: takes a pvl program, resolves and transforms it, then pretty-prints java for it
• Alpinist: (currently) takes a pvl program, resolves and transforms it, then pretty-prints pvl for it
• Run-time verification condition monitoring (coming soon): takes a java program, resolves and transforms it, then pretty-prints java for it

The initial concern between parsing and col is mostly whitespace, and a little bit of node support (think like += doesn't exist). In transformations (especially LangSpecificToCol) we can consider adding further metadata to the tree. I think most of these can just be stored in Origin. Example:

public class Test {
  void test() { x = 2 + 3; }
}

• I think whitespace should typically be attributed to the biggest node possible, so it should be e.g. Assign("x", Plus("2", "3")(beforeBinOp=" ", afterBinOp=" "))(beforeBinOp=" ", afterBinOp=" "). If 2+3 is simplified the correct output is x = 5, achieved by the space around = being stored in the Assign.
• this JavaClass becomes a Class(...)(javaAttributes=Seq("public")) or so. This means the fact it's public is no longer relevant for public and this origin metadata is not used in further transformations (!!!), but remembered for output anyway.
• we should strategize being able to insert expressions/statements fairly easily, so adding an assert in a block can ask the block what the indent is, or something like that.

[pieter-bos]

I noticed that scalameta claims to be lossless, maybe we should have a look at how they implement things.