c++ code generation at compile time

Stream: lean4

[Arthur Paulino]

Hello! One thing that @Tomas Skrivan and I are trying to achieve is to have a way of marking a definition as in

@[karray_compile]
def KArray.fadd : KArray Float -> KArray Float -> KArray Float := KArray.map2 (fun x y : Float => x + y)

And then some C code would be generated like this:

// karray_fadd.cpp

inline float fadd(float a, float b){
   return a + b;
}

extern "C" LEAN_EXPORT lean_obj_res karray_fadd(b_lean_obj_arg _a1, b_lean_obj_arg _a2) {
    karray*  a1  = karray_unbox(_a1);
    karray*  a2  = karray_unbox(_a2);
    ...

Assume that the precise instructions of this translation can be extracted from KArray.

So Tomas was thinking that maybe this can be achieved with not so much gymnastics. Does anyone know if it's possible?

Another strategy would rely on lake being able to run custom pre-processing code before actually calling leanc. Is this possible? Or would it be a nice feature to have?

The other strategy would be simply running a Lean script that does the preprocessing by ourselves, totally decoupled from lake build. But then It would make importing this package a bit troublesome because it would carry out this need for manual preprocessing calls.

We'd like to know what you think :pray:

[Mac]

@Arthur Paulino Part of this is what I am hoping to achieve with Alloy, but it is still WIP on both the Lake and Alloy sides.

[Joe Hendrix]

@Mac I'm working on bindings to some crypto routines, and definitely would like the ability to either generate C within Lean or have Haskell-style FFI libraries for working with C functions within Lean.

[Tomas Skrivan]

To partially achieve what @Arthur Paulino described, I would like to know how to:

1. Define a custom attribute
2. Run some Lean code once you write down a definition with that attribute, ideally in TermElabM monad, and have access to the definition.

This way I can inspect the expression of the definition and generate a file with C code. Can anyone point me where to start?