exporting a program's AST

Stream: Is there code for X?

[Petar Maymounkov]

I am investigating using Lean to specify and verify protocols, and then code-generate the protocols in another language (say Go).
In that regard, I am wondering if there is a way to export a complete Lean program's AST in some common format (like JSON/ProtoBuf/etc.)?

Thank you!

[Simon Hudon]

That is not currently supported. How would you use that information?

[Simon Hudon]

What is supported however is parsing olean files (object files) and extracting the definitions from there. A prototype exists in Rust and it's called rs-olean

[Petar Maymounkov]

For a Lean function to be convertible to a static-typed target language, it must have no dependent types.
So, my reasoning is:

1. Use Lean to define a function F with no dependent types in its own signature. (Inside, the definition of F may invoke dependent-type sub-functions.)
2. Traverse the definition of F recursively, expanding dependent Lean types (to non-dependent Lean types) as you go.
3. Map non-dependent Lean types to static types in the target language using a simple translation rule.

[Petar Maymounkov]

I recognize that evaluating the types of function calls may be hard to do from just the AST. An alternative strategy for code-generation would be to implement the generation in Lean itself, using Lean reflection to construct the target language AST and then dump it into an object file. I wonder if Lean supports enough reflection to accomplish this; and also can it write data structures to a file.

[Reid Barton]

There are several approaches that should be viable.

• Lean has a low-level export format (produced by lean --export) as described here. There are various existing external tools which can read and type check these files. In principle, I think these files contain all the information you need, although you may have to reconstruct typing information yourself (by implementing a type checker).
• A Lean tactic/"user command" has full access to the environment, including definitions; see here. (I am not sure whether it has access to proofs of lemmas, but I assume you don't need to translate these anyways.) It can also ask the kernel/elaborator for the type of terms, which you might find useful. I think there is a library that can produce JSON somewhere; that's simple enough anyways (I wrote one once, but I don't know where it went). Lean also has file IO, see leanpkg for example.
• Of course you can also do some of the translation in Lean, if you want to program in Lean.

[Mario Carneiro]

You can fairly easily write a function in lean that takes an expr as input and outputs a string containing the syntax of the target language. Especially if you are okay with generating ugly looking code, this is probably the simplest option

[Mario Carneiro]

lean has basically all the reflection capabilities you could hope for

[Mario Carneiro]

I am not sure whether it has access to proofs of lemmas, but I assume you don't need to translate these anyways.

Yes, you can inspect the proofs of theorems. They are provided as a task expr, meaning that you have to join on the (asynchronous) computation of the expression, but otherwise the theorem's proof is available.

[Petar Maymounkov]

Thank you! This is very helpful.