Best way to “compile” an attribute-based function

Stream: lean4

[Thomas Murrills]

What I mean by “compile” is the following:

I have a function useMyAttr : Environment → Input → Foo which looks up entries in an environment extension (in my case, a KeyedDeclsAttribute), then applies them (unsafely, via some eval…) to Input.

I’d like to write a function useMyAttrNow : Input → IO Foo which applies these entries. It doesn’t need to apply decls that will be tagged in the future; the ones in specific known files are all it needs.

Since I know the files that hold the tagged decls I care about, my current approach is to use importModules or withImportModules, then use that Environment.

I’m wondering if this is the “best” way, though. I don’t need the whole environment, and I could even use the environment useMyAttrNow is defined in instead of “re-importing” each time useMyAttrNow is used.

(I wonder if this is an “imaginary cost”, though, as maybe the environment doesn’t stick around in the form I’m imagining, and so we’d have to do the appropriate lookups in more or less the same way anyway.)

If there were a way to more statically say “here are all the keyed decls you need to try”, would it be worth it?

I suppose I’m also not sure what is really meant by IO.Ref under the hood, which is used in the implementation of KeyedDeclsAttribute—at least for built in attributes? (I have control over the attributes, so I could make them built in if desirable.)

[Kyle Miller]

It sounds like you're asking how to do the metaprogramming to read an environment extension and create a function from the data that's there? There's no need to eval anything, the idea is that you get the names of all the declarations that matter, and then you assemble it into an expression that does what you need it to do. You can do this from within an elaborator, which has access to the current environment state.

Here's an example of that: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Internationalization/near/402576630

[Thomas Murrills]

Hmm, I’m not sure that’s what I want to do…I do specifically need a function that lands in IO. Do you mean I’d spin up an elaborator within IO…?

[Kyle Miller]

For Advent of Code, I had a little fun and used an elaborator to create the main function: https://github.com/kmill/kmill-aoc2023/blob/main/AoC.lean#L36-L37

The elaborator is here and here's an example of it being applied.

[Kyle Miller]

It really depends on what you're trying to do though. What I'm showing you is how to handle staging. The environment is a purely compile time construct, and this sort of metaprogramming is how you can make some aspect of it survive to run time. I thought this might be what you were getting at, but if it's not you'll have to refine your question.

[Thomas Murrills]

Hmm, I think I see how that approach could be used in principle, but I guess the issue with it here is that I would probably want to use the keying provided by KeyedDeclsAttribute to look up which decls to apply in the course of dealing with some arbitrary Input (instead of having a function that just inlines all of them).

Actually, does it essentially inline all of them? Maybe I’d better get back to my computer and see what #print main looks like.

(Well, I think that’s what I’d want, anyway, but I could be wrong!)

I think you’re correct about me wanting to use some part of the environment during runtime, though.

[Kyle Miller]

I think you'll have to say what concrete problem you're working on, rather than talking in the abstract.

[Kyle Miller]

The key idea here is just that you can turn the data in your environment extension into data you can embed in your function.

I my case, I decided to encode that data in an if/else chain, but you can do whatever you want. It's not inlining bodies of the tagged declarations to be clear, it's just including the declaration names (as constants).

[Thomas Murrills]

Hmm, yeah—in that vein, I feel as though I need to “store the current KeyedDeclsAttribute lookup table somewhere in an olean”, but I’m not sure if this is, in fact, what I need. Or if it’s already there.

Basically the problem is “expand macros in IO”, except I’m using my own elab-like attribute instead of @[macro k].

[Kyle Miller]

It's still unclear to me what your concrete goals are. Is this meant to be in the realm of metaprogramming (i.e., compile-time activities) or in the realm of something that will work in a compiled program, given everything that has the attribute at compile time (i.e., a run time activity)?

[Thomas Murrills]

The latter; for more context, this is a “process a(n arbitrary) lean file via a frontend”-type situation, except my rewrite rules can only be known to the processing function, not the (potential, arbitrary) file which will be processed (so I can’t use its environment).