fix: Array.mk and Array.data externs

src/Init/Prelude.lean

@@ -1048,8 +1048,8 @@ They are implemented using dynamic arrays: https://en.wikipedia.org/wiki/Dynamic
 structure Array (α : Type u) where
   data : List α
 
-attribute [extern "lean_array_to_list"] Array.data
-attribute [extern "lean_list_to_array"] Array.mk
+attribute [extern "lean_array_data"] Array.data
+attribute [extern "lean_array_mk"] Array.mk
 
 /- The parameter `c` is the initial capacity -/
 @[extern "lean_mk_empty_array_with_capacity"]

src/include/lean/lean.h

@@ -885,8 +885,8 @@ static inline void lean_array_set_core(u_lean_obj_arg o, size_t i, lean_obj_arg
     assert(i < lean_array_size(o));
     lean_to_array(o)->m_data[i] = v;
 }
-lean_object * lean_array_mk(lean_obj_arg sz, lean_obj_arg fn);
-lean_object * lean_array_data(lean_obj_arg a, lean_obj_arg i);
+lean_object * lean_array_mk(lean_obj_arg l);
+lean_object * lean_array_data(lean_obj_arg a);
 
 /* Arrays of objects (high level API) */
 

src/runtime/object.cpp

@@ -264,26 +264,15 @@ object * array_mk_empty() {
     return g_array_empty;
 }
 
-extern "C" object * lean_array_mk(object * sz, object * fn) {
-    if (!lean_is_scalar(sz)) {
-        lean_dec_ref(sz);
-        lean_panic_out_of_memory();
-    }
-    size_t n = lean_unbox(sz);
-    object * r = lean_alloc_array(n, n);
-    for (size_t i = 0; i < n; i++) {
-        lean_inc_ref(fn);
-        lean_array_set_core(r, i, lean_apply_1(fn, lean_box(i)));
-    }
-    lean_dec_ref(fn);
-    return r;
+extern "C" object * lean_list_to_array(object *, object *);
+extern "C" object * lean_array_to_list(object *, object *);
+
+extern "C" object * lean_array_mk(lean_obj_arg lst) {
+    return lean_list_to_array(lean_box(0), lst);
 }
 
-extern "C" lean_object * lean_array_data(lean_obj_arg a, lean_obj_arg i) {
-    object * r = lean_array_fget(a, i);
-    lean_dec(a);
-    lean_dec(i);
-    return r;
+extern "C" lean_object * lean_array_data(lean_obj_arg a) {
+    return lean_array_to_list(lean_box(0), a);
 }
 
 extern "C" lean_obj_res lean_array_get_panic(lean_obj_arg def_val) {

tests/compiler/arrayMk.lean

@@ -0,0 +1,2 @@
+def step : Array Nat := Array.mk (List.range 10)
+def main : IO Unit := IO.print s!"{step.size}\n"

tests/compiler/arrayMk.lean.expected.out

@@ -0,0 +1 @@
+10