Improve error messages by antlr

[konnov]

The default messages by antlr are hardly readable:

examples/ReadersWriters/ReadersWriters.tnt:22:65 - error no viable alternative at input 'NumActorsdefToSet(s)=s.keys().map(i->s[i])defread(s)=s[1]=="read"defwrite(s)=s[1]=="write"valWaitingToRead=ToSet(waitingselectread)map(p->p._2)'
examples/ReadersWriters/ReadersWriters.tnt:22:57 - error extraneous input '->' expecting {'module', '{', '}', 'const', 'var', 'assume', 'type', 'import', 'val', 'def', 'pred', 'action', 'temporal', '(', '|', '[', '^', 'if', '&', STRING, BOOL, INT, 'and', 'or', 'iff', 'implies', 'subseteq', 'in', 'notin', '+', '-', '*', '/', '%', '>', '<', '>=', '<=', '!=', '==', '<-', IDENTIFIER}

For reference: syntax error, parsing, parser error

[shonfeder]

Here are some useful references:

• Catching exceptions: https://github.com/antlr/antlr4/blob/master/doc/parser-rules.md#catching-exceptions
• Adding a custom error listener: https://stackoverflow.com/questions/18132078/handling-errors-in-antlr4
• Using "error alternatives": https://stackoverflow.com/a/58115099

The last seems very clean!

[konnov]

Having spent over two days on exploring the ways to improve error reporting with antlr4, I must say that I am close to giving up. I had a bit of success in https://github.com/informalsystems/quint/pull/1221. However, it is still quite hard to figure out how to tell antlr4 to report reasonable errors about even trivially looking rules like declaration. Moreover, the interaction between syntax listeners, notifyErrorListeners, and BailErrorStrategy is quite tricky.

My conclusion is that we should use antlr4 for the happy path, that is, to produce an AST. The error explanation should be done via a different parser that is tuned to error explanation.

[konnov]

I have tried Peggy. It is producing nice error messages, but it does not have a real lexer. This makes error messages not so nice. There is also Ohmjs. Let's see how fast I hit its limitations.