lean_sys/primitive/
int8.rs

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

lean_sys/primitive/
int8.rs
