Hi Chris,
You write that a REPL should:
- Allow ... constants and variables to be declared.
- Allow operators to be defined and re-defined...
- Provide a command to display the definition of any symbol.
A set of declarations and definitions is a specification. I therefore
infer that a REPL would maintain a Current Specification that is
modified and viewed by command-line commands.
The first text editor I can remember using was called TECO. In those
days, video displays were too expensive for common use, so one
interacted with a computer using a teletype-style device with a
keyboard and a roll of paper. TECO maintained a current cursor
position, and one edited a file by keyboard commands to move the
cursor and to insert or delete characters at the cursor position. To
see the actual contents of the file, you executed a command to print
part of it--usually a few lines containing the cursor. When CRT
displays became common in the 1970s, they were first used as "glass
teletypes", treating the screen as a virtual roll of paper. People
soon switched to visual editors that made the screen a window on the
file that you edited visually--e.g., Emacs (which was first built on
top of TECO).
Your REPL seems to be a specification editor based on the TECO model,
treating the screen as a glass teletype. (Instead of viewing a few
lines around the cursor, the user displays an individual definition.)
However, unlike text files, specs have a logical structure. So, what
happens if you try to add a syntactically incorrect definition? One
possibility is to produce a syntactically incorrect spec, which you
then fix by actual TECO-style editing commands. However, I presume
that you intend the definition command to fail, so the user would have
to issue a whole new command to add the definition. Since you are
using a virtual paper roll rather than real paper, this is not hard to
do with copy/paste/edit starting from the incorrect command.
People who want a REPL interface apparently think it's a great step
forward to return to the 1960s. I lived through the 60s and I don't
think they were that great (except for the music). So, I will have no
part in implementing a REPL interface for TLA+. If I want to edit a
Current Specification, I will do it by putting the specification in a
buffer and editing it with something like Emacs, not something like
TECO. And TLA+ already provides a syntax for displaying a
specification in that buffer.
I couldn't tell if the Current Specification in your proposal is
actually what the Toolbox thinks is the current spec, so your REPL
command to modify a definition actually changes the .tla file. I
suspect it isn't. In that case, the Current Specification should have
its own buffer. This allows you to play with potential changes to the
spec--or make changes just for debugging purposes--without affecting
the official spec. There are any number of ways of doing this--for
example, with an easy to use repository. With a REPL, if you want to
change a definition in the spec to a modified version that you've
since changed, you will have to search back in the scroll for the
command that created it. With a repository, you could make lots of
checkpoints and go to the appropriate one. Another alternative is to
create new models instead of new checkpoints. As part of a model, the
Toolbox keeps the entire spec that was last checked by the model. I
believe you can open that spec in a read-only editor, but I don't
remember how. (I've never used it.) But it should be easy to add
Toolbox commands to allow the user to edit that saved version and
rerun TLC on it.
- Allow a key-press (presumably Ctrl-C) to promptly interrupt a
long-running evaluation.
That shouldn't be hard to add to the Toolbox, if clicking on a button
is too much work. Since you can have more than one model executing at
a time, there might be some problem in determining which one gets
interrupted.
- Allow explicit temporary local binding (shadowing) of constants and
variables, to test operators. This would only be allowed in commands
that did not have side-effects. i.e. It would not be allowed when
defining or redefining a symbol.
My recollection is that output from Assert(_,_) and PrintT(_) of
complex nested structures would occasionally be so hard to read that I
would copy/paste it into a text editor and manual reformat it a bit,
to clarify a problem.
Your recollection is probably correct. I have to do that sometimes.
No pretty-printer can automatically display a complex value the way I
want to see it because how I want to see the value depends on what I'm
looking for. So I might want the same value to de displayed in two
different ways. Mark's algorithm is not very sophisticated, so it can
probably be improved. But I doubt if it will be easy to make it very
much better.
Using TLC currently requires using the mouse quite a lot, whereas
using TLAPS can be done mostly from the keyboard.
There are many more things you can do with TLC than with TLAPS, so
doing everything with keyboard commands would be pretty complicated.
However, I believe that once a window is selected, any click of a
button on that window could be implemented as a keyboard command. I
don't know how to attach keyboard commands to individual windows.
Anyone who knows how can easily do it; they just have to coordinate
with me.
Cheers,
Leslie