lean_sys/primitive/
uint8.rs

1use crate::*;
2
3#[inline]
4pub unsafe fn lean_uint8_of_nat(a: b_lean_obj_arg) -> u8 {
5    if lean_is_scalar(a) {
6        lean_unbox(a) as u8
7    } else {
8        lean_uint8_of_big_nat(a)
9    }
10}
11
12#[inline]
13pub unsafe fn lean_uint8_of_nat_mk(a: lean_obj_arg) -> u8 {
14    let r = lean_uint8_of_nat(a);
15    lean_dec(a);
16    r
17}
18
19#[inline(always)]
20pub unsafe fn lean_uint8_to_nat(a: u8) -> lean_obj_res {
21    //TODO: why not just `lean_box`?
22    lean_usize_to_nat(a as usize)
23}
24
25#[inline(always)]
26pub fn lean_uint8_add(a1: u8, a2: u8) -> u8 {
27    a1.wrapping_add(a2)
28}
29
30#[inline(always)]
31pub fn lean_uint8_sub(a1: u8, a2: u8) -> u8 {
32    a1.wrapping_sub(a2)
33}
34
35#[inline(always)]
36pub fn lean_uint8_mul(a1: u8, a2: u8) -> u8 {
37    a1.wrapping_mul(a2)
38}
39
40#[inline(always)]
41pub fn lean_uint8_div(a1: u8, a2: u8) -> u8 {
42    if a2 == 0 {
43        0
44    } else {
45        a1 / a2
46    }
47}
48
49#[inline(always)]
50pub fn lean_uint8_mod(a1: u8, a2: u8) -> u8 {
51    if a2 == 0 {
52        a1
53    } else {
54        a1 % a2
55    }
56}
57
58#[inline(always)]
59pub fn lean_uint8_land(a1: u8, a2: u8) -> u8 {
60    a1 & a2
61}
62
63#[inline(always)]
64pub fn lean_uint8_lor(a1: u8, a2: u8) -> u8 {
65    a1 | a2
66}
67
68#[inline(always)]
69pub fn lean_uint8_xor(a1: u8, a2: u8) -> u8 {
70    a1 ^ a2
71}
72
73#[inline(always)]
74pub fn lean_uint8_shift_left(a1: u8, a2: u8) -> u8 {
75    a1.wrapping_shl(a2 as u32)
76}
77
78#[inline(always)]
79pub fn lean_uint8_shift_right(a1: u8, a2: u8) -> u8 {
80    a1.wrapping_shr(a2 as u32)
81}
82
83#[inline(always)]
84pub fn lean_uint8_complement(a: u8) -> u8 {
85    !a
86}
87
88#[inline(always)]
89pub fn lean_uint8_neg(a: u8) -> u8 {
90    0 - a
91}
92
93#[inline(always)]
94pub fn lean_uint8_dec_eq(a1: u8, a2: u8) -> u8 {
95    (a1 == a2) as u8
96}
97
98#[inline(always)]
99pub fn lean_uint8_dec_lt(a1: u8, a2: u8) -> u8 {
100    (a1 < a2) as u8
101}
102
103#[inline(always)]
104pub fn lean_uint8_dec_le(a1: u8, a2: u8) -> u8 {
105    (a1 <= a2) as u8
106}
107
108#[inline]
109pub fn lean_uint8_to_uint16(a: u8) -> u16 {
110    a as u16
111}
112#[inline]
113pub fn lean_uint8_to_uint32(a: u8) -> u32 {
114    a as u32
115}
116#[inline]
117pub fn lean_uint8_to_uint64(a: u8) -> u64 {
118    a as u64
119}
120#[inline]
121pub fn lean_uint8_to_usize(a: u8) -> usize {
122    a as usize
123}
124
125extern "C" {
126    pub fn lean_uint8_of_big_nat(a: b_lean_obj_arg) -> u8;
127}
lean_sys/primitive/uint8.rs

lean_sys/primitive/
uint8.rs
