commandElab behaving weirdly

Stream: lean4

[David Renshaw]

What is going on here? Why does the match not hit the .. case?

import Lean.Elab.Command

syntax (name := foobar) " ♫ " ((ident ident) <|> " .. ") : command

@[commandElab foobar] def elabFoobar : Lean.Elab.Command.CommandElab
| `(♫ $i1:ident $i2:ident) => do dbg_trace "idents"
| `(♫ ..) => do dbg_trace "dots"
| _ => do dbg_trace "no match"

♫ a b
-- "idents"

♫ ..
-- "no match"
-- why isn't this "dots"?

[David Renshaw]

I suppose I should just write separate syntax commands for the different branches.

import Lean.Elab.Command

syntax (name := foobar) " ♫ " ident ident : command
syntax (name := foobar') " ♫ " " .. " : command

@[commandElab foobar] def elabFoobar : Lean.Elab.Command.CommandElab
| `(♫ $i1:ident $i2:ident) => do dbg_trace "idents"
| _ => do dbg_trace "no match"

@[commandElab foobar'] def elabFoobar' : Lean.Elab.Command.CommandElab
| `(♫ ..) => do dbg_trace "dots"
| _ => do dbg_trace "no match"

♫ a b
-- "idents"

♫ ..
-- "dots", as expected

[Gabriel Ebner]

Short answer: you need to write group(ident ident). See lean4#1229

[Gabriel Ebner]

The thing is that Lean 4 parsers have an arity: they do not just parse a single syntax object, but a whole array (and the size of the array is the arity).

[Gabriel Ebner]

So ident produces one syntax, ident ident produces two syntaxes, ppLine produces no syntaxes.

[Gabriel Ebner]

Most of the code assumes that both sides of <|> have the same arity, that's why you ran into troubles here.

[David Renshaw]

another weird behavior I don't understand:

import Lean.Elab.Command

syntax (name := baz) " ♫ " Lean.binderIdent : command

@[commandElab baz] def elabBaz : Lean.Elab.Command.CommandElab
| `(♫ _) => do dbg_trace "underscore"
| `(♫ $i:ident) => do dbg_trace "ident"
| _ => do dbg_trace "no match"

♫ _
-- "underscore"

♫ f
-- "underscore"
-- why doesn't this print "ident"?

[David Renshaw]

If i switch the order of the match arms, then it behaves as I expect.

[David Renshaw]

Indeed, if I switch the order of these match arms in mathlib4, a bunch of things break: https://github.com/leanprover-community/mathlib4/blob/20c6d70bd1300d2b8dea061731b3e011380b94c3/Mathlib/Init/ExtendedBinder.lean#L31-L35

[David Renshaw]

Is the _ somehow also acting as a catch-all here?

[David Renshaw]

My hypothesis was that this had something to do with _ getting misinterpreted as a catch-all pattern, but the same problem happens if I use ~:

import Lean.Elab.Command

syntax binderIdent' := ident <|> "~"

syntax (name := baz) " ♫ " binderIdent' : command

@[commandElab baz] def elabBaz : Lean.Elab.Command.CommandElab
| `(♫ ~) => do dbg_trace "squiggle"
| `(♫ $i:ident) => do dbg_trace "ident"
| _ => do dbg_trace "no match"

♫ ~
-- "squiggle"

♫ f
-- "squiggle"
-- why doesn't this print "ident"?

[Sebastian Ullrich]

The short answer is that quotation patterns do not check atoms such as "~" here, so you need to put the non-atom pattern first. There is some related discussion at https://github.com/leanprover/lean4/issues/638.