How to `lean_dec`/`lean_inc`?

Stream: lean4

[Alexander Bentkamp]

When do I need to call lean_dec or lean_inc?

I implemented the following C function:

lean_object * state;

void send_message(char* msg){
  lean_object * s = lean_mk_string(msg);
  lean_object * res = game_send_message(s, state, io_world);
  if (lean_io_result_is_ok(res)) {
    lean_dec(state);
    state = lean_io_result_get_value(res);
    lean_dec(res);
  } else {
    lean_io_result_show_error(res);
    lean_dec(res);
  }
}

Here, game_send_message is an exported function implemented in Lean. The idea is that I would like to keep my state in a global variable and have it updated by game_send_message. Are the lean_dec calls correct like this?

[Kyle Miller]

I think you need lean_inc(state); after you set it since lean_io_result_get_value doesn't increment it itself

[Kyle Miller]

(I'm assuming you're initializing state elsewhere)

[Alexander Bentkamp]

Yes, I have another Lean-exported function that gives me the initial state.

[Alexander Bentkamp]

Okay, I guess since I am freeing the reference to res, then the state contained in res is also freed. So I need to explicitly lean_inc(state) to keep it, right?

[Kyle Miller]

Yeah, that's my understanding.

[Kyle Miller]

There's a chance you need to lean_inc(state); before game_send_message too, depending on whether it's doing a lean_dec(state) before returning

[Alexander Bentkamp]

I suppose I should also lean_dec(s)?

[Kyle Miller]

That depends on what game_send_message does with it

[Kyle Miller]

If you didn't annotate game_send_message to borrow particular arguments (with @& syntax), then it'll do lean_dec for you, I believe

[Kyle Miller]

(See https://lean-lang.org/lean4/doc/dev/ffi.html#borrowing)

[Kyle Miller]

So, if you didn't use that annotation, you need lean_inc(state) before game_send_message and no lean_dec(s) after it.

[Kyle Miller]

(Oh, I misread, only @[extern] uses @&, and @[export] doesn't -- every argument is owned rather than borrowed in the latter case.)

[Alexander Bentkamp]

Thanks, I think I got it now!