lean_rs/handle/
declaration.rs

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

lean_rs/handle/
declaration.rs
