elab `foo with x y`

Stream: lean4

[David Renshaw]

import Lean

open Lean Elab.Tactic

elab (name := foo) "foo " withArg:(" with " (colGt binderIdent)+)? : tactic =>
  do dbg_trace withArg
     pure ()

example : True := by
  foo with x y z -- prints `none`
  exact True.intro

why does this print none? I expect it to print the with x y z syntax.

[David Renshaw]

A similar thing apparently does work for the cases tactic: https://github.com/leanprover-community/mathlib4/blob/63a677d81af026760e1f530bb588696a123835c0/Mathlib/Tactic/Cases.lean#L93

[David Renshaw]

Aha!
Just needed more parens, seemingly:

elab (name := foo) "foo " withArg:((" with " (colGt binderIdent)+)?) : tactic =>
  do dbg_trace withArg
     pure ()

[David Renshaw]

I guess the ? binds less tightly than I was assuming it did.

[Mario Carneiro]

No, the parens are not about precedence there

[Mario Carneiro]

This looks like a bug in the macro parser (cc: @Sebastian Ullrich ): because the withArg nested parser has arity 2 (" with " (colGt binderIdent)+), calling getOptional? on it in the macro code yields none instead of the expected data

[Mario Carneiro]

it's possible that the macro can't do anything about it though since ATM parser arities are not known at compile time

[Mario Carneiro]

you should just not use elab for this and use a separate syntax / elab_rules:

syntax (name := foo) "foo " (" with " (colGt binderIdent)+)? : tactic
elab_rules : tactic
  | `(tactic| foo $[with $withArg*]?) => do
    dbg_trace withArg

[David Renshaw]

The (colGt binderIdent)+ -> $withArg* part there is surprising to me. The plus turns into a star?

[Mario Carneiro]

yes, there is no + modifier in patterns

[Mario Carneiro]

since they both bind as TSyntaxArray

[Mario Carneiro]

maybe we should add it just as a synonym to make things look more regular (no pun intended)

[David Renshaw]

I think that might be where I got stuck when I tried to do an elab_rules for this earlier.

[David Renshaw]

But it makes sense now that you explained it.

[Sebastian Ullrich]

Mario Carneiro said:

This looks like a bug in the macro parser (cc: Sebastian Ullrich ): because the withArg nested parser has arity 2 (" with " (colGt binderIdent)+), calling getOptional? on it in the macro code yields none instead of the expected data

Ah, hm, https://github.com/leanprover/lean4/blob/c672046767611565b84729db06a7c416625591b4/src/Lean/Elab/MacroArgUtil.lean#L39-L41

[Sebastian Ullrich]

The intention indeed was that macro/elab should only be used for "simple" arguments

[Mario Carneiro]

we assume the user knows what they are doing

famous last words

[Sebastian Ullrich]

It's not really for trust in the user but for lack of better options

[Mario Carneiro]

I think even a panic would be better than just returning none

[Mario Carneiro]

with this version, you have to go debugging to figure out what's wrong

[Sebastian Ullrich]

In theory we now have all the information we need to statically check this https://github.com/leanprover/lean4/pull/1229