lean_rs_sys/
external.rs

1//! External objects — externs and inline accessors from `lean.h:295–1332`.
2
3#![allow(clippy::inline_always)]
4
5use core::ffi::c_void;
6
7use crate::consts::LEAN_EXTERNAL;
8use crate::repr::LeanExternalObjectRepr;
9use crate::types::{lean_obj_res, lean_object};
10
11/// Finalizer signature stored in a `lean_external_class` (`lean.h:295`).
12pub type lean_external_finalize_proc = unsafe extern "C" fn(*mut c_void);
13
14/// Foreach signature stored in a `lean_external_class` (`lean.h:296`).
15pub type lean_external_foreach_proc = unsafe extern "C" fn(*mut c_void, *mut lean_object);
16
17unsafe extern "C" {
18    /// Register an external-object class. The returned pointer outlives the
19    /// process; the runtime does not free registered classes
20    /// (`lean.h:303`).
21    pub fn lean_register_external_class(
22        finalize: lean_external_finalize_proc,
23        foreach: lean_external_foreach_proc,
24    ) -> *mut c_void;
25}
26
27/// Allocate an external-data wrapper (`lean.h:1307–1313`).
28///
29/// # Safety
30///
31/// `cls` must come from [`lean_register_external_class`] and remain valid
32/// for the lifetime of the returned object; `data` will be passed verbatim
33/// to the class's finalize and foreach callbacks.
34#[inline(always)]
35pub unsafe fn lean_alloc_external(cls: *mut c_void, data: *mut c_void) -> lean_obj_res {
36    // SAFETY: `lean_alloc_object` returns a fresh small-object allocation
37    // sized for `LeanExternalObjectRepr`; we initialize the header, class,
38    // and data fields before returning.
39    unsafe {
40        let raw = crate::object::lean_alloc_object(core::mem::size_of::<LeanExternalObjectRepr>());
41        let repr = raw.cast::<LeanExternalObjectRepr>();
42        (*repr).header.m_rc = 1;
43        (*repr).header.m_tag = LEAN_EXTERNAL;
44        (*repr).header.m_other = 0;
45        (*repr).header.m_cs_sz = 0;
46        (*repr).class = cls;
47        (*repr).data = data;
48        raw
49    }
50}
51
52/// Read the external object's class pointer (`lean.h:1315–1317`).
53///
54/// # Safety
55///
56/// `o` must be a borrowed Lean external object.
57#[inline(always)]
58pub unsafe fn lean_get_external_class(o: *mut lean_object) -> *mut c_void {
59    // SAFETY: precondition above.
60    unsafe { (*o.cast::<LeanExternalObjectRepr>()).class }
61}
62
63/// Read the external object's data pointer (`lean.h:1319–1321`).
64///
65/// # Safety
66///
67/// Same as [`lean_get_external_class`]. The interpretation of the pointer
68/// is up to the class's finalize / foreach implementation.
69#[inline(always)]
70pub unsafe fn lean_get_external_data(o: *mut lean_object) -> *mut c_void {
71    // SAFETY: precondition above.
72    unsafe { (*o.cast::<LeanExternalObjectRepr>()).data }
73}
lean_rs_sys/external.rs

lean_rs_sys/
external.rs
