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

lean_rs_host/host/process/
query.rs
