lean_sys/primitive/
int64.rs

1use crate::*;
2
3#[inline]
4pub unsafe fn lean_int64_of_int(a: b_lean_obj_arg) -> u64 {
5    if lean_is_scalar(a) {
6        lean_scalar_to_int64(a) as u64
7    } else {
8        lean_int64_of_big_int(a) as u64
9    }
10}
11
12#[inline]
13pub unsafe fn lean_int64_of_nat(a: b_lean_obj_arg) -> u64 {
14    if lean_is_scalar(a) {
15        lean_unbox(a) as i64 as u64
16    } else {
17        lean_int64_of_big_int(a) as u64
18    }
19}
20
21#[inline(always)]
22pub unsafe fn lean_int64_to_int_sint(a: u64) -> lean_obj_res {
23    lean_int64_to_int(a as i64)
24}
25
26#[inline(always)]
27pub fn lean_int64_neg(a: u64) -> u64 {
28    (a as i64).wrapping_neg() as u64
29}
30
31#[inline(always)]
32pub fn lean_int64_add(a1: u64, a2: u64) -> u64 {
33    (a1 as i64).wrapping_add(a2 as i64) as u64
34}
35
36#[inline(always)]
37pub fn lean_int64_sub(a1: u64, a2: u64) -> u64 {
38    (a1 as i64).wrapping_sub(a2 as i64) as u64
39}
40
41#[inline(always)]
42pub fn lean_int64_mul(a1: u64, a2: u64) -> u64 {
43    (a1 as i64).wrapping_mul(a2 as i64) as u64
44}
45
46#[inline(always)]
47pub fn lean_int64_div(a1: u64, a2: u64) -> u64 {
48    if a2 == 0 {
49        0
50    } else {
51        (a1 as i64).wrapping_div(a2 as i64) as u64
52    }
53}
54
55#[inline(always)]
56pub fn lean_int64_mod(a1: u64, a2: u64) -> u64 {
57    if a2 == 0 {
58        a1
59    } else {
60        (a1 as i64).wrapping_rem(a2 as i64) as u64
61    }
62}
63
64#[inline(always)]
65pub fn lean_int64_land(a1: u64, a2: u64) -> u64 {
66    ((a1 as i64) & (a2 as i64)) as u64
67}
68
69#[inline(always)]
70pub fn lean_int64_lor(a1: u64, a2: u64) -> u64 {
71    ((a1 as i64) | (a2 as i64)) as u64
72}
73
74#[inline(always)]
75pub fn lean_int64_xor(a1: u64, a2: u64) -> u64 {
76    ((a1 as i64) ^ (a2 as i64)) as u64
77}
78
79#[inline(always)]
80pub fn lean_int64_shift_left(a1: u64, a2: u64) -> u64 {
81    let rhs = (a2 as i64 % 64 + 64) % 64; // this is smod 64
82    (a1 as i64).wrapping_shl(rhs as u32) as u64
83}
84
85#[inline(always)]
86pub fn lean_int64_shift_right(a1: u64, a2: u64) -> u64 {
87    let rhs = (a2 as i64 % 64 + 64) % 64; // this is smod 64
88    (a1 as i64).wrapping_shr(rhs as u32) as u64
89}
90
91#[inline(always)]
92pub fn lean_int64_complement(a: u64) -> u64 {
93    !(a as i64) as u64
94}
95
96#[inline(always)]
97pub fn lean_int64_abs(a: u64) -> u64 {
98    (a as i64).unsigned_abs()
99}
100
101#[inline(always)]
102pub fn lean_int64_dec_eq(a1: u64, a2: u64) -> u64 {
103    (a1 as i64 == a2 as i64) as u64
104}
105
106#[inline(always)]
107pub fn lean_int64_dec_lt(a1: u64, a2: u64) -> u64 {
108    ((a1 as i64) < a2 as i64) as u64
109}
110
111#[inline(always)]
112pub fn lean_int64_dec_le(a1: u64, a2: u64) -> u64 {
113    (a1 as i64 <= a2 as i64) as u64
114}
115
116#[inline]
117pub fn lean_int64_to_int8(a: u64) -> u8 {
118    a as i64 as i8 as u8
119}
120#[inline]
121pub fn lean_int64_to_int16(a: u64) -> u16 {
122    a as i64 as i16 as u16
123}
124#[inline]
125pub fn lean_int64_to_int32(a: u64) -> u32 {
126    a as i64 as i32 as u32
127}
128#[inline]
129pub fn lean_int64_to_isize(a: u64) -> usize {
130    a as i64 as isize as usize
131}
132
133extern "C" {
134    pub fn lean_int64_of_big_int(a: b_lean_obj_arg) -> i64;
135}
lean_sys/primitive/int64.rs

lean_sys/primitive/
int64.rs
