lean_sys/
thunk.rs

1/*! Thunks */
2use crate::*;
3
4#[inline]
5pub unsafe fn lean_mk_thunk(c: lean_obj_arg) -> lean_obj_res {
6    let o = lean_alloc_small_object(core::mem::size_of::<lean_thunk_object>() as c_uint);
7    lean_set_st_header(o, LeanThunk as u32, 0);
8    (raw_field!(o, lean_thunk_object, m_value) as *mut *mut lean_object)
9        .write(core::ptr::null_mut());
10    (raw_field!(o, lean_thunk_object, m_closure) as *mut lean_obj_arg).write(c);
11    o
12}
13
14/** Thunk.pure : A -> Thunk A */
15#[inline]
16pub unsafe fn lean_obj_res(v: lean_obj_arg) -> lean_obj_res {
17    let o = lean_alloc_small_object(core::mem::size_of::<lean_thunk_object>() as c_uint);
18    lean_set_st_header(o, LeanThunk as u32, 0);
19    (raw_field!(o, lean_thunk_object, m_value) as *mut lean_obj_arg).write(v);
20    (raw_field!(o, lean_thunk_object, m_closure) as *mut lean_obj_arg).write(core::ptr::null_mut());
21    o
22}
23
24extern "C" {
25    pub fn lean_thunk_get_core(t: *mut lean_object) -> *mut lean_object;
26}
27
28#[inline]
29pub unsafe fn lean_thunk_get(t: b_lean_obj_arg) -> b_lean_obj_res {
30    let r = *raw_field!(lean_to_thunk(t), lean_thunk_object, m_value);
31    if r != 0 {
32        r as *mut lean_object
33    } else {
34        lean_thunk_get_core(t)
35    }
36}
37
38#[inline]
39pub unsafe fn lean_thunk_get_own(t: b_lean_obj_arg) -> lean_obj_res {
40    let r = lean_thunk_get(t);
41    lean_inc(r);
42    r
43}
lean_sys/thunk.rs

lean_sys/
thunk.rs
