Convert FloatArray to ByteArray

Stream: lean4

[Tomas Skrivan]

How do I convert FloatArray to ByteArray and vice versa? Both are represented as lean_sarray_object but just modifying m_size and casting does not work.

On lean level I define these two functions

@[extern "scilean_float_array_to_byte_array"]
opaque FloatArray.toByteArray (x : FloatArray) : ByteArray

@[extern "scilean_byte_array_to_float_array"]
opaque ByteArray.toFloatArray (x : ByteArray) (h : x.size % 8 = 0) : FloatArray

Which are implemented by

#include <lean/lean.h>

LEAN_EXPORT lean_obj_res scilean_float_array_to_byte_array(lean_obj_arg a){
  lean_obj_res r;
  if (lean_is_exclusive(a)) r = a;
  else r = lean_copy_float_array(a);
  lean_to_sarray(r)->m_size *= 8;
  return r;
}

LEAN_EXPORT lean_obj_res scilean_byte_array_to_float_array(lean_obj_arg a){
  lean_obj_res r;
  if (lean_is_exclusive(a)) r = a;
  else r = lean_copy_byte_array(a);
  lean_to_sarray(r)->m_size /= 8;
  return r;
}

However when I run

  IO.println (FloatArray.mk #[1.0,2.0,3.0,4.0,3.0])
  IO.println (FloatArray.mk #[1.0,2.0,3.0,4.0,3.0] |>.toByteArray)
  IO.println (FloatArray.mk #[1.0,2.0,3.0,4.0,3.0] |>.toByteArray |>.toFloatArray sorry)

I get

[0.000000, 0.000000, 0.000000, 0.000000, 0.000000]
[0, 0, 0, 0, 0]
[1.000000, 2.000000, 3.000000, 4.000000, 3.000000]

[Eric Wieser]

Do you need to set the capacity as well?

[Eric Wieser]

I think you also need to set m_other = 1 when converting to a byte_array, and m_other = 8 when going back to float64

[Tomas Skrivan]

Yes you are right. Looking at lean 4 source code exactly aligns with that.

lean_alloc_sarray

static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) {
    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity);
    lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size);
    o->m_size = size;
    o->m_capacity = capacity;
    return (lean_object*)o;

lean_set_st_header

static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) {
    o->m_rc       = 1;
    o->m_tag      = tag;
    o->m_other    = other;
    o->m_cs_sz    = 0;

[Tomas Skrivan]

And it seems to work as expected now.