Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Relaxed antiquotation parsing #1272

Merged
merged 5 commits into from
Jul 23, 2022
Merged

Relaxed antiquotation parsing #1272

merged 5 commits into from
Jul 23, 2022

Conversation

Kha
Copy link
Member

@Kha Kha commented Jul 1, 2022

This is an incomplete implementation of an idea I mentioned in the Typed Macros PR: #1251 (comment) (the first half). In short, when encountering an antiquotation $x while running a parser p, we do not immediately assume that the entire antiquotation is for p but check if we p accepts $x and further tokens behind it. Thus the example `(structInstField| $id := $val) is interpreted as `(structInstField| $id:ident := $val:term), not `(structInstField| $id:structInstField <ERROR: expected ')'>.

Unfortunately, there are some regressions. One of them is defensible I think , but the other would likely require us to adapt the Lean grammar; see below.

@@ -254,7 +254,7 @@ macro_rules
syntax "repeat " doSeq " until " term : doElem

macro_rules
| `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq; if $cond then break)
| `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
Copy link
Member Author

@Kha Kha Jul 1, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this one makes sense: how many people would read the original line and conclude that $seq is not the first of two elements of do, but the entire content of it? With the relaxed antiquotation parser, we do now get seq : TSyntax `doElem in the modified line.
The fix only makes this marginally clearer; I would have liked (do $seq); ... better, which does interpret seq as a doSeq (or, with the second part of the comment linked above, as TSyntax [`doSeq, `doElem]). However, the parens terminate e.g. mutable variables, which is undesirable.

Copy link
Member

@gebner gebner Jul 1, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

To be fair, I can empathize with Lean here. I've also found the zoo of do-notation nonterminals a bit confusing at times.

Indentation would be another way to disambiguate this example:

`(doElem|
  repeat
    do $seq
    if $cond then break)

Excessive use of braces helps too:

`(doElem| repeat do { do $seq }; if $cond then break)

We could also remove the slightly misleading syntax for nested do and replace it by braces. (I think it's misleading because it's not a boundary for return like the normal do.)

syntax "{" doSeq "}" : doElem
-- then this should work
`(doElem| repeat { $seq }; if $cond then break)

A coercion from doSeq to doSeqItem could also help (but I guess you don't want a coercion to insert new tokens).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, it might be good to clean up the grammar there. And yes introducing tokens in a coercion probably isn't a good idea due to lack of access to getRef (though I even thought about a monadic coercion class that is automatically used by antiquotations).

src/Lean/Elab/MutualDef.lean Outdated Show resolved Hide resolved
@Kha Kha mentioned this pull request Jul 8, 2022
@Kha Kha force-pushed the relaxed-antiquots branch 2 times, most recently from e5f5195 to ec83b68 Compare July 9, 2022 11:59
@Kha Kha marked this pull request as ready for review July 9, 2022 11:59
@Kha Kha requested a review from leodemoura July 9, 2022 12:00
@Kha
Copy link
Member Author

Kha commented Jul 23, 2022

I'm going ahead and merging this as it should be a strict improvement now and I've been confused multiple times about why it didn't work on master yet.

@Kha Kha enabled auto-merge (rebase) July 23, 2022 14:02
@Kha Kha merged commit e589185 into leanprover:master Jul 23, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants