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        lean_box(lean_unbox(a1).saturating_div(lean_unbox(a2)))
81    } else {
82        lean_nat_big_div(a1, a2)
83    }
84}
85
86#[inline]
87pub unsafe fn lean_nat_mod(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
88    if lean_is_scalar(a1) && lean_is_scalar(a2) {
89        //TODO: likely
90        let a2 = lean_unbox(a2);
91        if a2 == 0 {
92            a1
93        } else {
94            lean_box(lean_unbox(a1) % a2)
95        }
96    } else {
97        lean_nat_big_mod(a1, a2)
98    }
99}
100
101#[inline]
102pub unsafe fn lean_nat_eq(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
103    a1 == a2 || lean_nat_big_eq(a1, a2)
104}
105
106#[inline(always)]
107pub unsafe fn lean_nat_dec_eq(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
108    lean_nat_eq(a1, a2) as u8
109}
110
111#[inline]
112pub unsafe fn lean_nat_le(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> bool {
113    if lean_is_scalar(a1) && lean_is_scalar(a2) {
114        //TODO: likely
115        lean_unbox(a1) <= lean_unbox(a2)
116    } else {
117        lean_nat_big_le(a1, a2)
118    }
119}
120
121#[inline(always)]
122pub unsafe fn lean_nat_dec_le(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
123    lean_nat_le(a1, a2) as u8
124}
125
126#[inline]
127pub unsafe fn lean_nat_lt(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_lt(a1, a2)
133    }
134}
135
136#[inline(always)]
137pub unsafe fn lean_nat_dec_lt(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> u8 {
138    lean_nat_lt(a1, a2) as u8
139}
140
141#[inline]
142pub unsafe fn lean_nat_land(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
143    if lean_is_scalar(a1) && lean_is_scalar(a2) {
144        //TODO: likely
145        lean_box(lean_unbox(a1) & lean_unbox(a2))
146    } else {
147        lean_nat_big_land(a1, a2)
148    }
149}
150
151#[inline]
152pub unsafe fn lean_nat_lor(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
153    if lean_is_scalar(a1) && lean_is_scalar(a2) {
154        //TODO: likely
155        lean_box(lean_unbox(a1) | lean_unbox(a2))
156    } else {
157        lean_nat_big_lor(a1, a2)
158    }
159}
160
161#[inline]
162pub unsafe fn lean_nat_lxor(a1: b_lean_obj_arg, a2: b_lean_obj_arg) -> lean_obj_res {
163    if lean_is_scalar(a1) && lean_is_scalar(a2) {
164        //TODO: likely
165        lean_box(lean_unbox(a1) ^ lean_unbox(a2))
166    } else {
167        lean_nat_big_xor(a1, a2)
168    }
169}
170
171extern "C" {
172    pub fn lean_nat_big_succ(a: *mut lean_object) -> *mut lean_object;
173    pub fn lean_nat_big_add(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
174    pub fn lean_nat_big_sub(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
175    pub fn lean_nat_big_mul(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
176    pub fn lean_nat_overflow_mul(a1: usize, a2: usize) -> *mut lean_object;
177    pub fn lean_nat_big_div(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
178    pub fn lean_nat_big_mod(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
179    pub fn lean_nat_big_eq(a1: *mut lean_object, a2: *mut lean_object) -> bool;
180    pub fn lean_nat_big_le(a1: *mut lean_object, a2: *mut lean_object) -> bool;
181    pub fn lean_nat_big_lt(a1: *mut lean_object, a2: *mut lean_object) -> bool;
182    pub fn lean_nat_big_land(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
183    pub fn lean_nat_big_lor(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
184    pub fn lean_nat_big_xor(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
185
186    pub fn lean_cstr_to_nat(n: *const u8) -> *mut lean_object;
187    pub fn lean_big_usize_to_nat(n: usize) -> *mut lean_object;
188    pub fn lean_big_uint64_to_nat(n: u64) -> *mut lean_object;
189
190    pub fn lean_nat_shiftl(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
191    pub fn lean_nat_shiftr(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
192    pub fn lean_nat_pow(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
193    pub fn lean_nat_gcd(a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
194    pub fn lean_nat_log2(a: *mut lean_object) -> *mut lean_object;
195}
196
197#[cfg(test)]
198mod test {
199    extern crate std;
200    use rand::{prelude::SliceRandom, Rng, SeedableRng};
201
202    use super::*;
203
204    unsafe fn slice_mul(s: &[u64]) -> *mut lean_object {
205        let r = s
206            .iter()
207            .map(|&x| lean_uint64_to_nat(x))
208            .fold(lean_uint64_to_nat(0), |a, b| lean_nat_mul(a, b));
209        assert!(lean_is_scalar(r) || lean_is_mpz(r));
210        r
211    }
212
213    #[test]
214    fn big_nat_multiplication_commutes_test() {
215        let mut rng = rand_xoshiro::Xoshiro256PlusPlus::seed_from_u64(0x568478687);
216        unsafe {
217            lean_initialize_runtime_module_locked();
218            let mut vec = std::vec::Vec::with_capacity(100);
219            for _ in 0..10 {
220                for _ in 0..100 {
221                    vec.push(rng.gen::<u64>())
222                }
223                let r = slice_mul(&vec[..]);
224                const M: u64 = 595468;
225                let m = lean_nat_mod(r, lean_uint64_to_nat(M));
226                assert!(lean_is_scalar(m));
227                let p = vec.iter().copied().fold(1, |l: u64, r| l.wrapping_mul(r)) % M;
228                assert_eq!(lean_unbox(m) as u64, p);
229                for _ in 0..4 {
230                    vec.shuffle(&mut rng);
231                    assert!(lean_nat_eq(r, slice_mul(&vec[..])));
232                }
233
234                vec.clear();
235            }
236        }
237    }
238}
lean_sys/nat.rs

lean_sys/
nat.rs
