lean_sys/primitive/
isize_.rs

1use crate::*;
2
3#[inline]
4pub unsafe fn lean_isize_of_int(a: b_lean_obj_arg) -> usize {
5    if lean_is_scalar(a) {
6        lean_scalar_to_int64(a) as isize as usize
7    } else {
8        lean_isize_of_big_int(a) as usize
9    }
10}
11
12#[inline]
13pub unsafe fn lean_isize_of_nat(a: b_lean_obj_arg) -> usize {
14    if lean_is_scalar(a) {
15        lean_unbox(a) as isize as usize
16    } else {
17        lean_isize_of_big_int(a) as usize
18    }
19}
20
21#[inline(always)]
22pub unsafe fn lean_isize_to_int(a: usize) -> lean_obj_res {
23    lean_int64_to_int(a as i64)
24}
25
26#[inline(always)]
27pub fn lean_isize_neg(a: usize) -> usize {
28    (a as isize).wrapping_neg() as usize
29}
30
31#[inline(always)]
32pub fn lean_isize_add(a1: usize, a2: usize) -> usize {
33    (a1 as isize).wrapping_add(a2 as isize) as usize
34}
35
36#[inline(always)]
37pub fn lean_isize_sub(a1: usize, a2: usize) -> usize {
38    (a1 as isize).wrapping_sub(a2 as isize) as usize
39}
40
41#[inline(always)]
42pub fn lean_isize_mul(a1: usize, a2: usize) -> usize {
43    (a1 as isize).wrapping_mul(a2 as isize) as usize
44}
45
46#[inline(always)]
47pub fn lean_isize_div(a1: usize, a2: usize) -> usize {
48    if a2 == 0 {
49        0
50    } else {
51        (a1 as isize).wrapping_div(a2 as isize) as usize
52    }
53}
54
55#[inline(always)]
56pub fn lean_isize_mod(a1: usize, a2: usize) -> usize {
57    if a2 == 0 {
58        a1
59    } else {
60        (a1 as isize).wrapping_rem(a2 as isize) as usize
61    }
62}
63
64#[inline(always)]
65pub fn lean_isize_land(a1: usize, a2: usize) -> usize {
66    ((a1 as isize) & (a2 as isize)) as usize
67}
68
69#[inline(always)]
70pub fn lean_isize_lor(a1: usize, a2: usize) -> usize {
71    ((a1 as isize) | (a2 as isize)) as usize
72}
73
74#[inline(always)]
75pub fn lean_isize_xor(a1: usize, a2: usize) -> usize {
76    ((a1 as isize) ^ (a2 as isize)) as usize
77}
78
79#[inline(always)]
80pub fn lean_isize_shift_left(a1: usize, a2: usize) -> usize {
81    const SIZE: isize = isize::BITS as isize;
82    let rhs = (a2 as isize % SIZE + SIZE) % SIZE; // this is smod
83    (a1 as isize).wrapping_shl(rhs as u32) as usize
84}
85
86#[inline(always)]
87pub fn lean_isize_shift_right(a1: usize, a2: usize) -> usize {
88    const SIZE: isize = isize::BITS as isize;
89    let rhs = (a2 as isize % SIZE + SIZE) % SIZE; // this is smod
90    (a1 as isize).wrapping_shr(rhs as u32) as usize
91}
92
93#[inline(always)]
94pub fn lean_isize_complement(a: usize) -> usize {
95    !(a as isize) as usize
96}
97
98#[inline(always)]
99pub fn lean_isize_abs(a: usize) -> usize {
100    (a as isize).unsigned_abs()
101}
102
103#[inline(always)]
104pub fn lean_isize_dec_eq(a1: usize, a2: usize) -> usize {
105    (a1 as isize == a2 as isize) as usize
106}
107
108#[inline(always)]
109pub fn lean_isize_dec_lt(a1: usize, a2: usize) -> usize {
110    ((a1 as isize) < a2 as isize) as usize
111}
112
113#[inline(always)]
114pub fn lean_isize_dec_le(a1: usize, a2: usize) -> usize {
115    (a1 as isize <= a2 as isize) as usize
116}
117
118#[inline]
119pub fn lean_isize_to_int8(a: usize) -> u8 {
120    a as isize as i8 as u8
121}
122#[inline]
123pub fn lean_isize_to_int16(a: usize) -> u16 {
124    a as isize as i16 as u16
125}
126#[inline]
127pub fn lean_isize_to_int32(a: usize) -> u32 {
128    a as isize as i32 as u32
129}
130#[inline]
131pub fn lean_isize_to_int64(a: usize) -> u64 {
132    a as isize as i64 as u64
133}
134
135extern "C" {
136    pub fn lean_isize_of_big_int(a: b_lean_obj_arg) -> isize;
137}
lean_sys/primitive/isize_.rs

lean_sys/primitive/
isize_.rs
