lean_sys/primitive/
boxing.rs

1/*! Boxing primitives */
2use crate::*;
3
4#[inline]
5pub unsafe fn lean_box_uint32(v: u32) -> lean_obj_res {
6    if core::mem::size_of::<*const ()>() == 4 {
7        // 32-bit implementation
8        let r = lean_alloc_ctor(0, 0, core::mem::size_of::<u32>() as c_uint);
9        lean_ctor_set_uint32(r, 0, v);
10        r
11    } else {
12        // 64-bit implementation
13        lean_box(v as usize)
14    }
15}
16
17#[inline]
18pub unsafe fn lean_unbox_uint32(o: b_lean_obj_arg) -> u32 {
19    if core::mem::size_of::<*const ()>() == 4 {
20        // 32-bit implementation
21        lean_ctor_get_uint32(o, 0)
22    } else {
23        // 64-bit implementation
24        lean_unbox(o) as u32
25    }
26}
27
28#[inline]
29pub unsafe fn lean_box_uint64(v: u64) -> lean_obj_res {
30    let r = lean_alloc_ctor(0, 0, core::mem::size_of::<u64>() as c_uint);
31    lean_ctor_set_uint64(r, 0, v);
32    r
33}
34
35#[inline(always)]
36pub unsafe fn lean_unbox_uint64(o: b_lean_obj_arg) -> u64 {
37    lean_ctor_get_uint64(o, 0)
38}
39
40#[inline]
41pub unsafe fn lean_box_usize(v: usize) -> lean_obj_res {
42    let r = lean_alloc_ctor(0, 0, core::mem::size_of::<usize>() as c_uint);
43    lean_ctor_set_usize(r, 0, v);
44    r
45}
46
47#[inline(always)]
48pub unsafe fn lean_unbox_usize(o: b_lean_obj_arg) -> usize {
49    lean_ctor_get_usize(o, 0)
50}
51
52#[inline]
53pub unsafe fn lean_box_float(v: f64) -> lean_obj_res {
54    let r = lean_alloc_ctor(0, 0, core::mem::size_of::<f64>() as c_uint);
55    lean_ctor_set_float(r, 0, v);
56    r
57}
58
59#[inline(always)]
60pub unsafe fn lean_unbox_float(o: b_lean_obj_arg) -> f64 {
61    lean_ctor_get_float(o, 0)
62}
63
64#[inline]
65pub unsafe fn lean_box_float32(v: f32) -> lean_obj_res {
66    let r = lean_alloc_ctor(0, 0, core::mem::size_of::<f32>() as c_uint);
67    lean_ctor_set_float32(r, 0, v);
68    r
69}
70
71#[inline(always)]
72pub unsafe fn lean_unbox_float32(o: b_lean_obj_arg) -> f32 {
73    lean_ctor_get_float32(o, 0)
74}
lean_sys/primitive/boxing.rs

lean_sys/primitive/
boxing.rs
