lean_sys/
string.rs

1/*! Strings */
2use crate::*;
3
4#[inline(always)]
5pub unsafe fn lean_alloc_string(size: usize, capacity: usize, len: usize) -> lean_obj_res {
6    let o = lean_alloc_object(core::mem::size_of::<lean_string_object>() + capacity)
7        as *mut lean_string_object;
8    lean_set_st_header(o as *mut _, LeanString as u32, 0);
9    (raw_field!(o, lean_string_object, m_size) as *mut usize).write(size);
10    (raw_field!(o, lean_string_object, m_capacity) as *mut usize).write(capacity);
11    (raw_field!(o, lean_string_object, m_length) as *mut usize).write(len);
12    o as *mut _
13}
14
15#[inline(always)]
16pub unsafe fn lean_string_capacity(o: *mut lean_object) -> usize {
17    *raw_field!(lean_to_string(o), lean_string_object, m_capacity)
18}
19
20#[inline(always)]
21pub unsafe fn lean_string_byte_size(o: *mut lean_object) -> usize {
22    core::mem::size_of::<lean_string_object>() + lean_string_capacity(o)
23}
24
25/** instance : inhabited char := ⟨'A'⟩ */
26#[inline(always)]
27pub fn lean_char_default_value() -> c_char {
28    'A' as c_char
29}
30
31#[inline(always)]
32pub unsafe fn lean_string_cstr(o: b_lean_obj_arg) -> *const u8 {
33    debug_assert!(lean_is_string(o));
34    raw_field!(lean_to_string(o), lean_string_object, m_data) as *const _
35}
36
37#[inline(always)]
38pub unsafe fn lean_string_size(o: b_lean_obj_arg) -> usize {
39    *raw_field!(lean_to_string(o), lean_string_object, m_size)
40}
41
42#[inline(always)]
43pub unsafe fn lean_string_len(o: b_lean_obj_arg) -> usize {
44    *raw_field!(lean_to_string(o), lean_string_object, m_length)
45}
46
47#[inline(always)]
48pub unsafe fn lean_string_data_byte_size(o: *mut lean_object) -> usize {
49    core::mem::size_of::<lean_string_object>() + lean_string_size(o)
50}
51
52#[inline(always)]
53pub unsafe fn lean_string_length(o: b_lean_obj_arg) -> lean_obj_res {
54    lean_box(lean_string_len(o))
55}
56
57#[inline]
58pub unsafe fn lean_string_utf8_at_end(s: b_lean_obj_arg, i: b_lean_obj_arg) -> u8 {
59    (!lean_is_scalar(i) || lean_unbox(i) >= lean_string_size(s) - 1) as u8
60}
61
62#[inline(always)]
63pub unsafe fn lean_string_utf8_byte_size(s: b_lean_obj_arg) -> lean_obj_res {
64    lean_box(lean_string_size(s) - 1)
65}
66
67#[inline]
68pub unsafe fn lean_string_eq(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool {
69    s1 == s2 || (lean_string_size(s1) == lean_string_size(s2) && lean_string_eq_cold(s1, s2))
70}
71
72#[inline(always)]
73pub unsafe fn lean_string_ne(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool {
74    !lean_string_eq(s1, s2)
75}
76
77#[inline(always)]
78pub unsafe fn lean_string_dec_eq(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> u8 {
79    lean_string_eq(s1, s2) as u8
80}
81
82#[inline(always)]
83pub unsafe fn lean_string_dec_lt(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> u8 {
84    lean_string_lt(s1, s2) as u8
85}
86
87#[inline(always)]
88pub unsafe fn lean_string_utf8_get_fast(s: b_lean_obj_arg, i: b_lean_obj_arg) -> u32 {
89    let st = lean_string_cstr(s);
90    let idx = lean_unbox(i);
91    let c = *st.add(idx);
92    if c & 0x80 == 0 {
93        c as u32
94    } else {
95        lean_string_utf8_get_fast_cold(st, idx, lean_string_size(s), c)
96    }
97}
98
99#[inline(always)]
100pub unsafe fn lean_string_get_byte_fast(s: b_lean_obj_arg, i: b_lean_obj_arg) -> u8 {
101    let str = lean_string_cstr(s);
102    let idx = lean_unbox(i);
103    *str.add(idx)
104}
105
106#[inline(always)]
107pub unsafe fn lean_string_utf8_next_fast(s: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res {
108    let s = lean_string_cstr(s);
109    let idx = lean_unbox(i);
110    let c = *s.add(idx);
111    if c & 0x80 == 0 {
112        lean_box(idx + 1)
113    } else {
114        lean_string_utf8_next_fast_cold(idx, c)
115    }
116}
117
118extern "C" {
119    pub fn lean_utf8_strlen(str: *const u8) -> usize;
120    pub fn lean_utf8_n_strlen(str: *const u8, n: usize) -> usize;
121    pub fn lean_mk_string_unchecked(s: *const u8, sz: usize, len: usize) -> lean_obj_res;
122    pub fn lean_mk_string_from_bytes(s: *const u8, sz: usize) -> lean_obj_res;
123    pub fn lean_mk_string_from_bytes_unchecked(s: *const u8, sz: usize) -> lean_obj_res;
124    pub fn lean_mk_ascii_string_unchecked(s: *const u8) -> lean_obj_res;
125    pub fn lean_mk_string(s: *const u8) -> lean_obj_res;
126    pub fn lean_string_push(s: lean_obj_arg, c: u32) -> lean_obj_res;
127    pub fn lean_string_append(s1: lean_obj_arg, s2: lean_obj_arg) -> lean_obj_res;
128    pub fn lean_string_mk(cs: lean_obj_arg) -> lean_obj_res;
129    pub fn lean_string_data(s: lean_obj_arg) -> lean_obj_res;
130    pub fn lean_string_utf8_get(s: b_lean_obj_arg, i: b_lean_obj_arg) -> u32;
131    pub fn lean_string_utf8_get_fast_cold(s: *const u8, i: usize, size: usize, c: u8) -> u32;
132    pub fn lean_string_utf8_next(s: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res;
133    pub fn lean_string_utf8_next_fast_cold(i: usize, c: u8) -> lean_obj_res;
134    pub fn lean_string_utf8_prev(s: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res;
135    pub fn lean_string_utf8_set(s: lean_obj_arg, i: b_lean_obj_arg, c: u32) -> lean_obj_res;
136    pub fn lean_string_utf8_extract(
137        s: b_lean_obj_arg,
138        b: b_lean_obj_arg,
139        e: b_lean_obj_arg,
140    ) -> lean_obj_res;
141    #[cold]
142    pub fn lean_string_eq_cold(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool;
143    pub fn lean_string_lt(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool;
144    pub fn lean_string_hash(s: b_lean_obj_arg) -> u64;
145    pub fn lean_string_of_usize(s: usize) -> lean_obj_res;
146}
lean_sys/string.rs

lean_sys/
string.rs
