[lexer] keyword protected quotation token for arbitrary text #9733
Conversation
|
Note that this is probably going to conflict with #8764, it might be worthwhile to factor out the common parts. |
|
I'm fine taking the conflicts, but #8764 seems to have stalled, I'll ping. |
|
Wrt the changes, they are quite orthogonal as far as I can tell. |
Indeed, but Pierre Marie is right in that some conflicts may arise (c.f. 4bc83c8). |
|
Sure. I was just offering to give you precedence. My change is smaller and it is hence easier to rebase. Of course this works for me only if you push your PR ahead, hence my ping. |
|
OK, I've tested it in elpi and it works for me. I've added the |
|
@ppedrot BTW some of this code and/or the delimiting convention could be used in coqpp too. I had to write |
|
ping @coq/parsing-maintainers (and @coq/doc-maintainers to tell me where I should put the doc of the QUOTATION token, especially the non-escaping rules). |
|
This should probably go in the “Syntax extension” chapter (https://coq.inria.fr/refman/user-extensions/syntax-extensions.html) if it impacts the users directly. If it only concerns the plugin writers, then it should go in the non-existing plugin writing documentation chapter 😈. Until then, you can just create a new Markdown file in |
|
The index in https://github.com/coq/coq/tree/master/dev#miscellaneous-information-about-the-code-devdoc should be updated if you create a new file in |
|
It does not concern users, unless they use an extension language that uses the feature. |
|
ping @coq/parsing-maintainers for the review |
| (** This should be functional but it is not due to the interface *) | ||
| val add_keyword : string -> unit | ||
| val add_keyword : ?quotation:starts_quotation -> string -> unit |
There was a problem hiding this comment.
Maybe it would be clearer to have two functions ? add_keyword and add_quotation ?
There was a problem hiding this comment.
I thought about that, but in the current model a quotation is always initiated by a keyword. So the API would look like
val add_keyword : string -> unit
val add_keyword_for_quotation : string -> unit
that is pretty much what we have in the patch...
|
This till lacks an assignee. @ppedrot can you take it? |
|
ping |
|
ping @ppedrot (time for 8.10 is running out) |
|
@gares Can you rebase? I'll merge it after. |
Tokens were having a double role: - the output of the lexer - the items of grammar entries, especially terminals Now tokens are the output of the lexer, and this paves the way for using a richer data type, eg including Loc.t Patterns, as in Plexing.pattern, only represent patterns (for tokens) and now have a bit more structure (eg the wildcard is represented as None, not as "", while a regular pattern for "x" as Some "x")
One can now register a quotation using a grammar rule with
QUOTATION("name:"). "name:" becomes a keyword and the token is
generated for name: followed by a an identifier or a parenthesized
text. Eg
constr:x
string:[....]
ltac:(....)
ltac:{....}
The delimiter is made of 1 or more occurrences of the same parenthesis,
eg ((.....)) or [[[[....]]]]. The idea being that if the text happens to
contain the closing delimiter, one can make the delimiter longer and avoid
confusion (no escaping). Eg
string:[[ .. ']' .. ]]
Nesting the delimiter is allowed, eg ((..((...))..)) is OK.
The text inside the quotation is returned as a string (including the
parentheses), so that a third party parser can take care of it.
Keywords don't need to end in ':'.
|
I did rebase the overlay, the error seems from another pr |
|
The error seems very related to this PR to me: |
|
Ah ok, the Ltac2 one is fixed now. |
|
Even weirder, I just rebased #9815 over this PR and CI passes (with just a simple overlay for ltac2). |
|
Restarted, and now it is green... I guess they pushed a bad commit |
…ry text Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
This PR implements a feature I could use in elpi. Today the only token that can carry arbitrary text is STRING that suffers from escaping shortcomings. This PR implements a class of tokens that can carry arbitrary text, so that 3rd party languages can be easily embedded in .v files.
From the last commit:
One can now register a quotation using a grammar rule with
QUOTATION "name:". In that casename:becomes a keyword and the token isgenerated for
name:followed by a an identifier or a parenthesizedtext. Eg
The delimiter is made of 1 or more occurrences of the same parenthesis,
eg
((.....))or[[[[....]]]]. The idea being that if the text happens tocontain the closing delimiter, one can make the delimiter longer and avoid
confusion (no escaping). Eg
Nesting the delimiter is allowed, eg
((..((...))..))is OK.The text inside the quotation is returned as a string (including the
parentheses), so that a third party parser can take care of it.
Keywords don't need to end in
:.