How to turn a macro_rules into an elab

Stream: metaprogramming / tactics

[Yaël Dillies]

I am trying to extend a macro_rules I wrote by adding some logic about expected types (see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.7Bx.20.E2.88.88.20s.20.7C.20p.20x.7D.20notation.20for.20finset ). Hence I need to use an elab instead. However, I don't even know what the elab corresponding to my macro_rules should be!

[Yaël Dillies]

Could someone explain me how to turn a macro_rules into an elab? I would be happy with a translation of this example from the metaprogramming book:

syntax:10 term:10 " RXOR " term:11 : term

macro_rules
  | `($l:term RXOR $r:term) => `($l && !$r)

elab (name := myName) "(" l:term " RXOR " r:term ")" : term => do
  return sorry -- What goes here?

[Damiano Testa]

Is this close enough?

import Lean
open Lean Elab Term
syntax:10 term:10 " RXOR " term:11 : term

macro_rules
  | `($l:term RXOR $r:term) => `($l && !$r)

elab (name := myName) "(" l:term " RXOR " r:term ")" : term => do
  let l ← elabTerm l none
  let r ← elabTerm r none
  Meta.mkAppM ``Or #[l, r]

[Yaël Dillies]

Hmm, I was hoping I could keep using the quotations...

[Yaël Dillies]

Can you translate the macro_rules from this message? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.7Bx.20.E2.88.88.20s.20.7C.20p.20x.7D.20notation.20for.20finset/near/428138832

[Damiano Testa]

This should also work:

elab (name := myName) "(" l:term " RXOR " r:term ")" : term => do
  elabTerm (← `($l || $r)) none