SepBy matcher being too greedy?

Stream: lean4

[Siddharth Bhat]

I'd like to have a trailing × symbol after a sepBy(str, "×") parser. It seems like within the syntax matcher, there is no way to match against such a syntax (I am unable to match against bar in the example below). How should I write the macro_rules for [bar|...] so I can parse the bar syntax defined below?

import Lean
import Lean.Parser
open Lean
open Lean.Parser

-- we want to parse terms of the form ["foo" × "bar" × ... ×  "quux" ×  10]
declare_syntax_cat bar
syntax sepBy(str, "×") "×" num : bar
syntax "[bar|" bar "]" : term

-- | ERROR: expected ×
macro_rules
| `([bar| $[ $xs ]×* × $y ]) => return quote xs

-- | ERROR: expected ×
macro_rules
| `([bar| $[ $xs ]×* $y ]) => return quote xs

-- vvv what does work vvv
-- The macro without the trailing ×  num works!
declare_syntax_cat foo
syntax sepBy(str, "×")  : foo
syntax "[foo|" foo "]" : term

macro_rules
| `([foo| $[ $xs ]×* ]) => return quote xs

[Sebastian Ullrich]

Yes, sepBy is greedy. I'm not sure how it could avoid that without arbitrary backtracking. You should use sepBy(str <|> num, "×") and enforce the typing in the macro rules instead.

[Leonardo de Moura]

You can also use notFollowedBy. Example:

declare_syntax_cat bar

syntax sepBy(str, "×", "×" notFollowedBy(num)) "×" num : bar

syntax "[bar|" bar "]" : term

macro_rules
| `([bar| $[ $xs ]×* × $y ]) => return Lean.quote (xs, y)

#check [bar| "foo" × "bar" × 10]
-- (#["foo", "bar"], 10) : Array String × Nat