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//!
15//! To render a handle as a Rust [`String`], call
16//! `LeanSession::name_to_string` (or `name_to_string_bulk` for a slice).
17//! There is intentionally no `Display`, `Eq`, or `From<String>` impl on
18//! the handle itself: forcing callers through an explicit method keeps
19//! the FFI cost and the "diagnostic only" semantics visible at the call
20//! site.
21
22use core::fmt;
23
24use lean_rs_sys::lean_object;
25
26use crate::abi::traits::{IntoLean, LeanAbi, TryFromLean, sealed};
27use crate::error::LeanResult;
28use crate::runtime::LeanRuntime;
29use crate::runtime::obj::Obj;
30
31/// Opaque, lifetime-bound handle to a `Lean.Name`.
32///
33/// `'lean` cascades from the [`crate::LeanRuntime`] borrow that produced
34/// the value, so a handle cannot outlive the runtime. Neither [`Send`]
35/// nor [`Sync`]: inherited from the crate-internal owned-object handle
36/// the type wraps.
37///
38/// [`Clone`] bumps the underlying refcount; [`Drop`] releases it. There
39/// are no public inherent methods: the handle is a pass-through that
40/// reaches Lean-authored operations through
41/// [`crate::module::LeanModule::exported`].
42pub struct LeanName<'lean> {
43    obj: Obj<'lean>,
44}
45
46impl Clone for LeanName<'_> {
47    fn clone(&self) -> Self {
48        Self { obj: self.obj.clone() }
49    }
50}
51
52impl fmt::Debug for LeanName<'_> {
53    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
54        // Opaque on purpose: the Rust side has no claim on Lean's
55        // structural identity. For a diagnostic string, route through a
56        // Lean-authored `Name.toString` export.
57        f.debug_struct("LeanName").finish_non_exhaustive()
58    }
59}
60
61impl sealed::SealedAbi for LeanName<'_> {}
62
63impl<'lean> LeanAbi<'lean> for LeanName<'lean> {
64    type CRepr = *mut lean_object;
65
66    fn into_c(self, _runtime: &'lean LeanRuntime) -> *mut lean_object {
67        self.obj.into_raw()
68    }
69
70    #[allow(
71        clippy::not_unsafe_ptr_arg_deref,
72        reason = "sealed trait — caller invariant documented on LeanAbi::from_c"
73    )]
74    fn from_c(c: *mut lean_object, runtime: &'lean LeanRuntime) -> LeanResult<Self> {
75        // SAFETY: `c` is an owned `lean_object*` produced by a Lean
76        // export returning `Lean.Name`; per Lake's `lean_obj_res`
77        // contract it carries one reference count. `runtime` witnesses
78        // `'lean`.
79        #[allow(unsafe_code)]
80        let obj = unsafe { Obj::from_owned_raw(runtime, c) };
81        Ok(Self { obj })
82    }
83}
84
85impl<'lean> TryFromLean<'lean> for LeanName<'lean> {
86    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
87        Ok(Self { obj })
88    }
89}
90
91impl<'lean> IntoLean<'lean> for LeanName<'lean> {
92    fn into_lean(self, _runtime: &'lean LeanRuntime) -> Obj<'lean> {
93        // The handle already wraps a fully-owned Lean object reference;
94        // hand it off unchanged. Required so `Vec<LeanName<'lean>>` can
95        // satisfy [`LeanAbi`] (which is bounded on
96        // `IntoLean + TryFromLean`) at the
97        // [`crate::LeanSession::query_declarations_bulk`] call site that
98        // marshals an `Array Name`.
99        self.obj
100    }
101}
lean_rs/handle/name.rs

lean_rs/handle/
name.rs
