Semantics of `incQuotDepth`?

Stream: lean4

[Siddharth Bhat]

Consider two syntax categories inner and outer, where syntax "<[" inner "]>" : outer, and inner supports antiquotations. Is it intended that for outer to allow inner to use antiquotations, outer must also be declared with incQuotDepth?

Perhaps code is easier to follow:

declare_syntax_cat inner
declare_syntax_cat outer

syntax "<[" inner "]>" : outer

syntax "[inner|" incQuotDepth(inner) "]" : term
macro_rules
| `([inner| $$($s)]) => return s

syntax "[outer|" outer "]" : term
macro_rules
| `([outer| <[ $k:inner ]> ]) => `([inner| $k])

syntax "[outerIncQuotDepth|" incQuotDepth(outer) "]" : term
macro_rules
| `([outerIncQuotDepth|  <[ $k:inner ]> ]) => `([inner| $k])


def g := "global string"

def innerQuot := [inner| $(g) ]
def outerIncQuotDepth := [outerIncQuotDepth| <[ $(g) ]> ]
-- I would expect `outerDoesNotWork` to work, because the quoting comes from inner, not outer!
-- error: expected inner
def outerDoesNotWork := [outer| <[ $(g) ]> ]

I'd like to understand if the fact that [outerIncQuotDepth|...] works, while [outer|...] does not intended behaviour. I find this somewhat counter-intuitive, since in my view, the anti-quoting of inner should be modular, and [outer|...] should not need to incQuotDepth to allow inner to perform antiquotation.

╰─$ lean --version                                                                                                                  1 ↵
Lean (version 4.0.0-nightly-2022-03-30, commit c9926b3a8b64, Release)

[Sebastian Ullrich]

Siddharth Bhat said:

and inner supports antiquotations

No, only one of your inner-embedding parsers supports antiquotations. If you do it consistently for all embeddings, it should work.

syntax "<[" incQuotDepth(inner) "]>" : outer

[Siddharth Bhat]

That's the part I find confusing about the semantics. It seems to me that my declaration of

syntax "[inner|" incQuotDepth(inner) "]" : term
macro_rules
| `([inner| $$($s)]) => return s

has created support for anti-quotation in any inner context.

However, for the antiquation of inner to work when nested, the outer context is obliged to declare:

syntax "[outerIncQuotDepth|" incQuotDepth(outer) "]" : term

which feels non-compositional to me --- the outer context (in my view) should not care if the inner context needs anti-quotation or not. Which is why I expected both declarations, [outer|...] and [outerIncQuotDepth|...] to work, and was surprised when only [outerIncQuotDepth|...] worked.

[Sebastian Ullrich]

Well, I suppose we can agree that the semantics can be confusing. This should fix them: https://github.com/leanprover/lean4/pull/1089