Stateful/Aggregating Macros?

Stream: lean4

[Andrés Goens]

I have a macro that I'm using to define some thing (a structure) and also remember its name in the structure, something like this

structure Thing (α : Type 0) where
  (thething : α)
  (name : String)

macro "defthing" name:ident " := " thing:term : command => `(def $name := Thing.mk $thing $(Lean.quote name.getId.toString))

defthing mything := 42
defthing myotherthing := 2
#eval mything.name -- "mything"

I would also like to aggregate all the structures I define this way:

def allthings := [mything, myotherthing]

Is there a nice way to do this with that macro too?

[Alexander Bentkamp]

Once a constant is defined, the definition cannot be changed. So there is no way to have allthings to be defined as [] first, then as [mything], and later as [mything, myotherthing].

[Alexander Bentkamp]

You could define a custom attribute thing and then mark all your definitions with it:

macro "defthing" name:ident " := " thing:term : command => `(@[thing] def $name := Thing.mk $thing $(Lean.quote name.getId.toString))

Then, using meta-programming, you can identify and collect all definitions marked @[thing]. Macros alone won't be able to do this.

[Andrés Goens]

that sounds like a good solution, thanks!

[Mario Carneiro]

You can see how this is done in mathport: There is a declaration of the @[trTactic] attribute, which creates an environment extension and adds all marked theorems to the extension. Then there is a trTactics! macro which expands to a list literal containing all tactics that have been marked so far. Then we mark lots of declarations with the attribute, and then call the macro after importing all the tagged declarations to get a big list.