lean_sys/array/
low_level.rs

1/*! Arrays of objects (low level API) */
2use crate::*;
3
4#[inline]
5pub unsafe fn lean_alloc_array(size: usize, capacity: usize) -> *mut lean_object {
6    let o = lean_alloc_object(
7        core::mem::size_of::<lean_array_object>() + core::mem::size_of::<*mut ()>() * capacity,
8    );
9    lean_set_st_header(o as *mut _, LeanArray as u32, 0);
10    (raw_field!(o, lean_array_object, m_size) as *mut usize).write(size);
11    (raw_field!(o, lean_array_object, m_capacity) as *mut usize).write(capacity);
12    o as *mut _
13}
14
15#[inline(always)]
16pub unsafe fn lean_array_size(o: b_lean_obj_arg) -> usize {
17    *(raw_field!(o, lean_array_object, m_size))
18}
19
20#[inline(always)]
21pub unsafe fn lean_array_capacity(o: b_lean_obj_arg) -> usize {
22    *(raw_field!(o, lean_array_object, m_capacity))
23}
24
25#[inline]
26pub unsafe fn lean_array_byte_size(o: b_lean_obj_arg) -> usize {
27    core::mem::size_of::<lean_array_object>()
28        + core::mem::size_of::<*mut ()>() * lean_array_capacity(o)
29}
30
31#[inline]
32pub unsafe fn lean_array_data_byte_size(o: b_lean_obj_arg) -> usize {
33    core::mem::size_of::<lean_array_object>() + core::mem::size_of::<*mut ()>() * lean_array_size(o)
34}
35
36#[inline(always)]
37pub unsafe fn lean_array_cptr(o: b_lean_obj_arg) -> *mut *mut lean_object {
38    raw_field!(o, lean_array_object, m_data) as *mut _
39}
40
41#[inline(always)]
42pub unsafe fn lean_array_set_size(o: u_lean_obj_arg, sz: usize) {
43    debug_assert!(lean_is_array(o));
44    debug_assert!(lean_is_exclusive(o));
45    debug_assert!(sz <= lean_array_capacity(o));
46    (raw_field!(lean_to_array(o), lean_array_object, m_size) as *mut usize).write(sz)
47}
48
49#[inline(always)]
50pub unsafe fn lean_array_get_core(o: b_lean_obj_arg, i: usize) -> b_lean_obj_res {
51    debug_assert!(i < lean_array_size(o));
52    *(raw_field!(lean_to_array(o), lean_array_object, m_data) as *mut *mut lean_object).add(i)
53}
54
55#[inline(always)]
56pub unsafe fn lean_array_set_core(o: u_lean_obj_arg, i: usize, v: lean_obj_arg) {
57    debug_assert!(!lean_has_rc(o) || lean_is_exclusive(o));
58    debug_assert!(i < lean_array_size(o));
59    (raw_field!(lean_to_array(o), lean_array_object, m_data) as *mut *mut lean_object)
60        .add(i)
61        .write(v)
62}
63
64extern "C" {
65    pub fn lean_array_mk(l: lean_obj_arg) -> *mut lean_object;
66    pub fn lean_array_to_list(a: lean_obj_arg) -> *mut lean_object;
67}
lean_sys/array/low_level.rs

lean_sys/array/
low_level.rs
