lean_rs_sys/
types.rs

1//! Opaque [`lean_object`] plus the calling-convention typedefs from
2//! `lean.h:131–168`.
3
4use core::marker::{PhantomData, PhantomPinned};
5
6/// Opaque handle to a Lean 4 heap object.
7///
8/// `lean_object` is **only ever held by pointer**. The published type is
9/// zero-sized + `!Send + !Sync + !Unpin`, so downstream code cannot read or
10/// write the underlying header (`m_rc`, `m_tag`, …) directly. Reach object
11/// state through this crate's `pub unsafe fn` helpers.
12///
13/// The C struct in `lean.h:131–136` is `{ int m_rc; unsigned m_cs_sz:16;
14/// unsigned m_other:8; unsigned m_tag:8; }` for 8 total bytes. A crate-
15/// private `LeanObjectRepr` mirrors that layout; the digest pinned at
16/// build time guarantees the C and Rust pictures match.
17#[repr(C)]
18pub struct lean_object {
19    _data: [u8; 0],
20    _marker: PhantomData<(*mut u8, PhantomPinned)>,
21}
22
23/// "Standard" object argument — caller transfers ownership of one refcount.
24pub type lean_obj_arg = *mut lean_object;
25
26/// "Borrowed" object argument — caller retains the refcount.
27pub type b_lean_obj_arg = *mut lean_object;
28
29/// "Unique" object argument — caller asserts the object is non-shared.
30pub type u_lean_obj_arg = *mut lean_object;
31
32/// "Standard" object result — callee returns a fresh owned refcount.
33pub type lean_obj_res = *mut lean_object;
34
35/// "Borrowed" object result — refcount belongs to a longer-lived owner.
36pub type b_lean_obj_res = *mut lean_object;
lean_rs_sys/types.rs

lean_rs_sys/
types.rs
