lean_sys/array/
high_level.rs

1/*! Arrays of objects (high level API) */
2use crate::*;
3
4#[inline]
5pub unsafe fn lean_array_sz(a: lean_obj_arg) -> *mut lean_object {
6    let r = lean_box(lean_array_size(a));
7    lean_dec(a);
8    r
9}
10
11#[inline(always)]
12pub unsafe fn lean_array_get_size(a: b_lean_obj_arg) -> *mut lean_object {
13    lean_box(lean_array_size(a))
14}
15
16#[inline(always)]
17pub unsafe fn lean_mk_empty_array() -> *mut lean_object {
18    lean_alloc_array(0, 0)
19}
20
21#[inline(always)]
22pub unsafe fn lean_mk_empty_array_with_capacity(capacity: b_lean_obj_arg) -> *mut lean_object {
23    if !lean_is_scalar(capacity) {
24        lean_internal_panic_out_of_memory()
25    }
26    lean_alloc_array(0, lean_unbox(capacity))
27}
28
29#[inline]
30pub unsafe fn lean_array_uget(a: b_lean_obj_arg, i: usize) -> lean_obj_res {
31    let r = lean_array_get_core(a, i);
32    lean_inc(r);
33    r
34}
35
36#[inline(always)]
37pub unsafe fn lean_array_fget(a: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res {
38    lean_array_uget(a, lean_unbox(i))
39}
40
41#[inline]
42pub unsafe fn lean_array_get(
43    def_val: b_lean_obj_arg,
44    a: b_lean_obj_arg,
45    i: b_lean_obj_arg,
46) -> lean_obj_res {
47    if lean_is_scalar(i) {
48        let idx = lean_unbox(i);
49        if idx < lean_array_size(a) {
50            lean_dec(def_val);
51            return lean_array_uget(a, idx);
52        }
53    }
54    /* Recall that if `i` is not a scalar, then it must be out of bounds because
55    i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
56    but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
57    In both cases, we would be out-of-memory. */
58    lean_array_get_panic(def_val)
59}
60
61#[inline(always)]
62pub unsafe fn lean_copy_array(a: lean_obj_arg) -> lean_obj_res {
63    lean_copy_expand_array(a, false)
64}
65
66#[inline(always)]
67pub unsafe fn lean_ensure_exclusive_array(a: lean_obj_arg) -> lean_obj_res {
68    if lean_is_exclusive(a) {
69        a
70    } else {
71        lean_copy_array(a)
72    }
73}
74
75#[inline]
76pub unsafe fn lean_array_uset(a: lean_obj_arg, i: usize, v: lean_obj_arg) -> *mut lean_object {
77    let r = lean_ensure_exclusive_array(a);
78    let it = lean_array_cptr(r).add(i);
79    lean_dec(*it);
80    *it = v;
81    r
82}
83
84#[inline]
85pub unsafe fn lean_array_fset(
86    a: lean_obj_arg,
87    i: b_lean_obj_arg,
88    v: lean_obj_arg,
89) -> *mut lean_object {
90    lean_array_uset(a, lean_unbox(i), v)
91}
92
93#[inline]
94pub unsafe fn lean_array_set(
95    a: lean_obj_arg,
96    i: b_lean_obj_arg,
97    v: lean_obj_arg,
98) -> *mut lean_object {
99    if lean_is_scalar(i) {
100        let idx = lean_unbox(i);
101        if idx < lean_array_size(a) {
102            return lean_array_uset(a, idx, v);
103        }
104    }
105    lean_array_set_panic(a, v)
106}
107
108#[inline]
109pub unsafe fn lean_array_pop(a: lean_obj_arg) -> *mut lean_object {
110    let r = lean_ensure_exclusive_array(a);
111    let sz = lean_array_size(a);
112    if sz == 0 {
113        return r;
114    }
115    let sz = sz - 1;
116    let last = lean_array_cptr(r).add(sz);
117    *(raw_field!(lean_to_array(r), lean_array_object, m_size) as *mut usize) = sz;
118    lean_dec(*last);
119    r
120}
121
122#[inline]
123pub unsafe fn lean_array_uswap(a: lean_obj_arg, i: usize, j: usize) -> *mut lean_object {
124    let r = lean_ensure_exclusive_array(a);
125    let it = lean_array_cptr(r);
126    core::ptr::swap(it.add(i), it.add(j));
127    r
128}
129
130#[inline(always)]
131pub unsafe fn lean_array_fswap(
132    a: lean_obj_arg,
133    i: b_lean_obj_arg,
134    j: b_lean_obj_arg,
135) -> *mut lean_object {
136    lean_array_uswap(a, lean_unbox(i), lean_unbox(j))
137}
138
139#[inline(always)]
140pub unsafe fn lean_array_swap(
141    a: lean_obj_arg,
142    i: b_lean_obj_arg,
143    j: b_lean_obj_arg,
144) -> *mut lean_object {
145    if !lean_is_scalar(i) || !lean_is_scalar(j) {
146        return a;
147    }
148    let i = lean_unbox(i);
149    let j = lean_unbox(j);
150    let sz = lean_array_size(a);
151    if i >= sz || j >= sz {
152        a
153    } else {
154        lean_array_uswap(a, i, j)
155    }
156}
157
158extern "C" {
159    pub fn lean_array_get_panic(def_val: lean_obj_arg) -> lean_obj_res;
160    pub fn lean_copy_expand_array(a: lean_obj_arg, expand: bool) -> lean_obj_res;
161    pub fn lean_array_set_panic(a: lean_obj_arg, v: lean_obj_arg) -> lean_obj_res;
162    pub fn lean_array_push(a: lean_obj_arg, v: lean_obj_arg) -> *mut lean_object;
163    pub fn lean_mk_array(n: lean_obj_arg, v: lean_obj_arg) -> *mut lean_object;
164
165}
lean_sys/array/high_level.rs

lean_sys/array/
high_level.rs
