Stream: Is there code for X?
Topic: exporting a program's AST
Petar Maymounkov (Apr 24 2020 at 18:32):
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.)?
Simon Hudon (Apr 24 2020 at 18:57):
That is not currently supported. How would you use that information?
Simon Hudon (Apr 24 2020 at 18:58):
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
Petar Maymounkov (Apr 24 2020 at 19:16):
For a Lean function to be convertible to a static-typed target language, it must have no dependent types.
So, my reasoning is:
- 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.)
- Traverse the definition of F recursively, expanding dependent Lean types (to non-dependent Lean types) as you go.
- Map non-dependent Lean types to static types in the target language using a simple translation rule.
Petar Maymounkov (Apr 24 2020 at 19:34):
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 (Apr 24 2020 at 20:53):
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 (Apr 25 2020 at 00:50):
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 (Apr 25 2020 at 00:51):
lean has basically all the reflection capabilities you could hope for
Mario Carneiro (Apr 25 2020 at 00:53):
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 (Apr 25 2020 at 02:25):
Thank you! This is very helpful.
Last updated: May 07 2021 at 21:10 UTC