Customizing the elaborator?

Stream: lean4

[Joey Eremondi]

I'm wondering, is there a way to customize the lean elaborator?

[Henrik Böving]

There is dozens of ways. What exactly do you want to do? @Joey Eremondi

[David Renshaw]

A good starting point might be: https://github.com/leanprover-community/lean4-metaprogramming-book/blob/master/md/main/07_elaboration.md

[Joey Eremondi]

I'm wondering, is there a way to customize the elaborator in lean?

I've seen some references in the docs to elaborators for type-aware macros. I'm wondering, is there a way to override existing forms without actually modifying the compiler? To have, for example, lambda or function application elaborate to something different?

I'm looking to do something like the CoqRETT plugin, where each datatype is modified to have additional constructors. Or like Cur, where core language forms can be redefined but you can still refer to the old version.

[Mario Carneiro]

yes

[Patrick Massot]

I'm afraid you will have to be more specific if you want a helpful answer.

[Mario Carneiro]

You seem to have asked the question expecting to get a "no" or "yes under these specific conditions", but the answer is more like "yes you can do almost every conceivable thing in this space" so you have to be more specific

[Joey Eremondi]

@Mario Carneiro @Patrick Massot @Henrik Böving Sorry, I submitted only the first line of the message by accident, I'm struggling with the mobile interface. Full message is https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Customizing.20the.20elaborator.3F/near/391024490

As an example, is there a way to re-define how lambda, application, and function types are elaborated in a specific file? For example, in the CoqRETT example I gave, they add exceptions to Coq by extending each datatype with an extra "error" constructor. Then all terms are elaborated into an Error monad. So an application f x is normally just elaborated into an application in the core language, but here instead it would be elaborated into do f' <- f ; x <- x; (f' x').

Or suppose I want to add a typecase feature to Lean, so I use a custom elaborator that turns all types into Codes of a Universe ala Tarski, and implicitly inserts calls to the interpretation function for those codes at each point needed.

So the idea is I can write code using all the normal language core constructs, but I have a custom elaborator that it goes through to translate it into something different in the core. Basically I want to change the language without modifying the compiler, especially without modifying the core language, so I know whatever I get out the other end is sound, even if it's different from what the normal elaborator would produce.

I guess I'm expecting a "no" because the only language I know of that can do this is Cur, which is built on Racket macros and is ridiculously extensible. Coq can do it, but requires you to write a custom plugin. But I've heard that Lean's macros are powerful and take a lot from e.g. Scheme and Racket macros, so I thought there was a chance it would be possible.

[Joey Eremondi]

@David Renshaw Did not know that book existed, looks like the entire thing is probably useful to me. Thanks!

[Mario Carneiro]

again, the answer is yes

[Joey Eremondi]

@Mario Carneiro Cool. How? Are there docs?

[Mario Carneiro]

David Renshaw said:

A good starting point might be: https://github.com/leanprover-community/lean4-metaprogramming-book/blob/master/md/main/07_elaboration.md

[Joey Eremondi]

@Mario Carneiro Looking through that now. It seems to tell how to add new forms to the language, but not how to override existing forms, especially ones that don't have names (that I know of), like lambda and application.

[Mario Carneiro]

They all have names

[Mario Carneiro]

if you ctrl-click on lambda it should take you to the definition

[Mario Carneiro]

src4#Lean.Parser.Term.fun

[Mario Carneiro]

to override an existing form you use elab_rules instead of elab

[Joey Eremondi]

Ahh, okay. Thanks!