Forcing return type to be `size_t`

Stream: lean4

[Tomas Skrivan]

Is there a way to force C code generation to return unboxed USize? I'm writing a wrapper for Eigen and I would like to minimize fiddling with reference counting as much as possible.

In the following example, a function tripletsGetRow returns USize but the generated C code returns lean_object * i.e. boxed size_t. Why is it happening?

structure Idx (n : USize) where
  val : USize
  property : val < n

structure Triplet (n m : USize) where
  row : Idx n
  col : Idx m
  val : Float

@[export triplets_get_row]
def tripletsGetRow (entries : Array (Triplet n m)) (i : USize) (p : i.toNat < entries.size) : USize := (entries.uget i p).row.1

@[extern "eigenlean_sparse_matrix_mk_from_triplets"]
constant SparseMatrix.mk (entries : @& Array (Triplet n m)) : SparseMatrix n m

The declaration of eigenlean_triplets_get_row is:

LEAN_EXPORT lean_object* eigenlean_triplets_get_row(size_t, size_t, lean_object*, size_t, lean_object*);

It can be prevented by changing the definition of Triplet to:

structure Triplet (n m : USize) where
  row : USize
  col : USize
  val : Float
  h_row : row < n
  h_col : col < n

Then eigenlean_triplets_get_row returns size_t as desired:

LEAN_EXPORT size_t eigenlean_triplets_get_row(size_t, size_t, lean_object*, size_t, lean_object*);

What is going on?

[Sebastian Ullrich]

@Leonardo de Moura This looks like some compiler confusion about whether Idx is unboxed or not

[Tomas Skrivan]

Also would it be possible to force the generated C code to accept entries as a reference?

@[export eigenlean_triplets_get_row]
def tripletsGetRow (entries : @& Array (Triplet n m)) (i : USize) (p : i.toNat < entries.size) : USize := (entries.uget i p).row.1

The generated code is:

LEAN_EXPORT size_t eigenlean_triplets_get_row(size_t x_1, size_t x_2, lean_object* x_3, size_t x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; size_t x_7;
x_6 = lean_array_uget(x_3, x_4);
lean_dec(x_3);
x_7 = lean_ctor_get_usize(x_6, 0);
lean_dec(x_6);
return x_7;
}
}

The lean_dec(x_3) indicates that the ref counter of entries is decreased.

[Sebastian Ullrich]

https://github.com/leanprover/lean4/issues/538