What creates StructureInfo?

Stream: lean4

[Max Nowak 🐉]

I'm doing some metaprogramming, taking existing structure T ... declarations, modifying them, and I add a modified structure T' ... via addDecl. But when I do Lean.getStructureInfo? T', I just get none back for some reason. Does addDecl not register T' as a structure by itself? I was hoping to profit from the amazing info (mapping idx to projection functions, etc) that StructureInfo provides.

[Wojciech Nawrocki]

If I recall correctly, addDecl is a fairly low-level function which will not do all the extra stuff that the elaborator for structures does, including registering StructureInfo. Is there a reason why you need to resort to addDecl instead of invoking the elaborator for structures, or easier still using a macro?

[Max Nowak 🐉]

I'm working on a translation of Lean to a logic which doesn't support polymorphism, so I am monomorphizing environment items, including ones such as Prod. At that point all I have is a Name and then that item's ConstantInfo. Based on that I generate Prod'. So I never have any Syntax to begin with, only the already-elaborated Expr.

[Thomas Murrills]

You might want to poke around in Lean.Elab.Structure; in addition to processing the syntax (which you don’t need to do) the functions there also deal with registering the structure as a structure, and I’m pretty sure some of them take in the elaborated expressions as arguments

[Wojciech Nawrocki]

@Max Nowak 🐺 oh, cool! I gave monomorphization a shot not so long ago here, but the approach I was trying ran into a wall of performance issues in the reduction engine. I think it could be made to work, but would require more serious work on verified reduction. Happy to chat about how monormphization could be done!

[Max Nowak 🐉]

I am yet to see how my toy performs, so we will see! What problems did you encounter, and what do you mean with reduction engine? Cool to see others also working on this.

What I'm doing is very simple: Every time I encounter an expression .app (.const X) args where X has Type binders, such as x : (α : Type) -> ..., I use those args to find what I need to mono to.
Type indices are handled before monomorphization (Vect α n becomes {v: Vect' α // v.len = n}, so I don't need to worry about them.
And when you encounter arguments to types which are values (and not just Types), there's two options:
1) Just monomorphize X to that specific value as well.
2) Include these parameters in the guarding predicate, similar to type indices.
I am saying these are the two approaches I've thought about, but I haven't gotten around to implementing either just yet haha.

[Max Nowak 🐉]

Ah nice you can register translators via an attribute and then it picks then first translator that "matches"?

[Wojciech Nawrocki]

What I'm doing is very simple: Every time I encounter an expression .app (.const X) args where X has Type binders, such as x : (α : Type) -> ..., I use those args to find what I need to mono to.

This is precisely what I was doing as well. The question, though, is how you want to justify to Lean that this transformation is correct, in particular that any further proofs about the monomorphized version are also proofs about the original statement using polymorphic expressions. This is where I ran into performance issues with reduction, because I was essentially trying to justify that X FooType = bodyOfX_at_FooType using partial evaluation on the LHS which mathematically follows by rfl; in practice, though, that rfl check is not feasible at the moment for large expressions.

[Wojciech Nawrocki]

Max Nowak 🐺 said:

Ah nice you can register translators via an attribute and then it picks then first translator that "matches"?

That's how the final stage of the translation from Lean expressions to SMTLIB works, after all preprocessing steps have been applied. Since monomorphization is a preprocessing step, it would happen before any translation. This staged approach is what successfully worked in Coq, e.g. in this paper from CPP 2023.