MetaM in FFI

Stream: lean4

[Marcus Rossel]

What would be the correct way to implement a function f : A → MetaM B in C? I'm guessing the signature would still be something like lean_obj_res f(input: lean_obj_arg), so the MetaM state must be somewhere in input and the return value must somehow be correctly wrapped for MetaM. I know such infrastructure exists for the IO monad, but I don't understand how it works as, for example, the implementation of lean_io_mk_world looks very odd to me:

static inline lean_obj_res lean_io_mk_world() { return lean_box(0); }

#xy: I'm trying to call type class synthesis from C.

[Henrik Böving]

No, the signature would be much longer, if you take a look at the IO functions in FFI you will see they always take a last parameter that is ignored. This parameter is the IO world parameter. Similarly all MetaM functions are desugared to C functions using the rules here. You'll end up with a function that takes the Meta Context, Meta State, Core Context, Core State and world parameter so 5 additional parameters.

: I'm trying to call type class synthesis from C.

That's not going to be trivially possible, type class synthesis has no stable export name so you will not be able to find the symbol consistently across changes, why do you want to do this?

[Marcus Rossel]

Henrik Böving said:

: I'm trying to call type class synthesis from C.

That's not going to be trivially possible, type class synthesis has no stable export name so you will not be able to find the symbol consistently across changes, why do you want to do this?

I guess I worded that poorly. I'm trying to call a Lean function f : String → MetaM Bool from C, where f needs to run type class synthesis. Is that possible, or does that suffer from the exact problem you mention here?

[Eric Wieser]

Do you have an Environent to do that synthesis within?

[Eric Wieser]

Or phrased another way; what monad are you morally in when you want to make the call from C; what state do you have around?

[Henrik Böving]

if you give that function a stable symbol and you have access to all the things that constitute a Meta state or the sufficient data to construct a meta state that works yes

[Marcus Rossel]

I guess I should explain my situation in more detail.
I want to write a Lean function f : A → MetaM B which is implemented by a C function g which needs to be able to call a Lean function h : String → MetaM Bool which can run type class synthesis. So my guess was that I probably need to pass around a bunch of state from f through g to h and back. Does that sound sensible?

[Eric Wieser]

Yeah, that sounds like the right approach

[Eric Wieser]

Ideally there'd be a #c_signaturecommand that just tells you the function signature to write in C (edit: or better yet, lean4#5829 so that your C compiler can tell you if the signature you wrote doesn't match)

[Marcus Rossel]

My problem now is that I don't know how that state is represented, or how I properly wrap return values with it.

[Eric Wieser]

You could look at the C output for a pure-lean MetaM function to deduce the signature,

[Marcus Rossel]

So, when I compile:

import Lean
open Lean

def hello (b : Bool) : MetaM Bool :=
  return b

I get:

LEAN_EXPORT lean_object* l_hello(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_hello___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);

LEAN_EXPORT lean_object* l_hello(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8;
x_7 = lean_box(x_1);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
return x_8;
}
}
LEAN_EXPORT lean_object* l_hello___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
uint8_t x_7; lean_object* x_8;
x_7 = lean_unbox(x_1);
lean_dec(x_1);
x_8 = l_hello(x_7, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_8;
}
}

Can I can ignore the ___boxed variant? And is the LEAN_EXPORT necessary? I haven't used that in my C functions so far.

[Marcus Rossel]

And what I find interesting about l_hello is that it completely ignores x_2, x_3, x_4 and x_5. Is that state that doesn't need to be returned, because it didn't change? Or are there other reasons?

[Eric Wieser]

If you call a CoreM or IO function from hello, you'll probably see which xs are used for which monad contexts

[Eric Wieser]

Of course you can also #reduce (types := true) MetaM Unit to get the full signature

[Tomas Skrivan]

Is the ___boxed variant generated if you add the attribute @[export "hello""] to the hello function?

Also you can write a lean function that accepts the file path of a lean file and outputs CoreM state and context. I think you can initialize MetaM state and context just with {}. So I believe that your function can have a signature FilePath -> Book -> IO Bool.

[Marcus Rossel]

Eric Wieser said:

Of course you can also #reduce MetaM Unit to get the full signature

Ahhhh:

Bool → Meta.Context → ST.Ref IO.RealWorld Meta.State → Core.Context → ST.Ref IO.RealWorld Core.State → IO.RealWorld → EStateM.Result Exception PUnit Bool

I don't understand why certain state does not have to be returned though.

[Eric Wieser]

It would be great if those type names appeared in the generated source

[Eric Wieser]

Marcus Rossel said:

I don't understand why certain state does not have to be returned though,

ST.Ref is magic / illegal

[Eric Wieser]

Like most performance optimizations

[Marcus Rossel]

I guess that leaves Core.Context (x_3) and IO.RealWorld (x_5). Why don't they need to be returned?

[Rudi Schneider]

I could imagine that it's mutated in-place, instead of being returned? After all, we're in C land there.

[Eric Wieser]

Tomas Skrivan said:

So I believe that your function can have a signature FilePath -> Book -> IO Bool.

I think this is a good answer to what turned out not to be the question that Marcus was asking

[Eric Wieser]

Marcus Rossel said:

I guess that leaves Core.Context (x_3) and IO.RealWorld (x_5). Why don't they need to be returned?

"Contexts" are by convention the bits that are not modified, so returning would be pointless

[Eric Wieser]

And IO.RealWorld is a big lie, which is always just ().

[Marcus Rossel]

Awesome, I think I know what to do now. Thanks!

[Marcus Rossel]

cc @memoryleak47

---

I'm stuck with a new problem which I don't understand. I've implemented the following chain of functions, which passes around all the MetaM state/context (x1, ..., x5):

LEAN: @[extern "run_eqsat_request"] opaque runRaw : Request → MetaM Result.Raw

                                       | corresponds to
                                       ↓

C:    lean_obj_res run_eqsat_request(lean_obj_arg req, lean_obj_arg x1, lean_obj_arg x2, lean_obj_arg x3, lean_obj_arg x4, lean_obj_arg x5)

                                       | calls
                                       ↓

RUST: some_function(void* x1, void* x2, void* x3, void* x4, void* x5)

                                       | can call
                                       ↓

C:    _Bool is_synthable(void* x1, void* x2, void* x3, void* x4, void* x5)

                                       | calls
                                       ↓

C:    lean_obj_res lean_is_synthable(lean_object* x1, lean_object* x2, lean_object* x3, lean_object* x4, lean_object* x5)

                                       | corresponds to
                                       ↓

LEAN: @[export lean_is_synthable] def isSynthable : MetaM Bool := ...

For cases where the Rust function some_function does not call is_synthable, everything works great. But when some_function does call is_synthable, I get an error error: Lean exited with code 139 after run_eqsat_request returns, but before runRaw completes. Specifically, this means that in the following function:

def run (req : Request) : MetaM Result := do
  let raw ← runRaw req
  panic! "NO"

... execution does return from run_eqsat_request , but does not reach the panic. From looking around, I couldn't tell what error code 139 is supposed to indicate. So right now I don't know how to debug this.

run_eq_sat_request

lean_obj_res run_eqsat_request(lean_obj_arg req, lean_obj_arg x1, lean_obj_arg x2, lean_obj_arg x3, lean_obj_arg x4, lean_obj_arg x5) {
    env e = {
        .x1 = x1,
        .x2 = x2,
        .x3 = x3,
        .x4 = x4,
        .x5 = x5,
    };
    lean_object* res = run_eqsat_request_impl(req, &e);
    lean_object* metam_state = lean_alloc_ctor(0, 2, 0);
    lean_ctor_set(metam_state, 0, res);
    lean_ctor_set(metam_state, 1, x5);
    return metam_state;
}

is_synthable

_Bool is_synthable(const void* v, const char* str) {
    env* e = (env*)v;
    lean_obj_res ty_str = lean_mk_string(str);
    lean_obj_res s = lean_is_synthable(ty_str, e->x1, e->x2, e->x3, e->x4, e->x5);

    switch (s->m_tag) {
        /* EStateM.Result.ok */ case 0: {
            // Note: The `Bool` is boxed for some reason.
            lean_obj_res b = lean_ctor_get(s, 0);
            size_t result = lean_unbox(b);
            return result != 0;
        }
        /* EStateM.Result.err */ case 1: {
            return false;
            // TODO: We should propagate the error back, as it would also be important
            //       to know whether we have a `MetaM` failure when we return from `runRaw`.
        }
        default: {
            exit(1);
        }
    }
}

lean_is_synthable

extern lean_obj_res lean_is_synthable(
    lean_object* ty_str,
    lean_object* x1,
    lean_object* x2,
    lean_object* x3,
    lean_object* x4,
    lean_object* x5
);