REPL enhancements

[Christopher Pacejo]

Hi, I'm very excited to see that a REPL has been added last year.  However it doesn't appear to have been developed much since then beyond the basic expression evaluation functionality in the initial import.

Would I be stepping on any toes if I started working on some enhanced functionality for it?  I have a few ideas I've been kicking around in a hacky shell-script-based REPL I made a few years ago that I'd be interested in porting over.  Namely:

1) The ability to define operators and instantiate modules.

2) The ability to declare variables, and initialize and update them (one iteration) via a specified predicate and user input to resolve nondeterminism (as with TLCExt!PickSuccessor).

3) The ability to define constants (same as in a TLC config file) to support model values, and extending modules which declare constants.

4) The ability to modify, list, and save to file what's been defined in the session.

I think these enhancements would help make the REPL a really useful tool for those learning the language, or those wanting to test and explore functionality of modules they are developing.

- Chris

[Markus Kuppe]

Hi Chris,

to the contrary, we would very much welcome enhancements to the REPL.
Can you please open an issue as a place to discuss technical details?
Some of what you propose is already possible. Other enhancements
probably need a closer look because of restrictions in TLC.

Thanks,
Markus

[Markus Kuppe]

On 18.05.21 10:34, Markus Kuppe wrote:
> Can you please open an issue as a place to discuss technical details?
> Some of what you propose is already possible. Other enhancements
> probably need a closer look because of restrictions in TLC.

https://github.com/tlaplus/tlaplus/issues/627


M.

[Willy Schultz]

Just for reference, I've added a basic REPL prototype into the web-based TLA+ interface/interpreter. Feel free to try it out and see if it may address any of the outstanding REPL feature desires.

[Andrew Helwer]

Awesome feature, Will! This handles constant-level expressions?

Andrew

[Willy Schultz]

> This handles constant-level expressions?

Yeah, basically. Expressions are evaluated in the context of the current definitions in the spec and any CONSTANT instantiations, though I currently didn't add a way to actually instantiate CONSTANT values while using the REPL interface. I don't think that's too critical, though. Personally, I find a large percentage of my REPL usage consists of evaluating constant expressions and maybe also testing out a few manually defined operators. 

Note that for evaluating expressions in the context of a current spec state, one can instead use the "Trace Expression" feature in the web interface, which allows for this.