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(always)]
42pub unsafe fn lean_array_fget_borrowed(a: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res {
43    lean_array_get_core(a, lean_unbox(i))
44}
45
46#[inline]
47pub unsafe fn lean_array_get(
48    def_val: lean_obj_arg,
49    a: b_lean_obj_arg,
50    i: b_lean_obj_arg,
51) -> lean_obj_res {
52    if lean_is_scalar(i) {
53        let idx = lean_unbox(i);
54        if idx < lean_array_size(a) {
55            lean_dec(def_val);
56            return lean_array_uget(a, idx);
57        }
58    }
59    /* Recall that if `i` is not a scalar, then it must be out of bounds because
60    i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
61    but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
62    In both cases, we would be out-of-memory. */
63    lean_array_get_panic(def_val)
64}
65
66#[inline]
67pub unsafe fn lean_array_get_borrowed(
68    def_val: lean_obj_arg,
69    a: b_lean_obj_arg,
70    i: b_lean_obj_arg,
71) -> lean_obj_res {
72    if lean_is_scalar(i) {
73        let idx = lean_unbox(i);
74        if idx < lean_array_size(a) {
75            lean_dec(def_val);
76            return lean_array_get_core(a, idx);
77        }
78    }
79    /* Recall that if `i` is not a scalar, then it must be out of bounds because
80    i > LEAN_MAX_SMALL_NAT == MAX_UNSIGNED >> 1
81    but each array entry is 8 bytes in 64-bit machines and 4 in 32-bit ones.
82    In both cases, we would be out-of-memory. */
83    lean_array_get_panic(def_val)
84}
85
86#[inline(always)]
87pub unsafe fn lean_copy_array(a: lean_obj_arg) -> lean_obj_res {
88    lean_copy_expand_array(a, false)
89}
90
91#[inline(always)]
92pub unsafe fn lean_ensure_exclusive_array(a: lean_obj_arg) -> lean_obj_res {
93    if lean_is_exclusive(a) {
94        a
95    } else {
96        lean_copy_array(a)
97    }
98}
99
100#[inline]
101pub unsafe fn lean_array_uset(a: lean_obj_arg, i: usize, v: lean_obj_arg) -> *mut lean_object {
102    let r = lean_ensure_exclusive_array(a);
103    let it = lean_array_cptr(r).add(i);
104    lean_dec(*it);
105    *it = v;
106    r
107}
108
109#[inline]
110pub unsafe fn lean_array_fset(
111    a: lean_obj_arg,
112    i: b_lean_obj_arg,
113    v: lean_obj_arg,
114) -> *mut lean_object {
115    lean_array_uset(a, lean_unbox(i), v)
116}
117
118#[inline]
119pub unsafe fn lean_array_set(
120    a: lean_obj_arg,
121    i: b_lean_obj_arg,
122    v: lean_obj_arg,
123) -> *mut lean_object {
124    if lean_is_scalar(i) {
125        let idx = lean_unbox(i);
126        if idx < lean_array_size(a) {
127            return lean_array_uset(a, idx, v);
128        }
129    }
130    lean_array_set_panic(a, v)
131}
132
133#[inline]
134pub unsafe fn lean_array_pop(a: lean_obj_arg) -> *mut lean_object {
135    let r = lean_ensure_exclusive_array(a);
136    let sz = lean_array_size(a);
137    if sz == 0 {
138        return r;
139    }
140    let sz = sz - 1;
141    let last = lean_array_cptr(r).add(sz);
142    *(raw_field!(lean_to_array(r), lean_array_object, m_size) as *mut usize) = sz;
143    lean_dec(*last);
144    r
145}
146
147#[inline]
148pub unsafe fn lean_array_uswap(a: lean_obj_arg, i: usize, j: usize) -> *mut lean_object {
149    let r = lean_ensure_exclusive_array(a);
150    let it = lean_array_cptr(r);
151    core::ptr::swap(it.add(i), it.add(j));
152    r
153}
154
155#[inline(always)]
156pub unsafe fn lean_array_fswap(
157    a: lean_obj_arg,
158    i: b_lean_obj_arg,
159    j: b_lean_obj_arg,
160) -> *mut lean_object {
161    lean_array_uswap(a, lean_unbox(i), lean_unbox(j))
162}
163
164#[inline(always)]
165pub unsafe fn lean_array_swap(
166    a: lean_obj_arg,
167    i: b_lean_obj_arg,
168    j: b_lean_obj_arg,
169) -> *mut lean_object {
170    if !lean_is_scalar(i) || !lean_is_scalar(j) {
171        return a;
172    }
173    let i = lean_unbox(i);
174    let j = lean_unbox(j);
175    let sz = lean_array_size(a);
176    if i >= sz || j >= sz {
177        a
178    } else {
179        lean_array_uswap(a, i, j)
180    }
181}
182
183extern "C" {
184    pub fn lean_array_get_panic(def_val: lean_obj_arg) -> lean_obj_res;
185    pub fn lean_copy_expand_array(a: lean_obj_arg, expand: bool) -> lean_obj_res;
186    pub fn lean_array_set_panic(a: lean_obj_arg, v: lean_obj_arg) -> lean_obj_res;
187    pub fn lean_array_push(a: lean_obj_arg, v: lean_obj_arg) -> *mut lean_object;
188    pub fn lean_mk_array(n: lean_obj_arg, v: lean_obj_arg) -> *mut lean_object;
189
190}
lean_sys/array/high_level.rs

lean_sys/array/
high_level.rs
