Fun with macros

Stream: lean4

[Marcus Rossel]

Hm, how would the right side need to be expressed? I'm trying to get a comma-seperated list of the ls.

macro "unfold " l:(ident+) : tactic =>
  `(simp only [$[$l:(ident+)],*])

... doesn't work.

[Sebastian Ullrich]

Ah, l:(ident+) probably is not a good idea because it will bind l to the dummy node containing all the idents. You'd have to unpack that one to use it in antiquotations, or avoid using macro.

macro "unfold " l:(ident+) : tactic =>
  `(simp only [$(l.getArgs),*])

syntax "unfold " ident+ : tactic
macro_rules
  | `(tactic| unfold $l*) => `(simp only [$l:ident,*])

[Sebastian Ullrich]

I will try to remove that footgun from macro tomorrow

[Marcus Rossel]

I'm guessing there are more functions like getArgs... What are those defined on?

[Sebastian Ullrich]

Lean.Syntax

[Sebastian Ullrich]

(auto completion does in fact work in that place!)

[Sebastian Ullrich]

For more info on antiquotations, see also §4.1 of https://arxiv.org/pdf/2001.10490.pdf#page=11

[Marcus Rossel]

It is not this getArgs :sweat_smile:

[Sebastian Ullrich]

Not quite, it's https://github.com/leanprover/lean4/blob/341b4ac652eb24471aeb55060f423fe6616025b2/src/Init/Prelude.lean#L1750-L1753 :) . You should be able to navigate there using go-to-definition.

[Marcus Rossel]

@Sebastian Ullrich You mention in your Hygienic-Macros-Paper that

Both commands [syntax and macro_rules] can only be used at the top level; we are not currently planning support for local macros.

I've implemented both the unfold and obtain inside a namespace though, and they work. Is this intended?

[Sebastian Ullrich]

The "top level" is the command level. Local macros would be at the term level.

[Mac]

Sebastian Ullrich said:

Ah, l:(ident+) probably is not a good idea because it will bind l to the dummy node containing all the idents. You'd have to unpack that one to use it in antiquotations, or avoid using macro.

Actually, you can also do this:

macro "unfold " l:many1(ident) : tactic =>
  `(simp only [$l,*])

[Marcus Rossel]

Mac said:

Actually, you can also do this:

macro "unfold " l:many1(ident) : tactic =>
  `(simp only [$l,*])

Not sure how it is for you, but both your and my variant give me an error along the lines of:

invalid 'simp', proposition expected
  (x_0 : Sort _abstMVar.0) → x_0

[Sebastian Ullrich]

Here you really want the :ident :) . simp can contain more than just a term.

[François G. Dorais]

Doesn't simp expect a list of simpLemma? This works for me:

syntax "unfold " simpLemma,+ (location)? : tactic
macro_rules
| `(tactic|unfold $ts,* $[$loc]?) => `(tactic|simp only [$ts,*] $[$loc]?)

I don't know how to coerce an ident into a simpLemma.

[Sebastian Ullrich]

$[...] can be used for that

syntax "unfold " withPosition((colGe ident)+) (location)? : tactic
macro_rules
  | `(tactic|unfold $ids* $[$loc]?) => `(tactic|simp only [$[$ids:ident],*] $[$loc]?)