Tab completion on check and friends

[marsella]

Right now, the Cryptol repl supports tab completion within the :prove and :exhaust commands, but not for :check or :type. It would be a very nice quality-of-life improvement to add completion!

Related issue #781.

[RyanGlScott]

Unless I'm mistaken, :type does have functioning tab completion. If I type this at the REPL:

Cryptol> :type rev

And then hit the Tab key, it autocompletes to reverse. That being said, autocompletion does not work if I try the same thing with:

Cryptol> :t rev

[RyanGlScott]

I think the reason that :t and :check fail to autocomplete is that there are multiple commands that have them as prefixes:

• :t: :type and :time
• :check: :check and :check-docstrings

As such, Cryptol refuses to commit to the autocompletion strategy for either command.

One way to improve this: if you have typed :check rev, then arguably you want the :check command, not :check-docstrings, due to the fact that there is a space after the :check prefix. If we see a situation where the a user has typed :<CMD> ... and <CMD> exactly matches a defined command (e.g., :check), then we should commit to that approach over any other ones (e.g., :check-docstrings).

I think this approach would also solve the :type versus :time problem. This is because Cryptol explicitly defines :t as an alias of :type, so :t ... should unambiguously pick :type's autocompletion strategy.