lean_sys/
nat.rs

1/*! Natural numbers */
2use crate::*;
3
4pub const LEAN_MAX_SMALL_NAT: usize = usize::MAX >> 1;
5
6#[inline]
7pub unsafe fn lean_usize_to_nat(n: usize) -> lean_obj_res {
8    if n <= LEAN_MAX_SMALL_NAT {
9        //TODO: likely
10        lean_box(n)
11    } else {
12        lean_big_usize_to_nat(n)
13    }
14}
15
16#[inline(always)]
17pub unsafe fn lean_unsigned_to_nat(n: c_uint) -> lean_obj_res {
18    lean_usize_to_nat(n as usize)
19}
20
21#[inline]
22pub unsafe fn lean_uint64_to_nat(n: u64) -> lean_obj_res {
23    if n <= LEAN_MAX_SMALL_NAT as u64 {
24        //TODO: likely
25        lean_box(n as usize)
26    } else {
27        lean_big_uint64_to_nat(n)
28    }
29}
30
31#[inline]
32pub unsafe fn lean_nat_succ(a: b_lean_obj_arg) -> lean_obj_res {
33    if lean_is_scalar(a) {
34        //TODO: likely
35        lean_usize_to_nat(lean_unbox(a) + 1)
36    } else {
37        lean_nat_big_succ(a)
38    }
39}
40
41#[inline]
42pub unsafe fn lean_nat_add(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
43    if lean_is_scalar(a1) && lean_is_scalar(a2) {
44        //TODO: likely
45        lean_usize_to_nat(lean_unbox(a1) + lean_unbox(a2))
46    } else {
47        lean_nat_big_add(a1, a2)
48    }
49}
50
51#[inline]
52pub unsafe fn lean_nat_sub(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
53    if lean_is_scalar(a1) && lean_is_scalar(a2) {
54        //TODO: likely
55        lean_box(lean_unbox(a1).saturating_sub(lean_unbox(a2)))
56    } else {
57        lean_nat_big_sub(a1, a2)
58    }
59}
60
61#[inline]
62pub unsafe fn lean_nat_mul(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
63    if lean_is_scalar(a1) && lean_is_scalar(a2) {
64        //TODO: likely
65        let a1 = lean_unbox(a1);
66        let a2 = lean_unbox(a2);
67        match a1.checked_mul(a2) {
68            Some(r) if r <= LEAN_MAX_SMALL_NAT => lean_box(r),
69            _ => lean_nat_overflow_mul(a1, a2),
70        }
71    } else {
72        lean_nat_big_mul(a1, a2)
73    }
74}
75
76#[inline]
77pub unsafe fn lean_nat_div(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
78    if lean_is_scalar(a1) && lean_is_scalar(a2) {
79        //TODO: likely
80        let n1 = lean_unbox(a1);
81        let n2 = lean_unbox(a2);
82        lean_box(if n2 == 0 { 0 } else { n1.saturating_div(n2) })
83    } else {
84        lean_nat_big_div(a1, a2)
85    }
86}
87
88/// assumes that a1 % a2 = 0
89#[inline]
90pub unsafe fn lean_nat_div_exact(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
91    if lean_is_scalar(a1) && lean_is_scalar(a2) {
92        //TODO: likely
93        let n1 = lean_unbox(a1);
94        let n2 = lean_unbox(a2);
95        lean_box(if n2 == 0 { 0 } else { n1.saturating_div(n2) })
96    } else {
97        lean_nat_big_div_exact(a1, a2)
98    }
99}
100
101#[inline]
102pub unsafe fn lean_nat_mod(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
103    if lean_is_scalar(a1) && lean_is_scalar(a2) {
104        //TODO: likely
105        let a2 = lean_unbox(a2);
106        if a2 == 0 {
107            a1
108        } else {
109            lean_box(lean_unbox(a1) % a2)
110        }
111    } else {
112        lean_nat_big_mod(a1, a2)
113    }
114}
115
116#[inline]
117pub unsafe fn lean_nat_eq(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
118    a1 == a2 || lean_nat_big_eq(a1, a2)
119}
120
121#[inline(always)]
122pub unsafe fn lean_nat_dec_eq(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
123    lean_nat_eq(a1, a2) as u8
124}
125
126#[inline]
127pub unsafe fn lean_nat_le(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
128    if lean_is_scalar(a1) && lean_is_scalar(a2) {
129        //TODO: likely
130        lean_unbox(a1) <= lean_unbox(a2)
131    } else {
132        lean_nat_big_le(a1, a2)
133    }
134}
135
136#[inline(always)]
137pub unsafe fn lean_nat_dec_le(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
138    lean_nat_le(a1, a2) as u8
139}
140
141#[inline]
142pub unsafe fn lean_nat_lt(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
143    if lean_is_scalar(a1) && lean_is_scalar(a2) {
144        //TODO: likely
145        lean_unbox(a1) < lean_unbox(a2)
146    } else {
147        lean_nat_big_lt(a1, a2)
148    }
149}
150
151#[inline(always)]
152pub unsafe fn lean_nat_dec_lt(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
153    lean_nat_lt(a1, a2) as u8
154}
155
156#[inline]
157pub unsafe fn lean_nat_land(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
158    if lean_is_scalar(a1) && lean_is_scalar(a2) {
159        //TODO: likely
160        lean_box(lean_unbox(a1) & lean_unbox(a2))
161    } else {
162        lean_nat_big_land(a1, a2)
163    }
164}
165
166#[inline]
167pub unsafe fn lean_nat_lor(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
168    if lean_is_scalar(a1) && lean_is_scalar(a2) {
169        //TODO: likely
170        lean_box(lean_unbox(a1) | lean_unbox(a2))
171    } else {
172        lean_nat_big_lor(a1, a2)
173    }
174}
175
176#[inline]
177pub unsafe fn lean_nat_lxor(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
178    if lean_is_scalar(a1) && lean_is_scalar(a2) {
179        //TODO: likely
180        lean_box(lean_unbox(a1) ^ lean_unbox(a2))
181    } else {
182        lean_nat_big_xor(a1, a2)
183    }
184}
185
186#[inline]
187pub unsafe fn lean_nat_shiftr(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
188    if lean_is_scalar(a1) && lean_is_scalar(a2) {
189        //TODO: likely
190        let s1 = lean_unbox(a1);
191        let s2 = lean_unbox(a2);
192        let r = if s2 < size_of::<usize>() * 8 {
193            s1 >> s2
194        } else {
195            0
196        };
197        lean_box(r)
198    } else {
199        lean_nat_big_shiftr(a1, a2)
200    }
201}
202
203extern "C" {
204    pub fn lean_nat_big_succ(a: *mut lean_object) -> *mut lean_object;
205    pub fn lean_nat_big_add(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
206    pub fn lean_nat_big_sub(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
207    pub fn lean_nat_big_mul(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
208    pub fn lean_nat_overflow_mul(a1: usize, a2: usize) -> *mut lean_object;
209    pub fn lean_nat_big_div(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
210    pub fn lean_nat_big_div_exact(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
211    pub fn lean_nat_big_mod(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
212    pub fn lean_nat_big_eq(a1: *mut lean_object, a2: *mut lean_object) -> bool;
213    pub fn lean_nat_big_le(a1: *mut lean_object, a2: *mut lean_object) -> bool;
214    pub fn lean_nat_big_lt(a1: *mut lean_object, a2: *mut lean_object) -> bool;
215    pub fn lean_nat_big_land(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
216    pub fn lean_nat_big_lor(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
217    pub fn lean_nat_big_xor(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
218
219    pub fn lean_cstr_to_nat(n: *const u8) -> *mut lean_object;
220    pub fn lean_big_usize_to_nat(n: usize) -> *mut lean_object;
221    pub fn lean_big_uint64_to_nat(n: u64) -> *mut lean_object;
222
223    pub fn lean_nat_shiftl(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
224    pub fn lean_nat_big_shiftr(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
225    pub fn lean_nat_pow(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
226    pub fn lean_nat_gcd(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
227    pub fn lean_nat_log2(a: *mut lean_object) -> *mut lean_object;
228}
229
230#[cfg(test)]
231mod test {
232    extern crate std;
233    use rand::{prelude::SliceRandom, Rng, SeedableRng};
234
235    use super::*;
236
237    unsafe fn slice_mul(s: &[u64]) -> *mut lean_object {
238        let r = s
239            .iter()
240            .map(|&x| lean_uint64_to_nat(x))
241            .fold(lean_uint64_to_nat(0), |a, b| lean_nat_mul(a, b));
242        assert!(lean_is_scalar(r) || lean_is_mpz(r));
243        r
244    }
245
246    #[test]
247    fn big_nat_multiplication_commutes_test() {
248        let mut rng = rand_xoshiro::Xoshiro256PlusPlus::seed_from_u64(0x568478687);
249        unsafe {
250            lean_initialize_runtime_module_locked();
251            let mut vec = std::vec::Vec::with_capacity(100);
252            for _ in 0..10 {
253                for _ in 0..100 {
254                    vec.push(rng.random::<u64>())
255                }
256                let r = slice_mul(&vec[..]);
257                const M: u64 = 595468;
258                let m = lean_nat_mod(r, lean_uint64_to_nat(M));
259                assert!(lean_is_scalar(m));
260                let p = vec.iter().copied().fold(1, |l: u64, r| l.wrapping_mul(r)) % M;
261                assert_eq!(lean_unbox(m) as u64, p);
262                for _ in 0..4 {
263                    vec.shuffle(&mut rng);
264                    assert!(lean_nat_eq(r, slice_mul(&vec[..])));
265                }
266
267                vec.clear();
268            }
269        }
270    }
271}
lean_sys/nat.rs

lean_sys/
nat.rs
