Referencing tokens in Menhir's .messages

I’ve finally got to trying Menhir’s incremental API and the new way of error reporting.
It works great so far, but now I wonder if I can reference actual tokens in error messages somehow.

Imaginary example:
grammar: FOO BAR BAZ
Expected a QUUX but found a BAZ ($3)

CompCert seems to do it somehow ( but I don’t understnand how.

It’s hinted at in the manual:

In CompCert, we allow a template for a diagnostic message to contain the special form $i, where i is an integer constant, understood as an index into the parser’s stack. The code in cparser/ automatically replaces this special form with the fragment of the source text that corresponds to this stack entry. This mechanism is not built into Menhir ; it is implemented in CompCert using Menhir’s incremental API.

It would be interesting to get some hooks for this behavior into Menhir directly. It can’t be completely seamless because different parsers will have different data structures for storing source text, but it could be made easy.

In my imagination, it would be perfect if the message function had access to a token_stack : token list and if you provide a string_of_token function, you could write something like:

foo: FOO BAR
## Ends in an errors in state 1
Expected a quux after a foo $1 but found a bar $2