lean_sys/sarray/
byte.rs

1/*! ByteArray (special case of Array of Scalars) */
2use crate::*;
3
4#[inline]
5pub unsafe fn lean_mk_empty_byte_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(1, 0, lean_unbox(capacity))
10}
11
12#[inline(always)]
13pub unsafe fn lean_byte_array_size(a: b_lean_obj_arg) -> lean_obj_res {
14    lean_box(lean_sarray_size(a))
15}
16
17#[inline(always)]
18pub unsafe fn lean_byte_array_uget(a: b_lean_obj_arg, i: usize) -> u8 {
19    debug_assert!(i < lean_sarray_size(a));
20    *lean_sarray_cptr(a).add(i)
21}
22
23#[inline]
24pub unsafe fn lean_byte_array_get(a: b_lean_obj_arg, i: b_lean_obj_arg) -> u8 {
25    if lean_is_scalar(i) {
26        let i = lean_unbox(i);
27        if i < lean_sarray_size(a) {
28            lean_byte_array_uget(a, i)
29        } else {
30            0
31        }
32    } else {
33        /* The index must be out of bounds. Otherwise we would be out of memory. */
34        0
35    }
36}
37
38#[inline(always)]
39pub unsafe fn lean_byte_array_fget(a: b_lean_obj_arg, i: b_lean_obj_arg) -> u8 {
40    lean_byte_array_uget(a, lean_unbox(i))
41}
42
43#[inline(always)]
44pub unsafe fn lean_byte_array_uset(a: lean_obj_arg, i: usize, v: u8) -> *mut lean_object {
45    let r = if lean_is_exclusive(a) {
46        a
47    } else {
48        lean_copy_byte_array(a)
49    };
50    let it = lean_sarray_cptr(r).add(i);
51    *it = v;
52    r
53}
54
55#[inline]
56pub unsafe fn lean_byte_array_set(a: lean_obj_arg, i: b_lean_obj_arg, v: u8) -> *mut lean_object {
57    if !lean_is_scalar(i) {
58        a
59    } else {
60        let i = lean_unbox(i);
61        if i >= lean_sarray_size(a) {
62            a
63        } else {
64            lean_byte_array_uset(a, i, v)
65        }
66    }
67}
68
69#[inline(always)]
70pub unsafe fn lean_byte_array_fset(a: lean_obj_arg, i: b_lean_obj_arg, v: u8) -> *mut lean_object {
71    lean_byte_array_uset(a, lean_unbox(i), v)
72}
73
74extern "C" {
75    pub fn lean_byte_array_mk(a: lean_obj_arg) -> lean_obj_res;
76    pub fn lean_byte_array_data(a: lean_obj_arg) -> lean_obj_res;
77    pub fn lean_copy_byte_array(a: lean_obj_arg) -> lean_obj_res;
78    pub fn lean_byte_array_push(a: lean_obj_arg, b: u8) -> lean_obj_res;
79}
lean_sys/sarray/byte.rs

lean_sys/sarray/
byte.rs
