lean_rs_sys/
string.rs

1//! String objects — externs and inline accessors from `lean.h:1157–1234`.
2
3#![allow(clippy::inline_always)]
4
5use core::ffi::c_char;
6
7use crate::repr::LeanStringObjectRepr;
8use crate::types::{b_lean_obj_arg, lean_obj_arg, lean_obj_res, lean_object};
9
10unsafe extern "C" {
11    pub fn lean_utf8_strlen(s: *const c_char) -> usize;
12    pub fn lean_utf8_n_strlen(s: *const c_char, n: usize) -> usize;
13
14    pub fn lean_mk_string(s: *const c_char) -> lean_obj_res;
15    pub fn lean_mk_string_unchecked(s: *const c_char, sz: usize, len: usize) -> lean_obj_res;
16    pub fn lean_mk_string_from_bytes(s: *const c_char, sz: usize) -> lean_obj_res;
17    pub fn lean_mk_string_from_bytes_unchecked(s: *const c_char, sz: usize) -> lean_obj_res;
18    pub fn lean_mk_ascii_string_unchecked(s: *const c_char) -> lean_obj_res;
19
20    pub fn lean_string_push(s: lean_obj_arg, c: u32) -> lean_obj_res;
21    pub fn lean_string_append(s1: lean_obj_arg, s2: b_lean_obj_arg) -> lean_obj_res;
22    pub fn lean_string_mk(cs: lean_obj_arg) -> lean_obj_res;
23    pub fn lean_string_data(s: lean_obj_arg) -> lean_obj_res;
24
25    pub fn lean_string_utf8_get(s: b_lean_obj_arg, i: b_lean_obj_arg) -> u32;
26    pub fn lean_string_utf8_next(s: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res;
27    pub fn lean_string_utf8_prev(s: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res;
28    pub fn lean_string_utf8_set(s: lean_obj_arg, i: b_lean_obj_arg, c: u32) -> lean_obj_res;
29    pub fn lean_string_utf8_extract(s: b_lean_obj_arg, b: b_lean_obj_arg, e: b_lean_obj_arg) -> lean_obj_res;
30
31    pub fn lean_string_eq_cold(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool;
32    pub fn lean_string_lt(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool;
33    pub fn lean_string_hash(s: b_lean_obj_arg) -> u64;
34}
35
36#[inline(always)]
37unsafe fn as_string<'a>(o: *mut lean_object) -> &'a LeanStringObjectRepr {
38    // SAFETY: caller asserts `o` is a Lean string heap object.
39    unsafe { &*o.cast::<LeanStringObjectRepr>() }
40}
41
42/// `m_size` field — byte length including the trailing `\0` (`lean.h:1182`).
43///
44/// # Safety
45///
46/// `o` must be a borrowed Lean string object.
47#[inline(always)]
48pub unsafe fn lean_string_size(o: b_lean_obj_arg) -> usize {
49    // SAFETY: precondition above; layout pinned by build digest.
50    unsafe { as_string(o).size }
51}
52
53/// `m_length` field — UTF-8 character count (`lean.h:1183`).
54///
55/// # Safety
56///
57/// Same as [`lean_string_size`].
58#[inline(always)]
59pub unsafe fn lean_string_len(o: b_lean_obj_arg) -> usize {
60    // SAFETY: precondition above.
61    unsafe { as_string(o).length }
62}
63
64/// `m_capacity` field (`lean.h:1169`).
65///
66/// # Safety
67///
68/// Same as [`lean_string_size`].
69#[inline(always)]
70pub unsafe fn lean_string_capacity(o: *mut lean_object) -> usize {
71    // SAFETY: precondition above.
72    unsafe { as_string(o).capacity }
73}
74
75/// Pointer to the string's NUL-terminated UTF-8 bytes (`lean.h:1178–1181`).
76///
77/// # Safety
78///
79/// `o` must be a borrowed Lean string object. The returned pointer is valid
80/// for as long as `o` retains the refcount that the caller borrowed.
81#[inline(always)]
82pub unsafe fn lean_string_cstr(o: b_lean_obj_arg) -> *const c_char {
83    // SAFETY: precondition above; flexible-array member at fixed offset.
84    unsafe { as_string(o).data.as_ptr().cast::<c_char>() }
85}
86
87/// Total allocation footprint of `o` (`lean.h:1170`).
88///
89/// # Safety
90///
91/// Same as [`lean_string_size`].
92///
93/// # Panics
94///
95/// Panics if `size_of::<LeanStringObjectRepr>() + capacity` overflows
96/// `usize`. The string came from a valid Lean allocation so the sum cannot
97/// realistically overflow; the panic surfaces a corrupted header rather
98/// than a recoverable condition.
99#[inline(always)]
100pub unsafe fn lean_string_byte_size(o: *mut lean_object) -> usize {
101    // SAFETY: precondition above. `capacity` came from a valid Lean string
102    // so the addition cannot overflow; `strict_add` surfaces a corrupted
103    // header as a panic instead of producing a wrong byte size.
104    unsafe { core::mem::size_of::<LeanStringObjectRepr>().strict_add(lean_string_capacity(o)) }
105}
lean_rs_sys/string.rs

lean_rs_sys/
string.rs
