Add support for initial context to evaluate commands

[klinvill]

trafficstars

Original observation from @lemmy:

I realized that the dialog could be used to support evaluating expressions in a spec that declares variables and/or constants, but lacks a model:

---------------------- MODULE ATD ---------------------
EXTENDS Naturals

CONSTANT N

ASSUME NIsPosNat == N \in Nat \ {0}

Node == 0 .. N-1
=============================================================================

If a user tries to evaluate Node, one gets:

Error evaluating expression:
The constant parameter N is not assigned a value by the configuration file.

It would be nice if one could type WITH N <- 42 in the prompt (suffix of regular TLA+ expression INSTANCE ATD WITH N <- 42).

[klinvill]

While using the prompt would be nice for cases where you only have a few constants (like above), it might get unwieldy for specs with many constants. This could be partly improved by persisting previous assignments at a project level. Would it be better to supply initial context by reading in constants from a config file?

[lemmy]

There is already TLC's config file (YourSpec.cfg), and I don't think TLA+ values should be persisted as project-level VSCode settings. Perhaps, it would be useful to generate a more complete YourSpec.cfg? Right now, the VSCode extension just generates CONSTANT, INIT, NEXT. However, we cannot write INSTANCE ATD WITH N <- 42 in YourSpec.cfg, thus we probably want MC.tla/MC.cfg (see https://github.com/alygin/vscode-tlaplus/issues/159).

On second thought, my initial observation (this issue) wasn't a good one. Sorry, I should have thought this through.

[klinvill]

I agree, I think it makes sense to take advantage of a more complete config like the MC approach you mention. In that case, I'd vote for deferring this until after issue 159 is resolved