lean_rs_sys/
closure.rs

1//! Closure objects — externs and inline accessors from `lean.h:762–813`.
2
3#![allow(clippy::inline_always)]
4// `arity` and `num_fixed` are stored as `u16` in the Lean closure object,
5// but the public allocator takes them as `u32` to match Lean's compiler ABI.
6// The narrowing is bounded by `LEAN_CLOSURE_MAX_ARGS == 16`, asserted via
7// `debug_assert!` below.
8#![allow(clippy::cast_possible_truncation)]
9
10use core::ffi::c_void;
11
12use crate::repr::LeanClosureObjectRepr;
13use crate::types::{b_lean_obj_arg, lean_obj_arg, lean_obj_res, lean_object, u_lean_obj_arg};
14
15unsafe extern "C" {
16    pub fn lean_apply_1(f: *mut lean_object, a1: *mut lean_object) -> *mut lean_object;
17    pub fn lean_apply_2(f: *mut lean_object, a1: *mut lean_object, a2: *mut lean_object) -> *mut lean_object;
18    pub fn lean_apply_3(
19        f: *mut lean_object,
20        a1: *mut lean_object,
21        a2: *mut lean_object,
22        a3: *mut lean_object,
23    ) -> *mut lean_object;
24    pub fn lean_apply_4(
25        f: *mut lean_object,
26        a1: *mut lean_object,
27        a2: *mut lean_object,
28        a3: *mut lean_object,
29        a4: *mut lean_object,
30    ) -> *mut lean_object;
31    pub fn lean_apply_5(
32        f: *mut lean_object,
33        a1: *mut lean_object,
34        a2: *mut lean_object,
35        a3: *mut lean_object,
36        a4: *mut lean_object,
37        a5: *mut lean_object,
38    ) -> *mut lean_object;
39    pub fn lean_apply_6(
40        f: *mut lean_object,
41        a1: *mut lean_object,
42        a2: *mut lean_object,
43        a3: *mut lean_object,
44        a4: *mut lean_object,
45        a5: *mut lean_object,
46        a6: *mut lean_object,
47    ) -> *mut lean_object;
48    pub fn lean_apply_7(
49        f: *mut lean_object,
50        a1: *mut lean_object,
51        a2: *mut lean_object,
52        a3: *mut lean_object,
53        a4: *mut lean_object,
54        a5: *mut lean_object,
55        a6: *mut lean_object,
56        a7: *mut lean_object,
57    ) -> *mut lean_object;
58    pub fn lean_apply_8(
59        f: *mut lean_object,
60        a1: *mut lean_object,
61        a2: *mut lean_object,
62        a3: *mut lean_object,
63        a4: *mut lean_object,
64        a5: *mut lean_object,
65        a6: *mut lean_object,
66        a7: *mut lean_object,
67        a8: *mut lean_object,
68    ) -> *mut lean_object;
69    pub fn lean_apply_9(
70        f: *mut lean_object,
71        a1: *mut lean_object,
72        a2: *mut lean_object,
73        a3: *mut lean_object,
74        a4: *mut lean_object,
75        a5: *mut lean_object,
76        a6: *mut lean_object,
77        a7: *mut lean_object,
78        a8: *mut lean_object,
79        a9: *mut lean_object,
80    ) -> *mut lean_object;
81    pub fn lean_apply_10(
82        f: *mut lean_object,
83        a1: *mut lean_object,
84        a2: *mut lean_object,
85        a3: *mut lean_object,
86        a4: *mut lean_object,
87        a5: *mut lean_object,
88        a6: *mut lean_object,
89        a7: *mut lean_object,
90        a8: *mut lean_object,
91        a9: *mut lean_object,
92        a10: *mut lean_object,
93    ) -> *mut lean_object;
94    pub fn lean_apply_11(
95        f: *mut lean_object,
96        a1: *mut lean_object,
97        a2: *mut lean_object,
98        a3: *mut lean_object,
99        a4: *mut lean_object,
100        a5: *mut lean_object,
101        a6: *mut lean_object,
102        a7: *mut lean_object,
103        a8: *mut lean_object,
104        a9: *mut lean_object,
105        a10: *mut lean_object,
106        a11: *mut lean_object,
107    ) -> *mut lean_object;
108    pub fn lean_apply_12(
109        f: *mut lean_object,
110        a1: *mut lean_object,
111        a2: *mut lean_object,
112        a3: *mut lean_object,
113        a4: *mut lean_object,
114        a5: *mut lean_object,
115        a6: *mut lean_object,
116        a7: *mut lean_object,
117        a8: *mut lean_object,
118        a9: *mut lean_object,
119        a10: *mut lean_object,
120        a11: *mut lean_object,
121        a12: *mut lean_object,
122    ) -> *mut lean_object;
123    pub fn lean_apply_13(
124        f: *mut lean_object,
125        a1: *mut lean_object,
126        a2: *mut lean_object,
127        a3: *mut lean_object,
128        a4: *mut lean_object,
129        a5: *mut lean_object,
130        a6: *mut lean_object,
131        a7: *mut lean_object,
132        a8: *mut lean_object,
133        a9: *mut lean_object,
134        a10: *mut lean_object,
135        a11: *mut lean_object,
136        a12: *mut lean_object,
137        a13: *mut lean_object,
138    ) -> *mut lean_object;
139    pub fn lean_apply_14(
140        f: *mut lean_object,
141        a1: *mut lean_object,
142        a2: *mut lean_object,
143        a3: *mut lean_object,
144        a4: *mut lean_object,
145        a5: *mut lean_object,
146        a6: *mut lean_object,
147        a7: *mut lean_object,
148        a8: *mut lean_object,
149        a9: *mut lean_object,
150        a10: *mut lean_object,
151        a11: *mut lean_object,
152        a12: *mut lean_object,
153        a13: *mut lean_object,
154        a14: *mut lean_object,
155    ) -> *mut lean_object;
156    pub fn lean_apply_15(
157        f: *mut lean_object,
158        a1: *mut lean_object,
159        a2: *mut lean_object,
160        a3: *mut lean_object,
161        a4: *mut lean_object,
162        a5: *mut lean_object,
163        a6: *mut lean_object,
164        a7: *mut lean_object,
165        a8: *mut lean_object,
166        a9: *mut lean_object,
167        a10: *mut lean_object,
168        a11: *mut lean_object,
169        a12: *mut lean_object,
170        a13: *mut lean_object,
171        a14: *mut lean_object,
172        a15: *mut lean_object,
173    ) -> *mut lean_object;
174    pub fn lean_apply_16(
175        f: *mut lean_object,
176        a1: *mut lean_object,
177        a2: *mut lean_object,
178        a3: *mut lean_object,
179        a4: *mut lean_object,
180        a5: *mut lean_object,
181        a6: *mut lean_object,
182        a7: *mut lean_object,
183        a8: *mut lean_object,
184        a9: *mut lean_object,
185        a10: *mut lean_object,
186        a11: *mut lean_object,
187        a12: *mut lean_object,
188        a13: *mut lean_object,
189        a14: *mut lean_object,
190        a15: *mut lean_object,
191        a16: *mut lean_object,
192    ) -> *mut lean_object;
193
194    /// Apply a closure to `n` arguments, where `n <= 16`.
195    pub fn lean_apply_n(f: *mut lean_object, n: u32, args: *mut *mut lean_object) -> *mut lean_object;
196    /// Apply a closure to `n` arguments, where `n > 16`.
197    pub fn lean_apply_m(f: *mut lean_object, n: u32, args: *mut *mut lean_object) -> *mut lean_object;
198}
199
200#[inline(always)]
201unsafe fn as_closure<'a>(o: *mut lean_object) -> &'a LeanClosureObjectRepr {
202    // SAFETY: caller asserts `o` is a Lean closure object.
203    unsafe { &*o.cast::<LeanClosureObjectRepr>() }
204}
205
206/// Code pointer of the closure (`lean.h:764`).
207///
208/// # Safety
209///
210/// `o` must be a borrowed Lean closure object.
211#[inline(always)]
212pub unsafe fn lean_closure_fun(o: *mut lean_object) -> *mut c_void {
213    // SAFETY: precondition above.
214    unsafe { as_closure(o).fun }
215}
216
217/// Arity of the closure's underlying function (`lean.h:765`).
218///
219/// # Safety
220///
221/// Same as [`lean_closure_fun`].
222#[inline(always)]
223pub unsafe fn lean_closure_arity(o: *mut lean_object) -> u16 {
224    // SAFETY: precondition above.
225    unsafe { as_closure(o).arity }
226}
227
228/// Number of arguments already captured in the closure (`lean.h:766`).
229///
230/// # Safety
231///
232/// Same as [`lean_closure_fun`].
233#[inline(always)]
234pub unsafe fn lean_closure_num_fixed(o: *mut lean_object) -> u16 {
235    // SAFETY: precondition above.
236    unsafe { as_closure(o).num_fixed }
237}
238
239/// Pointer to the closure's captured-argument array (`lean.h:767`).
240///
241/// # Safety
242///
243/// Same as [`lean_closure_fun`]; valid for `lean_closure_num_fixed(o)`
244/// elements.
245#[inline(always)]
246pub unsafe fn lean_closure_arg_cptr(o: *mut lean_object) -> *mut *mut lean_object {
247    // SAFETY: precondition above; flexible-array member offset is fixed.
248    unsafe { (&raw mut (*o.cast::<LeanClosureObjectRepr>()).objs).cast::<*mut lean_object>() }
249}
250
251/// Read the i-th captured argument (`lean.h:778`).
252///
253/// # Safety
254///
255/// `o` must be a borrowed Lean closure object and `i < num_fixed(o)`.
256#[inline(always)]
257pub unsafe fn lean_closure_get(o: b_lean_obj_arg, i: u32) -> *mut lean_object {
258    // SAFETY: precondition above.
259    unsafe { *lean_closure_arg_cptr(o).add(i as usize) }
260}
261
262/// Write the i-th captured argument (`lean.h:782`).
263///
264/// # Safety
265///
266/// `o` must be a unique Lean closure object, `i < num_fixed(o)`, and the
267/// caller transfers ownership of `a`.
268#[inline(always)]
269pub unsafe fn lean_closure_set(o: u_lean_obj_arg, i: u32, a: lean_obj_arg) {
270    // SAFETY: precondition above.
271    unsafe { *lean_closure_arg_cptr(o).add(i as usize) = a }
272}
273
274/// Allocate a closure of the requested arity with no captured arguments
275/// pre-bound (`lean.h:768–777`).
276///
277/// # Safety
278///
279/// `arity > 0`, `num_fixed < arity`. The returned object has tag
280/// `LeanClosure`, refcount 1, and uninitialized captured-arg storage; the
281/// caller must `lean_closure_set` every captured slot before invoking the
282/// closure.
283///
284/// # Panics
285///
286/// Panics if the closure's total allocation size overflows `usize`. This is
287/// impossible under Lean's `LEAN_CLOSURE_MAX_ARGS == 16` cap; the panic
288/// surfaces a runtime invariant breach rather than a recoverable condition.
289#[inline(always)]
290pub unsafe fn lean_alloc_closure(fun: *mut c_void, arity: u32, num_fixed: u32) -> lean_obj_res {
291    debug_assert!(arity > 0);
292    debug_assert!(num_fixed < arity);
293    // The product is bounded by `LEAN_CLOSURE_MAX_ARGS == 16`; a `usize`
294    // overflow is impossible on any supported target. `strict_*` panics on
295    // overflow so we surface a runtime invariant breach instead of silently
296    // mis-sizing the allocation.
297    let captured_bytes = core::mem::size_of::<*mut lean_object>().strict_mul(num_fixed as usize);
298    let size = core::mem::size_of::<LeanClosureObjectRepr>().strict_add(captured_bytes);
299    // SAFETY: `lean_alloc_object` is the runtime's small-object allocator;
300    // we initialize the header + fun + arity + num_fixed before returning.
301    unsafe {
302        let raw = crate::object::lean_alloc_object(size);
303        let repr = raw.cast::<LeanClosureObjectRepr>();
304        (*repr).header.m_rc = 1;
305        (*repr).header.m_tag = crate::consts::LEAN_CLOSURE;
306        (*repr).header.m_other = 0;
307        (*repr).header.m_cs_sz = 0;
308        (*repr).fun = fun;
309        (*repr).arity = arity as u16;
310        (*repr).num_fixed = num_fixed as u16;
311        raw
312    }
313}
lean_rs_sys/closure.rs

lean_rs_sys/
closure.rs
