Zulip Chat Archive

Stream: lean4

Topic: How to mactch an operator in Macro_rules


view this post on Zulip Lim, Thing-han (Mar 19 2021 at 06:28):

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.

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 08:32):

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.

view this post on Zulip Lim, Thing-han (Mar 19 2021 at 09:45):

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 ?

view this post on Zulip Lim, Thing-han (Mar 19 2021 at 09:48):

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

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 10:10):

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

view this post on Zulip Lim, Thing-han (Mar 19 2021 at 10:36):

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 ?

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 10:42):

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

view this post on Zulip Lim, Thing-han (Mar 19 2021 at 10:45):

I am just trying to write some macros like

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

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 10:56):

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.

view this post on Zulip Lim, Thing-han (Mar 19 2021 at 10:59):

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

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 11:00):

You are confusing the definition and the usage of a notation

view this post on Zulip Lim, Thing-han (Mar 19 2021 at 11:02):

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

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 11:08):

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

view this post on Zulip Lim, Thing-han (Mar 19 2021 at 11:09):

Ah ! ok I got it! Thank you!!


Last updated: May 07 2021 at 12:15 UTC