Disabling Macro Hygine?

Stream: lean4

[Siddharth Bhat]

I wish to write a macro which elaborates in the context of another macro. I use identifiers like i32 to refer to types. Unfortunately, since these types are identifiers, the hygiene system changes them to things like i32._@._hyg.746. These fail macro expansion (since they don't look like i<int>). Question: Can I disable hygiene for certain (known) identifiers?

For some context: I have a macro [mlir_op| ...] provides a low-level macro for building ASTs. A high level macro prettyOp
expands into [mlir_op| "std.prettyOp" : i32]. It is during this expansion that the i32 becomes i32._@._hyg.746, which fails the parserule for [mlir_type| $x:ident ].

import Lean.Parser
import Lean.Parser.Extra

open Lean
open Lean.Parser


mutual
inductive MLIRTy : Type where
| int : Int -> MLIRTy

inductive Op : Type where
 | mk: (name: String) -> (ty: MLIRTy) -> Op
end


declare_syntax_cat mlir_op
declare_syntax_cat mlir_type

syntax ident: mlir_type


syntax "[mlir_type|" mlir_type "]" : term

macro_rules
  | `([mlir_type| $x:ident ]) => do
        let xstr := x.getId.toString
        if xstr.front == 'i'
        then do
          let xstr' := xstr.drop 1
          match xstr'.toInt? with
          | some i =>
            let lit := Lean.Syntax.mkNumLit xstr'
            `(MLIRTy.int $lit)
          | none =>
              Macro.throwError $ "cannot convert suffix of i to int: " ++ xstr
        else Macro.throwError "expected i<int>" -- `(MLIRTy.int 1337)

def tyi32NoGap : MLIRTy := [mlir_type| i32]

syntax strLit ":" mlir_type : mlir_op
syntax "[mlir_op|" mlir_op "]" : term
macro_rules
  | `([mlir_op| $name:strLit : $ty:mlir_type ]) => do
        `(Op.mk $name [mlir_type| $ty])

syntax "prettyOp"  : mlir_op  -- operation that returns an i32
macro_rules
  | `([mlir_op|prettyOp]) => do `( [mlir_op| "std.prettyOp" : i32] )

def prettyBad0 := [mlir_op| prettyOp]
#print prettyBad0

[David Renshaw]

Does set_option hygiene false work for you? See e.g. https://github.com/leanprover/lean4/blob/fb27537b8ee686251f5e51d7daf6c467731994c3/tests/lean/unhygienic.lean#L15

[Siddharth Bhat]

Yes, this seems to do the trick! In particular, changing the rule for the macro expansion of prettyOp to be:

set_option hygiene false in
macro_rules
  | `([mlir_op|prettyOp]) => do `( [mlir_op| "std.prettyOp" : i32] )

works.

Now I must ask another question: Is this an abuse of the Lean macro system? Should Can I achieve the same effect in a different way? I am worried that disabling hygiene will have other effects that I don't anticipate.

[Gabriel Ebner]

You can use eraseMacroScopes to get the name the user typed (i).
I think you can also match on the i directly (i instead of $x:ident), but I'm not sure how that interacts with hygiene.