I'm trying to understand .messages file generated by menhir.

From this sample, we could use menhir parser.mly --list-errors > parser.messages to generate parser.messages. An error is like follows:

main: INT MINUS TIMES
##
## Ends in an error in state: 12.
##
## expr -> expr MINUS . expr [ TIMES RPAREN PLUS MINUS EOF DIV ]
##
## The known suffix of the stack is as follows:
## expr MINUS
##

<YOUR SYNTAX ERROR MESSAGE HERE>

Normally, --list-errors should compute all possible ways of causing an error. But I don't understand why ways like main: INT PLUS DIV and main: INT MINUS DIV are not included in parser.messages (however, expression like 5 / still correctly raises an error). Does anyone know the reason?

CodePudding user response：

Normally, the set of (error) deriviations is infinite, so there is no way of showing or computing it. Menhir heuristically tries to output useful error messages, but there's no guarantee that they will be exhaustive or even useful.