Automate extracting an expression into a separately-defined function

Summary

We would like to be able to extract arbitrary sub-expressions into separate named function, especially as a way to address brittleness (because the extracted functions could be treated opaquely) but also as a standard software engineering tool.

(Note: extracting a sequence of statements into a separate method is also a conceivable feature, but it's a bit more difficult and wouldn't have much effect on brittleness, so we'll potentially address that separately in the future.)

Background and Motivation

One of the most effective ways to reduce brittleness in Dafny is to hide information, and one of the key mechanisms for doing that is function opacity. To use function opacity, however, the expression you want to hide must be in a separately-defined function. Moving expressions like this is conceptually straightforward, but tedious to do manually, so having an automated mechanism to do it would be very convenient.

Proposed Feature

I envision this as conceptually working like a method ExtractFunction(file: string, start: pos, end: pos, name: string) (to use Dafny syntax) that would modify a file in place to take the expression starting at postition start and ending at position end and move it to the function named by name. It would produce an error if the text in the specified range is not a well-formed expression.

The most straightforward way to use this would be to select text within the IDE and invoke the refactoring as a code action. However, I propose to first implement it in a way that can work from the CLI and then add an IDE-based entry to that. We could potentially do that by allowing any Code Action to be invoked from the CLI and implementing it as a Code Action.

Alternatives

Without this feature, refactoring code to reduce brittleness is tedious. The feature isn't strictly necessary. Any needed refactoring could be done without it. But it would significantly save time.

It has precedent, with similar features available in the IDEs for many common languages.

As an alternative, instead of modifying the file in place, it could just print out the new function definition to the console. That could be easily piped into the clipboard and pasted into an editor, or appended to a file. This could also be a first step toward something that could modify a file in place.

dafny-lang / dafny