Pass optional syntax in macro

Stream: lean4

[Patrick Massot]

In the following code, a call to tactic bar is meant to expand to the same call to foo. But I don't know how to pass the optional syntax. Both variations below fail.

open Lean Parser Tactic

macro "foo" (location)? : tactic => `(tactic|done)

macro "bar" loc:(location)? : tactic => `(tactic|foo $loc)

macro "bar" loc:(location)? : tactic => `(tactic|foo $(mkOptionalNode loc))

[Mac Malone]

@Patrick Massot $[...]? is used for optional syntax:

macro "bar" loc?:(location)? : tactic => `(tactic|foo $[$loc?]?)

[Patrick Massot]

Thanks a lot. It almost work in my real use case. It fails in the presence of a mysterious & in the original syntax;

[Patrick Massot]

Something like

macro "foo" (&"baz")? (location)? : tactic => `(tactic|done)

macro "bar" ba:(&"baz")? loc:(location)? : tactic => `(tactic|foo $[$ba]? $[$loc]?)

[Sebastian Ullrich]

The syntax for individual tokens is a bit different

macro "bar" ba:(&"baz")? loc:(location)? : tactic => `(tactic|foo $[baz%$ba]? $[$loc]?)

[Patrick Massot]

Thanks!

[Patrick Massot]

Next I need to remember how to write a macro which expand to several tactic calls, fighting the difference between tactic and tactic_seq.

[Patrick Massot]

Say I want to add done after foo $[baz%$ba]? $[$loc]?, how do I do that?

[Sebastian Ullrich]

You can use parentheses to turn a tactic sequence into a single tactic

[Patrick Massot]

I knew there was a simple trick but I couldn't remember it. Thanks!

[Patrick Massot]

I hit again the same issue as in July but I can't get the above answer to work. If have a tactic whose definition starts with

elab tok:"rw_ineq" rules:rwRuleSeq loc:(location)? withArg:((" with " (colGt binderIdent)+)?) : tactic =>

and I want a macro rwa_ineq with the exact same syntax that call rw_ineq and then assumption. I tried

macro "rwa_ineq " rws:rwRuleSeq loc:(location)? withArg:(" with " (colGt binderIdent)+)? : tactic =>
  `(tactic| (rw_ineq $rws:rwRuleSeq $[$loc:location]? $[$withArg:location]?; assumption))

but that doesn't work.

Full code is

import Lean

open Lean Parser Meta Elab Term Tactic

elab tok:"rw_ineq" rules:rwRuleSeq loc:(location)? withArg:((" with " (colGt Lean.binderIdent)+)?) : tactic =>
  pure ()

macro "rwa_ineq " rws:rwRuleSeq loc:(location)? withArg:(" with " (colGt Lean.binderIdent)+)? : tactic =>
  `(tactic| (rw_ineq $rws:rwRuleSeq $[$loc:location]? $[$withArg:location]?; assumption))

[Kyle Miller]

Here's one way:

import Lean

open Lean Parser Meta Elab Term Tactic

syntax withClause := " with " (colGt Lean.binderIdent)?

elab tok:"rw_ineq" rules:rwRuleSeq loc:(location)? withArg:(withClause)? : tactic =>
  pure ()

macro "rwa_ineq " rws:rwRuleSeq loc:(location)? withArg:(withClause)? : tactic =>
  `(tactic| (rw_ineq $rws:rwRuleSeq $[$loc:location]? $[$withArg]?; assumption))

[Kyle Miller]

Here's another:

import Lean

open Lean Parser Meta Elab Term Tactic

elab tok:"rw_ineq" rules:rwRuleSeq loc:(location)? withArg:((" with " (colGt Lean.binderIdent)+)?) : tactic =>
  pure ()

syntax "rwa_ineq " rwRuleSeq (location)? (" with " (colGt Lean.binderIdent)+)? : tactic

macro_rules
  | `(tactic| rwa_ineq $rws $[$loc]? $[with $args*]?) =>
    `(tactic| rw_ineq $rws $[$loc]? $[with $args*]?)

[Patrick Massot]

Great, the first solution works (with minor ajustements to the code)! Thanks!

[Patrick Massot]

I'm still curious to understand why my original code didn't work (and it would be really great to have any of this documented somewhere).