How to mactch an operator in Macro_rules

Stream: lean4

[Lim, Thing-han]

How can I match an operator in the Macro_rules ?

I am trying to match an operator and do something corresponding to its affix.
For instance,

syntax "{| " term* " |}" : term
macro_rules
| `({| $a $op $b |}) => do
    match op with
     | `(infixl $[: $prec]? $[(name := $name)]? $[(priority := $prio)]? $op => $f) => sorry
     | _ => Macro.throwUnsupported

but it doesn't seem to work, and I am not sure what do I miss.

[Sebastian Ullrich]

Binary operators do not share a common syntax kind, nor can they be traced back to the original notation command. So whatever you are trying to do, I believe you need a fundamentally different approach.

[Lim, Thing-han]

Oh, does it mean that I am not able to identify if a syntax is operator or not, either using macro_rules or via the elaboration monad ?

[Lim, Thing-han]

Is is possible to get syntax (or some other structures) after the macro expansion of operators but before type checking ?

[Sebastian Ullrich]

Macro expansion and elaboration are intertwined, but you can call expandMacros explicitly to expand as much as possible (including all notations) without elaboration.

[Lim, Thing-han]

While using expandMacros to expand the operator notation as much as I want, will I need to first check if the syntax is of some kind of notation ?

[Sebastian Ullrich]

I still don't know what you are trying to do

[Lim, Thing-han]

I am just trying to write some macros like

macro {| $a $op1 $b $op2 $c ...|}  => `(($op2 <$> ($op1 <$> $a <*> $b) <*> $c) ...)

[Sebastian Ullrich]

I've never seen idiom brackets that work recursively like this, or are restricted to operators. In any case, the point stands that you cannot really distinguish infix operators from other syntax. But you can unfold them, using expandMacros.

[Lim, Thing-han]

But that I saw that expandMixfix can match the syntax to see if it's infix, prefix or postfix?

[Sebastian Ullrich]

You are confusing the definition and the usage of a notation

[Lim, Thing-han]

Is there documentation or which files should I look into to help me clarify it ?

[Sebastian Ullrich]

expandMixfix is called when you use the infix command, not when you use the operator created by it

[Lim, Thing-han]

Ah ! ok I got it! Thank you!!