Zulip Chat Archive

Stream: lean4

Topic: Quoting commands


Mario Carneiro (Jul 06 2021 at 00:34):

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 (Jul 06 2021 at 00:44):

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 (Jul 06 2021 at 01:17):

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 (Jul 06 2021 at 01:18):

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 (Jul 06 2021 at 07:21):

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 (Jul 06 2021 at 07:28):

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 (Jul 06 2021 at 07:43):

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

Mac (Jul 06 2021 at 15:15):

I think so.

Mario Carneiro (Jul 06 2021 at 19:03):

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 (Jul 06 2021 at 19:11):

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 (Jul 06 2021 at 19:12):

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

Sebastian Ullrich (Jul 06 2021 at 19:13):

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

Mario Carneiro (Jul 06 2021 at 19:15):

Are all those elaborators attaching to the same syntax?

Sebastian Ullrich (Jul 06 2021 at 19:15):

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 (Jul 06 2021 at 20:27):

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 (Jul 06 2021 at 21:03):

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 (Jul 06 2021 at 21:04):

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

Mario Carneiro (Jul 06 2021 at 21:19):

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 (Jul 06 2021 at 21:30):

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 (Jul 06 2021 at 21:30):

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.


Last updated: Dec 20 2023 at 11:08 UTC