Quoting commands

Stream: lean4

[Mario Carneiro]

How do I put a type ascription in a syntax quotation? The term defaulting is causing problems for me:

syntax "bla" : command

macro_rules | `(bla) => `(open foo) -- expected 'in'

I tried `(command| open foo) but it doesn't work (nor various attempts at a qualified name for the parser category).

[Mario Carneiro]

Does the missing space after "variable" mean anything?

@[builtinCommandParser] def «namespace»    := leading_parser "namespace " >> ident
@[builtinCommandParser] def «end»          := leading_parser "end " >> optional ident
@[builtinCommandParser] def «variable»     := leading_parser "variable" >> many1 Term.bracketedBinder
@[builtinCommandParser] def «universe»     := leading_parser "universe " >> many1 ident
...

[Mac]

Mario Carneiro said:

Does the missing space after "variable" mean anything?

It just won't be pretty-printed as "variable " but instead "variable" (i.e. variable {a} would be pretty printed variable{a}).

[Mac]

To your main question, you could always go for broke and define a command quotation yourself:

import Lean

syntax (name := cmdQuot) "`(command|" incQuotDepth(command) ")" : term

open Lean Elab Term Quotation in
@[termElab cmdQuot] def elabCmdQuot : TermElab :=
  adaptExpander stxQuot.expand

syntax "bla" ident : command

macro_rules | `(bla $id) => `(command| open $id:ident)

bla Lean -- works

[Sebastian Ullrich]

I believe when we implemented the quotations we did not have overlapping term/command syntax yet. We should probably use the longest parse of the two of them. And generalizing the quotation kind syntax to arbitrary categories/parsers is TBD (it actually already works with syntax_cat).

[Mac]

Sebastian Ullrich said:

And generalizing the quotation kind syntax to arbitrary categories/parsers is TBD (it actually already works with syntax_cat).

Would you happen to know if the custom command quotation hack I presented is perfectly serviceable substitute in end-user code until core gets around to that or are there some thorns / concerns one should keep in mind?

[Sebastian Ullrich]

Looks fine, it's identical to the built-in ones, right?

[Mac]

I think so.

[Mario Carneiro]

I'm going to need almost all other syntax categories as well soon, so that TBD interests me. Will it work if I just copy Mac's code for random parsers? The word command in incQuotDepth(command) is coming from a fairly small list of options, I think (category parsers?)

[Sebastian Ullrich]

Yes, it should work for any parser, category or not. In fact the Lean package uses a common macro to declare the elaborators: https://github.com/leanprover/lean4/blob/e2210ec4e04beb78289c37cbf9ee1ccee0d032db/src/Lean/Elab/Quotation.lean#L183-L195

[Mario Carneiro]

Oh great, can I use that too? Does that overload `(...) or does it define `(bla| ...)?

[Sebastian Ullrich]

That depends purely on your syntax definition going with it :) .

[Mario Carneiro]

Are all those elaborators attaching to the same syntax?

[Sebastian Ullrich]

In fact that last one should already implement `(p|...)` for any p : (Trailing)Parser in scope after all. It's just that the parser for command is called commandParser, and it takes an extra parameter, so it didn't work out of the box for this one.

[Mac]

Sebastian Ullrich said:

In fact the Lean package uses a common macro to declare the elaborators: https://github.com/leanprover/lean4/blob/e2210ec4e04beb78289c37cbf9ee1ccee0d032db/src/Lean/Elab/Quotation.lean#L183-L195

Note that while I stole the code for my example from this macro, I did not use it directly because it defines builtin parsers rather than normal parsers -- the later being the kind of parser you generally want for user code (as it works in the same file).

[Mario Carneiro]

Why doesn't this work? (Using `(command| doesn't seem to make a difference.)

import Lean
open Lean

example (bis : Array Syntax) : MacroM Syntax :=
  `(variable $[$bis]+)
          -- ^ expected '(', '*', '[', '{' or identifier

[Mario Carneiro]

I tried sticking :bracketedBinder in various places but I couldn't find one that was syntactically correct

[Mario Carneiro]

This looks like a similar issue (using Mac's command| quotation):

example (foo : Syntax) (names : Array Syntax) : MacroM Syntax :=
  `(command| open $foo ($[$names]*))
                    -- ^ expected ')'

[Mac]

Mario Carneiro said:

Why doesn't this work? (Using `(command| doesn't seem to make a difference.)

import Lean
open Lean

example (bis : Array Syntax) : MacroM Syntax :=
  `(variable $[$bis]+)
          -- ^ expected '(', '*', '[', '{' or identifier

This doesn't work because there is no $[...]+ (with a plus), there is only a $[...]* (with an asterisk).

[Mac]

Mario Carneiro said:

This looks like a similar issue (using Mac's command| quotation):

example (foo : Syntax) (names : Array Syntax) : MacroM Syntax :=
  `(command| open $foo ($[$names]*))
                    -- ^ expected ')'

This one doesn't work because $foo needs to be $foo:ident.