lean-sys 0.0.3

Bindings to Lean 4's C API
Documentation 
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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

/*! 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
}

#[inline(always)]
pub unsafe fn lean_string_utf8_get_fast(s: b_lean_obj_arg, i: b_lean_obj_arg) -> u32 {
    let st = lean_string_cstr(s);
    let idx = lean_unbox(i);
    let c = *st.add(idx) as u8;
    if c & 0x80 == 0 {
        c as u32
    } else {
        lean_string_utf8_get_fast_cold(st, idx, lean_string_size(s), c)
    }
}

#[inline(always)]
pub unsafe fn lean_string_utf8_next_fast(s: b_lean_obj_arg, i: b_lean_obj_arg) -> lean_obj_res {
    let s = lean_string_cstr(s);
    let idx = lean_unbox(i);
    let c = *s.add(idx) as u8;
    if c & 0x80 == 0 {
        lean_box(idx + 1)
    } else {
        lean_string_utf8_next_fast_cold(idx, c)
    }
}

#[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_get_fast_cold(s: *const u8, i: usize, size: usize, c: u8) -> 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_next_fast_cold(i: usize, c: u8) -> 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;
}