Lean nested syntax extension with identifiers

Stream: lean4

[Andrés Goens]

I'm trying to do a syntax extension along the lines of this tutorial. Defining special syntax to interpret my syntax categories as terms seems to work well, except that it breaks when I have an identifier at the end of a chain of nests. I tried breaking this into a #MWE:

import Lean.Syntax

declare_syntax_cat expr

syntax expr "+" expr : expr
syntax ident : expr

syntax "[expr|" expr "]" : term

macro_rules
| `([expr| $lhs:ident + $rhs:ident]) => do
  let lhsString := lhs.getId.toString
  let lhsSyntax := Lean.quote lhsString
  `($lhsSyntax ++ " + " ++ [expr|$rhs])

macro_rules
| `([expr|$x:ident]) => do
let xString : String := x.getId.toString
return Lean.quote xString


#check [expr| bar]
#check [expr| foo + bar]

The first #check will work great and produce "bar" : String, the second one works for the lhs where I've inlined it, and will complain about the rhs, with:

elaboration function for '«term[expr|_]»' has not been implemented
  [expr|bar]

This is clearly what it was just able to elaborate above! Am I doing something wrong here, or is this a yet unimplemented feature in the syntax extension? Thanks!

[Arthur Paulino]

You need to tell Lean about `([expr|$x:expr])

declare_syntax_cat expr

syntax expr " + " expr : expr
syntax ident : expr

syntax "[expr|" expr "]" : term

macro_rules
| `([expr| $lhs:ident + $rhs:ident]) =>
  let lhsString := lhs.getId.toString
  let lhsSyntax := Lean.quote lhsString
  `($lhsSyntax ++ " + " ++ [expr|$rhs])
| `([expr|$x:ident]) =>
  let xString : String := x.getId.toString
  return Lean.quote xString
| `([expr|$x:expr]) =>
  let xString : String := x.getId.toString
  return Lean.quote xString


#check [expr| bar]
#check [expr| foo + bar] -- "foo" ++ " + " ++ "bar" : String

I think the third case needs adjustments towards generality though