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//!
17//! Two render paths cover the cost/quality tradeoff and the host stack
18//! exposes both deliberately. `LeanSession::expr_to_string_raw` walks
19//! `Expr.toString` directly — cheap, deterministic, ugly — and is the
20//! right choice for indexing, logging, and search keys. The optional
21//! `lean_rs_host::meta::pp_expr` service runs
22//! `Lean.PrettyPrinter.ppExpr` under the standard heartbeat budget; it
23//! is the form a Lean user reads, but pays for elaboration context and
24//! can time out. There is intentionally no `Display`, `Eq`, or
25//! `FromStr` impl on the handle itself: forcing callers through an
26//! explicit method keeps the FFI cost and the "diagnostic only"
27//! semantics visible at the call site.
28
29use core::fmt;
30
31use lean_rs_sys::lean_object;
32
33use crate::abi::traits::{IntoLean, LeanAbi, TryFromLean, sealed};
34use crate::error::LeanResult;
35use crate::runtime::LeanRuntime;
36use crate::runtime::obj::Obj;
37
38/// Opaque, lifetime-bound handle to a `Lean.Expr`.
39///
40/// `'lean` cascades from the [`crate::LeanRuntime`] borrow that produced
41/// the value, so a handle cannot outlive the runtime. Neither [`Send`]
42/// nor [`Sync`]: inherited from the crate-internal owned-object handle
43/// the type wraps.
44///
45/// [`Clone`] bumps the underlying refcount; [`Drop`] releases it. There
46/// are no public inherent methods: the handle is a pass-through that
47/// reaches Lean-authored operations through
48/// [`crate::module::LeanModule::exported`].
49pub struct LeanExpr<'lean> {
50    obj: Obj<'lean>,
51}
52
53impl Clone for LeanExpr<'_> {
54    fn clone(&self) -> Self {
55        Self { obj: self.obj.clone() }
56    }
57}
58
59impl fmt::Debug for LeanExpr<'_> {
60    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
61        // Opaque on purpose: the Rust side has no claim on Lean's
62        // structural identity. For a diagnostic string, route through a
63        // Lean-authored `Expr` pretty-printer export.
64        f.debug_struct("LeanExpr").finish_non_exhaustive()
65    }
66}
67
68impl sealed::SealedAbi for LeanExpr<'_> {}
69
70impl<'lean> LeanAbi<'lean> for LeanExpr<'lean> {
71    type CRepr = *mut lean_object;
72
73    fn into_c(self, _runtime: &'lean LeanRuntime) -> *mut lean_object {
74        self.obj.into_raw()
75    }
76
77    #[allow(
78        clippy::not_unsafe_ptr_arg_deref,
79        reason = "sealed trait — caller invariant documented on LeanAbi::from_c"
80    )]
81    fn from_c(c: *mut lean_object, runtime: &'lean LeanRuntime) -> LeanResult<Self> {
82        // SAFETY: `c` is an owned `lean_object*` produced by a Lean
83        // export returning `Lean.Expr`; per Lake's `lean_obj_res`
84        // contract it carries one reference count. `runtime` witnesses
85        // `'lean`.
86        #[allow(unsafe_code)]
87        let obj = unsafe { Obj::from_owned_raw(runtime, c) };
88        Ok(Self { obj })
89    }
90}
91
92impl<'lean> TryFromLean<'lean> for LeanExpr<'lean> {
93    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
94        Ok(Self { obj })
95    }
96}
97
98impl<'lean> IntoLean<'lean> for LeanExpr<'lean> {
99    fn into_lean(self, _runtime: &'lean LeanRuntime) -> Obj<'lean> {
100        // The handle already wraps a fully-owned Lean object reference;
101        // hand it off unchanged. Required so `Option<LeanExpr<'lean>>`
102        // can satisfy [`LeanAbi`] (which is itself bounded on
103        // `IntoLean + TryFromLean`) at the `LeanSession::elaborate`
104        // call site that takes an optional expected type.
105        self.obj
106    }
107}
lean_rs/handle/expr.rs

lean_rs/handle/
expr.rs
