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

/*! FloatArray (special case of Array of Scalars) */
use crate::*;

#[inline]
pub unsafe fn lean_mk_empty_float_array(capacity: b_lean_obj_arg) -> lean_obj_res {
    if !lean_is_scalar(capacity) {
        lean_internal_panic_out_of_memory()
    }
    lean_alloc_sarray(
        std::mem::size_of::<f64>() as c_uint,
        0,
        lean_unbox(capacity),
    )
}

#[inline(always)]
pub unsafe fn lean_float_array_size(a: b_lean_obj_arg) -> lean_obj_res {
    lean_box(lean_sarray_size(a))
}

#[inline(always)]
pub unsafe fn lean_float_array_cptr(a: b_lean_obj_arg) -> *mut f64 {
    lean_sarray_cptr(a) as *mut _
}

#[inline(always)]
pub unsafe fn lean_float_array_uget(a: b_lean_obj_arg, i: usize) -> f64 {
    debug_assert!(i < lean_sarray_size(a));
    *lean_float_array_cptr(a).add(i)
}

#[inline]
pub unsafe fn lean_float_array_get(a: b_lean_obj_arg, i: b_lean_obj_arg) -> f64 {
    if lean_is_scalar(i) {
        let i = lean_unbox(i);
        if i < lean_sarray_size(a) {
            lean_float_array_uget(a, i)
        } else {
            0.0
        }
    } else {
        /* The index must be out of bounds. Otherwise we would be out of memory. */
        0.0
    }
}

#[inline(always)]
pub unsafe fn lean_float_array_fget(a: b_lean_obj_arg, i: b_lean_obj_arg) -> f64 {
    lean_float_array_uget(a, lean_unbox(i))
}

#[inline(always)]
pub unsafe fn lean_float_array_uset(a: lean_obj_arg, i: usize, v: f64) -> *mut lean_object {
    let r = if lean_is_exclusive(a) {
        a
    } else {
        lean_copy_byte_array(a)
    };
    let it = lean_float_array_cptr(r).add(i);
    *it = v;
    r
}

#[inline]
pub unsafe fn lean_float_array_set(a: lean_obj_arg, i: b_lean_obj_arg, v: f64) -> *mut lean_object {
    if !lean_is_scalar(i) {
        a
    } else {
        let i = lean_unbox(i);
        if i >= lean_sarray_size(a) {
            a
        } else {
            lean_float_array_uset(a, i, v)
        }
    }
}

#[inline(always)]
pub unsafe fn lean_float_array_fset(
    a: lean_obj_arg,
    i: b_lean_obj_arg,
    v: f64,
) -> *mut lean_object {
    lean_float_array_uset(a, lean_unbox(i), v)
}

#[link(name = "leanshared")]
extern "C" {
    pub fn lean_float_array_mk(a: lean_obj_arg) -> lean_obj_res;
    pub fn lean_float_array_data(a: lean_obj_arg) -> lean_obj_res;
    pub fn lean_copy_float_array(a: lean_obj_arg) -> lean_obj_res;
    pub fn lean_float_array_push(a: lean_obj_arg, d: f64) -> lean_obj_res;
}