Zulip Chat Archive

Stream: lean4

Topic: commandElab behaving weirdly


David Renshaw (Jun 23 2022 at 17:15):

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 (Jun 23 2022 at 17:35):

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 (Jun 23 2022 at 18:09):

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

Gabriel Ebner (Jun 23 2022 at 18:09):

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 (Jun 23 2022 at 18:10):

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

Gabriel Ebner (Jun 23 2022 at 18:11):

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

David Renshaw (Jun 23 2022 at 19:55):

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 (Jun 23 2022 at 19:56):

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

David Renshaw (Jun 23 2022 at 20:36):

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 (Jun 23 2022 at 20:37):

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

David Renshaw (Jun 23 2022 at 20:58):

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 (Jun 24 2022 at 13:07):

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.


Last updated: Dec 20 2023 at 11:08 UTC