lean_rs_host/host/meta/
options.rs

1//! Bounded option bundle for [`crate::LeanSession::run_meta`].
2//!
3//! Mirrors [`crate::host::elaboration::LeanElabOptions`] in spirit: every
4//! setter saturates rather than rejecting out-of-range values, the bounds
5//! exist as safety rails the call site never has to write `.map_err`
6//! around. Parallel rather than shared because meta-services carry no
7//! source position (no `file_label`) and do carry a reducibility setting
8//! ([`LeanMetaTransparency`]) that has no analogue in elaboration.
9//!
10//! The heartbeat and diagnostic-byte ceilings reuse the existing
11//! `LEAN_HEARTBEAT_LIMIT_*` / `LEAN_DIAGNOSTIC_BYTE_LIMIT_*` constants
12//! from [`crate::host::elaboration`] — the underlying Lean machinery
13//! (`Lean.maxHeartbeats`) and the failure-bytes invariant are the same.
14
15use crate::host::elaboration::{
16    LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT, LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX, LEAN_HEARTBEAT_LIMIT_DEFAULT,
17    LEAN_HEARTBEAT_LIMIT_MAX,
18};
19use lean_rs::abi::traits::{IntoLean, TryFromLean, conversion_error};
20use lean_rs::error::{LeanResult, bound_message};
21use lean_rs::{LeanRuntime, Obj};
22
23/// Reducibility setting threaded into the bounded `MetaM` runner.
24///
25/// Maps 1-1 onto Lean's `Meta.TransparencyMode` at 4.29.1. Declaration
26/// order doubles as the on-wire byte the Lean shim reads; the
27/// [`Self::as_byte`] accessor exposes that contract for the dispatch
28/// site. `#[non_exhaustive]` so toolchain refinements can extend the
29/// taxonomy (e.g., a hypothetical `None`) without breaking exhaustive
30/// matches downstream.
31#[derive(Copy, Clone, Debug, Default, Eq, PartialEq)]
32#[non_exhaustive]
33pub enum LeanMetaTransparency {
34    /// Lean's standard reducibility — non-reducible / non-irreducible
35    /// definitions unfold on demand.
36    #[default]
37    Default,
38    /// Only `@[reducible]` definitions unfold. Useful when you want
39    /// [`crate::host::meta::whnf`] to expose the surface structure of a
40    /// term without diving into expensive bodies.
41    Reducible,
42    /// `Default` plus the bodies of instance bindings.
43    Instances,
44    /// Every definition unfolds. Most aggressive setting — also the
45    /// most likely to blow the heartbeat budget on non-trivial terms.
46    All,
47}
48
49impl LeanMetaTransparency {
50    /// On-wire byte the Lean shim's `transparencyOfByte` reads.
51    #[must_use]
52    pub fn as_byte(self) -> u8 {
53        match self {
54            Self::Default => 0,
55            Self::Reducible => 1,
56            Self::Instances => 2,
57            Self::All => 3,
58        }
59    }
60
61    fn from_byte(byte: u8) -> LeanResult<Self> {
62        match byte {
63            0 => Ok(Self::Default),
64            1 => Ok(Self::Reducible),
65            2 => Ok(Self::Instances),
66            3 => Ok(Self::All),
67            other => Err(conversion_error(format!(
68                "expected LeanMetaTransparency byte 0..=3, found {other}"
69            ))),
70        }
71    }
72}
73
74impl<'lean> IntoLean<'lean> for LeanMetaTransparency {
75    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
76        self.as_byte().into_lean(runtime)
77    }
78}
79
80impl<'lean> TryFromLean<'lean> for LeanMetaTransparency {
81    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
82        Self::from_byte(u8::try_from_lean(obj)?)
83    }
84}
85
86/// Bounded options threaded into [`crate::LeanSession::run_meta`].
87///
88/// Construct through [`Self::new`] or [`Default::default`] and chain
89/// the per-field builder methods. Each setter saturates at the same
90/// ceiling [`crate::LeanElabOptions`] uses; the namespace context is
91/// bounded at [`lean_rs::LEAN_ERROR_MESSAGE_LIMIT`].
92///
93/// ```ignore
94/// let opts = LeanMetaOptions::new()
95///     .heartbeat_limit(50_000)
96///     .transparency(LeanMetaTransparency::Reducible);
97/// ```
98#[derive(Clone, Debug)]
99pub struct LeanMetaOptions {
100    namespace_context: String,
101    heartbeat_limit: u64,
102    diagnostic_byte_limit: usize,
103    transparency: LeanMetaTransparency,
104}
105
106impl LeanMetaOptions {
107    /// Construct an options bundle with the documented defaults: empty
108    /// namespace context, [`LEAN_HEARTBEAT_LIMIT_DEFAULT`] heartbeats,
109    /// [`LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT`] bytes of diagnostics, and
110    /// [`LeanMetaTransparency::Default`] reducibility.
111    #[must_use]
112    pub fn new() -> Self {
113        Self {
114            namespace_context: String::new(),
115            heartbeat_limit: LEAN_HEARTBEAT_LIMIT_DEFAULT,
116            diagnostic_byte_limit: LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT,
117            transparency: LeanMetaTransparency::Default,
118        }
119    }
120
121    /// Replace the heartbeat limit. Values above
122    /// [`LEAN_HEARTBEAT_LIMIT_MAX`] saturate at the ceiling.
123    #[must_use]
124    pub fn heartbeat_limit(mut self, heartbeats: u64) -> Self {
125        self.heartbeat_limit = heartbeats.min(LEAN_HEARTBEAT_LIMIT_MAX);
126        self
127    }
128
129    /// Replace the diagnostic byte budget. Values above
130    /// [`LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX`] saturate at the ceiling.
131    /// Threaded through the ABI; the current single-message failure
132    /// branches do not actively truncate (Rust's `LeanDiagnostic`
133    /// decoder already bounds at [`lean_rs::LEAN_ERROR_MESSAGE_LIMIT`]).
134    /// Multi-message services would consume the budget the same way
135    /// the elaboration shim's `serializeMessages` does.
136    #[must_use]
137    pub fn diagnostic_byte_limit(mut self, bytes: usize) -> Self {
138        self.diagnostic_byte_limit = bytes.min(LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX);
139        self
140    }
141
142    /// Replace the namespace context the meta runner opens before
143    /// evaluating the action (default empty, meaning the imported
144    /// environment's root namespace). Long strings truncate at
145    /// [`lean_rs::LEAN_ERROR_MESSAGE_LIMIT`] on a UTF-8 char boundary.
146    #[must_use]
147    pub fn namespace_context(mut self, ns: &str) -> Self {
148        self.namespace_context = bound_message(ns.to_owned());
149        self
150    }
151
152    /// Replace the reducibility setting. Default is
153    /// [`LeanMetaTransparency::Default`], matching Lean's `Meta`
154    /// default.
155    #[must_use]
156    pub fn transparency(mut self, transparency: LeanMetaTransparency) -> Self {
157        self.transparency = transparency;
158        self
159    }
160
161    // -- crate-internal accessors used by the dispatch site -----------
162
163    #[allow(
164        dead_code,
165        reason = "first caller lands with the run_meta dispatch in the same prompt"
166    )]
167    pub(crate) fn namespace_context_str(&self) -> &str {
168        &self.namespace_context
169    }
170
171    pub(crate) fn heartbeats(&self) -> u64 {
172        self.heartbeat_limit
173    }
174
175    pub(crate) fn diagnostic_byte_limit_usize(&self) -> usize {
176        self.diagnostic_byte_limit
177    }
178
179    pub(crate) fn transparency_byte(&self) -> u8 {
180        self.transparency.as_byte()
181    }
182}
183
184impl Default for LeanMetaOptions {
185    fn default() -> Self {
186        Self::new()
187    }
188}
189
190#[cfg(test)]
191mod tests {
192    use super::*;
193    use lean_rs::error::LEAN_ERROR_MESSAGE_LIMIT;
194
195    #[test]
196    fn defaults_match_published_constants() {
197        let opts = LeanMetaOptions::new();
198        assert_eq!(opts.heartbeats(), LEAN_HEARTBEAT_LIMIT_DEFAULT);
199        assert_eq!(opts.diagnostic_byte_limit_usize(), LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT);
200        assert_eq!(opts.namespace_context_str(), "");
201        assert_eq!(opts.transparency_byte(), 0);
202    }
203
204    #[test]
205    fn heartbeat_setter_saturates_at_max() {
206        let opts = LeanMetaOptions::new().heartbeat_limit(u64::MAX);
207        assert_eq!(opts.heartbeats(), LEAN_HEARTBEAT_LIMIT_MAX);
208    }
209
210    #[test]
211    fn diagnostic_byte_limit_setter_saturates_at_max() {
212        let opts = LeanMetaOptions::new().diagnostic_byte_limit(usize::MAX);
213        assert_eq!(opts.diagnostic_byte_limit_usize(), LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX);
214    }
215
216    #[test]
217    fn namespace_context_bounded() {
218        let long = "x".repeat(LEAN_ERROR_MESSAGE_LIMIT * 2);
219        let opts = LeanMetaOptions::new().namespace_context(&long);
220        assert!(opts.namespace_context_str().len() <= LEAN_ERROR_MESSAGE_LIMIT);
221    }
222
223    #[test]
224    fn transparency_byte_matches_lean_constructor_order() {
225        assert_eq!(LeanMetaTransparency::Default.as_byte(), 0);
226        assert_eq!(LeanMetaTransparency::Reducible.as_byte(), 1);
227        assert_eq!(LeanMetaTransparency::Instances.as_byte(), 2);
228        assert_eq!(LeanMetaTransparency::All.as_byte(), 3);
229    }
230}
lean_rs_host/host/meta/options.rs

lean_rs_host/host/meta/
options.rs
