Allowing antiquotes in custom syntax extensions?

Stream: lean4

[Andrés Goens]

I was trying to allow antiquotes in my custom syntax extensions (to get a sort of "template" syntax). I can make it work for individual syntax extensions manually by just passing the identifiers along in the macros, kind of like this:

import Lean
declare_syntax_cat paramident
declare_syntax_cat decl

syntax  ident : paramident
syntax "£" ident : paramident

syntax "var" paramident ":" paramident : decl
syntax "[decl|" decl "]" : term
macro_rules
  |  `(paramident| $x:ident) => `($(Lean.quote x.getId.toString))
  |  `(paramident| £ $x:ident ) => `($x)

open Lean.TSyntax.Compat in
macro_rules
  | `(decl| var $i:paramident : $t:paramident ) => `(($i,$t))
  | `([decl| $x]) => `(decl| $x)

def foo := "bar"
#eval [decl| var £foo : foo] -- ("bar", "foo")

This seems to have two disadvantages, however:

- I couldn't quite figure out how to use $ for my custom antiquotations (but I guess £ works here as well, it's got a sense of irony there)
- It's not very generic: I'd have to do this for every possible subterm in my syntax if I want to be able to replace it.

Looking at the code that does the antiquotation for Lean it seems that there's already a parser generator for antiquotations that but it's not exposed to the syntax extensions. Would it make sense to add that there to be able to define places where we can use antiquotes to custom syntax (in a similar way to e.g. sepBy)? It doesn't seem to be easily doable in a project-specific/library way.

[Gabriel Ebner]

It is possible to use the built-in antiquotations for your own syntax as well. For example in quote4, you can write q($x + $y) and the $x is used for custom purposes. The only downside is that you have zero control over where the antiquotations are allowed (they are allowed anywhere you'd be able to write them in a syntax quotation e.g. [decl $foo] would be valid syntax).

[Andrés Goens]

oh, interesting, and how do you do that?

[Andrés Goens]

that's actually exactly what I want to allow, although what I was suggesting could give more fine control

[Gabriel Ebner]

You can look in the souce code for inspiration: https://github.com/gebner/quote4/blob/06023076e5b41510171b43d82cbfabc82b2fd5dd/Qq/Macro.lean#L420-L421

You don't need to do anything to enable the antiquotations. You just need to handle them when going through the syntax tree with the antiquotKind? etc. functions.

[Andrés Goens]

oh, I see, so you define and manually call your own parser :sweat_smile: I guess that should also work (although I'm a bit scared of looking into that code) thanks for the inspiration :)

[Gabriel Ebner]

No custom parser just a custom macro rule. I think in your case something like the following (completely untested) should work:

macro_rules (kind := paramident)
  | stx => do
    if stx.isAntiquotKind?.isSome && stx.getAntiquotTerm.isIdent then
      quote stx.getAntiquotTerm
    else
      Macro.throwUnsupported

[Andrés Goens]

oh, that look pretty neat, thanks :smiley: ! (I'll try that and post the full example later for reference)

[Mac]

So I was trying to adapt his example to use antiquotes, but ran into the following error that I am struggling to debug:

import Lean
open Lean Parser

declare_syntax_cat decl

#check incQuotDepth -- incQuotDepth : Parser → Parser
syntax "[decl|" incQuotDepth(decl) "]" : term
  -- error: parser 'incQuotDepth' was not found???

@Gabriel Ebner any ideas as to why Lean claims incQuotDepth is missing?

[Gabriel Ebner]

incQuotDepth is no longer necessary

[Andrés Goens]

I was trying to get this to work too for this simple example and I can't figure it out. Apparently the antiquoted term is not of that kind then, but gets a derived "pseudo antiquot" kind ,paramident.pseudo.antiquot in the example and a corresponding error elaboration function for 'paramident.pseudo.antiquot' has not been implemented . I can't seem to find a way to implement the parser for that, as neither of the ways I'd think works, like

macro_rules (kind := paramident.pseudo.antiquot)

or

@[macro paramident.pseudo.antiquot]
def parseParamIdent : Lean.Macro

or even

syntax (name := paramidentantiq) "$" ident : paramident
@[macro paramidentantiq]
def parseParamIdent : Lean.Macro

[Andrés Goens]

I guess because the kind annotation takes an ident, and the @[macro ...] annotation seems to only want explicitly-named syntax, not these derived kinds

[Sebastian Ullrich]

@Andrés Goens Requiring TSyntax.Compat should be a big red flag suggesting that you're doing something wrong. Indeed you can't just return a paramident as a term, because it's not a term. The appropriate solution for that is to add a separate syntax for interpreting paramident, in which case antiquotations can naturally be implemented as cancelling out the surrounding quotation.

import Lean
declare_syntax_cat paramident
declare_syntax_cat decl

syntax ident : paramident

syntax "var" paramident ":" paramident : decl
syntax "`[decl|" decl "]" : term
syntax "`[paramident|" paramident "]" : term

open Lean

macro_rules
  |  `(`[paramident| $x:ident]) => `($(quote x.getId.toString))
  |  `(`[paramident| $x]) => if x.raw.isAntiquot then pure x.raw.getAntiquotTerm else Macro.throwUnsupported

macro_rules
  | `(`[decl| var $i : $t]) => `((`[paramident| $i], `[paramident| $t]))

def foo := "bar"
#eval `[decl| var $foo : foo] -- ("bar", "foo")

[Andrés Goens]

Thanks for the explanation @Sebastian Ullrich! I Does that mean we (now) shouldn't use the backtick (syntax_cat|...) pattern in macro rules? And do we then need an extra syntax for every nonterminal (i.e. syntax_cat) to take it to a term? Because strictly speaking that extra syntax should be unnecessary, right? We're just using it to define the macros there (and we might even not want to expose that). I thought we could define macros between arbitrary syntax_cats

[Sebastian Ullrich]

A macro from some custom syntax category into itself is fine (though Lean won't ever call it by itself, you need expandMacros for that). A macro from one category into another doesn't make sense to me, the resulting syntax tree will not be well-formed.