diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 8290fe254e..0035db2443 100644 --- a/src/Init/Prelude.lean +++ b/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"] diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 92ee093194..128ce46fe8 100644 --- a/src/include/lean/lean.h +++ b/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) */ diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 4a7c2caac4..ac41324d28 100644 --- a/src/runtime/object.cpp +++ b/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) { diff --git a/tests/compiler/arrayMk.lean b/tests/compiler/arrayMk.lean new file mode 100644 index 0000000000..5ca9b25404 --- /dev/null +++ b/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" diff --git a/tests/compiler/arrayMk.lean.expected.out b/tests/compiler/arrayMk.lean.expected.out new file mode 100644 index 0000000000..f599e28b8a --- /dev/null +++ b/tests/compiler/arrayMk.lean.expected.out @@ -0,0 +1 @@ +10