lean_rs_sys/
io.rs

1//! `IO`-result helpers — mirrors `lean.h:2893–2907`.
2//!
3//! `IO α` results from compiled Lean are encoded as constructors with tag 0
4//! (`ok`) or tag 1 (`error`). The single object payload sits in constructor
5//! slot 0; reading it requires the `ctor` accessors implemented against
6//! `LeanCtorObjectRepr`.
7
8#![allow(clippy::inline_always)]
9
10use crate::repr::LeanCtorObjectRepr;
11use crate::types::{b_lean_obj_arg, b_lean_obj_res, lean_obj_arg, lean_obj_res, lean_object};
12
13unsafe extern "C" {
14    /// Signal that runtime initialization is complete; subsequent allocations
15    /// should not flag objects as persistent (`lean.h:2907`).
16    pub fn lean_io_mark_end_initialization();
17}
18
19#[inline(always)]
20unsafe fn ctor_get0(r: b_lean_obj_arg) -> *mut lean_object {
21    // SAFETY: caller asserts `r` is an IO-result constructor whose first
22    // object slot holds the payload.
23    unsafe {
24        let ctor = r.cast::<LeanCtorObjectRepr>();
25        *(*ctor).objs.as_ptr()
26    }
27}
28
29/// True if `r` is an `IO.ok` result (`lean.h:2893`).
30///
31/// # Safety
32///
33/// `r` must be a borrowed Lean `IO α` result.
34#[inline(always)]
35pub unsafe fn lean_io_result_is_ok(r: b_lean_obj_arg) -> bool {
36    // SAFETY: precondition above; tag read is layout-pinned.
37    unsafe { crate::object::lean_ptr_tag(r) == 0 }
38}
39
40/// True if `r` is an `IO.error` result (`lean.h:2894`).
41///
42/// # Safety
43///
44/// Same as [`lean_io_result_is_ok`].
45#[inline(always)]
46pub unsafe fn lean_io_result_is_error(r: b_lean_obj_arg) -> bool {
47    // SAFETY: precondition above.
48    unsafe { crate::object::lean_ptr_tag(r) == 1 }
49}
50
51/// Borrow the value out of an `IO.ok` result (`lean.h:2895`).
52///
53/// # Safety
54///
55/// `r` must be a borrowed Lean `IO α` result tagged `ok`. The returned
56/// pointer aliases storage owned by `r`; the caller must not free `r` while
57/// the borrow is live.
58#[inline(always)]
59pub unsafe fn lean_io_result_get_value(r: b_lean_obj_arg) -> b_lean_obj_res {
60    // SAFETY: precondition above.
61    unsafe { ctor_get0(r) }
62}
63
64/// Borrow the error out of an `IO.error` result (`lean.h:2896`).
65///
66/// # Safety
67///
68/// `r` must be a borrowed Lean `IO α` result tagged `error`.
69#[inline(always)]
70pub unsafe fn lean_io_result_get_error(r: b_lean_obj_arg) -> b_lean_obj_res {
71    // SAFETY: precondition above.
72    unsafe { ctor_get0(r) }
73}
74
75/// Take ownership of the value out of an `IO.ok` result (`lean.h:2898–2903`).
76///
77/// # Safety
78///
79/// `r` must be a Lean `IO α` result tagged `ok` and owned by the caller.
80/// This function bumps the value's refcount and decrements `r`'s; after the
81/// call `r` is no longer valid.
82#[inline(always)]
83pub unsafe fn lean_io_result_take_value(r: lean_obj_arg) -> lean_obj_res {
84    // SAFETY: precondition above; calls into refcount helpers with the same
85    // invariants.
86    unsafe {
87        let v = ctor_get0(r);
88        crate::refcount::lean_inc(v);
89        crate::refcount::lean_dec(r);
90        v
91    }
92}
lean_rs_sys/io.rs

lean_rs_sys/
io.rs
