1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

/*! Strings */
use crate::*;

#[inline(always)]
pub unsafe fn lean_alloc_string(size: usize, capacity: usize, len: usize) -> lean_obj_res {
    let o = lean_alloc_object(std::mem::size_of::<lean_string_object>() + capacity)
        as *mut lean_string_object;
    lean_set_st_header(o as *mut _, LeanString as u32, 0);
    (raw_field!(o, lean_string_object, m_size) as *mut usize).write(size);
    (raw_field!(o, lean_string_object, m_capacity) as *mut usize).write(capacity);
    (raw_field!(o, lean_string_object, m_length) as *mut usize).write(len);
    o as *mut _
}

#[inline(always)]
pub unsafe fn lean_string_capacity(o: *mut lean_object) -> usize {
    *raw_field!(lean_to_string(o), lean_string_object, m_capacity)
}

#[inline(always)]
pub unsafe fn lean_string_byte_size(o: *mut lean_object) -> usize {
    std::mem::size_of::<lean_string_object>() + lean_string_capacity(o)
}

/** instance : inhabited char := ⟨'A'⟩ */
#[inline(always)]
pub fn lean_char_default_value() -> c_char {
    'A' as c_char
}

#[inline(always)]
pub unsafe fn lean_string_cstr(o: b_lean_obj_arg) -> *const u8 {
    debug_assert!(lean_is_string(o));
    raw_field!(lean_to_string(o), lean_string_object, m_data) as *const _
}

#[inline(always)]
pub unsafe fn lean_string_size(o: b_lean_obj_arg) -> usize {
    *raw_field!(lean_to_string(o), lean_string_object, m_size)
}

#[inline(always)]
pub unsafe fn lean_string_len(o: b_lean_obj_arg) -> usize {
    *raw_field!(lean_to_string(o), lean_string_object, m_length)
}

#[inline(always)]
pub unsafe fn lean_string_length(o: b_lean_obj_arg) -> lean_obj_res {
    lean_box(lean_string_len(o))
}

#[inline]
pub unsafe fn lean_string_utf8_at_end(s: b_lean_obj_arg, i: b_lean_obj_arg) -> u8 {
    (!lean_is_scalar(i) || lean_unbox(i) >= lean_string_size(s) - 1) as u8
}

#[inline(always)]
pub unsafe fn lean_string_utf8_byte_size(s: b_lean_obj_arg) -> lean_obj_res {
    lean_box(lean_string_size(s) - 1)
}

#[inline]
pub unsafe fn lean_string_eq(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool {
    s1 == s2 || (lean_string_size(s1) == lean_string_size(s2) && lean_string_eq_cold(s1, s2))
}

#[inline(always)]
pub unsafe fn lean_string_ne(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool {
    !lean_string_eq(s1, s2)
}

#[inline(always)]
pub unsafe fn lean_string_dec_eq(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> u8 {
    lean_string_eq(s1, s2) as u8
}

#[inline(always)]
pub unsafe fn lean_string_dec_lt(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> u8 {
    lean_string_lt(s1, s2) as u8
}

#[link(name = "leanshared")]
extern "C" {
    pub fn lean_utf8_strlen(str: *const u8) -> usize;
    pub fn lean_utf8_n_strlen(str: *const u8, n: usize) -> usize;
    pub fn lean_mk_string_from_bytes(s: *const u8, sz: usize) -> lean_obj_res;
    pub fn lean_mk_string(s: *const u8) -> lean_obj_res;
    pub fn lean_string_push(s: lean_obj_arg, c: u32) -> lean_obj_res;
    pub fn lean_string_append(s1: lean_obj_arg, s2: lean_obj_arg) -> lean_obj_res;
    pub fn lean_string_mk(cs: lean_obj_arg) -> lean_obj_res;
    pub fn lean_string_data(s: lean_obj_arg) -> lean_obj_res;
    pub fn lean_string_utf8_get(s: b_lean_obj_arg, i: b_lean_obj_arg) -> u32;
    pub fn lean_string_utf8_next(s: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res;
    pub fn lean_string_utf8_prev(s: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res;
    pub fn lean_string_utf8_set(s: lean_obj_arg, i: b_lean_obj_arg, c: u32) -> lean_obj_res;
    pub fn lean_string_utf8_extract(
        s: b_lean_obj_arg,
        b: b_lean_obj_arg,
        e: b_lean_obj_arg,
    ) -> lean_obj_res;
    #[cold]
    pub fn lean_string_eq_cold(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool;
    pub fn lean_string_lt(s1: b_lean_obj_arg, s2: b_lean_obj_arg) -> bool;
    pub fn lean_string_hash(s: b_lean_obj_arg) -> u64;
}