lean_sys/
constructor.rs

1/*! Constructor objects */
2use crate::*;
3
4#[inline(always)]
5pub unsafe fn lean_ctor_num_objs(o: *mut lean_object) -> c_uint {
6    debug_assert!(lean_is_ctor(o));
7    lean_ptr_other(o)
8}
9
10#[inline(always)]
11pub unsafe fn lean_ctor_obj_cptr(o: *mut lean_object) -> *mut *mut lean_object {
12    debug_assert!(lean_is_ctor(o));
13    raw_field!(lean_to_ctor(o), lean_ctor_object, m_objs) as *mut _
14}
15
16#[inline]
17pub unsafe fn lean_ctor_scalar_cptr(o: *mut lean_object) -> *mut u8 {
18    debug_assert!(lean_is_ctor(o));
19    lean_ctor_obj_cptr(o).add(lean_ctor_num_objs(o) as usize) as *mut u8
20}
21
22#[inline]
23pub unsafe fn lean_alloc_ctor(
24    tag: c_uint,
25    num_objs: c_uint,
26    scalar_sz: c_uint,
27) -> *mut lean_object {
28    debug_assert!(
29        tag <= LeanMaxCtorTag as c_uint
30            && num_objs < LEAN_MAX_CTOR_FIELDS
31            && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE
32    );
33    let o = lean_alloc_ctor_memory(
34        core::mem::size_of::<lean_ctor_object>() as c_uint
35            + (core::mem::size_of::<*const ()>() as c_uint) * num_objs
36            + scalar_sz,
37    );
38    lean_set_st_header(o, tag, num_objs);
39    o
40}
41
42#[inline(always)]
43pub unsafe fn lean_ctor_get(o: b_lean_obj_arg, i: c_uint) -> b_lean_obj_res {
44    debug_assert!(i < lean_ctor_num_objs(o));
45    *lean_ctor_obj_cptr(o).add(i as usize)
46}
47
48#[inline(always)]
49pub unsafe fn lean_ctor_set(o: b_lean_obj_arg, i: c_uint, v: lean_obj_arg) {
50    debug_assert!(i < lean_ctor_num_objs(o));
51    *lean_ctor_obj_cptr(o).add(i as usize) = v;
52}
53
54#[inline(always)]
55pub unsafe fn lean_ctor_set_tag(o: b_lean_obj_arg, new_tag: u8) {
56    debug_assert!(new_tag <= LeanMaxCtorTag);
57    (raw_field!(o, lean_object, m_tag) as *mut u8).write(new_tag)
58}
59
60#[inline]
61pub unsafe fn lean_ctor_release(o: b_lean_obj_arg, i: c_uint) {
62    debug_assert!(i < lean_ctor_num_objs(o));
63    let objs = lean_ctor_obj_cptr(o);
64    lean_dec(*objs.add(1));
65    *objs.add(i as usize) = lean_box(0)
66}
67
68#[inline(always)]
69pub unsafe fn lean_ctor_get_usize(o: b_lean_obj_arg, i: c_uint) -> usize {
70    debug_assert!(i >= lean_ctor_num_objs(o));
71    *(lean_ctor_obj_cptr(o).add(i as usize) as *const usize)
72}
73
74#[inline(always)]
75pub unsafe fn lean_ctor_get_uint8(o: b_lean_obj_arg, offset: c_uint) -> u8 {
76    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
77    *(lean_ctor_obj_cptr(o) as *const u8).add(offset as usize)
78}
79
80#[inline(always)]
81pub unsafe fn lean_ctor_get_uint16(o: b_lean_obj_arg, offset: c_uint) -> u16 {
82    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
83    ((lean_ctor_obj_cptr(o) as *const u8).add(offset as usize) as *const u16).read()
84}
85
86#[inline(always)]
87pub unsafe fn lean_ctor_get_uint32(o: b_lean_obj_arg, offset: c_uint) -> u32 {
88    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
89    ((lean_ctor_obj_cptr(o) as *const u8).add(offset as usize) as *const u32).read()
90}
91
92#[inline(always)]
93pub unsafe fn lean_ctor_get_uint64(o: b_lean_obj_arg, offset: c_uint) -> u64 {
94    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
95    ((lean_ctor_obj_cptr(o) as *const u8).add(offset as usize) as *const u64).read()
96}
97
98#[inline(always)]
99pub unsafe fn lean_ctor_get_float(o: b_lean_obj_arg, offset: c_uint) -> f64 {
100    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
101    ((lean_ctor_obj_cptr(o) as *const u8).add(offset as usize) as *const f64).read()
102}
103
104#[inline(always)]
105pub unsafe fn lean_ctor_get_float32(o: b_lean_obj_arg, offset: c_uint) -> f32 {
106    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
107    ((lean_ctor_obj_cptr(o) as *const u8).add(offset as usize) as *const f32).read()
108}
109
110#[inline(always)]
111pub unsafe fn lean_ctor_set_usize(o: b_lean_obj_arg, i: c_uint, v: usize) {
112    debug_assert!(i >= lean_ctor_num_objs(o));
113    (lean_ctor_obj_cptr(o).add(i as usize) as *mut usize).write(v)
114}
115
116#[inline(always)]
117pub unsafe fn lean_ctor_set_uint8(o: b_lean_obj_arg, offset: c_uint, v: u8) {
118    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
119    (lean_ctor_obj_cptr(o) as *mut u8)
120        .add(offset as usize)
121        .write(v)
122}
123
124#[inline(always)]
125pub unsafe fn lean_ctor_set_uint16(o: b_lean_obj_arg, offset: c_uint, v: u16) {
126    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
127    ((lean_ctor_obj_cptr(o) as *mut u8).add(offset as usize) as *mut u16).write(v)
128}
129
130#[inline(always)]
131pub unsafe fn lean_ctor_set_uint32(o: b_lean_obj_arg, offset: c_uint, v: u32) {
132    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
133    ((lean_ctor_obj_cptr(o) as *mut u8).add(offset as usize) as *mut u32).write(v)
134}
135
136#[inline(always)]
137pub unsafe fn lean_ctor_set_uint64(o: b_lean_obj_arg, offset: c_uint, v: u64) {
138    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
139    ((lean_ctor_obj_cptr(o) as *mut u8).add(offset as usize) as *mut u64).write(v)
140}
141
142#[inline(always)]
143pub unsafe fn lean_ctor_set_float(o: b_lean_obj_arg, offset: c_uint, v: f64) {
144    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
145    ((lean_ctor_obj_cptr(o) as *mut u8).add(offset as usize) as *mut f64).write(v)
146}
147
148#[inline(always)]
149pub unsafe fn lean_ctor_set_float32(o: b_lean_obj_arg, offset: c_uint, v: f32) {
150    debug_assert!(offset >= lean_ctor_num_objs(o) * core::mem::size_of::<*const ()>() as c_uint);
151    ((lean_ctor_obj_cptr(o) as *mut u8).add(offset as usize) as *mut f32).write(v)
152}
lean_sys/constructor.rs

lean_sys/
constructor.rs
