lean_sys/sarray/
float.rs

1/*! FloatArray (special case of Array of Scalars) */
2use crate::*;
3
4#[inline]
5pub unsafe fn lean_mk_empty_float_array(capacity: b_lean_obj_arg) -> lean_obj_res {
6    if !lean_is_scalar(capacity) {
7        lean_internal_panic_out_of_memory()
8    }
9    lean_alloc_sarray(
10        core::mem::size_of::<f64>() as c_uint,
11        0,
12        lean_unbox(capacity),
13    )
14}
15
16#[inline(always)]
17pub unsafe fn lean_float_array_size(a: b_lean_obj_arg) -> lean_obj_res {
18    lean_box(lean_sarray_size(a))
19}
20
21#[inline(always)]
22pub unsafe fn lean_float_array_cptr(a: b_lean_obj_arg) -> *mut f64 {
23    lean_sarray_cptr(a) as *mut _
24}
25
26#[inline(always)]
27pub unsafe fn lean_float_array_uget(a: b_lean_obj_arg, i: usize) -> f64 {
28    debug_assert!(i < lean_sarray_size(a));
29    *lean_float_array_cptr(a).add(i)
30}
31
32#[inline]
33pub unsafe fn lean_float_array_get(a: b_lean_obj_arg, i: b_lean_obj_arg) -> f64 {
34    if lean_is_scalar(i) {
35        let i = lean_unbox(i);
36        if i < lean_sarray_size(a) {
37            lean_float_array_uget(a, i)
38        } else {
39            0.0
40        }
41    } else {
42        /* The index must be out of bounds. Otherwise we would be out of memory. */
43        0.0
44    }
45}
46
47#[inline(always)]
48pub unsafe fn lean_float_array_fget(a: b_lean_obj_arg, i: b_lean_obj_arg) -> f64 {
49    lean_float_array_uget(a, lean_unbox(i))
50}
51
52#[inline(always)]
53pub unsafe fn lean_float_array_uset(a: lean_obj_arg, i: usize, v: f64) -> *mut lean_object {
54    let r = if lean_is_exclusive(a) {
55        a
56    } else {
57        lean_copy_byte_array(a)
58    };
59    let it = lean_float_array_cptr(r).add(i);
60    *it = v;
61    r
62}
63
64#[inline]
65pub unsafe fn lean_float_array_set(a: lean_obj_arg, i: b_lean_obj_arg, v: f64) -> *mut lean_object {
66    if !lean_is_scalar(i) {
67        a
68    } else {
69        let i = lean_unbox(i);
70        if i >= lean_sarray_size(a) {
71            a
72        } else {
73            lean_float_array_uset(a, i, v)
74        }
75    }
76}
77
78#[inline(always)]
79pub unsafe fn lean_float_array_fset(
80    a: lean_obj_arg,
81    i: b_lean_obj_arg,
82    v: f64,
83) -> *mut lean_object {
84    lean_float_array_uset(a, lean_unbox(i), v)
85}
86
87extern "C" {
88    pub fn lean_float_array_mk(a: lean_obj_arg) -> lean_obj_res;
89    pub fn lean_float_array_data(a: lean_obj_arg) -> lean_obj_res;
90    pub fn lean_copy_float_array(a: lean_obj_arg) -> lean_obj_res;
91    pub fn lean_float_array_push(a: lean_obj_arg, d: f64) -> lean_obj_res;
92}
lean_sys/sarray/float.rs

lean_sys/sarray/
float.rs
