lean_rs/handle/
name.rs

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

lean_rs/handle/
name.rs
