lean_sys/sarray/
mod.rs

1/*! Array of scalars */
2use crate::*;
3
4pub mod byte;
5pub mod float;
6pub use byte::*;
7pub use float::*;
8
9#[inline]
10pub unsafe fn lean_alloc_sarray(elem_size: c_uint, size: usize, capacity: usize) -> lean_obj_res {
11    let o = lean_alloc_object(
12        core::mem::size_of::<lean_sarray_object>() + (elem_size as usize) * capacity,
13    ) as *mut lean_sarray_object;
14    lean_set_st_header(o as *mut _, LeanScalarArray as u32, elem_size);
15    (raw_field!(o, lean_sarray_object, m_size) as *mut usize).write(size);
16    (raw_field!(o, lean_sarray_object, m_capacity) as *mut usize).write(capacity);
17    o as *mut _
18}
19
20#[inline(always)]
21pub unsafe fn lean_sarray_elem_size(o: *const lean_object) -> c_uint {
22    debug_assert!(lean_is_sarray(o));
23    lean_ptr_other(o)
24}
25
26#[inline(always)]
27pub unsafe fn lean_sarray_capacity(o: *const lean_object) -> usize {
28    *raw_field!(lean_to_sarray(o as *mut _), lean_sarray_object, m_capacity)
29}
30
31#[inline]
32pub unsafe fn lean_sarray_byte_size(o: *const lean_object) -> usize {
33    size_of::<lean_sarray_object>() + lean_sarray_elem_size(o) as usize * lean_sarray_capacity(o)
34}
35
36#[inline(always)]
37pub unsafe fn lean_sarray_size(o: *const lean_object) -> usize {
38    *raw_field!(lean_to_sarray(o as *mut _), lean_sarray_object, m_size)
39}
40
41#[inline(always)]
42pub unsafe fn lean_sarray_data_byte_size(o: *const lean_object) -> usize {
43    size_of::<lean_sarray_object>() + lean_sarray_elem_size(o) as usize * lean_sarray_size(o)
44}
45
46#[inline(always)]
47pub unsafe fn lean_sarray_set_size(o: u_lean_obj_arg, sz: usize) {
48    debug_assert!(lean_is_exclusive(o));
49    debug_assert!(sz <= lean_sarray_capacity(o));
50    (raw_field!(lean_to_sarray(o), lean_sarray_object, m_size) as *mut usize).write(sz);
51}
52
53#[inline(always)]
54pub unsafe fn lean_sarray_cptr(o: *mut lean_object) -> *mut u8 {
55    raw_field!(lean_to_sarray(o), lean_sarray_object, m_data) as *mut _
56}
lean_sys/sarray/mod.rs

lean_sys/sarray/
mod.rs
