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

lean_rs_host/host/meta/
options.rs
