lean_sys/
int.rs

1/*! Integers */
2use crate::*;
3
4pub const LEAN_MAX_SMALL_INT: c_int = if core::mem::size_of::<*const ()>() == 8 {
5    c_int::MAX
6} else {
7    c_int::MAX >> 1
8};
9pub const LEAN_MIN_SMALL_INT: c_int = if core::mem::size_of::<*const ()>() == 8 {
10    c_int::MIN
11} else {
12    c_int::MIN >> 1
13};
14
15#[inline]
16pub unsafe fn lean_int_to_int(n: c_int) -> lean_obj_res {
17    #[allow(clippy::absurd_extreme_comparisons, clippy::manual_range_contains)]
18    if n <= LEAN_MAX_SMALL_INT && n >= LEAN_MIN_SMALL_INT {
19        lean_box(n as usize)
20    } else {
21        lean_big_int_to_int(n)
22    }
23}
24
25#[inline]
26pub unsafe fn lean_int64_to_int(n: i64) -> lean_obj_res {
27    if n <= LEAN_MAX_SMALL_INT as i64 && n >= LEAN_MIN_SMALL_INT as i64 {
28        //TODO: likely
29        lean_box(n as usize)
30    } else {
31        lean_big_int64_to_int(n)
32    }
33}
34
35#[inline(always)]
36pub unsafe fn lean_scalar_to_int64(a: b_lean_obj_arg) -> i64 {
37    debug_assert!(lean_is_scalar(a));
38    lean_unbox(a) as i64
39}
40
41#[inline(always)]
42pub unsafe fn lean_scalar_to_int(a: b_lean_obj_arg) -> c_int {
43    debug_assert!(lean_is_scalar(a));
44    lean_unbox(a) as c_int
45}
46
47#[inline]
48pub unsafe fn lean_nat_to_int(a: lean_obj_arg) -> lean_obj_res {
49    if lean_is_scalar(a) {
50        let v = lean_unbox(a);
51        if v <= LEAN_MAX_SMALL_INT as usize {
52            a
53        } else {
54            lean_big_size_t_to_int(v)
55        }
56    } else {
57        a
58    }
59}
60
61#[inline]
62pub unsafe fn lean_int_neg(a: b_lean_obj_arg) -> lean_obj_res {
63    if lean_is_scalar(a) {
64        //TODO: likely
65        lean_int64_to_int(-lean_scalar_to_int64(a))
66    } else {
67        lean_int_big_neg(a)
68    }
69}
70
71#[inline]
72pub unsafe fn lean_int_neg_succ_of_nat(a: lean_obj_arg) -> lean_obj_res {
73    let s = lean_nat_succ(a);
74    lean_dec(a);
75    let i = lean_nat_to_int(s); /* Recall that `lean_nat_to_int` consumes the argument */
76    let r = lean_int_neg(i);
77    lean_dec(i);
78    r
79}
80
81#[inline]
82pub unsafe fn lean_int_add(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
83    if lean_is_scalar(a1) && lean_is_scalar(a2) {
84        lean_int64_to_int(lean_scalar_to_int64(a1) + lean_scalar_to_int64(a2))
85    } else {
86        lean_int_big_add(a1, a2)
87    }
88}
89
90#[inline]
91pub unsafe fn lean_int_sub(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
92    if lean_is_scalar(a1) && lean_is_scalar(a2) {
93        lean_int64_to_int(lean_scalar_to_int64(a1) - lean_scalar_to_int64(a2))
94    } else {
95        lean_int_big_sub(a1, a2)
96    }
97}
98
99#[inline]
100pub unsafe fn lean_int_mul(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
101    if lean_is_scalar(a1) && lean_is_scalar(a2) {
102        lean_int64_to_int(lean_scalar_to_int64(a1) * lean_scalar_to_int64(a2))
103    } else {
104        lean_int_big_mul(a1, a2)
105    }
106}
107
108#[inline]
109pub unsafe fn lean_int_div(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
110    if lean_is_scalar(a1) && lean_is_scalar(a2) {
111        let a2 = lean_scalar_to_int(a2) as i64;
112        if a2 == 0 {
113            lean_box(0)
114        } else {
115            lean_int64_to_int(lean_scalar_to_int(a1) as i64 / a2)
116        }
117    } else {
118        lean_int_big_div(a1, a2)
119    }
120}
121
122#[inline]
123pub unsafe fn lean_int_div_exact(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
124    if lean_is_scalar(a1) && lean_is_scalar(a2) {
125        let a2 = lean_scalar_to_int(a2) as i64;
126        if a2 == 0 {
127            lean_box(0)
128        } else {
129            lean_int64_to_int(lean_scalar_to_int(a1) as i64 / a2)
130        }
131    } else {
132        lean_int_big_div_exact(a1, a2)
133    }
134}
135
136#[inline]
137pub unsafe fn lean_int_mod(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
138    if lean_is_scalar(a1) && lean_is_scalar(a2) {
139        let a2 = lean_scalar_to_int64(a2);
140        if a2 == 0 {
141            a1
142        } else {
143            lean_int64_to_int(lean_scalar_to_int64(a1) % a2)
144        }
145    } else {
146        lean_int_big_mod(a1, a2)
147    }
148}
149
150pub unsafe fn lean_int_ediv(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
151    if lean_is_scalar(a1) && lean_is_scalar(a2) {
152        if core::mem::size_of::<usize>() == 8 {
153            /* 64-bit version, we use 64-bit numbers to avoid overflow when v1 == LEAN_MIN_SMALL_INT. */
154            let n = lean_scalar_to_int64(a1);
155            let d = lean_scalar_to_int64(a2);
156            if d == 0 {
157                lean_box(0)
158            } else {
159                let mut q = n / d;
160                let r = n % d;
161                if r < 0 {
162                    q = if d > 0 { q - 1 } else { q + 1 };
163                }
164                lean_int64_to_int(q)
165            }
166        } else {
167            /* 32-bit version */
168            let n = lean_scalar_to_int(a1);
169            let d = lean_scalar_to_int(a2);
170            if d == 0 {
171                lean_box(0)
172            } else {
173                let mut q = n / d;
174                let r = n % d;
175                if r < 0 {
176                    q = if d > 0 { q - 1 } else { q + 1 };
177                }
178                lean_int_to_int(q)
179            }
180        }
181    } else {
182        lean_int_big_ediv(a1, a2)
183    }
184}
185
186pub unsafe fn lean_int_emod(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
187    if lean_is_scalar(a1) && lean_is_scalar(a2) {
188        if core::mem::size_of::<usize>() == 8 {
189            /* 64-bit version, we use 64-bit numbers to avoid overflow when v1 == LEAN_MIN_SMALL_INT. */
190            let n = lean_scalar_to_int64(a1);
191            let d = lean_scalar_to_int64(a2);
192            if d == 0 {
193                a1
194            } else {
195                let mut r = n % d;
196                if r < 0 {
197                    r = if d > 0 { r + d } else { r - d };
198                }
199                lean_int64_to_int(r)
200            }
201        } else {
202            /* 32-bit version */
203            let n = lean_scalar_to_int(a1);
204            let d = lean_scalar_to_int(a2);
205            if d == 0 {
206                a1
207            } else {
208                let mut r = n % d;
209                if r < 0 {
210                    r = if d > 0 { r + d } else { r - d };
211                }
212                lean_int_to_int(r)
213            }
214        }
215    } else {
216        lean_int_big_emod(a1, a2)
217    }
218}
219
220#[inline]
221pub unsafe fn lean_int_eq(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
222    a1 == a2 || lean_int_big_eq(a1, a2)
223}
224
225#[inline(always)]
226pub unsafe fn lean_int_ne(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
227    !lean_int_eq(a1, a2)
228}
229
230#[inline]
231pub unsafe fn lean_int_le(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
232    if lean_is_scalar(a1) && lean_is_scalar(a2) {
233        lean_scalar_to_int64(a1) <= lean_scalar_to_int64(a2)
234    } else {
235        lean_int_big_le(a1, a2)
236    }
237}
238
239#[inline]
240pub unsafe fn lean_int_lt(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
241    if lean_is_scalar(a1) && lean_is_scalar(a2) {
242        lean_scalar_to_int64(a1) < lean_scalar_to_int64(a2)
243    } else {
244        lean_int_big_lt(a1, a2)
245    }
246}
247
248#[inline]
249pub unsafe fn lean_int_to_nat(a: lean_obj_arg) -> lean_obj_res {
250    debug_assert!(!lean_int_lt(a, lean_box(0)));
251    if lean_is_scalar(a) {
252        a
253    } else {
254        lean_big_int_to_nat(a)
255    }
256}
257
258#[inline]
259pub unsafe fn lean_nat_abs(i: b_lean_obj_arg) -> lean_obj_res {
260    if lean_int_lt(i, lean_box(0)) {
261        lean_int_to_nat(lean_int_neg(i))
262    } else {
263        lean_inc(i);
264        lean_int_to_nat(i)
265    }
266}
267
268#[inline]
269pub unsafe fn lean_int_dec_eq(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
270    lean_int_eq(a1, a2) as u8
271}
272
273#[inline]
274pub unsafe fn lean_int_dec_le(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
275    lean_int_le(a1, a2) as u8
276}
277
278#[inline]
279pub unsafe fn lean_int_dec_lt(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
280    lean_int_lt(a1, a2) as u8
281}
282
283#[inline]
284pub unsafe fn lean_int_dec_nonneg(a: b_lean_obj_arg) -> u8 {
285    (if lean_is_scalar(a) {
286        //TODO: likely
287        lean_scalar_to_int(a) >= 0
288    } else {
289        lean_int_big_nonneg(a)
290    }) as u8
291}
292
293extern "C" {
294    pub fn lean_int_big_neg(a: *mut lean_object) -> *mut lean_object;
295    pub fn lean_int_big_add(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
296    pub fn lean_int_big_sub(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
297    pub fn lean_int_big_mul(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
298    pub fn lean_int_big_div(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
299    pub fn lean_int_big_div_exact(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
300    pub fn lean_int_big_mod(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
301    pub fn lean_int_big_ediv(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
302    pub fn lean_int_big_emod(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
303    pub fn lean_int_big_eq(a1: *mut lean_object, a2: *mut lean_object) -> bool;
304    pub fn lean_int_big_le(a1: *mut lean_object, a2: *mut lean_object) -> bool;
305    pub fn lean_int_big_lt(a1: *mut lean_object, a2: *mut lean_object) -> bool;
306    pub fn lean_int_big_nonneg(a: *mut lean_object) -> bool;
307
308    pub fn lean_cstr_to_int(n: *const u8) -> *mut lean_object;
309    pub fn lean_big_int_to_int(n: c_int) -> *mut lean_object;
310    pub fn lean_big_size_t_to_int(n: usize) -> *mut lean_object;
311    pub fn lean_big_int64_to_int(n: i64) -> *mut lean_object;
312
313    pub fn lean_big_int_to_nat(a: lean_obj_arg) -> lean_obj_res;
314}
lean_sys/int.rs

lean_sys/
int.rs
