Feature Request: `update vars` command

[hwayne]

Motivation

This came up in the Community Outreach meeting as a good potential first "refactoring tool" for TLA+. Given we have the AST, we know 1) all of the variables in the system, and 2) know if vars is an operator. It is also a lot of tedious work to update vars every time we add or remove a variable.

With that in mind, it may be useful to make a VSCode command that automatically updates vars with all variables.

How it works

Given

VARIABLES x, y
+ VARIABLES z
VARIABLES w

vars <<x, y, w>>

The refactoring would be

VARIABLES x, y
VARIABLES z
VARIABLES w

- vars <<x, y, w>>
+ vars <<x, y, z, w>>

Implementation

Probably just a new command like tlaplus.refactor.update_vars

Concerns

Complex var tuples

I often break vars down into subsets of variables:

state_vars == <<a, b, c>>
aux_vars == <<d, e, f>>
vars == <<state_vars, aux_vars, g, h>>

What should the refactor do in this case?

EXTENDS

EXTENDS Foo

VARIABLES x

vars == <<x>>

What if Foo also defines variables? Should those be included in vars?

Would this be a problem for PlusCal?