antiquot parsing

Stream: lean4

[Siddharth Bhat]

Consider:

declare_syntax_cat lhs
declare_syntax_cat exp

syntax lhs "~=" num : exp
syntax str : lhs

syntax "`[lhs|" lhs "]": term
syntax "`[exp|" exp "]": term

macro_rules
| `(`[lhs| $x:str ]) => return x
| `(`[exp| $x:lhs ~= $y:num ]) => `((`[lhs| $x], $y))
| `(`[lhs| $$($x) ]) => return x
| `(`[exp| $$($x) ]) => return x

def exp1 := `[exp| $(("one", 1))]
#eval exp1 -- ("one", 1)


def exp2 := `[exp| "two" ~= 2]
#eval exp2  -- ("two", 2)

-- expected: ("three", 3)
def exp3 := `[exp| $("thre" + "e") ~= 3]
#eval exp3 -- expected ']'

The grammar parses as

<exp> -> "$("<term>")"

We want it to parse is as:

<exp> -> <lhs> "=" <rhs>
<exp> -> "$("<term>")" "~=" <rhs>

I am unsure how to ask the parser to backtrack on the failed parse of <expr> -> "$(" <term> ")".

[Sebastian Ullrich]

That sounds like https://github.com/leanprover/lean4/pull/1272