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