1use crate::*;
3
4#[inline]
5pub unsafe fn lean_alloc_external(
6 cls: *mut lean_external_class,
7 data: *mut c_void,
8) -> *mut lean_object {
9 let o = lean_alloc_small_object(core::mem::size_of::<lean_external_object>() as c_uint);
10 lean_set_st_header(o, LeanExternal as u32, 0);
11 (raw_field!(o, lean_external_object, m_class) as *mut *mut lean_external_class).write(cls);
12 (raw_field!(o, lean_external_object, m_data) as *mut *mut c_void).write(data);
13 o
14}
15
16#[inline(always)]
17pub unsafe fn lean_get_external_class(o: *mut lean_object) -> *mut lean_external_class {
18 *raw_field!(lean_to_external(o), lean_external_object, m_class)
19}
20
21#[inline(always)]
22pub unsafe fn lean_get_external_data(o: *mut lean_object) -> *mut c_void {
23 *raw_field!(lean_to_external(o), lean_external_object, m_data)
24}
25
26#[inline(always)]
27pub unsafe fn lean_set_external_data(o: *mut lean_object, data: *mut c_void) -> *mut lean_object {
28 if lean_is_exclusive(o) {
29 (raw_field!(lean_to_external(o), lean_external_object, m_data) as *mut *mut c_void)
30 .write(data);
31 o
32 } else {
33 let o_new = lean_alloc_external(lean_get_external_class(o), data);
34 lean_dec_ref(o);
35 o_new
36 }
37}
38
39extern "C" {
40 pub fn lean_register_external_class(
41 _: lean_external_finalize_proc,
42 _: lean_external_foreach_proc,
43 ) -> *mut lean_external_class;
44}