Comments at the REPL

[brianhuffman]

In ghci, the interpreter doesn't complain if I enter an empty line. It also doesn't complain if I enter a line containing only a comment.

GHCi, version 8.8.3: https://www.haskell.org/ghc/  :? for help
Loaded package environment from /Users/huffman/.ghc/x86_64-darwin-8.8.3/environments/default
Prelude>
Prelude> -- comment
Prelude> {- comment -}
Prelude>

In cryptol, the interpreter is fine with completely empty lines, or lines containing only spaces. However, it gives a parse error if I enter a line with only a comment:

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.9.0 (a28e7b9, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol>
Cryptol> // comment

Parse error at <interactive>:3:0,
  unexpected: end of file
Cryptol> /* comment */

Parse error at <interactive>:3:0,
  unexpected: end of file
Cryptol>

It might be nice to support this; then I'd be able to put comments in .icry files, for example.

[yav]

The issue here is that if we are trying to parse an expression, and a comment is not a valid expression. I guess we could add a top-level "comment" production to the parser (which would be just empty), and first try to use that, and only if it fails we parse an expression. Or, perhaps we could first run the lexer, inspect the tokens, and based on the decide what parser to run, which could help with completion. Neither seems very nice.

I wonder if we may want to think more carefully about the syntax of the language used at the REPL and write a proper parser for it? We've talked about this in the past, and I think at one point SAW was supposed to be that language, but clearly that went into a different direction. To be clear, I am not suggesting we change what the language looks like (although obviously we can make adjustments), but maybe how we implement it.

[brianhuffman]

Well, a blank line is not a valid expression either, and yet somehow we manage not to report a parse error if the user just presses Enter on a blank line. How does that work?

[yav]

We just check if all isSpace before processing the command.

[brianhuffman]

We should be able to implement this easily by adding a new parser production for "optional expression". Then the lexer can take care of removing the comment. We can then also remove the special-case code that exists now for checking whether a line contains only whitespace.