lean_rs/handle/
expr.rs

1//! Opaque handle for `Lean.Expr`.
2//!
3//! [`LeanExpr`] is a receipt for an owned Lean expression 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 — `.bvar`, `.const`, `.app`, `toString`, `==` — live
7//! in Lean exports the caller reaches through
8//! [`crate::module::LeanModule::exported`]. Rust deliberately offers no
9//! constructor for `Expr`: rebuilding the Lean term algebra outside the
10//! kernel would either be wrong (lacking elaboration / type checking)
11//! or duplicate Lean's responsibility.
12//!
13//! Display text obtained from a Lean export is diagnostic, not a
14//! semantic key; use a Lean-authored equality export when semantics
15//! matter (see the module docs on [`crate::handle`]).
16
17use core::fmt;
18
19use lean_rs_sys::lean_object;
20
21use crate::abi::traits::{IntoLean, 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.Expr`.
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 LeanExpr<'lean> {
38    obj: Obj<'lean>,
39}
40
41impl Clone for LeanExpr<'_> {
42    fn clone(&self) -> Self {
43        Self { obj: self.obj.clone() }
44    }
45}
46
47impl fmt::Debug for LeanExpr<'_> {
48    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
49        // Opaque on purpose: the Rust side has no claim on Lean's
50        // structural identity. For a diagnostic string, route through a
51        // Lean-authored `Expr` pretty-printer export.
52        f.debug_struct("LeanExpr").finish_non_exhaustive()
53    }
54}
55
56impl sealed::SealedAbi for LeanExpr<'_> {}
57
58impl<'lean> LeanAbi<'lean> for LeanExpr<'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.Expr`; 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 LeanExpr<'lean> {
81    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
82        Ok(Self { obj })
83    }
84}
85
86impl<'lean> IntoLean<'lean> for LeanExpr<'lean> {
87    fn into_lean(self, _runtime: &'lean LeanRuntime) -> Obj<'lean> {
88        // The handle already wraps a fully-owned Lean object reference;
89        // hand it off unchanged. Required so `Option<LeanExpr<'lean>>`
90        // can satisfy [`LeanAbi`] (which is itself bounded on
91        // `IntoLean + TryFromLean`) at the `LeanSession::elaborate`
92        // call site that takes an optional expected type.
93        self.obj
94    }
95}
lean_rs/handle/expr.rs

lean_rs/handle/
expr.rs
