Documentation of Array runtime Behaviour

Stream: lean4 dev

[Kiran]

Is there any documentation of the runtime representation of scalar arrays? I assume Array Float etc. is a sarray? or is it a vanilla array and can I get the value using lean_unbox(lean_array_cptr(args_raw)[i])?

[Kiran]

okay, after playing around a bit, I think I've figured out the behaviour. In an array, scalar values less than 64 bytes are stored inline and can be accessed via unbox, scalar values equal to 64 bytes are accessible through lean_ctor_obj_cptr

[Kiran]

mhhm but not float32 it seems

[Robin Arnez]

Values are stored just boxed (i.e. lean_object*) inside of Arrays, just like in Prod, etc.

[Robin Arnez]

https://lean-lang.org/doc/reference/latest//find/?domain=Verso.Genre.Manual.section&name=ffi-types should contain information about this, although it doesn't mention Float32

[Henrik Böving]

Float32 is a historically very recent addition that wasn't played with much so I'm not too surprised about this