lean_rs_sys/
nat_int.rs

1//! Bignum dispatch — externs from `lean.h:1334–1853` plus the small-int
2//! ceiling constants.
3
4use crate::types::{b_lean_obj_arg, lean_obj_res, lean_object};
5
6/// Largest `Nat` that fits in a scalar pointer (`lean.h:1336`).
7/// On 64-bit hosts this is `usize::MAX >> 1`.
8pub const LEAN_MAX_SMALL_NAT: usize = usize::MAX >> 1;
9
10/// Largest scalar-encodable `Int` (`lean.h:1544`). On 64-bit hosts this is
11/// `i32::MAX`; on 32-bit hosts it is `i32::MAX >> 1`.
12pub const LEAN_MAX_SMALL_INT: i64 = if core::mem::size_of::<*mut ()>() == 8 {
13    i32::MAX as i64
14} else {
15    (i32::MAX >> 1) as i64
16};
17
18/// Smallest scalar-encodable `Int` (`lean.h:1545`).
19pub const LEAN_MIN_SMALL_INT: i64 = if core::mem::size_of::<*mut ()>() == 8 {
20    i32::MIN as i64
21} else {
22    (i32::MIN >> 1) as i64
23};
24
25unsafe extern "C" {
26    // Nat arithmetic (`lean.h:1338–1351`)
27    pub fn lean_nat_big_succ(a: *mut lean_object) -> *mut lean_object;
28    pub fn lean_nat_big_add(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
29    pub fn lean_nat_big_sub(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
30    pub fn lean_nat_big_mul(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
31    pub fn lean_nat_overflow_mul(a1: usize, a2: usize) -> *mut lean_object;
32    pub fn lean_nat_big_div(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
33    pub fn lean_nat_big_div_exact(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
34    pub fn lean_nat_big_mod(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
35    pub fn lean_nat_big_eq(a1: *mut lean_object, a2: *mut lean_object) -> bool;
36    pub fn lean_nat_big_le(a1: *mut lean_object, a2: *mut lean_object) -> bool;
37    pub fn lean_nat_big_lt(a1: *mut lean_object, a2: *mut lean_object) -> bool;
38
39    // Int arithmetic (`lean.h:1546–1558`)
40    pub fn lean_int_big_neg(a: *mut lean_object) -> *mut lean_object;
41    pub fn lean_int_big_add(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
42    pub fn lean_int_big_sub(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
43    pub fn lean_int_big_mul(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
44    pub fn lean_int_big_div(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
45    pub fn lean_int_big_div_exact(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
46    pub fn lean_int_big_mod(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
47    pub fn lean_int_big_ediv(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
48    pub fn lean_int_big_emod(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
49    pub fn lean_int_big_eq(a1: *mut lean_object, a2: *mut lean_object) -> bool;
50    pub fn lean_int_big_le(a1: *mut lean_object, a2: *mut lean_object) -> bool;
51    pub fn lean_int_big_lt(a1: *mut lean_object, a2: *mut lean_object) -> bool;
52    pub fn lean_int_big_nonneg(a: *mut lean_object) -> bool;
53
54    // Widening conversions (`lean.h:1353–1355`, `lean.h:1560–1563`)
55    pub fn lean_cstr_to_nat(s: *const core::ffi::c_char) -> lean_obj_res;
56    pub fn lean_big_usize_to_nat(n: usize) -> lean_obj_res;
57    pub fn lean_big_uint64_to_nat(n: u64) -> lean_obj_res;
58    pub fn lean_cstr_to_int(s: *const core::ffi::c_char) -> lean_obj_res;
59    pub fn lean_big_int_to_int(n: i32) -> lean_obj_res;
60    pub fn lean_big_size_t_to_int(n: usize) -> lean_obj_res;
61    pub fn lean_big_int64_to_int(n: i64) -> lean_obj_res;
62
63    // Narrowing (`lean.h:1871`)
64    pub fn lean_uint8_of_big_nat(a: b_lean_obj_arg) -> u8;
65}
lean_rs_sys/nat_int.rs

lean_rs_sys/
nat_int.rs
