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).

[Alex Keizer]

I'm running into similar issues: I currently have a macro like this

macro res:mlir_op_operand " = " "llvm.mlir.constant" x:num " : " t:mlir_type : mlir_op =>

I'd like to make the " : " t:mlir_type part optional. In a macro_rules, I can write $[: $t]? and everything works, but in a macro this doesn't seem to work. Going by the messages in this thread, the syntax for macro seems to be t:(" : " mlir_type), but now the bound t is of type TSyntax Name.anonymous, rather than the t : TSyntax `mlir_type I originally had.

I guess I could index into it, but I'd rather not. Is there not an equivalent of $[: $t]? which allows me to bind just the part I actually want?

[Kyle Miller]

Not to my knowledge. I would suggest either the withClause example or writing a separate syntax and using macro_rules instead.

[Alex Keizer]

The annoying thing is that the " : " token occurs only in the input, in the thing I'm rewriting to I only want the actual t. I was hoping to avoid the duplication macro_rules gives, but knowing there's no good alternatiove will let me stop worrying about it, thanks!

[Alex Keizer]

I've got another question about optional syntax and macros, now about how to deal with optional parts that are just atomic tokens. How do I combine the two match arms into one in the following MWE:

import Lean
open Lean

syntax neg_num := "-"? num

/-- Convert a possibly negated numeral into a term representing the same value -/
def negNumToTerm : TSyntax ``neg_num → MacroM Term
-- This works, but I'd like to combine the first two cases
  | `(neg_num| $x:num) => `($x:num)
  | `(neg_num| -$x:num) => `(-$x:num)
  | _ => Macro.throwUnsupported


def negNumToTerm₂ : TSyntax ``neg_num → MacroM Term
  | `(neg_num| $[-]? $x:num) =>
  --           ^^^^^ I can match this part optionally
    `(term| $[-]? $x:num)
  --        ^^^^^ This, however, Lean does not like (`unexpected token ...`)
  -- I'm unsure how to then output the minus conditionally, or even how to
  -- give a name to the matched minus to check whether it was present or not in
  -- the macro body
  | _ => Macro.throwUnsupported

[Damiano Testa]

You can give a name to the token, by using the syntax $[-%$minus]?.

I'm not sure how to feed minus back into the syntax, though.

[Damiano Testa]

Actually, this seems to work, but I am not sure if it is what you want:

  | `(neg_num| $[-%$minus]? $x:num) => `($(⟨minus.getD default⟩) $x:num)

[Alex Keizer]

Thanks! I didn't know about the % syntax. It'd be cool if we could somehow control which token controls a $[...]? antiquotation (i.e., on the RHS), without that token being part of the actual output.
For now, I'll just accept the two-match arms version is probably the most concise it gets, without impacting readability too much

[Kyle Miller]

The - isn't just a token here; in -$x:num it's parsing as the syntax for negation. It looks something like this:

• Syntax of kind «term-_»
  • arg[0]: - atom
  • arg[1]: ... syntax for $x ...

You can't conditionally include - or not because this «term-_» node is an essential part of it being negation.

[Kyle Miller]

If you want to combine the cases, you could at least do this:

def negNumToTerm : TSyntax ``neg_num → MacroM Term
  | `(neg_num| $[-%$min]? $x:num) =>
    if min.isSome then
      `(-$x)
    else
      `($x)
  | _ => Macro.throwUnsupported

[Kyle Miller]

Damiano Testa said:

  | `(neg_num| $[-%$minus]? $x:num) => `($(⟨minus.getD default⟩) $x:num)

This is surely not correct. If you're ever writing $(⟨x⟩) you have to proceed very carefully because it's converting x to have type Syntax and then allowing it to be used as TSyntax k for any k, even if it's not correct.

If you look at what this code expands to (using #print negNumToTerm) you can see that it takes minus, uses default if it's missing (which for syntax is Syntax.missing, which will signal an error during elaboration), and then creates a function application Syntax with this result as the function and $x as the argument.

[Damiano Testa]

Oh, right: juxtaposition is function application!

[Robert Maxton]

Same question:

import Batteries.Tactic.Init

namespace Tactic.Conv
macro (name := cast) "cast " h?:(term)? : conv => `(conv | equals (cast ?h ?rhs) => rfl $[; exact $h?]?)

[Robert Maxton]

I can get it to compile as

macro (name := cast) "cast " h?:(term)? : conv => do
  let tacs ← if let some h := h? then `(tacticSeq| rfl; exact $h ) else `(tacticSeq| rfl)
  `(conv | equals (cast ?h ?rhs) => $tacs)

(this doesn't really do the thing I want, but that's a separate problem)
but I'd like to understand why the first version doesn't work.

[Kyle Miller]

Here's a trick:

macro (name := cast) "cast " h?:(term)? : conv =>
  `(conv | equals (cast ?h ?rhs) => rfl; $[exact $(h?.toArray)]*)

[Kyle Miller]

The issue is that $[...]? is for optional syntax nodes, but a tactic sequence is a sequence of syntax nodes. We're able to splice in an array of nodes this way, and we can use Option.toArray to make it be compatible.

[Kyle Miller]

I wonder if $[...]* should be friendly able to handle Option like this automatically?

Or maybe sequences should accept $[...]? syntax too in antiquotations?

(Or both?)

[Robert Maxton]

Ahhh, I see. I vaguely recall running into a similar problem last year, too, where the "can't simultaneously expand multiple sequences of different lengths" restriction turned out to mean that you couldn't expand an optional term and an array of length > 1.

[Robert Maxton]

Anyway, thanks!