Most idiomatic way to (meta)programatically generate inducti

Stream: lean4

[Alex Keizer]

As part of a macro I'm implementing I want to generate an inductive type and add it to the environment.
I've found MonadEnv.addDecl that does the "adding to the environment" part, but it requires a fully elaborated Declaration object, so using it is quite painful.

So, I figured I could reuse the command elaborator if only I could produce a Syntax tree. However, the number of constructors, and the indices/parameters of my inductive type depend on the input to my macro, so generating this Syntax tree is not quite straightforward, either.

A third route seems to just generate a string with the inductive definition, using all the ease of string formatting/concatenation, and then feed that string to the lean parser somehow? In fact, I'm porting code from lean3 which does exactly this, using parser.with_input. Is there a lean4 equivalent to this method? I've tried to look for it, and Parser.runParserCategory seems to do it, but it's documented as "convenience function for testing", so I'm a bit hesitant to use it.

Is there a generally agreed upon clean/idiomatic way to generate new declarations in a macro's elaborator?
The last one seems easiest to use, but it feels quite hackish

[Arthur Paulino]

If you have the code as a String, you can call Lean's frontend like this. But I'm also interested in knowing the most appropriate way to do this.

But this is not clear to me: what type of data do you have that carries information about your inductive type in the first place? Do you have a "meta" inductive type that carries the data about your inductive type? A structure? A raw string?

[Arthur Paulino]

Expliciting the final use case with the code that you'd like to see working might help

[Alex Keizer]

I'm trying to implement a data macro as drop-in replacement for inductive, but then using QPFs as their foundation.
So I have an InductiveType struct that has the specification given by the user, and from that I want to derive the required QPF-constructions.

[Alex Keizer]

So, for example

data Tree (α β : Type 2) : Type _
  | nil : Tree α β
  | node (a : α) : (β → Tree α β) → Tree α β

Should turn into

inductive Tree.HeadT (β : Type 2) : Type _
  | nil : HeadT β
  | node : HeadT β

[Simon Hudon]

I think addDecl is the approach you need if you're creating an inductive type use terms that are already elaborated. There are helper functions like mkAppM that can help make it less painful by inferring some of the arguments for you. Going from Expr to Syntax and back to Expr gives you new ways for your compilation to fail, and you should be careful about going that way

[Alex Keizer]

Only the parameters that occur negatively are preserved, I want the same number of constructors, with the same name, but the type should just be a simple enumeration

[Alex Keizer]

The main difficulty is that I only have a fully elaborated InductiveType for the original data Tree declaration.
From that we can certainly make an InductiveType for Tree.HeadT, but it involves a few steps that feel redundant.

Nevertheless, you are right about the extra conversions being a bit brittle, so I'll try going that route a bit more

[Alex Keizer]

Arthur Paulino said:

If you have the code as a String, you can call Lean's frontend like this. But I'm also interested in knowing the most appropriate way to do this.

Thanks for the pointer, I'd somehow written runFrontend off because it takes a filename, and I didn't want to put my generated code in a file, I reckon the filename is only used for error reporting and I could provide a bogus name?
Otoh, it does run in IO, which makes me a bit suspicious again.

[Sébastien Michelland]

Have you seen elabInductiveViews? It takes a data structure as parameter, I think you could generate Tree.HeadT just from a list of strings.

[Alex Keizer]

Yeah, InductiveView takes a ref : Syntax, though. Do you reckon I could use a bogus value for ref?

[Sébastien Michelland]

Yes you can set Syntax.missing. Some other bits take Syntax as well, but you can just craft it. For instance, you could set

type? := some (← `((β: Type 2) → Type _)),

Assuming you are in a suitable monad such as CommandElabM.

Also I'm not sure this is idiomatic but I believe this is what the inductive command elaborates to.

[Sébastien Michelland]

I figure I could show you the code I'm using directly: https://github.com/opencompl/lean-mlir-semantics/blob/master/MLIRSemantics/Util/Metagen.lean#L110-L157
It's very much experimental and currently (1) sets dummy constructor arguments, and (2) hacks to use evalExpr, which is unsafe and thus normally not allowed in command elaborators. But it might help as far as generating an inductive is concerned.

The file itself is self-contained, you can run it without cloning the repo.