Disable hygiene for specific variables

Stream: metaprogramming / tactics

[Pavel Klimov]

I want to use elaborators to automatically generate definitions. Naturally, I want to combine it from parts. Here is some basic test:

macro "m1" : command => `(
  def f (x : List Nat) := x.sum
)
m1
#eval f [1, 2, 3]

It says

Unknown identifier `f`

Because f is hidden under hygiene names mangling. You can disable hygiene like in following code:

macro "m1" : command => set_option hygiene false in `(
  def f (x : List Nat) := x.sum
)
m1
#eval f [1, 2, 3]

And it will work as intended. Other workaround I found when I tried to pass f as an argument to macro, and it did work, but I still want to generate identifier inside macro, so I came to following idea:

macro "m1" : command =>
  let f := Lean.Syntax.ident .none "f".toSubstring `f [] |>  Lean.TSyntax.mk
  `(
  def $f (x : List Nat) := x.sum
)
m1
#eval f [1, 2, 3]

So, it is utilizing behavior of antiquotations. Antiquotations inserted as they are. Issues comes when I want to generate x and then use it in syntax like x.sum. Why? Well, it turns out that x.sum is actually inserted in syntax as a name. And x and x.sum are different names. So, if pattern which have x.sum have different hygiene, then to make it work, I need to force them to match. Another issue is, x can be in different places which require different TSyntax kind. And, I don't know other way than just making new variable for each TSyntax kind.

Is there any good / intended way to work with situations like this, except set_option hygiene false?

[Aaron Liu]

Well there's Unhygienic.run

[Pavel Klimov]

Aaron Liu :

Well there's Unhygienic.run

Any example? I don't understand documentation about Unhygenic. When I tried Unhygenic.run instead of set_option hygiene false, instead of f I got f._@.UnhygienicMain._hyg.1

[Robin Arnez]

Unhygienic.run doesn't disable hygiene but it uses dummy hygiene data.

[Robin Arnez]

What you're supposed to do is something similar to what you did in your third code snippet, except there's a function for it (docs#Lean.mkIdent):

open Lean

macro "m1" : command => `(def $(mkIdent `f) (x : List Nat) := x.sum)
m1
#eval f [1, 2, 3] -- works