lean_rs/handle/
level.rs

1//! Opaque handle for `Lean.Level`.
2//!
3//! [`LeanLevel`] is a receipt for an owned universe-level value produced
4//! on the Lean side. The Rust API is intentionally minimal: it carries
5//! the handle through the FFI boundary and nothing else. Construction
6//! and inspection — `.zero`, `.succ`, `.max`, `toString`, `==` — live in
7//! Lean exports the caller reaches through
8//! [`crate::module::LeanModule::exported`].
9//!
10//! Display text obtained from a Lean export is diagnostic, not a
11//! semantic key; use a Lean-authored equality export when semantics
12//! matter (see the module docs on [`crate::handle`]).
13
14use core::fmt;
15
16use lean_rs_sys::lean_object;
17
18use crate::abi::traits::{LeanAbi, TryFromLean, sealed};
19use crate::error::LeanResult;
20use crate::runtime::LeanRuntime;
21use crate::runtime::obj::Obj;
22
23/// Opaque, lifetime-bound handle to a `Lean.Level`.
24///
25/// `'lean` cascades from the [`crate::LeanRuntime`] borrow that produced
26/// the value, so a handle cannot outlive the runtime. Neither [`Send`]
27/// nor [`Sync`]: inherited from the crate-internal owned-object handle
28/// the type wraps.
29///
30/// [`Clone`] bumps the underlying refcount; [`Drop`] releases it. There
31/// are no public inherent methods: the handle is a pass-through that
32/// reaches Lean-authored operations through
33/// [`crate::module::LeanModule::exported`].
34pub struct LeanLevel<'lean> {
35    obj: Obj<'lean>,
36}
37
38impl Clone for LeanLevel<'_> {
39    fn clone(&self) -> Self {
40        Self { obj: self.obj.clone() }
41    }
42}
43
44impl fmt::Debug for LeanLevel<'_> {
45    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
46        // Opaque on purpose: the Rust side has no claim on Lean's
47        // structural identity. For a diagnostic string, route through a
48        // Lean-authored `Level` pretty-printer export.
49        f.debug_struct("LeanLevel").finish_non_exhaustive()
50    }
51}
52
53impl sealed::SealedAbi for LeanLevel<'_> {}
54
55impl<'lean> LeanAbi<'lean> for LeanLevel<'lean> {
56    type CRepr = *mut lean_object;
57
58    fn into_c(self, _runtime: &'lean LeanRuntime) -> *mut lean_object {
59        self.obj.into_raw()
60    }
61
62    #[allow(
63        clippy::not_unsafe_ptr_arg_deref,
64        reason = "sealed trait — caller invariant documented on LeanAbi::from_c"
65    )]
66    fn from_c(c: *mut lean_object, runtime: &'lean LeanRuntime) -> LeanResult<Self> {
67        // SAFETY: `c` is an owned `lean_object*` produced by a Lean
68        // export returning `Lean.Level`; per Lake's `lean_obj_res`
69        // contract it carries one reference count. `runtime` witnesses
70        // `'lean`.
71        #[allow(unsafe_code)]
72        let obj = unsafe { Obj::from_owned_raw(runtime, c) };
73        Ok(Self { obj })
74    }
75}
76
77impl<'lean> TryFromLean<'lean> for LeanLevel<'lean> {
78    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
79        Ok(Self { obj })
80    }
81}
lean_rs/handle/level.rs

lean_rs/handle/
level.rs
