epfl-lara/lisa

Print errors from parsing in a meaningful way

SimonGuilloud opened this issue · 4 comments

Error when parsing a statement or formula look like "Caused by: lisa.utils.Parser$ParserException: Unexpected input: )
", lost in the stack trace.
We should instead print meaningfull error messages before making the program fail, indicating the parsing of which formula caused the crash, and ideally, if it is in a proof, at which line

I'm working on an error reporting system. Key for the parser will be to throw a specific error right at the called function, not multiple levels bellow.

Couple of comments for context:

  1. Whenever a program fails due to an uncaught exception, the exception type and message is displayed on top (followed by the stack trace). Hence the priority is to make the exception message include as much relevant information as possible (no need for separate prints).
  2. It is certainly useful to include the formula being parsed. However, it is difficult to add information beyond that, because the parser crashes once it cannot find a rule that matches the next token, and only provides this token along with error indication. So we can say that the parser couldn't parse this token in this formula [at this position -- to be added] but that's it.

Sounds like a non-controversial step is to provide the position. Scallion should already have functionality for that.

@vkuncak: working on it!