[tlaplus] REPL enhancements

[Christopher Pacejo <colanderman@xxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7e444bd5-9dc5-441e-81b0-1ed772459c48n%40googlegroups.com.