Lean 4 C AST API

Stream: lean4

[Suresh Kannan]

What would be best place to look within the lean 4 C source in order to construct a Lean 4 AST programmatically using C or C++.

The goal is to use Lean but develope a different frontend DSL that once parsed constructs a Lean 4 AST.

[James Gallicchio]

So, most of the lean compiler is written in Lean. Here is the quick rundown of how Lean is compiled:

1. parsing takes an input file and returns a concrete syntax tree (CST)
2. elaboration takes the CST down to lean expressions (Lean.Expr)
3. typechecking occurs on expressions (I think it's actually mutually recursive with elaboration? this part is complicated)
4. code generation takes expressions to an intermediate representation (Lean.IR.Expr I think?) and then from the IR down to C

So, if you want to use Lean's typechecker, you'll have to interact with the frontend components, which are written in Lean. This is called "reverse FFI" and I think people have discussed how to do this on other Zulip threads.

[James Gallicchio]

Most of the time the easiest language to interface with Lean compilation is Lean itself. So, the easiest way to build Lean CSTs and Exprs programmatically is to write your program in Lean.

There are a few projects which provide alternate frontends to Lean -- off the top of my head, lean4game and lean-verbose, both of them are written in Lean itself

[Suresh Kannan]

Thank you James. Very useful, I will grok some of this and take heed of writing it in lean itself.

[Kim Morrison]

The other alternative frontend is the REPL.

[Kim Morrison]

There's also an frontend API at https://github.com/semorrison/lean-training-data/blob/master/TrainingData/Frontend.lean that may be useful.