lean_rs_host/host/process/
query.rs

1//! Bounded module-query projections returned by
2//! [`crate::LeanSession::process_module_query`].
3//!
4//! Callers choose a query shape; Lean owns module-header handling,
5//! elaboration, info-tree traversal, cursor selection, and bounded
6//! rendering. Rust decodes only the requested projection.
7
8use lean_rs::abi::nat;
9use lean_rs::abi::structure::{alloc_ctor_with_objects, take_ctor_objects, view};
10use lean_rs::abi::traits::{IntoLean, LeanAbi, TryFromLean, conversion_error, sealed};
11use lean_rs::{LeanRuntime, Obj};
12use lean_toolchain::LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX;
13
14use crate::host::elaboration::LeanElabFailure;
15
16/// Query shape for one header-aware Lean module processing request.
17#[derive(Clone, Debug, Eq, PartialEq)]
18pub enum ModuleQuery {
19    /// Return only diagnostics from elaborating the module.
20    Diagnostics,
21    /// Return type information for the innermost term covering `line:column`.
22    TypeAt {
23        /// 1-indexed line in the original source.
24        line: u32,
25        /// 1-indexed column in the original source.
26        column: u32,
27    },
28    /// Return tactic goals for the innermost tactic context covering `line:column`.
29    GoalAt {
30        /// 1-indexed line in the original source.
31        line: u32,
32        /// 1-indexed column in the original source.
33        column: u32,
34    },
35    /// Return binder/use-site references whose recorded name exactly matches `name`.
36    References {
37        /// Fully-qualified Lean name or binder name as the elaborator records it.
38        name: String,
39    },
40}
41
42/// Explicit byte budgets for a batched module query.
43///
44/// The default is 8 KiB per rendered field and 64 KiB for the combined
45/// selector payload. Setters and ABI encoding clamp oversized values at
46/// [`LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX`], so direct struct literals cannot send an
47/// unbounded render request into Lean.
48#[derive(Clone, Debug, Eq, PartialEq)]
49pub struct ModuleQueryOutputBudgets {
50    /// Maximum UTF-8 bytes for one rendered field.
51    pub per_field_bytes: u32,
52    /// Maximum estimated UTF-8 bytes for all selector results in the batch.
53    pub total_bytes: u32,
54}
55
56impl Default for ModuleQueryOutputBudgets {
57    fn default() -> Self {
58        Self {
59            per_field_bytes: 8 * 1024,
60            total_bytes: 64 * 1024,
61        }
62    }
63}
64
65impl ModuleQueryOutputBudgets {
66    /// Construct the default output budget bundle.
67    #[must_use]
68    pub fn new() -> Self {
69        Self::default()
70    }
71
72    /// Replace the per-field byte budget, saturating at
73    /// [`LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX`].
74    #[must_use]
75    pub fn per_field_bytes(mut self, bytes: u32) -> Self {
76        self.per_field_bytes = clamp_output_budget(bytes);
77        self
78    }
79
80    /// Replace the total batch byte budget, saturating at
81    /// [`LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX`].
82    #[must_use]
83    pub fn total_bytes(mut self, bytes: u32) -> Self {
84        self.total_bytes = clamp_output_budget(bytes);
85        self
86    }
87
88    fn normalized(self) -> Self {
89        Self {
90            per_field_bytes: clamp_output_budget(self.per_field_bytes),
91            total_bytes: clamp_output_budget(self.total_bytes),
92        }
93    }
94}
95
96fn clamp_output_budget(bytes: u32) -> u32 {
97    let max = u32::try_from(LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX).unwrap_or(u32::MAX);
98    bytes.min(max)
99}
100
101/// Intent selector for one proof position inside a declaration.
102#[derive(Clone, Debug, Default, Eq, PartialEq)]
103pub enum ProofPositionSelector {
104    /// The first tactic state — the point after the first tactic has run.
105    #[default]
106    Default,
107    /// The `index`-th tactic state — after the index-th tactic has run.
108    Index { index: u32 },
109    /// The tactic whose source text exactly matches `text`.
110    AfterText { text: String, occurrence: Option<u32> },
111    /// The goal state before any tactic runs — the pristine entry goal. A proof
112    /// attempt splices its candidate before the first tactic, so a from-scratch
113    /// tactic block elaborates against this goal.
114    Entry,
115}
116
117/// Target for a non-mutating proof attempt.
118#[derive(Clone, Debug, Eq, PartialEq)]
119pub enum ProofEditTarget {
120    Declaration {
121        name: String,
122        position: ProofPositionSelector,
123    },
124}
125
126/// One proof candidate to splice into an in-memory overlay.
127#[derive(Clone, Debug, Eq, PartialEq)]
128pub struct ProofCandidate {
129    pub id: String,
130    pub text: String,
131}
132
133/// Bounded request to try proof snippets without mutating source files.
134#[derive(Clone, Debug, Eq, PartialEq)]
135pub struct ProofAttemptRequest {
136    pub source: String,
137    pub edit: ProofEditTarget,
138    pub candidates: Vec<ProofCandidate>,
139    pub budgets: ModuleQueryOutputBudgets,
140}
141
142/// Per-candidate proof attempt status.
143#[derive(Clone, Copy, Debug, Eq, PartialEq)]
144pub enum ProofAttemptStatus {
145    Closed,
146    Progressed,
147    Failed,
148    Timeout,
149    BudgetExceeded,
150    NotAttempted,
151    Unsupported,
152}
153
154/// Per-candidate proof attempt result row.
155#[derive(Clone, Debug)]
156pub struct ProofAttemptRow {
157    pub id: String,
158    pub status: ProofAttemptStatus,
159    pub candidate_text: RenderedInfo,
160    pub diagnostics: LeanElabFailure,
161    pub downstream_diagnostics: LeanElabFailure,
162    pub goals: Vec<RenderedInfo>,
163    pub declaration: Option<DeclarationTargetInfo>,
164    pub proof_position: Option<ProofPositionSummary>,
165    pub output_truncated: bool,
166}
167
168/// Informational summary of the resolved proof position.
169#[derive(Clone, Debug, Eq, PartialEq)]
170pub struct ProofPositionSummary {
171    pub index: u32,
172    pub tactic: RenderedInfo,
173}
174
175/// Valid proof-state boundary a selector can target.
176#[derive(Clone, Debug, Eq, PartialEq)]
177pub struct ProofBoundaryCandidate {
178    pub index: u32,
179    pub kind: String,
180    pub source: ModuleSourceSpan,
181    pub excerpt: RenderedInfo,
182}
183
184/// Envelope for a bounded proof attempt.
185#[derive(Clone, Debug)]
186pub struct ProofAttemptEnvelope {
187    pub candidates: Vec<ProofAttemptRow>,
188    pub candidate_limit: u32,
189    pub candidates_truncated: bool,
190    /// Goal state at the resolved proof position before any candidate ran —
191    /// the selected tactic's `goals_before`, identical to what the
192    /// proof-position query reports as `goals_before` at the same position,
193    /// rendered once per batch by the shim. Empty when the entry state is
194    /// degraded or unresolvable (resolution failure or the source-text
195    /// fallback).
196    pub entry_goals: Vec<RenderedInfo>,
197    /// Local hypotheses at the resolved proof position, rendered once per
198    /// batch with the proof-position query's pretty locals mode from the same
199    /// `goals_before` state — identical to what the proof-position query
200    /// reports as `locals` at the same position. Empty under the same
201    /// conditions as `entry_goals`.
202    pub locals: Vec<LocalInfo>,
203}
204
205/// Header-aware proof attempt outcome.
206#[derive(Clone, Debug)]
207pub enum ProofAttemptOutcome {
208    Ok {
209        result: ProofAttemptEnvelope,
210        imports: Vec<String>,
211    },
212    MissingImports {
213        result: ProofAttemptEnvelope,
214        imports: Vec<String>,
215        missing: Vec<String>,
216    },
217    HeaderParseFailed {
218        diagnostics: LeanElabFailure,
219    },
220    Unsupported,
221}
222
223/// Target declaration for verification.
224#[derive(Clone, Debug, Eq, PartialEq)]
225pub enum DeclarationVerificationTarget {
226    Name { name: String },
227    Span { span: ModuleSourceSpan },
228}
229
230/// Policy for `sorry`-like constructs during declaration verification.
231#[derive(Clone, Copy, Debug, Eq, PartialEq)]
232pub enum SorryPolicy {
233    Allow,
234    Deny,
235}
236
237/// Bounded request to verify one declaration in a source snapshot.
238#[derive(Clone, Debug, Eq, PartialEq)]
239pub struct DeclarationVerificationRequest {
240    pub source: String,
241    pub target: DeclarationVerificationTarget,
242    pub sorry_policy: SorryPolicy,
243    pub report_axioms: bool,
244    pub budgets: ModuleQueryOutputBudgets,
245}
246
247/// One target inside a batch declaration-verification request.
248#[derive(Clone, Debug, Eq, PartialEq)]
249pub struct DeclarationVerificationBatchItem {
250    pub id: String,
251    pub target: DeclarationVerificationTarget,
252}
253
254/// Bounded request to verify several declarations in one source snapshot.
255#[derive(Clone, Debug, Eq, PartialEq)]
256pub struct DeclarationVerificationBatchRequest {
257    pub source: String,
258    pub targets: Vec<DeclarationVerificationBatchItem>,
259    pub sorry_policy: SorryPolicy,
260    pub report_axioms: bool,
261    pub budgets: ModuleQueryOutputBudgets,
262}
263
264/// Verification policy result.
265#[derive(Clone, Copy, Debug, Eq, PartialEq)]
266pub enum DeclarationVerificationStatus {
267    Accepted,
268    Rejected,
269    NotFound,
270    Ambiguous,
271    Timeout,
272    BudgetExceeded,
273    Unsupported,
274    NeedsBuild,
275}
276
277/// Bounded facts returned by declaration verification.
278#[derive(Clone, Debug)]
279#[allow(
280    clippy::struct_excessive_bools,
281    reason = "verification booleans are independent wire facts for policy decisions"
282)]
283pub struct DeclarationVerificationFacts {
284    pub target: Option<DeclarationTargetInfo>,
285    pub diagnostics: LeanElabFailure,
286    pub unresolved_goals: Vec<RenderedInfo>,
287    pub contains_sorry: bool,
288    pub contains_admit: bool,
289    pub contains_sorry_ax: bool,
290    pub axioms: Vec<String>,
291    pub axioms_truncated: bool,
292    pub output_truncated: bool,
293    pub candidates: Vec<DeclarationTargetInfo>,
294    pub axioms_available: bool,
295}
296
297/// Header-aware declaration verification outcome.
298#[derive(Clone, Debug)]
299pub enum DeclarationVerificationOutcome {
300    Ok {
301        status: DeclarationVerificationStatus,
302        facts: Box<DeclarationVerificationFacts>,
303        imports: Vec<String>,
304    },
305    MissingImports {
306        status: DeclarationVerificationStatus,
307        facts: Box<DeclarationVerificationFacts>,
308        imports: Vec<String>,
309        missing: Vec<String>,
310    },
311    HeaderParseFailed {
312        diagnostics: LeanElabFailure,
313    },
314    Unsupported,
315}
316
317/// One ordered row inside a batch declaration-verification result.
318#[derive(Clone, Debug)]
319pub struct DeclarationVerificationBatchRow {
320    pub id: String,
321    pub target: DeclarationVerificationTarget,
322    pub status: DeclarationVerificationStatus,
323    pub facts: Box<DeclarationVerificationFacts>,
324}
325
326/// Header-aware batch declaration-verification outcome.
327#[derive(Clone, Debug)]
328pub enum DeclarationVerificationBatchOutcome {
329    Ok {
330        results: Vec<DeclarationVerificationBatchRow>,
331        imports: Vec<String>,
332    },
333    MissingImports {
334        results: Vec<DeclarationVerificationBatchRow>,
335        imports: Vec<String>,
336        missing: Vec<String>,
337    },
338    HeaderParseFailed {
339        diagnostics: LeanElabFailure,
340    },
341    Unsupported,
342}
343
344/// One selector inside a batched module-processing request.
345#[derive(Clone, Debug, Eq, PartialEq)]
346pub enum ModuleQuerySelector {
347    Diagnostics {
348        id: String,
349    },
350    ProofState {
351        id: String,
352        line: u32,
353        column: u32,
354    },
355    ProofStateInDeclaration {
356        id: String,
357        declaration: String,
358        position: ProofPositionSelector,
359        /// Render local hypotheses as raw, fully-elaborated `Expr` text rather
360        /// than the default notation-aware delaboration. Expert opt-out.
361        locals_raw: bool,
362    },
363    TypeAt {
364        id: String,
365        line: u32,
366        column: u32,
367    },
368    References {
369        id: String,
370        name: String,
371    },
372    DeclarationTarget {
373        id: String,
374        name: Option<String>,
375        line: Option<u32>,
376        column: Option<u32>,
377    },
378    SurroundingDeclaration {
379        id: String,
380        line: u32,
381        column: u32,
382    },
383    DeclarationOutline {
384        id: String,
385    },
386}
387
388impl ModuleQuerySelector {
389    #[must_use]
390    pub fn id(&self) -> &str {
391        match self {
392            Self::Diagnostics { id }
393            | Self::ProofState { id, .. }
394            | Self::ProofStateInDeclaration { id, .. }
395            | Self::TypeAt { id, .. }
396            | Self::References { id, .. }
397            | Self::DeclarationTarget { id, .. }
398            | Self::SurroundingDeclaration { id, .. } => id,
399            Self::DeclarationOutline { id } => id,
400        }
401    }
402}
403
404impl<'lean> IntoLean<'lean> for ModuleQuery {
405    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
406        match self {
407            Self::Diagnostics => 0u8.into_lean(runtime),
408            Self::TypeAt { line, column } => {
409                alloc_ctor_with_objects(runtime, 1, [line.into_lean(runtime), column.into_lean(runtime)])
410            }
411            Self::GoalAt { line, column } => {
412                alloc_ctor_with_objects(runtime, 2, [line.into_lean(runtime), column.into_lean(runtime)])
413            }
414            Self::References { name } => alloc_ctor_with_objects(runtime, 3, [name.into_lean(runtime)]),
415        }
416    }
417}
418
419impl<'lean> IntoLean<'lean> for ModuleQueryOutputBudgets {
420    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
421        let normalized = self.normalized();
422        alloc_ctor_with_objects(
423            runtime,
424            0,
425            [
426                normalized.per_field_bytes.into_lean(runtime),
427                normalized.total_bytes.into_lean(runtime),
428            ],
429        )
430    }
431}
432
433impl sealed::SealedAbi for ModuleQueryOutputBudgets {}
434
435impl<'lean> LeanAbi<'lean> for ModuleQueryOutputBudgets {
436    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
437
438    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
439        self.into_lean(runtime).into_raw()
440    }
441
442    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
443        Err(conversion_error(
444            "ModuleQueryOutputBudgets cannot decode a Lean call result; it is an argument-only type",
445        ))
446    }
447}
448
449impl sealed::SealedAbi for &ModuleQueryOutputBudgets {}
450
451impl<'lean> LeanAbi<'lean> for &ModuleQueryOutputBudgets {
452    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
453
454    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
455        self.clone().into_lean(runtime).into_raw()
456    }
457
458    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
459        Err(conversion_error(
460            "&ModuleQueryOutputBudgets cannot decode a Lean call result; use ModuleQueryOutputBudgets for owned values",
461        ))
462    }
463}
464
465impl<'lean> IntoLean<'lean> for ModuleQuerySelector {
466    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
467        match self {
468            Self::Diagnostics { id } => alloc_ctor_with_objects(runtime, 0, [id.into_lean(runtime)]),
469            Self::ProofState { id, line, column } => alloc_ctor_with_objects(
470                runtime,
471                1,
472                [
473                    id.into_lean(runtime),
474                    line.into_lean(runtime),
475                    column.into_lean(runtime),
476                ],
477            ),
478            Self::TypeAt { id, line, column } => alloc_ctor_with_objects(
479                runtime,
480                2,
481                [
482                    id.into_lean(runtime),
483                    line.into_lean(runtime),
484                    column.into_lean(runtime),
485                ],
486            ),
487            Self::References { id, name } => {
488                alloc_ctor_with_objects(runtime, 3, [id.into_lean(runtime), name.into_lean(runtime)])
489            }
490            Self::DeclarationTarget { id, name, line, column } => alloc_ctor_with_objects(
491                runtime,
492                4,
493                [
494                    id.into_lean(runtime),
495                    name.into_lean(runtime),
496                    line.into_lean(runtime),
497                    column.into_lean(runtime),
498                ],
499            ),
500            Self::SurroundingDeclaration { id, line, column } => alloc_ctor_with_objects(
501                runtime,
502                5,
503                [
504                    id.into_lean(runtime),
505                    line.into_lean(runtime),
506                    column.into_lean(runtime),
507                ],
508            ),
509            Self::ProofStateInDeclaration {
510                id,
511                declaration,
512                position,
513                locals_raw,
514            } => alloc_ctor_with_objects(
515                runtime,
516                6,
517                [
518                    id.into_lean(runtime),
519                    declaration.into_lean(runtime),
520                    position.into_lean(runtime),
521                    u32::from(locals_raw).into_lean(runtime),
522                ],
523            ),
524            Self::DeclarationOutline { id } => alloc_ctor_with_objects(runtime, 7, [id.into_lean(runtime)]),
525        }
526    }
527}
528
529impl<'lean> TryFromLean<'lean> for ModuleQuerySelector {
530    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
531        drop(obj);
532        Err(conversion_error(
533            "ModuleQuerySelector cannot decode a Lean call result; it is an argument-only type",
534        ))
535    }
536}
537
538impl sealed::SealedAbi for ModuleQuerySelector {}
539
540impl<'lean> LeanAbi<'lean> for ModuleQuerySelector {
541    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
542
543    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
544        self.into_lean(runtime).into_raw()
545    }
546
547    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
548        Err(conversion_error(
549            "ModuleQuerySelector cannot decode a Lean call result; it is an argument-only type",
550        ))
551    }
552}
553
554impl sealed::SealedAbi for ModuleQuery {}
555
556impl<'lean> LeanAbi<'lean> for ModuleQuery {
557    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
558
559    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
560        self.into_lean(runtime).into_raw()
561    }
562
563    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
564        Err(conversion_error(
565            "ModuleQuery cannot decode a Lean call result; it is an argument-only type",
566        ))
567    }
568}
569
570impl sealed::SealedAbi for &ModuleQuery {}
571
572impl<'lean> LeanAbi<'lean> for &ModuleQuery {
573    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
574
575    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
576        self.clone().into_lean(runtime).into_raw()
577    }
578
579    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
580        Err(conversion_error(
581            "&ModuleQuery cannot decode a Lean call result; use ModuleQuery for owned values",
582        ))
583    }
584}
585
586/// Source span in the original file. Positions are 1-based.
587#[derive(Clone, Debug, Eq, PartialEq)]
588pub struct ModuleSourceSpan {
589    pub start_line: u32,
590    pub start_column: u32,
591    pub end_line: u32,
592    pub end_column: u32,
593}
594
595impl<'lean> TryFromLean<'lean> for ModuleSourceSpan {
596    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
597        let [sl, sc, el, ec] = take_ctor_objects::<4>(obj, 0, "ModuleSourceSpan")?;
598        Ok(Self {
599            start_line: u32::try_from_lean(sl)?,
600            start_column: u32::try_from_lean(sc)?,
601            end_line: u32::try_from_lean(el)?,
602            end_column: u32::try_from_lean(ec)?,
603        })
604    }
605}
606
607impl<'lean> IntoLean<'lean> for ModuleSourceSpan {
608    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
609        alloc_ctor_with_objects(
610            runtime,
611            0,
612            [
613                self.start_line.into_lean(runtime),
614                self.start_column.into_lean(runtime),
615                self.end_line.into_lean(runtime),
616                self.end_column.into_lean(runtime),
617            ],
618        )
619    }
620}
621
622impl<'lean> IntoLean<'lean> for ProofPositionSelector {
623    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
624        match self {
625            Self::Default => 0u8.into_lean(runtime),
626            Self::Index { index } => alloc_ctor_with_objects(runtime, 1, [index.into_lean(runtime)]),
627            Self::AfterText { text, occurrence } => {
628                alloc_ctor_with_objects(runtime, 2, [text.into_lean(runtime), occurrence.into_lean(runtime)])
629            }
630            Self::Entry => 3u8.into_lean(runtime),
631        }
632    }
633}
634
635impl<'lean> IntoLean<'lean> for ProofEditTarget {
636    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
637        match self {
638            Self::Declaration { name, position } => {
639                alloc_ctor_with_objects(runtime, 0, [name.into_lean(runtime), position.into_lean(runtime)])
640            }
641        }
642    }
643}
644
645impl<'lean> IntoLean<'lean> for ProofCandidate {
646    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
647        alloc_ctor_with_objects(runtime, 0, [self.id.into_lean(runtime), self.text.into_lean(runtime)])
648    }
649}
650
651impl<'lean> IntoLean<'lean> for ProofAttemptRequest {
652    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
653        alloc_ctor_with_objects(
654            runtime,
655            0,
656            [
657                self.source.into_lean(runtime),
658                self.edit.into_lean(runtime),
659                self.candidates.into_lean(runtime),
660                self.budgets.into_lean(runtime),
661            ],
662        )
663    }
664}
665
666impl sealed::SealedAbi for ProofAttemptRequest {}
667
668impl<'lean> LeanAbi<'lean> for ProofAttemptRequest {
669    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
670
671    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
672        self.into_lean(runtime).into_raw()
673    }
674
675    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
676        Err(conversion_error(
677            "ProofAttemptRequest cannot decode a Lean call result; it is an argument-only type",
678        ))
679    }
680}
681
682impl sealed::SealedAbi for &ProofAttemptRequest {}
683
684impl<'lean> LeanAbi<'lean> for &ProofAttemptRequest {
685    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
686
687    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
688        self.clone().into_lean(runtime).into_raw()
689    }
690
691    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
692        Err(conversion_error(
693            "&ProofAttemptRequest cannot decode a Lean call result; use ProofAttemptRequest for owned values",
694        ))
695    }
696}
697
698impl<'lean> IntoLean<'lean> for DeclarationVerificationTarget {
699    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
700        match self {
701            Self::Name { name } => alloc_ctor_with_objects(runtime, 0, [name.into_lean(runtime)]),
702            Self::Span { span } => alloc_ctor_with_objects(runtime, 1, [span.into_lean(runtime)]),
703        }
704    }
705}
706
707impl<'lean> TryFromLean<'lean> for DeclarationVerificationTarget {
708    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
709        match sum_tag(&obj)? {
710            0 => {
711                let [name] = take_ctor_objects::<1>(obj, 0, "DeclarationVerificationTarget::name")?;
712                Ok(Self::Name {
713                    name: String::try_from_lean(name)?,
714                })
715            }
716            1 => {
717                let [span] = take_ctor_objects::<1>(obj, 1, "DeclarationVerificationTarget::span")?;
718                Ok(Self::Span {
719                    span: ModuleSourceSpan::try_from_lean(span)?,
720                })
721            }
722            other => Err(conversion_error(format!(
723                "expected Lean DeclarationVerificationTarget ctor (tag 0..=1), found tag {other}"
724            ))),
725        }
726    }
727}
728
729impl<'lean> IntoLean<'lean> for SorryPolicy {
730    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
731        match self {
732            Self::Allow => 0u32.into_lean(runtime),
733            Self::Deny => 1u32.into_lean(runtime),
734        }
735    }
736}
737
738impl<'lean> IntoLean<'lean> for DeclarationVerificationRequest {
739    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
740        alloc_ctor_with_objects(
741            runtime,
742            0,
743            [
744                self.source.into_lean(runtime),
745                self.target.into_lean(runtime),
746                self.sorry_policy.into_lean(runtime),
747                (u32::from(self.report_axioms)).into_lean(runtime),
748                self.budgets.into_lean(runtime),
749            ],
750        )
751    }
752}
753
754impl sealed::SealedAbi for DeclarationVerificationRequest {}
755
756impl<'lean> LeanAbi<'lean> for DeclarationVerificationRequest {
757    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
758
759    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
760        self.into_lean(runtime).into_raw()
761    }
762
763    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
764        Err(conversion_error(
765            "DeclarationVerificationRequest cannot decode a Lean call result; it is an argument-only type",
766        ))
767    }
768}
769
770impl sealed::SealedAbi for &DeclarationVerificationRequest {}
771
772impl<'lean> LeanAbi<'lean> for &DeclarationVerificationRequest {
773    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
774
775    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
776        self.clone().into_lean(runtime).into_raw()
777    }
778
779    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
780        Err(conversion_error(
781            "&DeclarationVerificationRequest cannot decode a Lean call result; use DeclarationVerificationRequest for owned values",
782        ))
783    }
784}
785
786impl<'lean> IntoLean<'lean> for DeclarationVerificationBatchItem {
787    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
788        alloc_ctor_with_objects(runtime, 0, [self.id.into_lean(runtime), self.target.into_lean(runtime)])
789    }
790}
791
792impl<'lean> IntoLean<'lean> for DeclarationVerificationBatchRequest {
793    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
794        alloc_ctor_with_objects(
795            runtime,
796            0,
797            [
798                self.source.into_lean(runtime),
799                self.targets.into_lean(runtime),
800                self.sorry_policy.into_lean(runtime),
801                (u32::from(self.report_axioms)).into_lean(runtime),
802                self.budgets.into_lean(runtime),
803            ],
804        )
805    }
806}
807
808impl sealed::SealedAbi for DeclarationVerificationBatchRequest {}
809
810impl<'lean> LeanAbi<'lean> for DeclarationVerificationBatchRequest {
811    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
812
813    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
814        self.into_lean(runtime).into_raw()
815    }
816
817    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
818        Err(conversion_error(
819            "DeclarationVerificationBatchRequest cannot decode a Lean call result; it is an argument-only type",
820        ))
821    }
822}
823
824impl sealed::SealedAbi for &DeclarationVerificationBatchRequest {}
825
826impl<'lean> LeanAbi<'lean> for &DeclarationVerificationBatchRequest {
827    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
828
829    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
830        self.clone().into_lean(runtime).into_raw()
831    }
832
833    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
834        Err(conversion_error(
835            "&DeclarationVerificationBatchRequest cannot decode a Lean call result; use DeclarationVerificationBatchRequest for owned values",
836        ))
837    }
838}
839
840/// Bounded rendered Lean text.
841#[derive(Clone, Debug, Eq, PartialEq)]
842pub struct RenderedInfo {
843    pub value: String,
844    pub truncated: bool,
845}
846
847impl<'lean> TryFromLean<'lean> for RenderedInfo {
848    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
849        let truncated = bool_tail(&obj, 0, "RenderedInfo.truncated")?;
850        let [value] = take_ctor_objects::<1>(obj, 0, "RenderedInfo")?;
851        Ok(Self {
852            value: String::try_from_lean(value)?,
853            truncated,
854        })
855    }
856}
857
858/// One identifier occurrence the elaborator recorded.
859#[derive(Clone, Debug, Eq, PartialEq)]
860pub struct NameRefNode {
861    pub start_line: u32,
862    pub start_column: u32,
863    pub end_line: u32,
864    pub end_column: u32,
865    pub name: String,
866    pub is_binder: bool,
867}
868
869impl<'lean> TryFromLean<'lean> for NameRefNode {
870    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
871        let is_binder = bool_tail(&obj, 0, "NameRefNode.isBinder")?;
872        let [sl, sc, el, ec, nm] = take_ctor_objects::<5>(obj, 0, "NameRefNode")?;
873        Ok(Self {
874            start_line: u32::try_from_lean(sl)?,
875            start_column: u32::try_from_lean(sc)?,
876            end_line: u32::try_from_lean(el)?,
877            end_column: u32::try_from_lean(ec)?,
878            name: String::try_from_lean(nm)?,
879            is_binder,
880        })
881    }
882}
883
884/// Result for [`ModuleQuery::TypeAt`].
885#[derive(Clone, Debug, Eq, PartialEq)]
886pub enum TypeAtResult {
887    Term {
888        span: ModuleSourceSpan,
889        expr: RenderedInfo,
890        type_str: RenderedInfo,
891        expected_type: Option<RenderedInfo>,
892    },
893    NoTerm,
894}
895
896impl<'lean> TryFromLean<'lean> for TypeAtResult {
897    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
898        match sum_tag(&obj)? {
899            0 => {
900                let [span, expr, type_str, expected_type] = take_ctor_objects::<4>(obj, 0, "TypeAtResult::term")?;
901                Ok(Self::Term {
902                    span: ModuleSourceSpan::try_from_lean(span)?,
903                    expr: RenderedInfo::try_from_lean(expr)?,
904                    type_str: RenderedInfo::try_from_lean(type_str)?,
905                    expected_type: Option::<RenderedInfo>::try_from_lean(expected_type)?,
906                })
907            }
908            1 => Ok(Self::NoTerm),
909            other => Err(conversion_error(format!(
910                "expected Lean TypeAtResult ctor (tag 0..=1), found tag {other}"
911            ))),
912        }
913    }
914}
915
916/// Result for [`ModuleQuery::GoalAt`].
917#[derive(Clone, Debug, Eq, PartialEq)]
918pub enum GoalAtResult {
919    Goal {
920        span: ModuleSourceSpan,
921        goals_before: Vec<String>,
922        goals_after: Vec<String>,
923        truncated: bool,
924    },
925    NoTacticContext,
926}
927
928impl<'lean> TryFromLean<'lean> for GoalAtResult {
929    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
930        match sum_tag(&obj)? {
931            0 => {
932                let truncated = bool_tail(&obj, 0, "GoalAtResult::goal.truncated")?;
933                let [span, before, after] = take_ctor_objects::<3>(obj, 0, "GoalAtResult::goal")?;
934                Ok(Self::Goal {
935                    span: ModuleSourceSpan::try_from_lean(span)?,
936                    goals_before: Vec::<String>::try_from_lean(before)?,
937                    goals_after: Vec::<String>::try_from_lean(after)?,
938                    truncated,
939                })
940            }
941            1 => Ok(Self::NoTacticContext),
942            other => Err(conversion_error(format!(
943                "expected Lean GoalAtResult ctor (tag 0..=1), found tag {other}"
944            ))),
945        }
946    }
947}
948
949/// Result for [`ModuleQuery::References`].
950#[derive(Clone, Debug, Eq, PartialEq)]
951pub struct ReferencesResult {
952    pub references: Vec<NameRefNode>,
953    pub truncated: bool,
954}
955
956impl<'lean> TryFromLean<'lean> for ReferencesResult {
957    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
958        let truncated = bool_tail(&obj, 0, "ReferencesResult.truncated")?;
959        let [references] = take_ctor_objects::<1>(obj, 0, "ReferencesResult")?;
960        Ok(Self {
961            references: Vec::<NameRefNode>::try_from_lean(references)?,
962            truncated,
963        })
964    }
965}
966
967/// One rendered local declaration in a proof-state result.
968#[derive(Clone, Debug, Eq, PartialEq)]
969pub struct LocalInfo {
970    pub name: String,
971    pub binder_info: String,
972    pub type_str: RenderedInfo,
973    pub value: Option<RenderedInfo>,
974}
975
976impl<'lean> TryFromLean<'lean> for LocalInfo {
977    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
978        let [name, binder_info, type_str, value] = take_ctor_objects::<4>(obj, 0, "LocalInfo")?;
979        Ok(Self {
980            name: String::try_from_lean(name)?,
981            binder_info: String::try_from_lean(binder_info)?,
982            type_str: RenderedInfo::try_from_lean(type_str)?,
983            value: Option::<RenderedInfo>::try_from_lean(value)?,
984        })
985    }
986}
987
988/// Source metadata for the declaration surrounding a proof-agent query.
989#[derive(Clone, Debug, Eq, PartialEq)]
990pub struct DeclarationTargetInfo {
991    pub short_name: String,
992    pub declaration_name: String,
993    pub namespace_name: String,
994    pub declaration_kind: String,
995    pub declaration_span: ModuleSourceSpan,
996    pub name_span: ModuleSourceSpan,
997    pub body_span: ModuleSourceSpan,
998}
999
1000impl<'lean> TryFromLean<'lean> for DeclarationTargetInfo {
1001    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1002        let [
1003            short_name,
1004            declaration_name,
1005            namespace_name,
1006            declaration_kind,
1007            declaration_span,
1008            name_span,
1009            body_span,
1010        ] = take_ctor_objects::<7>(obj, 0, "DeclarationTargetInfo")?;
1011        Ok(Self {
1012            short_name: String::try_from_lean(short_name)?,
1013            declaration_name: String::try_from_lean(declaration_name)?,
1014            namespace_name: String::try_from_lean(namespace_name)?,
1015            declaration_kind: String::try_from_lean(declaration_kind)?,
1016            declaration_span: ModuleSourceSpan::try_from_lean(declaration_span)?,
1017            name_span: ModuleSourceSpan::try_from_lean(name_span)?,
1018            body_span: ModuleSourceSpan::try_from_lean(body_span)?,
1019        })
1020    }
1021}
1022
1023/// Result for [`ModuleQuerySelector::DeclarationTarget`].
1024#[derive(Clone, Debug, Eq, PartialEq)]
1025pub enum DeclarationTargetResult {
1026    Target(DeclarationTargetInfo),
1027    NotFound,
1028    Ambiguous(Vec<DeclarationTargetInfo>),
1029}
1030
1031impl<'lean> TryFromLean<'lean> for DeclarationTargetResult {
1032    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1033        match sum_tag(&obj)? {
1034            0 => {
1035                let [info] = take_ctor_objects::<1>(obj, 0, "DeclarationTargetResult::target")?;
1036                Ok(Self::Target(DeclarationTargetInfo::try_from_lean(info)?))
1037            }
1038            1 => Ok(Self::NotFound),
1039            2 => {
1040                let [candidates] = take_ctor_objects::<1>(obj, 2, "DeclarationTargetResult::ambiguous")?;
1041                Ok(Self::Ambiguous(Vec::<DeclarationTargetInfo>::try_from_lean(
1042                    candidates,
1043                )?))
1044            }
1045            other => Err(conversion_error(format!(
1046                "expected Lean DeclarationTargetResult ctor (tag 0..=2), found tag {other}"
1047            ))),
1048        }
1049    }
1050}
1051
1052/// Result for [`ModuleQuerySelector::DeclarationOutline`].
1053#[derive(Clone, Debug, Eq, PartialEq)]
1054pub struct DeclarationOutlineResult {
1055    pub declarations: Vec<DeclarationTargetInfo>,
1056    pub truncated: bool,
1057}
1058
1059impl<'lean> TryFromLean<'lean> for DeclarationOutlineResult {
1060    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1061        let truncated = bool_tail(&obj, 0, "DeclarationOutlineResult.truncated")?;
1062        let [declarations] = take_ctor_objects::<1>(obj, 0, "DeclarationOutlineResult")?;
1063        Ok(Self {
1064            declarations: Vec::<DeclarationTargetInfo>::try_from_lean(declarations)?,
1065            truncated,
1066        })
1067    }
1068}
1069
1070impl<'lean> TryFromLean<'lean> for ProofAttemptStatus {
1071    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1072        Self::from_scalar(sum_tag(&obj)?)
1073    }
1074}
1075
1076impl ProofAttemptStatus {
1077    fn from_scalar(value: u8) -> lean_rs::LeanResult<Self> {
1078        match value {
1079            0 => Ok(Self::Closed),
1080            1 => Ok(Self::Progressed),
1081            2 => Ok(Self::Failed),
1082            3 => Ok(Self::Timeout),
1083            4 => Ok(Self::BudgetExceeded),
1084            5 => Ok(Self::NotAttempted),
1085            6 => Ok(Self::Unsupported),
1086            other => Err(conversion_error(format!(
1087                "expected Lean ProofAttemptStatus ctor (tag 0..=6), found tag {other}"
1088            ))),
1089        }
1090    }
1091}
1092
1093impl<'lean> TryFromLean<'lean> for ProofPositionSummary {
1094    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1095        let [index, tactic] = take_ctor_objects::<2>(obj, 0, "ProofPositionSummary")?;
1096        Ok(Self {
1097            index: u32::try_from_lean(index)?,
1098            tactic: RenderedInfo::try_from_lean(tactic)?,
1099        })
1100    }
1101}
1102
1103impl<'lean> TryFromLean<'lean> for ProofBoundaryCandidate {
1104    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1105        let [index, kind, source, excerpt] = take_ctor_objects::<4>(obj, 0, "ProofBoundaryCandidate")?;
1106        Ok(Self {
1107            index: u32::try_from_lean(index)?,
1108            kind: String::try_from_lean(kind)?,
1109            source: ModuleSourceSpan::try_from_lean(source)?,
1110            excerpt: RenderedInfo::try_from_lean(excerpt)?,
1111        })
1112    }
1113}
1114
1115impl<'lean> TryFromLean<'lean> for ProofAttemptRow {
1116    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1117        let ctor = view(&obj).ctor_shape(0, 7, "ProofAttemptRow")?;
1118        let status = ProofAttemptStatus::from_scalar(ctor.uint8(0, "ProofAttemptRow.status")?)?;
1119        let output_truncated = ctor.bool(1, "ProofAttemptRow.outputTruncated")?;
1120        let [
1121            id,
1122            candidate_text,
1123            diagnostics,
1124            downstream_diagnostics,
1125            goals,
1126            declaration,
1127            proof_position,
1128        ] = take_ctor_objects::<7>(obj, 0, "ProofAttemptRow")?;
1129        Ok(Self {
1130            id: String::try_from_lean(id)?,
1131            status,
1132            candidate_text: RenderedInfo::try_from_lean(candidate_text)?,
1133            diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1134            downstream_diagnostics: LeanElabFailure::try_from_lean(downstream_diagnostics)?,
1135            goals: Vec::<RenderedInfo>::try_from_lean(goals)?,
1136            declaration: Option::<DeclarationTargetInfo>::try_from_lean(declaration)?,
1137            proof_position: Option::<ProofPositionSummary>::try_from_lean(proof_position)?,
1138            output_truncated,
1139        })
1140    }
1141}
1142
1143impl<'lean> TryFromLean<'lean> for ProofAttemptEnvelope {
1144    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1145        let candidates_truncated = bool_tail(&obj, 0, "ProofAttemptEnvelope.candidatesTruncated")?;
1146        let [candidates, candidate_limit, entry_goals, locals] =
1147            take_ctor_objects::<4>(obj, 0, "ProofAttemptEnvelope")?;
1148        Ok(Self {
1149            candidates: Vec::<ProofAttemptRow>::try_from_lean(candidates)?,
1150            candidate_limit: u32::try_from_lean(candidate_limit)?,
1151            candidates_truncated,
1152            entry_goals: Vec::<RenderedInfo>::try_from_lean(entry_goals)?,
1153            locals: Vec::<LocalInfo>::try_from_lean(locals)?,
1154        })
1155    }
1156}
1157
1158impl<'lean> TryFromLean<'lean> for ProofAttemptOutcome {
1159    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1160        match sum_tag(&obj)? {
1161            0 => {
1162                let [result, imports] = take_ctor_objects::<2>(obj, 0, "ProofAttemptOutcome::ok")?;
1163                Ok(Self::Ok {
1164                    result: ProofAttemptEnvelope::try_from_lean(result)?,
1165                    imports: Vec::<String>::try_from_lean(imports)?,
1166                })
1167            }
1168            1 => {
1169                let [result, imports, missing] = take_ctor_objects::<3>(obj, 1, "ProofAttemptOutcome::missingImports")?;
1170                Ok(Self::MissingImports {
1171                    result: ProofAttemptEnvelope::try_from_lean(result)?,
1172                    imports: Vec::<String>::try_from_lean(imports)?,
1173                    missing: Vec::<String>::try_from_lean(missing)?,
1174                })
1175            }
1176            2 => {
1177                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ProofAttemptOutcome::headerParseFailed")?;
1178                Ok(Self::HeaderParseFailed {
1179                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1180                })
1181            }
1182            3 => Ok(Self::Unsupported),
1183            other => Err(conversion_error(format!(
1184                "expected Lean ProofAttemptOutcome ctor (tag 0..=3), found tag {other}"
1185            ))),
1186        }
1187    }
1188}
1189
1190impl<'lean> TryFromLean<'lean> for DeclarationVerificationStatus {
1191    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1192        Self::from_scalar(sum_tag(&obj)?)
1193    }
1194}
1195
1196impl DeclarationVerificationStatus {
1197    fn from_scalar(value: u8) -> lean_rs::LeanResult<Self> {
1198        match value {
1199            0 => Ok(Self::Accepted),
1200            1 => Ok(Self::Rejected),
1201            2 => Ok(Self::NotFound),
1202            3 => Ok(Self::Ambiguous),
1203            4 => Ok(Self::Timeout),
1204            5 => Ok(Self::BudgetExceeded),
1205            6 => Ok(Self::Unsupported),
1206            7 => Ok(Self::NeedsBuild),
1207            other => Err(conversion_error(format!(
1208                "expected Lean DeclarationVerificationStatus ctor (tag 0..=7), found tag {other}"
1209            ))),
1210        }
1211    }
1212}
1213
1214impl<'lean> TryFromLean<'lean> for DeclarationVerificationFacts {
1215    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1216        let contains_sorry = bool_tail(&obj, 0, "DeclarationVerificationFacts.containsSorry")?;
1217        let contains_admit = bool_tail(&obj, 1, "DeclarationVerificationFacts.containsAdmit")?;
1218        let contains_sorry_ax = bool_tail(&obj, 2, "DeclarationVerificationFacts.containsSorryAx")?;
1219        let axioms_truncated = bool_tail(&obj, 3, "DeclarationVerificationFacts.axiomsTruncated")?;
1220        let output_truncated = bool_tail(&obj, 4, "DeclarationVerificationFacts.outputTruncated")?;
1221        let axioms_available = bool_tail(&obj, 5, "DeclarationVerificationFacts.axiomsAvailable")?;
1222        let [target, diagnostics, unresolved_goals, axioms, candidates] =
1223            take_ctor_objects::<5>(obj, 0, "DeclarationVerificationFacts")?;
1224        Ok(Self {
1225            target: Option::<DeclarationTargetInfo>::try_from_lean(target)?,
1226            diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1227            unresolved_goals: Vec::<RenderedInfo>::try_from_lean(unresolved_goals)?,
1228            contains_sorry,
1229            contains_admit,
1230            contains_sorry_ax,
1231            axioms: Vec::<String>::try_from_lean(axioms)?,
1232            axioms_truncated,
1233            output_truncated,
1234            candidates: Vec::<DeclarationTargetInfo>::try_from_lean(candidates)?,
1235            axioms_available,
1236        })
1237    }
1238}
1239
1240impl<'lean> TryFromLean<'lean> for DeclarationVerificationOutcome {
1241    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1242        match sum_tag(&obj)? {
1243            0 => {
1244                let ctor = view(&obj).ctor_shape(0, 2, "DeclarationVerificationOutcome::ok")?;
1245                let status = DeclarationVerificationStatus::from_scalar(
1246                    ctor.uint8(0, "DeclarationVerificationOutcome::ok.status")?,
1247                )?;
1248                let [facts, imports] = take_ctor_objects::<2>(obj, 0, "DeclarationVerificationOutcome::ok")?;
1249                Ok(Self::Ok {
1250                    status,
1251                    facts: Box::new(DeclarationVerificationFacts::try_from_lean(facts)?),
1252                    imports: Vec::<String>::try_from_lean(imports)?,
1253                })
1254            }
1255            1 => {
1256                let ctor = view(&obj).ctor_shape(1, 3, "DeclarationVerificationOutcome::missingImports")?;
1257                let status = DeclarationVerificationStatus::from_scalar(
1258                    ctor.uint8(0, "DeclarationVerificationOutcome::missingImports.status")?,
1259                )?;
1260                let [facts, imports, missing] =
1261                    take_ctor_objects::<3>(obj, 1, "DeclarationVerificationOutcome::missingImports")?;
1262                Ok(Self::MissingImports {
1263                    status,
1264                    facts: Box::new(DeclarationVerificationFacts::try_from_lean(facts)?),
1265                    imports: Vec::<String>::try_from_lean(imports)?,
1266                    missing: Vec::<String>::try_from_lean(missing)?,
1267                })
1268            }
1269            2 => {
1270                let [diagnostics] =
1271                    take_ctor_objects::<1>(obj, 2, "DeclarationVerificationOutcome::headerParseFailed")?;
1272                Ok(Self::HeaderParseFailed {
1273                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1274                })
1275            }
1276            3 => Ok(Self::Unsupported),
1277            other => Err(conversion_error(format!(
1278                "expected Lean DeclarationVerificationOutcome ctor (tag 0..=3), found tag {other}"
1279            ))),
1280        }
1281    }
1282}
1283
1284impl<'lean> TryFromLean<'lean> for DeclarationVerificationBatchRow {
1285    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1286        let ctor = view(&obj).ctor_shape(0, 3, "DeclarationVerificationBatchRow")?;
1287        let status =
1288            DeclarationVerificationStatus::from_scalar(ctor.uint8(0, "DeclarationVerificationBatchRow.status")?)?;
1289        let [id, target, facts] = take_ctor_objects::<3>(obj, 0, "DeclarationVerificationBatchRow")?;
1290        Ok(Self {
1291            id: String::try_from_lean(id)?,
1292            target: DeclarationVerificationTarget::try_from_lean(target)?,
1293            status,
1294            facts: Box::new(DeclarationVerificationFacts::try_from_lean(facts)?),
1295        })
1296    }
1297}
1298
1299impl<'lean> TryFromLean<'lean> for DeclarationVerificationBatchOutcome {
1300    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1301        match sum_tag(&obj)? {
1302            0 => {
1303                let [results, imports] = take_ctor_objects::<2>(obj, 0, "DeclarationVerificationBatchOutcome::ok")?;
1304                Ok(Self::Ok {
1305                    results: Vec::<DeclarationVerificationBatchRow>::try_from_lean(results)?,
1306                    imports: Vec::<String>::try_from_lean(imports)?,
1307                })
1308            }
1309            1 => {
1310                let [results, imports, missing] =
1311                    take_ctor_objects::<3>(obj, 1, "DeclarationVerificationBatchOutcome::missingImports")?;
1312                Ok(Self::MissingImports {
1313                    results: Vec::<DeclarationVerificationBatchRow>::try_from_lean(results)?,
1314                    imports: Vec::<String>::try_from_lean(imports)?,
1315                    missing: Vec::<String>::try_from_lean(missing)?,
1316                })
1317            }
1318            2 => {
1319                let [diagnostics] =
1320                    take_ctor_objects::<1>(obj, 2, "DeclarationVerificationBatchOutcome::headerParseFailed")?;
1321                Ok(Self::HeaderParseFailed {
1322                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1323                })
1324            }
1325            3 => Ok(Self::Unsupported),
1326            other => Err(conversion_error(format!(
1327                "expected Lean DeclarationVerificationBatchOutcome ctor (tag 0..=3), found tag {other}"
1328            ))),
1329        }
1330    }
1331}
1332
1333/// Proof-state payload for one cursor.
1334#[derive(Clone, Debug, Eq, PartialEq)]
1335pub struct ProofStateInfo {
1336    pub declaration_name: Option<String>,
1337    pub namespace_name: String,
1338    pub safe_edit: Option<DeclarationTargetInfo>,
1339    pub span: ModuleSourceSpan,
1340    pub goals_before: Vec<String>,
1341    pub goals_after: Vec<String>,
1342    pub locals: Vec<LocalInfo>,
1343    pub expected_type: Option<RenderedInfo>,
1344    pub truncated: bool,
1345    pub proof_boundaries: Vec<ProofBoundaryCandidate>,
1346    pub proof_boundaries_truncated: bool,
1347}
1348
1349impl<'lean> TryFromLean<'lean> for ProofStateInfo {
1350    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1351        let truncated = bool_tail(&obj, 0, "ProofStateInfo.truncated")?;
1352        let proof_boundaries_truncated = bool_tail(&obj, 1, "ProofStateInfo.proofBoundariesTruncated")?;
1353        let [
1354            declaration_name,
1355            namespace_name,
1356            safe_edit,
1357            span,
1358            goals_before,
1359            goals_after,
1360            locals,
1361            expected_type,
1362            proof_boundaries,
1363        ] = take_ctor_objects::<9>(obj, 0, "ProofStateInfo")?;
1364        Ok(Self {
1365            declaration_name: Option::<String>::try_from_lean(declaration_name)?,
1366            namespace_name: String::try_from_lean(namespace_name)?,
1367            safe_edit: Option::<DeclarationTargetInfo>::try_from_lean(safe_edit)?,
1368            span: ModuleSourceSpan::try_from_lean(span)?,
1369            goals_before: Vec::<String>::try_from_lean(goals_before)?,
1370            goals_after: Vec::<String>::try_from_lean(goals_after)?,
1371            locals: Vec::<LocalInfo>::try_from_lean(locals)?,
1372            expected_type: Option::<RenderedInfo>::try_from_lean(expected_type)?,
1373            truncated,
1374            proof_boundaries: Vec::<ProofBoundaryCandidate>::try_from_lean(proof_boundaries)?,
1375            proof_boundaries_truncated,
1376        })
1377    }
1378}
1379
1380/// Result for [`ModuleQuerySelector::ProofState`].
1381#[derive(Clone, Debug, Eq, PartialEq)]
1382pub enum ProofStateResult {
1383    State(Box<ProofStateInfo>),
1384    Unavailable {
1385        message: String,
1386        proof_boundaries: Vec<ProofBoundaryCandidate>,
1387        proof_boundaries_truncated: bool,
1388    },
1389    Ambiguous {
1390        candidates: Vec<DeclarationTargetInfo>,
1391    },
1392    NeedsBuild {
1393        missing: Vec<String>,
1394    },
1395}
1396
1397impl<'lean> TryFromLean<'lean> for ProofStateResult {
1398    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1399        match sum_tag(&obj)? {
1400            0 => {
1401                let [info] = take_ctor_objects::<1>(obj, 0, "ProofStateResult::state")?;
1402                Ok(Self::State(Box::new(ProofStateInfo::try_from_lean(info)?)))
1403            }
1404            1 => {
1405                let proof_boundaries_truncated = view(&obj)
1406                    .ctor_shape(1, 2, "ProofStateResult::unavailable")?
1407                    .bool(0, "ProofStateResult::unavailable.proofBoundariesTruncated")?;
1408                let [message, proof_boundaries] = take_ctor_objects::<2>(obj, 1, "ProofStateResult::unavailable")?;
1409                Ok(Self::Unavailable {
1410                    message: String::try_from_lean(message)?,
1411                    proof_boundaries: Vec::<ProofBoundaryCandidate>::try_from_lean(proof_boundaries)?,
1412                    proof_boundaries_truncated,
1413                })
1414            }
1415            2 => {
1416                let [candidates] = take_ctor_objects::<1>(obj, 2, "ProofStateResult::ambiguous")?;
1417                Ok(Self::Ambiguous {
1418                    candidates: Vec::<DeclarationTargetInfo>::try_from_lean(candidates)?,
1419                })
1420            }
1421            3 => {
1422                let [missing] = take_ctor_objects::<1>(obj, 3, "ProofStateResult::needsBuild")?;
1423                Ok(Self::NeedsBuild {
1424                    missing: Vec::<String>::try_from_lean(missing)?,
1425                })
1426            }
1427            other => Err(conversion_error(format!(
1428                "expected Lean ProofStateResult ctor (tag 0..=3), found tag {other}"
1429            ))),
1430        }
1431    }
1432}
1433
1434/// Result for [`ModuleQuerySelector::SurroundingDeclaration`].
1435#[derive(Clone, Debug, Eq, PartialEq)]
1436pub enum SurroundingDeclarationResult {
1437    Declaration(DeclarationTargetInfo),
1438    None,
1439}
1440
1441impl<'lean> TryFromLean<'lean> for SurroundingDeclarationResult {
1442    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1443        match sum_tag(&obj)? {
1444            0 => {
1445                let [info] = take_ctor_objects::<1>(obj, 0, "SurroundingDeclarationResult::declaration")?;
1446                Ok(Self::Declaration(DeclarationTargetInfo::try_from_lean(info)?))
1447            }
1448            1 => Ok(Self::None),
1449            other => Err(conversion_error(format!(
1450                "expected Lean SurroundingDeclarationResult ctor (tag 0..=1), found tag {other}"
1451            ))),
1452        }
1453    }
1454}
1455
1456/// Typed payload returned by a successful module query.
1457#[derive(Clone, Debug)]
1458pub enum ModuleQueryResult {
1459    Diagnostics(LeanElabFailure),
1460    TypeAt(TypeAtResult),
1461    GoalAt(GoalAtResult),
1462    References(ReferencesResult),
1463}
1464
1465impl<'lean> TryFromLean<'lean> for ModuleQueryResult {
1466    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1467        match sum_tag(&obj)? {
1468            0 => {
1469                let [failure] = take_ctor_objects::<1>(obj, 0, "ModuleQueryResult::diagnostics")?;
1470                Ok(Self::Diagnostics(LeanElabFailure::try_from_lean(failure)?))
1471            }
1472            1 => {
1473                let [result] = take_ctor_objects::<1>(obj, 1, "ModuleQueryResult::typeAt")?;
1474                Ok(Self::TypeAt(TypeAtResult::try_from_lean(result)?))
1475            }
1476            2 => {
1477                let [result] = take_ctor_objects::<1>(obj, 2, "ModuleQueryResult::goalAt")?;
1478                Ok(Self::GoalAt(GoalAtResult::try_from_lean(result)?))
1479            }
1480            3 => {
1481                let [result] = take_ctor_objects::<1>(obj, 3, "ModuleQueryResult::references")?;
1482                Ok(Self::References(ReferencesResult::try_from_lean(result)?))
1483            }
1484            other => Err(conversion_error(format!(
1485                "expected Lean ModuleQueryResult ctor (tag 0..=3), found tag {other}"
1486            ))),
1487        }
1488    }
1489}
1490
1491/// Typed payload returned by one successful batch selector.
1492#[derive(Clone, Debug)]
1493pub enum ModuleQueryBatchResult {
1494    Diagnostics(LeanElabFailure),
1495    ProofState(ProofStateResult),
1496    TypeAt(TypeAtResult),
1497    References(ReferencesResult),
1498    DeclarationTarget(DeclarationTargetResult),
1499    SurroundingDeclaration(SurroundingDeclarationResult),
1500    DeclarationOutline(DeclarationOutlineResult),
1501}
1502
1503impl<'lean> TryFromLean<'lean> for ModuleQueryBatchResult {
1504    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1505        match sum_tag(&obj)? {
1506            0 => {
1507                let [failure] = take_ctor_objects::<1>(obj, 0, "ModuleQueryBatchResult::diagnostics")?;
1508                Ok(Self::Diagnostics(LeanElabFailure::try_from_lean(failure)?))
1509            }
1510            1 => {
1511                let [result] = take_ctor_objects::<1>(obj, 1, "ModuleQueryBatchResult::proofState")?;
1512                Ok(Self::ProofState(ProofStateResult::try_from_lean(result)?))
1513            }
1514            2 => {
1515                let [result] = take_ctor_objects::<1>(obj, 2, "ModuleQueryBatchResult::typeAt")?;
1516                Ok(Self::TypeAt(TypeAtResult::try_from_lean(result)?))
1517            }
1518            3 => {
1519                let [result] = take_ctor_objects::<1>(obj, 3, "ModuleQueryBatchResult::references")?;
1520                Ok(Self::References(ReferencesResult::try_from_lean(result)?))
1521            }
1522            4 => {
1523                let [result] = take_ctor_objects::<1>(obj, 4, "ModuleQueryBatchResult::declarationTarget")?;
1524                Ok(Self::DeclarationTarget(DeclarationTargetResult::try_from_lean(result)?))
1525            }
1526            5 => {
1527                let [result] = take_ctor_objects::<1>(obj, 5, "ModuleQueryBatchResult::surroundingDeclaration")?;
1528                Ok(Self::SurroundingDeclaration(
1529                    SurroundingDeclarationResult::try_from_lean(result)?,
1530                ))
1531            }
1532            6 => {
1533                let [result] = take_ctor_objects::<1>(obj, 6, "ModuleQueryBatchResult::declarationOutline")?;
1534                Ok(Self::DeclarationOutline(DeclarationOutlineResult::try_from_lean(
1535                    result,
1536                )?))
1537            }
1538            other => Err(conversion_error(format!(
1539                "expected Lean ModuleQueryBatchResult ctor (tag 0..=6), found tag {other}"
1540            ))),
1541        }
1542    }
1543}
1544
1545/// One selector result in a batched module query.
1546#[derive(Clone, Debug)]
1547pub enum ModuleQueryBatchItem {
1548    Ok {
1549        id: String,
1550        result: Box<ModuleQueryBatchResult>,
1551    },
1552    Unavailable {
1553        id: String,
1554        message: String,
1555    },
1556    BudgetExceeded {
1557        id: String,
1558        message: String,
1559    },
1560}
1561
1562impl ModuleQueryBatchItem {
1563    #[must_use]
1564    pub fn id(&self) -> &str {
1565        match self {
1566            Self::Ok { id, .. } | Self::Unavailable { id, .. } | Self::BudgetExceeded { id, .. } => id,
1567        }
1568    }
1569}
1570
1571impl<'lean> TryFromLean<'lean> for ModuleQueryBatchItem {
1572    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1573        match sum_tag(&obj)? {
1574            0 => {
1575                let [id, result] = take_ctor_objects::<2>(obj, 0, "ModuleQueryBatchItem::ok")?;
1576                Ok(Self::Ok {
1577                    id: String::try_from_lean(id)?,
1578                    result: Box::new(ModuleQueryBatchResult::try_from_lean(result)?),
1579                })
1580            }
1581            1 => {
1582                let [id, message] = take_ctor_objects::<2>(obj, 1, "ModuleQueryBatchItem::unavailable")?;
1583                Ok(Self::Unavailable {
1584                    id: String::try_from_lean(id)?,
1585                    message: String::try_from_lean(message)?,
1586                })
1587            }
1588            2 => {
1589                let [id, message] = take_ctor_objects::<2>(obj, 2, "ModuleQueryBatchItem::budgetExceeded")?;
1590                Ok(Self::BudgetExceeded {
1591                    id: String::try_from_lean(id)?,
1592                    message: String::try_from_lean(message)?,
1593                })
1594            }
1595            other => Err(conversion_error(format!(
1596                "expected Lean ModuleQueryBatchItem ctor (tag 0..=2), found tag {other}"
1597            ))),
1598        }
1599    }
1600}
1601
1602/// Successful batch selector envelope.
1603#[derive(Clone, Debug)]
1604pub struct ModuleQueryBatchEnvelope {
1605    pub items: Vec<ModuleQueryBatchItem>,
1606    pub total_truncated: bool,
1607}
1608
1609impl<'lean> TryFromLean<'lean> for ModuleQueryBatchEnvelope {
1610    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1611        let total_truncated = bool_tail(&obj, 0, "ModuleQueryBatchEnvelope.totalTruncated")?;
1612        let [items] = take_ctor_objects::<1>(obj, 0, "ModuleQueryBatchEnvelope")?;
1613        Ok(Self {
1614            items: Vec::<ModuleQueryBatchItem>::try_from_lean(items)?,
1615            total_truncated,
1616        })
1617    }
1618}
1619
1620/// Worker-side module snapshot cache status for a batched module query.
1621#[derive(Clone, Copy, Debug, Eq, PartialEq)]
1622pub enum ModuleQueryCacheStatus {
1623    Hit,
1624    Miss,
1625    Rebuilt,
1626    Evicted,
1627}
1628
1629impl<'lean> TryFromLean<'lean> for ModuleQueryCacheStatus {
1630    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1631        match sum_tag(&obj)? {
1632            0 => Ok(Self::Hit),
1633            1 => Ok(Self::Miss),
1634            2 => Ok(Self::Rebuilt),
1635            3 => Ok(Self::Evicted),
1636            other => Err(conversion_error(format!(
1637                "expected Lean ModuleQueryCacheStatus ctor (tag 0..=3), found tag {other}"
1638            ))),
1639        }
1640    }
1641}
1642
1643impl ModuleQueryCacheStatus {
1644    fn from_scalar_tail(byte: u8) -> lean_rs::LeanResult<Self> {
1645        match byte {
1646            0 => Ok(Self::Hit),
1647            1 => Ok(Self::Miss),
1648            2 => Ok(Self::Rebuilt),
1649            3 => Ok(Self::Evicted),
1650            other => Err(conversion_error(format!(
1651                "expected Lean ModuleQueryCacheStatus scalar tag 0..=3, found {other}"
1652            ))),
1653        }
1654    }
1655}
1656
1657/// Phase timings for cached batched module queries, in microseconds.
1658#[derive(Clone, Debug, Eq, PartialEq)]
1659pub struct ModuleQueryTimings {
1660    pub header_import_micros: u64,
1661    pub elaboration_micros: u64,
1662    pub projection_micros: u64,
1663    pub rendering_micros: u64,
1664}
1665
1666impl<'lean> TryFromLean<'lean> for ModuleQueryTimings {
1667    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1668        let ctor = view(&obj).ctor_shape(0, 0, "ModuleQueryTimings")?;
1669        Ok(Self {
1670            header_import_micros: ctor.uint64(0, "ModuleQueryTimings.headerImportMicros")?,
1671            elaboration_micros: ctor.uint64(8, "ModuleQueryTimings.elaborationMicros")?,
1672            projection_micros: ctor.uint64(16, "ModuleQueryTimings.projectionMicros")?,
1673            rendering_micros: ctor.uint64(24, "ModuleQueryTimings.renderingMicros")?,
1674        })
1675    }
1676}
1677
1678/// Cache and timing facts attached to cached batched module-query outcomes.
1679#[derive(Clone, Debug, Eq, PartialEq)]
1680pub struct ModuleQueryCacheFacts {
1681    pub cache_status: ModuleQueryCacheStatus,
1682    pub timings: ModuleQueryTimings,
1683    pub output_bytes: u64,
1684    pub cache_entry_count: Option<u64>,
1685    pub cache_approx_bytes: Option<u64>,
1686}
1687
1688impl<'lean> TryFromLean<'lean> for ModuleQueryCacheFacts {
1689    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1690        let ctor = view(&obj).ctor_shape(0, 3, "ModuleQueryCacheFacts")?;
1691        let output_bytes = ctor.uint64(0, "ModuleQueryCacheFacts.outputBytes")?;
1692        let cache_status = ctor.uint8(8, "ModuleQueryCacheFacts.cacheStatus")?;
1693        let [timings, cache_entry_count, cache_approx_bytes] = take_ctor_objects::<3>(obj, 0, "ModuleQueryCacheFacts")?;
1694        Ok(Self {
1695            cache_status: ModuleQueryCacheStatus::from_scalar_tail(cache_status)?,
1696            timings: ModuleQueryTimings::try_from_lean(timings)?,
1697            output_bytes,
1698            cache_entry_count: option_nat_u64(cache_entry_count)?,
1699            cache_approx_bytes: option_nat_u64(cache_approx_bytes)?,
1700        })
1701    }
1702}
1703
1704/// Cache policy passed to the Lean-side module snapshot cache.
1705#[derive(Clone, Debug, Eq, PartialEq)]
1706pub struct ModuleQueryCachePolicy {
1707    pub file_identity: String,
1708    pub key: String,
1709    pub max_entries: u64,
1710    pub ttl_millis: u64,
1711    pub max_bytes: u64,
1712}
1713
1714/// Header-aware module-query outcome.
1715#[derive(Clone, Debug)]
1716pub enum ModuleQueryOutcome {
1717    Ok {
1718        result: ModuleQueryResult,
1719        imports: Vec<String>,
1720    },
1721    MissingImports {
1722        result: ModuleQueryResult,
1723        imports: Vec<String>,
1724        missing: Vec<String>,
1725    },
1726    HeaderParseFailed {
1727        diagnostics: LeanElabFailure,
1728    },
1729    Unsupported,
1730}
1731
1732impl<'lean> TryFromLean<'lean> for ModuleQueryOutcome {
1733    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1734        match sum_tag(&obj)? {
1735            0 => {
1736                let [result, imports] = take_ctor_objects::<2>(obj, 0, "ModuleQueryOutcome::ok")?;
1737                Ok(Self::Ok {
1738                    result: ModuleQueryResult::try_from_lean(result)?,
1739                    imports: Vec::<String>::try_from_lean(imports)?,
1740                })
1741            }
1742            1 => {
1743                let [result, imports, missing] = take_ctor_objects::<3>(obj, 1, "ModuleQueryOutcome::missingImports")?;
1744                Ok(Self::MissingImports {
1745                    result: ModuleQueryResult::try_from_lean(result)?,
1746                    imports: Vec::<String>::try_from_lean(imports)?,
1747                    missing: Vec::<String>::try_from_lean(missing)?,
1748                })
1749            }
1750            2 => {
1751                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ModuleQueryOutcome::headerParseFailed")?;
1752                Ok(Self::HeaderParseFailed {
1753                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1754                })
1755            }
1756            3 => Ok(Self::Unsupported),
1757            other => Err(conversion_error(format!(
1758                "expected Lean ModuleQueryOutcome ctor (tag 0..=3), found tag {other}"
1759            ))),
1760        }
1761    }
1762}
1763
1764/// Header-aware batched module-query outcome.
1765#[derive(Clone, Debug)]
1766pub enum ModuleQueryBatchOutcome {
1767    Ok {
1768        result: ModuleQueryBatchEnvelope,
1769        imports: Vec<String>,
1770    },
1771    MissingImports {
1772        result: ModuleQueryBatchEnvelope,
1773        imports: Vec<String>,
1774        missing: Vec<String>,
1775    },
1776    HeaderParseFailed {
1777        diagnostics: LeanElabFailure,
1778    },
1779    Unsupported,
1780}
1781
1782impl<'lean> TryFromLean<'lean> for ModuleQueryBatchOutcome {
1783    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1784        match sum_tag(&obj)? {
1785            0 => {
1786                let [result, imports] = take_ctor_objects::<2>(obj, 0, "ModuleQueryBatchOutcome::ok")?;
1787                Ok(Self::Ok {
1788                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
1789                    imports: Vec::<String>::try_from_lean(imports)?,
1790                })
1791            }
1792            1 => {
1793                let [result, imports, missing] =
1794                    take_ctor_objects::<3>(obj, 1, "ModuleQueryBatchOutcome::missingImports")?;
1795                Ok(Self::MissingImports {
1796                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
1797                    imports: Vec::<String>::try_from_lean(imports)?,
1798                    missing: Vec::<String>::try_from_lean(missing)?,
1799                })
1800            }
1801            2 => {
1802                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ModuleQueryBatchOutcome::headerParseFailed")?;
1803                Ok(Self::HeaderParseFailed {
1804                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1805                })
1806            }
1807            3 => Ok(Self::Unsupported),
1808            other => Err(conversion_error(format!(
1809                "expected Lean ModuleQueryBatchOutcome ctor (tag 0..=3), found tag {other}"
1810            ))),
1811        }
1812    }
1813}
1814
1815/// Header-aware batched module-query outcome with cache/timing facts.
1816#[derive(Clone, Debug)]
1817pub enum ModuleQueryBatchCachedOutcome {
1818    Ok {
1819        result: ModuleQueryBatchEnvelope,
1820        imports: Vec<String>,
1821        facts: ModuleQueryCacheFacts,
1822    },
1823    MissingImports {
1824        result: ModuleQueryBatchEnvelope,
1825        imports: Vec<String>,
1826        missing: Vec<String>,
1827        facts: ModuleQueryCacheFacts,
1828    },
1829    HeaderParseFailed {
1830        diagnostics: LeanElabFailure,
1831        facts: ModuleQueryCacheFacts,
1832    },
1833    Unsupported,
1834}
1835
1836impl<'lean> TryFromLean<'lean> for ModuleQueryBatchCachedOutcome {
1837    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1838        match sum_tag(&obj)? {
1839            0 => {
1840                let [result, imports, facts] = take_ctor_objects::<3>(obj, 0, "ModuleQueryBatchCachedOutcome::ok")?;
1841                Ok(Self::Ok {
1842                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
1843                    imports: Vec::<String>::try_from_lean(imports)?,
1844                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
1845                })
1846            }
1847            1 => {
1848                let [result, imports, missing, facts] =
1849                    take_ctor_objects::<4>(obj, 1, "ModuleQueryBatchCachedOutcome::missingImports")?;
1850                Ok(Self::MissingImports {
1851                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
1852                    imports: Vec::<String>::try_from_lean(imports)?,
1853                    missing: Vec::<String>::try_from_lean(missing)?,
1854                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
1855                })
1856            }
1857            2 => {
1858                let [diagnostics, facts] =
1859                    take_ctor_objects::<2>(obj, 2, "ModuleQueryBatchCachedOutcome::headerParseFailed")?;
1860                Ok(Self::HeaderParseFailed {
1861                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1862                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
1863                })
1864            }
1865            3 => Ok(Self::Unsupported),
1866            other => Err(conversion_error(format!(
1867                "expected Lean ModuleQueryBatchCachedOutcome ctor (tag 0..=3), found tag {other}"
1868            ))),
1869        }
1870    }
1871}
1872
1873/// Result of clearing the Lean-side module snapshot cache.
1874#[derive(Clone, Debug, Eq, PartialEq)]
1875pub struct ModuleSnapshotCacheClearResult {
1876    pub entries_cleared: u64,
1877    pub approx_bytes_cleared: u64,
1878}
1879
1880impl<'lean> TryFromLean<'lean> for ModuleSnapshotCacheClearResult {
1881    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1882        let ctor = view(&obj).ctor_shape(0, 0, "ModuleSnapshotCacheClearResult")?;
1883        Ok(Self {
1884            entries_cleared: ctor.uint64(0, "ModuleSnapshotCacheClearResult.entriesCleared")?,
1885            approx_bytes_cleared: ctor.uint64(8, "ModuleSnapshotCacheClearResult.approxBytesCleared")?,
1886        })
1887    }
1888}
1889
1890fn option_nat_u64(obj: Obj<'_>) -> lean_rs::LeanResult<Option<u64>> {
1891    match sum_tag(&obj)? {
1892        0 => Ok(None),
1893        1 => {
1894            let [value] = take_ctor_objects::<1>(obj, 1, "Option::some Nat")?;
1895            Ok(Some(nat::try_to_u64(value)?))
1896        }
1897        other => Err(conversion_error(format!(
1898            "expected Lean Option Nat ctor (tag 0..=1), found tag {other}"
1899        ))),
1900    }
1901}
1902
1903fn bool_tail(obj: &Obj<'_>, offset: u32, label: &str) -> lean_rs::LeanResult<bool> {
1904    let ctor = view(obj).ctor()?;
1905    if ctor.tag() != 0 {
1906        return Err(conversion_error(format!(
1907            "expected Lean {label} constructor tag 0, found tag {}",
1908            ctor.tag()
1909        )));
1910    }
1911    ctor.bool(offset, label)
1912}
1913
1914fn sum_tag(obj: &Obj<'_>) -> lean_rs::LeanResult<u8> {
1915    view(obj).sum_tag()
1916}
1917
1918#[cfg(test)]
1919mod tests {
1920    use super::*;
1921
1922    #[test]
1923    fn module_query_output_budget_defaults_match_policy() {
1924        let budgets = ModuleQueryOutputBudgets::new();
1925        assert_eq!(budgets.per_field_bytes, 8 * 1024);
1926        assert_eq!(budgets.total_bytes, 64 * 1024);
1927    }
1928
1929    #[test]
1930    fn module_query_output_budget_setters_saturate() {
1931        let budgets = ModuleQueryOutputBudgets::new()
1932            .per_field_bytes(u32::MAX)
1933            .total_bytes(u32::MAX);
1934        let max = clamp_output_budget(u32::MAX);
1935        assert_eq!(budgets.per_field_bytes, max);
1936        assert_eq!(budgets.total_bytes, max);
1937    }
1938
1939    #[test]
1940    fn module_query_output_budget_normalization_clamps_struct_literals() {
1941        let budgets = ModuleQueryOutputBudgets {
1942            per_field_bytes: u32::MAX,
1943            total_bytes: u32::MAX,
1944        }
1945        .normalized();
1946        let max = clamp_output_budget(u32::MAX);
1947        assert_eq!(budgets.per_field_bytes, max);
1948        assert_eq!(budgets.total_bytes, max);
1949    }
1950}
lean_rs_host/host/process/query.rs

lean_rs_host/host/process/
query.rs
