Macros without prefix/suffix

Stream: lean4

[Siddharth Bhat]

Consider the macro kvbare which creates custom syntax str ^^^ str to create a key-value tuple:

declare_syntax_cat kvbare
syntax str "^^^" str  : kvbare

syntax "kvbare% " kvbare : term
macro_rules
  | `(kvbare% $i ^^^  $j ) => `( $i )

def foobare := (kvbare%  "foobare"  ^^^  "barbare" )

The above errors with:

Lean (version 4.0.0, commit db5df69db460, Release)

error: elaboration function for '«termKvbare%_»' has not been implemented
kvbare% "foobare"^^^"barbare"

I'm quite puzzled as to what's going on since a small change in the macro, which adds a prefix of [ and a suffix of ] succeeds:

declare_syntax_cat kv
syntax "[" str "^^^" str "]" : kv

syntax "kv% " kv : term
macro_rules
  | `(kv% [ $i ^^^  $j ]) => `( $i )

def foo := (kv% [ "foo"  ^^^  "bar" ] )

Is there some way to get the original macro (kvbare) working? If not, what's the problem with it? (lack of prefix/suffix?)

[Leonardo de Moura]

The problem is that the pattern

macro_rules
  | `(kvbare% $i ^^^  $j ) => `( $i )

is being interpreted as

macro_rules
  | `(kvbare% $i:kvbare ^^^  $j:term ) => `( $i )

Recall that we have

infixl:58 " ^^^ " => HXor.hXor

To get the behavior you expect, you should write

macro_rules
  | `(kvbare% $i:strLit ^^^  $j:strLit ) => `( $i )

[Leonardo de Moura]

In the future, we should display the category of pattern variables when we hover over them in VS Code. I think it will help users to diagnose this kind of problem.