local elaborators

Stream: lean4

[Simon Hudon]

If I have a function to elaborate a def command, is there an attribute I can apply to it (possibly with keyword local) so that in a given namespace or section it gets used instead of the built-in elaborator for def?

[Mario Carneiro]

Are you replacing the def elaborator entirely?

[Mario Carneiro]

if so, you can accomplish this by making a high priority syntax which overrides def

[Simon Hudon]

Yes but I'd like to do the replacement in the elaborator of myfunky_namespace, that's why it seems like applying an attribute inside the elaborator seems like the most straightforward option

[Simon Hudon]

More specifically, I wand to write

def elabMyFunkyNamespace : AllTheProperTypes := do
elabCommand (<- ``(namespace foo))
-- apply attribute to my ready-to-go `def`-elaborator substitute

[Mario Carneiro]

I don't think it's possible to give elab overrides for existing syntax, but I could be wrong

[Simon Hudon]

Yeah, I was afraid of that. I'd rather not copy / paste the parsing code for declaration. Let's bite that bullet for now

[Sebastian Ullrich]

Mario Carneiro said:

I don't think it's possible to give elab overrides for existing syntax, but I could be wrong

It is

elab_rules : command
  | `(#eval $e) => IO.println "eval thyself"

[Sebastian Ullrich]

@Simon Hudon Are you looking for

namespace foo
scoped elab_rules ...

or does it need to be more dynamic than that?

[Simon Hudon]

Nice!

What I'm looking for would be more like

namespace foo
local elab_rules ...

I'm using constant to create an opaque definition and this kind of namespace allows you to temporarily make the definition transparent (read: make definition about the underlying term of the constant). Every def in that section needs to do the normal thing in addition to transporting all the definition to use the opaque type. When you encounter end, the elaborator should disappear.

[Simon Hudon]

Cool, I just tried and the following matches my declarations:

elab_rules : command
| `($d:declaration) => println!"my elab"

[Simon Hudon]

One more detail @Sebastian Ullrich : when I include `($d:declaration) inside a command quasi-quotation, it kind of looks like it's going to try to splice something called d right in that pattern. How do I make sure it looks like a bound variable?

[Sebastian Ullrich]

If I understood you correctly, you'll want to move the antiquotation one level deeper: $$d:declaration

[Simon Hudon]

Ah ok! I think we're on the same page but just to spell this out: I'm creating a quasi-quotation of a list of commands in which I splice nothing. Inside that quasi-quotation, there will be a syntax pattern for declaration inside a elab_rules command. That pattern needs to bind variable d and that's what the anti-quotation of level 2 will accomplish. Makes sense?

Also, am I using the quotation vocabulary correctly?

[Sebastian Ullrich]

Sounds good, though splicing is usually reserved to inserting a sequence of elements I believe

[Simon Hudon]

Ah I see. Thanks! So "anti-quotation" is what I should call those?

[Sebastian Ullrich]

Yes