lean_sys/
closure.rs

1/*! Closures */
2use crate::*;
3
4#[inline(always)]
5pub unsafe fn lean_closure_fun(o: *mut lean_object) -> *mut c_void {
6    *raw_field!(lean_to_closure(o), lean_closure_object, m_fun)
7}
8
9#[inline(always)]
10pub unsafe fn lean_closure_arity(o: *mut lean_object) -> c_uint {
11    *raw_field!(lean_to_closure(o), lean_closure_object, m_arity) as u32
12}
13
14#[inline(always)]
15pub unsafe fn lean_closure_num_fixed(o: *mut lean_object) -> c_uint {
16    *raw_field!(lean_to_closure(o), lean_closure_object, m_num_fixed) as u32
17}
18
19#[inline(always)]
20pub unsafe fn lean_closure_arg_cptr(o: *mut lean_object) -> *mut *mut lean_object {
21    raw_field!(lean_to_closure(o), lean_closure_object, m_objs) as *mut _
22}
23
24#[inline]
25pub unsafe fn lean_alloc_closure(
26    fun: *mut c_void,
27    arity: c_uint,
28    num_fixed: c_uint,
29) -> lean_obj_res {
30    debug_assert!(arity > 0);
31    debug_assert!(num_fixed < arity);
32    let o = lean_alloc_small_object(
33        core::mem::size_of::<lean_closure_object>() as c_uint
34            + core::mem::size_of::<*const ()>() as c_uint * num_fixed,
35    );
36    lean_set_st_header(o, LeanClosure as u32, 0);
37    (raw_field!(o, lean_closure_object, m_fun) as *mut *mut c_void).write(fun);
38    (raw_field!(o, lean_closure_object, m_arity) as *mut u16).write(arity as u16);
39    (raw_field!(o, lean_closure_object, m_num_fixed) as *mut u16).write(num_fixed as u16);
40    o
41}
42
43#[inline(always)]
44pub unsafe fn lean_closure_get(o: b_lean_obj_arg, i: c_uint) -> b_lean_obj_res {
45    debug_assert!(i <= lean_closure_num_fixed(o));
46    *(raw_field!(lean_to_closure(o), lean_closure_object, m_objs) as *mut *mut lean_object)
47        .add(i as usize)
48}
49
50#[inline(always)]
51pub unsafe fn lean_closure_set(o: u_lean_obj_arg, i: c_uint, a: lean_obj_arg) {
52    debug_assert!(i <= lean_closure_num_fixed(o));
53    // Why is the reference count not decremented here?
54    (raw_field!(lean_to_closure(o), lean_closure_object, m_objs) as *mut *mut lean_object)
55        .add(i as usize)
56        .write(a)
57}
58
59extern "C" {
60    pub fn lean_apply_1(f: *mut lean_object, a1: *mut lean_object) -> *mut lean_object;
61    pub fn lean_apply_2(
62        f: *mut lean_object,
63        a1: *mut lean_object,
64        a2: *mut lean_object,
65    ) -> *mut lean_object;
66    pub fn lean_apply_3(
67        f: *mut lean_object,
68        a1: *mut lean_object,
69        a2: *mut lean_object,
70        a3: *mut lean_object,
71    ) -> *mut lean_object;
72    pub fn lean_apply_4(
73        f: *mut lean_object,
74        a1: *mut lean_object,
75        a2: *mut lean_object,
76        a3: *mut lean_object,
77        a4: *mut lean_object,
78    ) -> *mut lean_object;
79    pub fn lean_apply_5(
80        f: *mut lean_object,
81        a1: *mut lean_object,
82        a2: *mut lean_object,
83        a3: *mut lean_object,
84        a4: *mut lean_object,
85        a5: *mut lean_object,
86    ) -> *mut lean_object;
87    pub fn lean_apply_6(
88        f: *mut lean_object,
89        a1: *mut lean_object,
90        a2: *mut lean_object,
91        a3: *mut lean_object,
92        a4: *mut lean_object,
93        a5: *mut lean_object,
94        a6: *mut lean_object,
95    ) -> *mut lean_object;
96    pub fn lean_apply_7(
97        f: *mut lean_object,
98        a1: *mut lean_object,
99        a2: *mut lean_object,
100        a3: *mut lean_object,
101        a4: *mut lean_object,
102        a5: *mut lean_object,
103        a6: *mut lean_object,
104        a7: *mut lean_object,
105    ) -> *mut lean_object;
106    pub fn lean_apply_8(
107        f: *mut lean_object,
108        a1: *mut lean_object,
109        a2: *mut lean_object,
110        a3: *mut lean_object,
111        a4: *mut lean_object,
112        a5: *mut lean_object,
113        a6: *mut lean_object,
114        a7: *mut lean_object,
115        a8: *mut lean_object,
116    ) -> *mut lean_object;
117    pub fn lean_apply_9(
118        f: *mut lean_object,
119        a1: *mut lean_object,
120        a2: *mut lean_object,
121        a3: *mut lean_object,
122        a4: *mut lean_object,
123        a5: *mut lean_object,
124        a6: *mut lean_object,
125        a7: *mut lean_object,
126        a8: *mut lean_object,
127        a9: *mut lean_object,
128    ) -> *mut lean_object;
129    pub fn lean_apply_10(
130        f: *mut lean_object,
131        a1: *mut lean_object,
132        a2: *mut lean_object,
133        a3: *mut lean_object,
134        a4: *mut lean_object,
135        a5: *mut lean_object,
136        a6: *mut lean_object,
137        a7: *mut lean_object,
138        a8: *mut lean_object,
139        a9: *mut lean_object,
140        a10: *mut lean_object,
141    ) -> *mut lean_object;
142    pub fn lean_apply_11(
143        f: *mut lean_object,
144        a1: *mut lean_object,
145        a2: *mut lean_object,
146        a3: *mut lean_object,
147        a4: *mut lean_object,
148        a5: *mut lean_object,
149        a6: *mut lean_object,
150        a7: *mut lean_object,
151        a8: *mut lean_object,
152        a9: *mut lean_object,
153        a10: *mut lean_object,
154        a11: *mut lean_object,
155    ) -> *mut lean_object;
156    pub fn lean_apply_12(
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    ) -> *mut lean_object;
171    pub fn lean_apply_13(
172        f: *mut lean_object,
173        a1: *mut lean_object,
174        a2: *mut lean_object,
175        a3: *mut lean_object,
176        a4: *mut lean_object,
177        a5: *mut lean_object,
178        a6: *mut lean_object,
179        a7: *mut lean_object,
180        a8: *mut lean_object,
181        a9: *mut lean_object,
182        a10: *mut lean_object,
183        a11: *mut lean_object,
184        a12: *mut lean_object,
185        a13: *mut lean_object,
186    ) -> *mut lean_object;
187    pub fn lean_apply_14(
188        f: *mut lean_object,
189        a1: *mut lean_object,
190        a2: *mut lean_object,
191        a3: *mut lean_object,
192        a4: *mut lean_object,
193        a5: *mut lean_object,
194        a6: *mut lean_object,
195        a7: *mut lean_object,
196        a8: *mut lean_object,
197        a9: *mut lean_object,
198        a10: *mut lean_object,
199        a11: *mut lean_object,
200        a12: *mut lean_object,
201        a13: *mut lean_object,
202        a14: *mut lean_object,
203    ) -> *mut lean_object;
204    pub fn lean_apply_15(
205        f: *mut lean_object,
206        a1: *mut lean_object,
207        a2: *mut lean_object,
208        a3: *mut lean_object,
209        a4: *mut lean_object,
210        a5: *mut lean_object,
211        a6: *mut lean_object,
212        a7: *mut lean_object,
213        a8: *mut lean_object,
214        a9: *mut lean_object,
215        a10: *mut lean_object,
216        a11: *mut lean_object,
217        a12: *mut lean_object,
218        a13: *mut lean_object,
219        a14: *mut lean_object,
220        a15: *mut lean_object,
221    ) -> *mut lean_object;
222    pub fn lean_apply_16(
223        f: *mut lean_object,
224        a1: *mut lean_object,
225        a2: *mut lean_object,
226        a3: *mut lean_object,
227        a4: *mut lean_object,
228        a5: *mut lean_object,
229        a6: *mut lean_object,
230        a7: *mut lean_object,
231        a8: *mut lean_object,
232        a9: *mut lean_object,
233        a10: *mut lean_object,
234        a11: *mut lean_object,
235        a12: *mut lean_object,
236        a13: *mut lean_object,
237        a14: *mut lean_object,
238        a15: *mut lean_object,
239        a16: *mut lean_object,
240    ) -> *mut lean_object;
241    pub fn lean_apply_n(f: *mut lean_object, args: *mut *mut lean_object) -> *mut lean_object;
242    /** Pre: n > 16 */
243    pub fn lean_apply_m(f: *mut lean_object, args: *mut *mut lean_object) -> *mut lean_object;
244}
lean_sys/closure.rs

lean_sys/
closure.rs
