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};
12
13use crate::host::elaboration::LeanElabFailure;
14
15/// Query shape for one header-aware Lean module processing request.
16#[derive(Clone, Debug, Eq, PartialEq)]
17pub enum ModuleQuery {
18    /// Return only diagnostics from elaborating the module.
19    Diagnostics,
20    /// Return type information for the innermost term covering `line:column`.
21    TypeAt {
22        /// 1-indexed line in the original source.
23        line: u32,
24        /// 1-indexed column in the original source.
25        column: u32,
26    },
27    /// Return tactic goals for the innermost tactic context covering `line:column`.
28    GoalAt {
29        /// 1-indexed line in the original source.
30        line: u32,
31        /// 1-indexed column in the original source.
32        column: u32,
33    },
34    /// Return binder/use-site references whose recorded name exactly matches `name`.
35    References {
36        /// Fully-qualified Lean name or binder name as the elaborator records it.
37        name: String,
38    },
39}
40
41/// Explicit byte budgets for a batched module query.
42#[derive(Clone, Debug, Eq, PartialEq)]
43pub struct ModuleQueryOutputBudgets {
44    pub per_field_bytes: u32,
45    pub total_bytes: u32,
46}
47
48impl Default for ModuleQueryOutputBudgets {
49    fn default() -> Self {
50        Self {
51            per_field_bytes: 8 * 1024,
52            total_bytes: 64 * 1024,
53        }
54    }
55}
56
57/// Intent selector for one proof position inside a declaration.
58#[derive(Clone, Debug, Default, Eq, PartialEq)]
59pub enum ProofPositionSelector {
60    #[default]
61    Default,
62    Index {
63        index: u32,
64    },
65    AfterText {
66        text: String,
67        occurrence: Option<u32>,
68    },
69}
70
71/// Target for a non-mutating proof attempt.
72#[derive(Clone, Debug, Eq, PartialEq)]
73pub enum ProofEditTarget {
74    Declaration {
75        name: String,
76        position: ProofPositionSelector,
77    },
78}
79
80/// One proof candidate to splice into an in-memory overlay.
81#[derive(Clone, Debug, Eq, PartialEq)]
82pub struct ProofCandidate {
83    pub id: String,
84    pub text: String,
85}
86
87/// Bounded request to try proof snippets without mutating source files.
88#[derive(Clone, Debug, Eq, PartialEq)]
89pub struct ProofAttemptRequest {
90    pub source: String,
91    pub edit: ProofEditTarget,
92    pub candidates: Vec<ProofCandidate>,
93    pub budgets: ModuleQueryOutputBudgets,
94}
95
96/// Per-candidate proof attempt status.
97#[derive(Clone, Copy, Debug, Eq, PartialEq)]
98pub enum ProofAttemptStatus {
99    Closed,
100    Progressed,
101    Failed,
102    Timeout,
103    BudgetExceeded,
104    Unsupported,
105}
106
107/// Per-candidate proof attempt result row.
108#[derive(Clone, Debug)]
109pub struct ProofAttemptRow {
110    pub id: String,
111    pub status: ProofAttemptStatus,
112    pub candidate_text: RenderedInfo,
113    pub diagnostics: LeanElabFailure,
114    pub downstream_diagnostics: LeanElabFailure,
115    pub goals: Vec<RenderedInfo>,
116    pub declaration: Option<DeclarationTargetInfo>,
117    pub proof_position: Option<ProofPositionSummary>,
118    pub output_truncated: bool,
119}
120
121/// Informational summary of the resolved proof position.
122#[derive(Clone, Debug, Eq, PartialEq)]
123pub struct ProofPositionSummary {
124    pub index: u32,
125    pub tactic: RenderedInfo,
126}
127
128/// Envelope for a bounded proof attempt.
129#[derive(Clone, Debug)]
130pub struct ProofAttemptEnvelope {
131    pub candidates: Vec<ProofAttemptRow>,
132    pub candidate_limit: u32,
133    pub candidates_truncated: bool,
134}
135
136/// Header-aware proof attempt outcome.
137#[derive(Clone, Debug)]
138pub enum ProofAttemptOutcome {
139    Ok {
140        result: ProofAttemptEnvelope,
141        imports: Vec<String>,
142    },
143    MissingImports {
144        result: ProofAttemptEnvelope,
145        imports: Vec<String>,
146        missing: Vec<String>,
147    },
148    HeaderParseFailed {
149        diagnostics: LeanElabFailure,
150    },
151    Unsupported,
152}
153
154/// Target declaration for verification.
155#[derive(Clone, Debug, Eq, PartialEq)]
156pub enum DeclarationVerificationTarget {
157    Name { name: String },
158    Span { span: ModuleSourceSpan },
159}
160
161/// Policy for `sorry`-like constructs during declaration verification.
162#[derive(Clone, Copy, Debug, Eq, PartialEq)]
163pub enum SorryPolicy {
164    Allow,
165    Deny,
166}
167
168/// Bounded request to verify one declaration in a source snapshot.
169#[derive(Clone, Debug, Eq, PartialEq)]
170pub struct DeclarationVerificationRequest {
171    pub source: String,
172    pub target: DeclarationVerificationTarget,
173    pub sorry_policy: SorryPolicy,
174    pub report_axioms: bool,
175    pub budgets: ModuleQueryOutputBudgets,
176}
177
178/// Verification policy result.
179#[derive(Clone, Copy, Debug, Eq, PartialEq)]
180pub enum DeclarationVerificationStatus {
181    Accepted,
182    Rejected,
183    NotFound,
184    Ambiguous,
185    Timeout,
186    BudgetExceeded,
187    Unsupported,
188    NeedsBuild,
189}
190
191/// Bounded facts returned by declaration verification.
192#[derive(Clone, Debug)]
193#[allow(
194    clippy::struct_excessive_bools,
195    reason = "verification booleans are independent wire facts for policy decisions"
196)]
197pub struct DeclarationVerificationFacts {
198    pub target: Option<DeclarationTargetInfo>,
199    pub diagnostics: LeanElabFailure,
200    pub unresolved_goals: Vec<RenderedInfo>,
201    pub contains_sorry: bool,
202    pub contains_admit: bool,
203    pub contains_sorry_ax: bool,
204    pub axioms: Vec<String>,
205    pub axioms_truncated: bool,
206    pub output_truncated: bool,
207    pub candidates: Vec<DeclarationTargetInfo>,
208    pub axioms_available: bool,
209}
210
211/// Header-aware declaration verification outcome.
212#[derive(Clone, Debug)]
213pub enum DeclarationVerificationOutcome {
214    Ok {
215        status: DeclarationVerificationStatus,
216        facts: Box<DeclarationVerificationFacts>,
217        imports: Vec<String>,
218    },
219    MissingImports {
220        status: DeclarationVerificationStatus,
221        facts: Box<DeclarationVerificationFacts>,
222        imports: Vec<String>,
223        missing: Vec<String>,
224    },
225    HeaderParseFailed {
226        diagnostics: LeanElabFailure,
227    },
228    Unsupported,
229}
230
231/// One selector inside a batched module-processing request.
232#[derive(Clone, Debug, Eq, PartialEq)]
233pub enum ModuleQuerySelector {
234    Diagnostics {
235        id: String,
236    },
237    ProofState {
238        id: String,
239        line: u32,
240        column: u32,
241    },
242    ProofStateInDeclaration {
243        id: String,
244        declaration: String,
245        position: ProofPositionSelector,
246    },
247    TypeAt {
248        id: String,
249        line: u32,
250        column: u32,
251    },
252    References {
253        id: String,
254        name: String,
255    },
256    DeclarationTarget {
257        id: String,
258        name: Option<String>,
259        line: Option<u32>,
260        column: Option<u32>,
261    },
262    SurroundingDeclaration {
263        id: String,
264        line: u32,
265        column: u32,
266    },
267}
268
269impl ModuleQuerySelector {
270    #[must_use]
271    pub fn id(&self) -> &str {
272        match self {
273            Self::Diagnostics { id }
274            | Self::ProofState { id, .. }
275            | Self::ProofStateInDeclaration { id, .. }
276            | Self::TypeAt { id, .. }
277            | Self::References { id, .. }
278            | Self::DeclarationTarget { id, .. }
279            | Self::SurroundingDeclaration { id, .. } => id,
280        }
281    }
282}
283
284impl<'lean> IntoLean<'lean> for ModuleQuery {
285    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
286        match self {
287            Self::Diagnostics => 0u8.into_lean(runtime),
288            Self::TypeAt { line, column } => {
289                alloc_ctor_with_objects(runtime, 1, [line.into_lean(runtime), column.into_lean(runtime)])
290            }
291            Self::GoalAt { line, column } => {
292                alloc_ctor_with_objects(runtime, 2, [line.into_lean(runtime), column.into_lean(runtime)])
293            }
294            Self::References { name } => alloc_ctor_with_objects(runtime, 3, [name.into_lean(runtime)]),
295        }
296    }
297}
298
299impl<'lean> IntoLean<'lean> for ModuleQueryOutputBudgets {
300    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
301        alloc_ctor_with_objects(
302            runtime,
303            0,
304            [
305                self.per_field_bytes.into_lean(runtime),
306                self.total_bytes.into_lean(runtime),
307            ],
308        )
309    }
310}
311
312impl sealed::SealedAbi for ModuleQueryOutputBudgets {}
313
314impl<'lean> LeanAbi<'lean> for ModuleQueryOutputBudgets {
315    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
316
317    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
318        self.into_lean(runtime).into_raw()
319    }
320
321    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
322        Err(conversion_error(
323            "ModuleQueryOutputBudgets cannot decode a Lean call result; it is an argument-only type",
324        ))
325    }
326}
327
328impl sealed::SealedAbi for &ModuleQueryOutputBudgets {}
329
330impl<'lean> LeanAbi<'lean> for &ModuleQueryOutputBudgets {
331    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
332
333    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
334        self.clone().into_lean(runtime).into_raw()
335    }
336
337    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
338        Err(conversion_error(
339            "&ModuleQueryOutputBudgets cannot decode a Lean call result; use ModuleQueryOutputBudgets for owned values",
340        ))
341    }
342}
343
344impl<'lean> IntoLean<'lean> for ModuleQuerySelector {
345    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
346        match self {
347            Self::Diagnostics { id } => alloc_ctor_with_objects(runtime, 0, [id.into_lean(runtime)]),
348            Self::ProofState { id, line, column } => alloc_ctor_with_objects(
349                runtime,
350                1,
351                [
352                    id.into_lean(runtime),
353                    line.into_lean(runtime),
354                    column.into_lean(runtime),
355                ],
356            ),
357            Self::TypeAt { id, line, column } => alloc_ctor_with_objects(
358                runtime,
359                2,
360                [
361                    id.into_lean(runtime),
362                    line.into_lean(runtime),
363                    column.into_lean(runtime),
364                ],
365            ),
366            Self::References { id, name } => {
367                alloc_ctor_with_objects(runtime, 3, [id.into_lean(runtime), name.into_lean(runtime)])
368            }
369            Self::DeclarationTarget { id, name, line, column } => alloc_ctor_with_objects(
370                runtime,
371                4,
372                [
373                    id.into_lean(runtime),
374                    name.into_lean(runtime),
375                    line.into_lean(runtime),
376                    column.into_lean(runtime),
377                ],
378            ),
379            Self::SurroundingDeclaration { id, line, column } => alloc_ctor_with_objects(
380                runtime,
381                5,
382                [
383                    id.into_lean(runtime),
384                    line.into_lean(runtime),
385                    column.into_lean(runtime),
386                ],
387            ),
388            Self::ProofStateInDeclaration {
389                id,
390                declaration,
391                position,
392            } => alloc_ctor_with_objects(
393                runtime,
394                6,
395                [
396                    id.into_lean(runtime),
397                    declaration.into_lean(runtime),
398                    position.into_lean(runtime),
399                ],
400            ),
401        }
402    }
403}
404
405impl<'lean> TryFromLean<'lean> for ModuleQuerySelector {
406    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
407        drop(obj);
408        Err(conversion_error(
409            "ModuleQuerySelector cannot decode a Lean call result; it is an argument-only type",
410        ))
411    }
412}
413
414impl sealed::SealedAbi for ModuleQuerySelector {}
415
416impl<'lean> LeanAbi<'lean> for ModuleQuerySelector {
417    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
418
419    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
420        self.into_lean(runtime).into_raw()
421    }
422
423    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
424        Err(conversion_error(
425            "ModuleQuerySelector cannot decode a Lean call result; it is an argument-only type",
426        ))
427    }
428}
429
430impl sealed::SealedAbi for ModuleQuery {}
431
432impl<'lean> LeanAbi<'lean> for ModuleQuery {
433    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
434
435    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
436        self.into_lean(runtime).into_raw()
437    }
438
439    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
440        Err(conversion_error(
441            "ModuleQuery cannot decode a Lean call result; it is an argument-only type",
442        ))
443    }
444}
445
446impl sealed::SealedAbi for &ModuleQuery {}
447
448impl<'lean> LeanAbi<'lean> for &ModuleQuery {
449    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
450
451    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
452        self.clone().into_lean(runtime).into_raw()
453    }
454
455    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
456        Err(conversion_error(
457            "&ModuleQuery cannot decode a Lean call result; use ModuleQuery for owned values",
458        ))
459    }
460}
461
462/// Source span in the original file. Positions are 1-based.
463#[derive(Clone, Debug, Eq, PartialEq)]
464pub struct ModuleSourceSpan {
465    pub start_line: u32,
466    pub start_column: u32,
467    pub end_line: u32,
468    pub end_column: u32,
469}
470
471impl<'lean> TryFromLean<'lean> for ModuleSourceSpan {
472    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
473        let [sl, sc, el, ec] = take_ctor_objects::<4>(obj, 0, "ModuleSourceSpan")?;
474        Ok(Self {
475            start_line: u32::try_from_lean(sl)?,
476            start_column: u32::try_from_lean(sc)?,
477            end_line: u32::try_from_lean(el)?,
478            end_column: u32::try_from_lean(ec)?,
479        })
480    }
481}
482
483impl<'lean> IntoLean<'lean> for ModuleSourceSpan {
484    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
485        alloc_ctor_with_objects(
486            runtime,
487            0,
488            [
489                self.start_line.into_lean(runtime),
490                self.start_column.into_lean(runtime),
491                self.end_line.into_lean(runtime),
492                self.end_column.into_lean(runtime),
493            ],
494        )
495    }
496}
497
498impl<'lean> IntoLean<'lean> for ProofPositionSelector {
499    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
500        match self {
501            Self::Default => 0u8.into_lean(runtime),
502            Self::Index { index } => alloc_ctor_with_objects(runtime, 1, [index.into_lean(runtime)]),
503            Self::AfterText { text, occurrence } => {
504                alloc_ctor_with_objects(runtime, 2, [text.into_lean(runtime), occurrence.into_lean(runtime)])
505            }
506        }
507    }
508}
509
510impl<'lean> IntoLean<'lean> for ProofEditTarget {
511    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
512        match self {
513            Self::Declaration { name, position } => {
514                alloc_ctor_with_objects(runtime, 0, [name.into_lean(runtime), position.into_lean(runtime)])
515            }
516        }
517    }
518}
519
520impl<'lean> IntoLean<'lean> for ProofCandidate {
521    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
522        alloc_ctor_with_objects(runtime, 0, [self.id.into_lean(runtime), self.text.into_lean(runtime)])
523    }
524}
525
526impl<'lean> IntoLean<'lean> for ProofAttemptRequest {
527    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
528        alloc_ctor_with_objects(
529            runtime,
530            0,
531            [
532                self.source.into_lean(runtime),
533                self.edit.into_lean(runtime),
534                self.candidates.into_lean(runtime),
535                self.budgets.into_lean(runtime),
536            ],
537        )
538    }
539}
540
541impl sealed::SealedAbi for ProofAttemptRequest {}
542
543impl<'lean> LeanAbi<'lean> for ProofAttemptRequest {
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            "ProofAttemptRequest cannot decode a Lean call result; it is an argument-only type",
553        ))
554    }
555}
556
557impl sealed::SealedAbi for &ProofAttemptRequest {}
558
559impl<'lean> LeanAbi<'lean> for &ProofAttemptRequest {
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            "&ProofAttemptRequest cannot decode a Lean call result; use ProofAttemptRequest for owned values",
569        ))
570    }
571}
572
573impl<'lean> IntoLean<'lean> for DeclarationVerificationTarget {
574    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
575        match self {
576            Self::Name { name } => alloc_ctor_with_objects(runtime, 0, [name.into_lean(runtime)]),
577            Self::Span { span } => alloc_ctor_with_objects(runtime, 1, [span.into_lean(runtime)]),
578        }
579    }
580}
581
582impl<'lean> IntoLean<'lean> for SorryPolicy {
583    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
584        match self {
585            Self::Allow => 0u32.into_lean(runtime),
586            Self::Deny => 1u32.into_lean(runtime),
587        }
588    }
589}
590
591impl<'lean> IntoLean<'lean> for DeclarationVerificationRequest {
592    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
593        alloc_ctor_with_objects(
594            runtime,
595            0,
596            [
597                self.source.into_lean(runtime),
598                self.target.into_lean(runtime),
599                self.sorry_policy.into_lean(runtime),
600                (u32::from(self.report_axioms)).into_lean(runtime),
601                self.budgets.into_lean(runtime),
602            ],
603        )
604    }
605}
606
607impl sealed::SealedAbi for DeclarationVerificationRequest {}
608
609impl<'lean> LeanAbi<'lean> for DeclarationVerificationRequest {
610    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
611
612    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
613        self.into_lean(runtime).into_raw()
614    }
615
616    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
617        Err(conversion_error(
618            "DeclarationVerificationRequest cannot decode a Lean call result; it is an argument-only type",
619        ))
620    }
621}
622
623impl sealed::SealedAbi for &DeclarationVerificationRequest {}
624
625impl<'lean> LeanAbi<'lean> for &DeclarationVerificationRequest {
626    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
627
628    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
629        self.clone().into_lean(runtime).into_raw()
630    }
631
632    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
633        Err(conversion_error(
634            "&DeclarationVerificationRequest cannot decode a Lean call result; use DeclarationVerificationRequest for owned values",
635        ))
636    }
637}
638
639/// Bounded rendered Lean text.
640#[derive(Clone, Debug, Eq, PartialEq)]
641pub struct RenderedInfo {
642    pub value: String,
643    pub truncated: bool,
644}
645
646impl<'lean> TryFromLean<'lean> for RenderedInfo {
647    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
648        let truncated = bool_tail(&obj, 0, "RenderedInfo.truncated")?;
649        let [value] = take_ctor_objects::<1>(obj, 0, "RenderedInfo")?;
650        Ok(Self {
651            value: String::try_from_lean(value)?,
652            truncated,
653        })
654    }
655}
656
657/// One identifier occurrence the elaborator recorded.
658#[derive(Clone, Debug, Eq, PartialEq)]
659pub struct NameRefNode {
660    pub start_line: u32,
661    pub start_column: u32,
662    pub end_line: u32,
663    pub end_column: u32,
664    pub name: String,
665    pub is_binder: bool,
666}
667
668impl<'lean> TryFromLean<'lean> for NameRefNode {
669    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
670        let is_binder = bool_tail(&obj, 0, "NameRefNode.isBinder")?;
671        let [sl, sc, el, ec, nm] = take_ctor_objects::<5>(obj, 0, "NameRefNode")?;
672        Ok(Self {
673            start_line: u32::try_from_lean(sl)?,
674            start_column: u32::try_from_lean(sc)?,
675            end_line: u32::try_from_lean(el)?,
676            end_column: u32::try_from_lean(ec)?,
677            name: String::try_from_lean(nm)?,
678            is_binder,
679        })
680    }
681}
682
683/// Result for [`ModuleQuery::TypeAt`].
684#[derive(Clone, Debug, Eq, PartialEq)]
685pub enum TypeAtResult {
686    Term {
687        span: ModuleSourceSpan,
688        expr: RenderedInfo,
689        type_str: RenderedInfo,
690        expected_type: Option<RenderedInfo>,
691    },
692    NoTerm,
693}
694
695impl<'lean> TryFromLean<'lean> for TypeAtResult {
696    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
697        match sum_tag(&obj)? {
698            0 => {
699                let [span, expr, type_str, expected_type] = take_ctor_objects::<4>(obj, 0, "TypeAtResult::term")?;
700                Ok(Self::Term {
701                    span: ModuleSourceSpan::try_from_lean(span)?,
702                    expr: RenderedInfo::try_from_lean(expr)?,
703                    type_str: RenderedInfo::try_from_lean(type_str)?,
704                    expected_type: Option::<RenderedInfo>::try_from_lean(expected_type)?,
705                })
706            }
707            1 => Ok(Self::NoTerm),
708            other => Err(conversion_error(format!(
709                "expected Lean TypeAtResult ctor (tag 0..=1), found tag {other}"
710            ))),
711        }
712    }
713}
714
715/// Result for [`ModuleQuery::GoalAt`].
716#[derive(Clone, Debug, Eq, PartialEq)]
717pub enum GoalAtResult {
718    Goal {
719        span: ModuleSourceSpan,
720        goals_before: Vec<String>,
721        goals_after: Vec<String>,
722        truncated: bool,
723    },
724    NoTacticContext,
725}
726
727impl<'lean> TryFromLean<'lean> for GoalAtResult {
728    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
729        match sum_tag(&obj)? {
730            0 => {
731                let truncated = bool_tail(&obj, 0, "GoalAtResult::goal.truncated")?;
732                let [span, before, after] = take_ctor_objects::<3>(obj, 0, "GoalAtResult::goal")?;
733                Ok(Self::Goal {
734                    span: ModuleSourceSpan::try_from_lean(span)?,
735                    goals_before: Vec::<String>::try_from_lean(before)?,
736                    goals_after: Vec::<String>::try_from_lean(after)?,
737                    truncated,
738                })
739            }
740            1 => Ok(Self::NoTacticContext),
741            other => Err(conversion_error(format!(
742                "expected Lean GoalAtResult ctor (tag 0..=1), found tag {other}"
743            ))),
744        }
745    }
746}
747
748/// Result for [`ModuleQuery::References`].
749#[derive(Clone, Debug, Eq, PartialEq)]
750pub struct ReferencesResult {
751    pub references: Vec<NameRefNode>,
752    pub truncated: bool,
753}
754
755impl<'lean> TryFromLean<'lean> for ReferencesResult {
756    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
757        let truncated = bool_tail(&obj, 0, "ReferencesResult.truncated")?;
758        let [references] = take_ctor_objects::<1>(obj, 0, "ReferencesResult")?;
759        Ok(Self {
760            references: Vec::<NameRefNode>::try_from_lean(references)?,
761            truncated,
762        })
763    }
764}
765
766/// One rendered local declaration in a proof-state result.
767#[derive(Clone, Debug, Eq, PartialEq)]
768pub struct LocalInfo {
769    pub name: String,
770    pub binder_info: String,
771    pub type_str: RenderedInfo,
772    pub value: Option<RenderedInfo>,
773}
774
775impl<'lean> TryFromLean<'lean> for LocalInfo {
776    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
777        let [name, binder_info, type_str, value] = take_ctor_objects::<4>(obj, 0, "LocalInfo")?;
778        Ok(Self {
779            name: String::try_from_lean(name)?,
780            binder_info: String::try_from_lean(binder_info)?,
781            type_str: RenderedInfo::try_from_lean(type_str)?,
782            value: Option::<RenderedInfo>::try_from_lean(value)?,
783        })
784    }
785}
786
787/// Source metadata for the declaration surrounding a proof-agent query.
788#[derive(Clone, Debug, Eq, PartialEq)]
789pub struct DeclarationTargetInfo {
790    pub short_name: String,
791    pub declaration_name: String,
792    pub namespace_name: String,
793    pub declaration_kind: String,
794    pub declaration_span: ModuleSourceSpan,
795    pub name_span: ModuleSourceSpan,
796    pub body_span: ModuleSourceSpan,
797}
798
799impl<'lean> TryFromLean<'lean> for DeclarationTargetInfo {
800    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
801        let [
802            short_name,
803            declaration_name,
804            namespace_name,
805            declaration_kind,
806            declaration_span,
807            name_span,
808            body_span,
809        ] = take_ctor_objects::<7>(obj, 0, "DeclarationTargetInfo")?;
810        Ok(Self {
811            short_name: String::try_from_lean(short_name)?,
812            declaration_name: String::try_from_lean(declaration_name)?,
813            namespace_name: String::try_from_lean(namespace_name)?,
814            declaration_kind: String::try_from_lean(declaration_kind)?,
815            declaration_span: ModuleSourceSpan::try_from_lean(declaration_span)?,
816            name_span: ModuleSourceSpan::try_from_lean(name_span)?,
817            body_span: ModuleSourceSpan::try_from_lean(body_span)?,
818        })
819    }
820}
821
822/// Result for [`ModuleQuerySelector::DeclarationTarget`].
823#[derive(Clone, Debug, Eq, PartialEq)]
824pub enum DeclarationTargetResult {
825    Target(DeclarationTargetInfo),
826    NotFound,
827    Ambiguous(Vec<DeclarationTargetInfo>),
828}
829
830impl<'lean> TryFromLean<'lean> for DeclarationTargetResult {
831    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
832        match sum_tag(&obj)? {
833            0 => {
834                let [info] = take_ctor_objects::<1>(obj, 0, "DeclarationTargetResult::target")?;
835                Ok(Self::Target(DeclarationTargetInfo::try_from_lean(info)?))
836            }
837            1 => Ok(Self::NotFound),
838            2 => {
839                let [candidates] = take_ctor_objects::<1>(obj, 2, "DeclarationTargetResult::ambiguous")?;
840                Ok(Self::Ambiguous(Vec::<DeclarationTargetInfo>::try_from_lean(
841                    candidates,
842                )?))
843            }
844            other => Err(conversion_error(format!(
845                "expected Lean DeclarationTargetResult ctor (tag 0..=2), found tag {other}"
846            ))),
847        }
848    }
849}
850
851impl<'lean> TryFromLean<'lean> for ProofAttemptStatus {
852    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
853        Self::from_scalar(sum_tag(&obj)?)
854    }
855}
856
857impl ProofAttemptStatus {
858    fn from_scalar(value: u8) -> lean_rs::LeanResult<Self> {
859        match value {
860            0 => Ok(Self::Closed),
861            1 => Ok(Self::Progressed),
862            2 => Ok(Self::Failed),
863            3 => Ok(Self::Timeout),
864            4 => Ok(Self::BudgetExceeded),
865            5 => Ok(Self::Unsupported),
866            other => Err(conversion_error(format!(
867                "expected Lean ProofAttemptStatus ctor (tag 0..=5), found tag {other}"
868            ))),
869        }
870    }
871}
872
873impl<'lean> TryFromLean<'lean> for ProofPositionSummary {
874    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
875        let [index, tactic] = take_ctor_objects::<2>(obj, 0, "ProofPositionSummary")?;
876        Ok(Self {
877            index: u32::try_from_lean(index)?,
878            tactic: RenderedInfo::try_from_lean(tactic)?,
879        })
880    }
881}
882
883impl<'lean> TryFromLean<'lean> for ProofAttemptRow {
884    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
885        let ctor = view(&obj).ctor_shape(0, 7, "ProofAttemptRow")?;
886        let status = ProofAttemptStatus::from_scalar(ctor.uint8(0, "ProofAttemptRow.status")?)?;
887        let output_truncated = ctor.bool(1, "ProofAttemptRow.outputTruncated")?;
888        let [
889            id,
890            candidate_text,
891            diagnostics,
892            downstream_diagnostics,
893            goals,
894            declaration,
895            proof_position,
896        ] = take_ctor_objects::<7>(obj, 0, "ProofAttemptRow")?;
897        Ok(Self {
898            id: String::try_from_lean(id)?,
899            status,
900            candidate_text: RenderedInfo::try_from_lean(candidate_text)?,
901            diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
902            downstream_diagnostics: LeanElabFailure::try_from_lean(downstream_diagnostics)?,
903            goals: Vec::<RenderedInfo>::try_from_lean(goals)?,
904            declaration: Option::<DeclarationTargetInfo>::try_from_lean(declaration)?,
905            proof_position: Option::<ProofPositionSummary>::try_from_lean(proof_position)?,
906            output_truncated,
907        })
908    }
909}
910
911impl<'lean> TryFromLean<'lean> for ProofAttemptEnvelope {
912    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
913        let candidates_truncated = bool_tail(&obj, 0, "ProofAttemptEnvelope.candidatesTruncated")?;
914        let [candidates, candidate_limit] = take_ctor_objects::<2>(obj, 0, "ProofAttemptEnvelope")?;
915        Ok(Self {
916            candidates: Vec::<ProofAttemptRow>::try_from_lean(candidates)?,
917            candidate_limit: u32::try_from_lean(candidate_limit)?,
918            candidates_truncated,
919        })
920    }
921}
922
923impl<'lean> TryFromLean<'lean> for ProofAttemptOutcome {
924    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
925        match sum_tag(&obj)? {
926            0 => {
927                let [result, imports] = take_ctor_objects::<2>(obj, 0, "ProofAttemptOutcome::ok")?;
928                Ok(Self::Ok {
929                    result: ProofAttemptEnvelope::try_from_lean(result)?,
930                    imports: Vec::<String>::try_from_lean(imports)?,
931                })
932            }
933            1 => {
934                let [result, imports, missing] = take_ctor_objects::<3>(obj, 1, "ProofAttemptOutcome::missingImports")?;
935                Ok(Self::MissingImports {
936                    result: ProofAttemptEnvelope::try_from_lean(result)?,
937                    imports: Vec::<String>::try_from_lean(imports)?,
938                    missing: Vec::<String>::try_from_lean(missing)?,
939                })
940            }
941            2 => {
942                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ProofAttemptOutcome::headerParseFailed")?;
943                Ok(Self::HeaderParseFailed {
944                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
945                })
946            }
947            3 => Ok(Self::Unsupported),
948            other => Err(conversion_error(format!(
949                "expected Lean ProofAttemptOutcome ctor (tag 0..=3), found tag {other}"
950            ))),
951        }
952    }
953}
954
955impl<'lean> TryFromLean<'lean> for DeclarationVerificationStatus {
956    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
957        Self::from_scalar(sum_tag(&obj)?)
958    }
959}
960
961impl DeclarationVerificationStatus {
962    fn from_scalar(value: u8) -> lean_rs::LeanResult<Self> {
963        match value {
964            0 => Ok(Self::Accepted),
965            1 => Ok(Self::Rejected),
966            2 => Ok(Self::NotFound),
967            3 => Ok(Self::Ambiguous),
968            4 => Ok(Self::Timeout),
969            5 => Ok(Self::BudgetExceeded),
970            6 => Ok(Self::Unsupported),
971            7 => Ok(Self::NeedsBuild),
972            other => Err(conversion_error(format!(
973                "expected Lean DeclarationVerificationStatus ctor (tag 0..=7), found tag {other}"
974            ))),
975        }
976    }
977}
978
979impl<'lean> TryFromLean<'lean> for DeclarationVerificationFacts {
980    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
981        let contains_sorry = bool_tail(&obj, 0, "DeclarationVerificationFacts.containsSorry")?;
982        let contains_admit = bool_tail(&obj, 1, "DeclarationVerificationFacts.containsAdmit")?;
983        let contains_sorry_ax = bool_tail(&obj, 2, "DeclarationVerificationFacts.containsSorryAx")?;
984        let axioms_truncated = bool_tail(&obj, 3, "DeclarationVerificationFacts.axiomsTruncated")?;
985        let output_truncated = bool_tail(&obj, 4, "DeclarationVerificationFacts.outputTruncated")?;
986        let axioms_available = bool_tail(&obj, 5, "DeclarationVerificationFacts.axiomsAvailable")?;
987        let [target, diagnostics, unresolved_goals, axioms, candidates] =
988            take_ctor_objects::<5>(obj, 0, "DeclarationVerificationFacts")?;
989        Ok(Self {
990            target: Option::<DeclarationTargetInfo>::try_from_lean(target)?,
991            diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
992            unresolved_goals: Vec::<RenderedInfo>::try_from_lean(unresolved_goals)?,
993            contains_sorry,
994            contains_admit,
995            contains_sorry_ax,
996            axioms: Vec::<String>::try_from_lean(axioms)?,
997            axioms_truncated,
998            output_truncated,
999            candidates: Vec::<DeclarationTargetInfo>::try_from_lean(candidates)?,
1000            axioms_available,
1001        })
1002    }
1003}
1004
1005impl<'lean> TryFromLean<'lean> for DeclarationVerificationOutcome {
1006    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1007        match sum_tag(&obj)? {
1008            0 => {
1009                let ctor = view(&obj).ctor_shape(0, 2, "DeclarationVerificationOutcome::ok")?;
1010                let status = DeclarationVerificationStatus::from_scalar(
1011                    ctor.uint8(0, "DeclarationVerificationOutcome::ok.status")?,
1012                )?;
1013                let [facts, imports] = take_ctor_objects::<2>(obj, 0, "DeclarationVerificationOutcome::ok")?;
1014                Ok(Self::Ok {
1015                    status,
1016                    facts: Box::new(DeclarationVerificationFacts::try_from_lean(facts)?),
1017                    imports: Vec::<String>::try_from_lean(imports)?,
1018                })
1019            }
1020            1 => {
1021                let ctor = view(&obj).ctor_shape(1, 3, "DeclarationVerificationOutcome::missingImports")?;
1022                let status = DeclarationVerificationStatus::from_scalar(
1023                    ctor.uint8(0, "DeclarationVerificationOutcome::missingImports.status")?,
1024                )?;
1025                let [facts, imports, missing] =
1026                    take_ctor_objects::<3>(obj, 1, "DeclarationVerificationOutcome::missingImports")?;
1027                Ok(Self::MissingImports {
1028                    status,
1029                    facts: Box::new(DeclarationVerificationFacts::try_from_lean(facts)?),
1030                    imports: Vec::<String>::try_from_lean(imports)?,
1031                    missing: Vec::<String>::try_from_lean(missing)?,
1032                })
1033            }
1034            2 => {
1035                let [diagnostics] =
1036                    take_ctor_objects::<1>(obj, 2, "DeclarationVerificationOutcome::headerParseFailed")?;
1037                Ok(Self::HeaderParseFailed {
1038                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1039                })
1040            }
1041            3 => Ok(Self::Unsupported),
1042            other => Err(conversion_error(format!(
1043                "expected Lean DeclarationVerificationOutcome ctor (tag 0..=3), found tag {other}"
1044            ))),
1045        }
1046    }
1047}
1048
1049/// Proof-state payload for one cursor.
1050#[derive(Clone, Debug, Eq, PartialEq)]
1051pub struct ProofStateInfo {
1052    pub declaration_name: Option<String>,
1053    pub namespace_name: String,
1054    pub safe_edit: Option<DeclarationTargetInfo>,
1055    pub span: ModuleSourceSpan,
1056    pub goals_before: Vec<String>,
1057    pub goals_after: Vec<String>,
1058    pub locals: Vec<LocalInfo>,
1059    pub expected_type: Option<RenderedInfo>,
1060    pub truncated: bool,
1061}
1062
1063impl<'lean> TryFromLean<'lean> for ProofStateInfo {
1064    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1065        let truncated = bool_tail(&obj, 0, "ProofStateInfo.truncated")?;
1066        let [
1067            declaration_name,
1068            namespace_name,
1069            safe_edit,
1070            span,
1071            goals_before,
1072            goals_after,
1073            locals,
1074            expected_type,
1075        ] = take_ctor_objects::<8>(obj, 0, "ProofStateInfo")?;
1076        Ok(Self {
1077            declaration_name: Option::<String>::try_from_lean(declaration_name)?,
1078            namespace_name: String::try_from_lean(namespace_name)?,
1079            safe_edit: Option::<DeclarationTargetInfo>::try_from_lean(safe_edit)?,
1080            span: ModuleSourceSpan::try_from_lean(span)?,
1081            goals_before: Vec::<String>::try_from_lean(goals_before)?,
1082            goals_after: Vec::<String>::try_from_lean(goals_after)?,
1083            locals: Vec::<LocalInfo>::try_from_lean(locals)?,
1084            expected_type: Option::<RenderedInfo>::try_from_lean(expected_type)?,
1085            truncated,
1086        })
1087    }
1088}
1089
1090/// Result for [`ModuleQuerySelector::ProofState`].
1091#[derive(Clone, Debug, Eq, PartialEq)]
1092pub enum ProofStateResult {
1093    State(Box<ProofStateInfo>),
1094    Unavailable { message: String },
1095    Ambiguous { candidates: Vec<DeclarationTargetInfo> },
1096    NeedsBuild { missing: Vec<String> },
1097}
1098
1099impl<'lean> TryFromLean<'lean> for ProofStateResult {
1100    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1101        match sum_tag(&obj)? {
1102            0 => {
1103                let [info] = take_ctor_objects::<1>(obj, 0, "ProofStateResult::state")?;
1104                Ok(Self::State(Box::new(ProofStateInfo::try_from_lean(info)?)))
1105            }
1106            1 => {
1107                let [message] = take_ctor_objects::<1>(obj, 1, "ProofStateResult::unavailable")?;
1108                Ok(Self::Unavailable {
1109                    message: String::try_from_lean(message)?,
1110                })
1111            }
1112            2 => {
1113                let [candidates] = take_ctor_objects::<1>(obj, 2, "ProofStateResult::ambiguous")?;
1114                Ok(Self::Ambiguous {
1115                    candidates: Vec::<DeclarationTargetInfo>::try_from_lean(candidates)?,
1116                })
1117            }
1118            3 => {
1119                let [missing] = take_ctor_objects::<1>(obj, 3, "ProofStateResult::needsBuild")?;
1120                Ok(Self::NeedsBuild {
1121                    missing: Vec::<String>::try_from_lean(missing)?,
1122                })
1123            }
1124            other => Err(conversion_error(format!(
1125                "expected Lean ProofStateResult ctor (tag 0..=3), found tag {other}"
1126            ))),
1127        }
1128    }
1129}
1130
1131/// Result for [`ModuleQuerySelector::SurroundingDeclaration`].
1132#[derive(Clone, Debug, Eq, PartialEq)]
1133pub enum SurroundingDeclarationResult {
1134    Declaration(DeclarationTargetInfo),
1135    None,
1136}
1137
1138impl<'lean> TryFromLean<'lean> for SurroundingDeclarationResult {
1139    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1140        match sum_tag(&obj)? {
1141            0 => {
1142                let [info] = take_ctor_objects::<1>(obj, 0, "SurroundingDeclarationResult::declaration")?;
1143                Ok(Self::Declaration(DeclarationTargetInfo::try_from_lean(info)?))
1144            }
1145            1 => Ok(Self::None),
1146            other => Err(conversion_error(format!(
1147                "expected Lean SurroundingDeclarationResult ctor (tag 0..=1), found tag {other}"
1148            ))),
1149        }
1150    }
1151}
1152
1153/// Typed payload returned by a successful module query.
1154#[derive(Clone, Debug)]
1155pub enum ModuleQueryResult {
1156    Diagnostics(LeanElabFailure),
1157    TypeAt(TypeAtResult),
1158    GoalAt(GoalAtResult),
1159    References(ReferencesResult),
1160}
1161
1162impl<'lean> TryFromLean<'lean> for ModuleQueryResult {
1163    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1164        match sum_tag(&obj)? {
1165            0 => {
1166                let [failure] = take_ctor_objects::<1>(obj, 0, "ModuleQueryResult::diagnostics")?;
1167                Ok(Self::Diagnostics(LeanElabFailure::try_from_lean(failure)?))
1168            }
1169            1 => {
1170                let [result] = take_ctor_objects::<1>(obj, 1, "ModuleQueryResult::typeAt")?;
1171                Ok(Self::TypeAt(TypeAtResult::try_from_lean(result)?))
1172            }
1173            2 => {
1174                let [result] = take_ctor_objects::<1>(obj, 2, "ModuleQueryResult::goalAt")?;
1175                Ok(Self::GoalAt(GoalAtResult::try_from_lean(result)?))
1176            }
1177            3 => {
1178                let [result] = take_ctor_objects::<1>(obj, 3, "ModuleQueryResult::references")?;
1179                Ok(Self::References(ReferencesResult::try_from_lean(result)?))
1180            }
1181            other => Err(conversion_error(format!(
1182                "expected Lean ModuleQueryResult ctor (tag 0..=3), found tag {other}"
1183            ))),
1184        }
1185    }
1186}
1187
1188/// Typed payload returned by one successful batch selector.
1189#[derive(Clone, Debug)]
1190pub enum ModuleQueryBatchResult {
1191    Diagnostics(LeanElabFailure),
1192    ProofState(ProofStateResult),
1193    TypeAt(TypeAtResult),
1194    References(ReferencesResult),
1195    DeclarationTarget(DeclarationTargetResult),
1196    SurroundingDeclaration(SurroundingDeclarationResult),
1197}
1198
1199impl<'lean> TryFromLean<'lean> for ModuleQueryBatchResult {
1200    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1201        match sum_tag(&obj)? {
1202            0 => {
1203                let [failure] = take_ctor_objects::<1>(obj, 0, "ModuleQueryBatchResult::diagnostics")?;
1204                Ok(Self::Diagnostics(LeanElabFailure::try_from_lean(failure)?))
1205            }
1206            1 => {
1207                let [result] = take_ctor_objects::<1>(obj, 1, "ModuleQueryBatchResult::proofState")?;
1208                Ok(Self::ProofState(ProofStateResult::try_from_lean(result)?))
1209            }
1210            2 => {
1211                let [result] = take_ctor_objects::<1>(obj, 2, "ModuleQueryBatchResult::typeAt")?;
1212                Ok(Self::TypeAt(TypeAtResult::try_from_lean(result)?))
1213            }
1214            3 => {
1215                let [result] = take_ctor_objects::<1>(obj, 3, "ModuleQueryBatchResult::references")?;
1216                Ok(Self::References(ReferencesResult::try_from_lean(result)?))
1217            }
1218            4 => {
1219                let [result] = take_ctor_objects::<1>(obj, 4, "ModuleQueryBatchResult::declarationTarget")?;
1220                Ok(Self::DeclarationTarget(DeclarationTargetResult::try_from_lean(result)?))
1221            }
1222            5 => {
1223                let [result] = take_ctor_objects::<1>(obj, 5, "ModuleQueryBatchResult::surroundingDeclaration")?;
1224                Ok(Self::SurroundingDeclaration(
1225                    SurroundingDeclarationResult::try_from_lean(result)?,
1226                ))
1227            }
1228            other => Err(conversion_error(format!(
1229                "expected Lean ModuleQueryBatchResult ctor (tag 0..=5), found tag {other}"
1230            ))),
1231        }
1232    }
1233}
1234
1235/// One selector result in a batched module query.
1236#[derive(Clone, Debug)]
1237pub enum ModuleQueryBatchItem {
1238    Ok {
1239        id: String,
1240        result: Box<ModuleQueryBatchResult>,
1241    },
1242    Unavailable {
1243        id: String,
1244        message: String,
1245    },
1246    BudgetExceeded {
1247        id: String,
1248        message: String,
1249    },
1250}
1251
1252impl ModuleQueryBatchItem {
1253    #[must_use]
1254    pub fn id(&self) -> &str {
1255        match self {
1256            Self::Ok { id, .. } | Self::Unavailable { id, .. } | Self::BudgetExceeded { id, .. } => id,
1257        }
1258    }
1259}
1260
1261impl<'lean> TryFromLean<'lean> for ModuleQueryBatchItem {
1262    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1263        match sum_tag(&obj)? {
1264            0 => {
1265                let [id, result] = take_ctor_objects::<2>(obj, 0, "ModuleQueryBatchItem::ok")?;
1266                Ok(Self::Ok {
1267                    id: String::try_from_lean(id)?,
1268                    result: Box::new(ModuleQueryBatchResult::try_from_lean(result)?),
1269                })
1270            }
1271            1 => {
1272                let [id, message] = take_ctor_objects::<2>(obj, 1, "ModuleQueryBatchItem::unavailable")?;
1273                Ok(Self::Unavailable {
1274                    id: String::try_from_lean(id)?,
1275                    message: String::try_from_lean(message)?,
1276                })
1277            }
1278            2 => {
1279                let [id, message] = take_ctor_objects::<2>(obj, 2, "ModuleQueryBatchItem::budgetExceeded")?;
1280                Ok(Self::BudgetExceeded {
1281                    id: String::try_from_lean(id)?,
1282                    message: String::try_from_lean(message)?,
1283                })
1284            }
1285            other => Err(conversion_error(format!(
1286                "expected Lean ModuleQueryBatchItem ctor (tag 0..=2), found tag {other}"
1287            ))),
1288        }
1289    }
1290}
1291
1292/// Successful batch selector envelope.
1293#[derive(Clone, Debug)]
1294pub struct ModuleQueryBatchEnvelope {
1295    pub items: Vec<ModuleQueryBatchItem>,
1296    pub total_truncated: bool,
1297}
1298
1299impl<'lean> TryFromLean<'lean> for ModuleQueryBatchEnvelope {
1300    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1301        let total_truncated = bool_tail(&obj, 0, "ModuleQueryBatchEnvelope.totalTruncated")?;
1302        let [items] = take_ctor_objects::<1>(obj, 0, "ModuleQueryBatchEnvelope")?;
1303        Ok(Self {
1304            items: Vec::<ModuleQueryBatchItem>::try_from_lean(items)?,
1305            total_truncated,
1306        })
1307    }
1308}
1309
1310/// Worker-side module snapshot cache status for a batched module query.
1311#[derive(Clone, Copy, Debug, Eq, PartialEq)]
1312pub enum ModuleQueryCacheStatus {
1313    Hit,
1314    Miss,
1315    Rebuilt,
1316    Evicted,
1317}
1318
1319impl<'lean> TryFromLean<'lean> for ModuleQueryCacheStatus {
1320    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1321        match sum_tag(&obj)? {
1322            0 => Ok(Self::Hit),
1323            1 => Ok(Self::Miss),
1324            2 => Ok(Self::Rebuilt),
1325            3 => Ok(Self::Evicted),
1326            other => Err(conversion_error(format!(
1327                "expected Lean ModuleQueryCacheStatus ctor (tag 0..=3), found tag {other}"
1328            ))),
1329        }
1330    }
1331}
1332
1333impl ModuleQueryCacheStatus {
1334    fn from_scalar_tail(byte: u8) -> lean_rs::LeanResult<Self> {
1335        match byte {
1336            0 => Ok(Self::Hit),
1337            1 => Ok(Self::Miss),
1338            2 => Ok(Self::Rebuilt),
1339            3 => Ok(Self::Evicted),
1340            other => Err(conversion_error(format!(
1341                "expected Lean ModuleQueryCacheStatus scalar tag 0..=3, found {other}"
1342            ))),
1343        }
1344    }
1345}
1346
1347/// Phase timings for cached batched module queries, in microseconds.
1348#[derive(Clone, Debug, Eq, PartialEq)]
1349pub struct ModuleQueryTimings {
1350    pub header_import_micros: u64,
1351    pub elaboration_micros: u64,
1352    pub projection_micros: u64,
1353    pub rendering_micros: u64,
1354}
1355
1356impl<'lean> TryFromLean<'lean> for ModuleQueryTimings {
1357    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1358        let ctor = view(&obj).ctor_shape(0, 0, "ModuleQueryTimings")?;
1359        Ok(Self {
1360            header_import_micros: ctor.uint64(0, "ModuleQueryTimings.headerImportMicros")?,
1361            elaboration_micros: ctor.uint64(8, "ModuleQueryTimings.elaborationMicros")?,
1362            projection_micros: ctor.uint64(16, "ModuleQueryTimings.projectionMicros")?,
1363            rendering_micros: ctor.uint64(24, "ModuleQueryTimings.renderingMicros")?,
1364        })
1365    }
1366}
1367
1368/// Cache and timing facts attached to cached batched module-query outcomes.
1369#[derive(Clone, Debug, Eq, PartialEq)]
1370pub struct ModuleQueryCacheFacts {
1371    pub cache_status: ModuleQueryCacheStatus,
1372    pub timings: ModuleQueryTimings,
1373    pub output_bytes: u64,
1374    pub cache_entry_count: Option<u64>,
1375    pub cache_approx_bytes: Option<u64>,
1376}
1377
1378impl<'lean> TryFromLean<'lean> for ModuleQueryCacheFacts {
1379    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1380        let ctor = view(&obj).ctor_shape(0, 3, "ModuleQueryCacheFacts")?;
1381        let output_bytes = ctor.uint64(0, "ModuleQueryCacheFacts.outputBytes")?;
1382        let cache_status = ctor.uint8(8, "ModuleQueryCacheFacts.cacheStatus")?;
1383        let [timings, cache_entry_count, cache_approx_bytes] = take_ctor_objects::<3>(obj, 0, "ModuleQueryCacheFacts")?;
1384        Ok(Self {
1385            cache_status: ModuleQueryCacheStatus::from_scalar_tail(cache_status)?,
1386            timings: ModuleQueryTimings::try_from_lean(timings)?,
1387            output_bytes,
1388            cache_entry_count: option_nat_u64(cache_entry_count)?,
1389            cache_approx_bytes: option_nat_u64(cache_approx_bytes)?,
1390        })
1391    }
1392}
1393
1394/// Cache policy passed to the Lean-side module snapshot cache.
1395#[derive(Clone, Debug, Eq, PartialEq)]
1396pub struct ModuleQueryCachePolicy {
1397    pub file_identity: String,
1398    pub key: String,
1399    pub max_entries: u64,
1400    pub ttl_millis: u64,
1401    pub max_bytes: u64,
1402}
1403
1404/// Header-aware module-query outcome.
1405#[derive(Clone, Debug)]
1406pub enum ModuleQueryOutcome {
1407    Ok {
1408        result: ModuleQueryResult,
1409        imports: Vec<String>,
1410    },
1411    MissingImports {
1412        result: ModuleQueryResult,
1413        imports: Vec<String>,
1414        missing: Vec<String>,
1415    },
1416    HeaderParseFailed {
1417        diagnostics: LeanElabFailure,
1418    },
1419    Unsupported,
1420}
1421
1422impl<'lean> TryFromLean<'lean> for ModuleQueryOutcome {
1423    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1424        match sum_tag(&obj)? {
1425            0 => {
1426                let [result, imports] = take_ctor_objects::<2>(obj, 0, "ModuleQueryOutcome::ok")?;
1427                Ok(Self::Ok {
1428                    result: ModuleQueryResult::try_from_lean(result)?,
1429                    imports: Vec::<String>::try_from_lean(imports)?,
1430                })
1431            }
1432            1 => {
1433                let [result, imports, missing] = take_ctor_objects::<3>(obj, 1, "ModuleQueryOutcome::missingImports")?;
1434                Ok(Self::MissingImports {
1435                    result: ModuleQueryResult::try_from_lean(result)?,
1436                    imports: Vec::<String>::try_from_lean(imports)?,
1437                    missing: Vec::<String>::try_from_lean(missing)?,
1438                })
1439            }
1440            2 => {
1441                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ModuleQueryOutcome::headerParseFailed")?;
1442                Ok(Self::HeaderParseFailed {
1443                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1444                })
1445            }
1446            3 => Ok(Self::Unsupported),
1447            other => Err(conversion_error(format!(
1448                "expected Lean ModuleQueryOutcome ctor (tag 0..=3), found tag {other}"
1449            ))),
1450        }
1451    }
1452}
1453
1454/// Header-aware batched module-query outcome.
1455#[derive(Clone, Debug)]
1456pub enum ModuleQueryBatchOutcome {
1457    Ok {
1458        result: ModuleQueryBatchEnvelope,
1459        imports: Vec<String>,
1460    },
1461    MissingImports {
1462        result: ModuleQueryBatchEnvelope,
1463        imports: Vec<String>,
1464        missing: Vec<String>,
1465    },
1466    HeaderParseFailed {
1467        diagnostics: LeanElabFailure,
1468    },
1469    Unsupported,
1470}
1471
1472impl<'lean> TryFromLean<'lean> for ModuleQueryBatchOutcome {
1473    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1474        match sum_tag(&obj)? {
1475            0 => {
1476                let [result, imports] = take_ctor_objects::<2>(obj, 0, "ModuleQueryBatchOutcome::ok")?;
1477                Ok(Self::Ok {
1478                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
1479                    imports: Vec::<String>::try_from_lean(imports)?,
1480                })
1481            }
1482            1 => {
1483                let [result, imports, missing] =
1484                    take_ctor_objects::<3>(obj, 1, "ModuleQueryBatchOutcome::missingImports")?;
1485                Ok(Self::MissingImports {
1486                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
1487                    imports: Vec::<String>::try_from_lean(imports)?,
1488                    missing: Vec::<String>::try_from_lean(missing)?,
1489                })
1490            }
1491            2 => {
1492                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ModuleQueryBatchOutcome::headerParseFailed")?;
1493                Ok(Self::HeaderParseFailed {
1494                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1495                })
1496            }
1497            3 => Ok(Self::Unsupported),
1498            other => Err(conversion_error(format!(
1499                "expected Lean ModuleQueryBatchOutcome ctor (tag 0..=3), found tag {other}"
1500            ))),
1501        }
1502    }
1503}
1504
1505/// Header-aware batched module-query outcome with cache/timing facts.
1506#[derive(Clone, Debug)]
1507pub enum ModuleQueryBatchCachedOutcome {
1508    Ok {
1509        result: ModuleQueryBatchEnvelope,
1510        imports: Vec<String>,
1511        facts: ModuleQueryCacheFacts,
1512    },
1513    MissingImports {
1514        result: ModuleQueryBatchEnvelope,
1515        imports: Vec<String>,
1516        missing: Vec<String>,
1517        facts: ModuleQueryCacheFacts,
1518    },
1519    HeaderParseFailed {
1520        diagnostics: LeanElabFailure,
1521        facts: ModuleQueryCacheFacts,
1522    },
1523    Unsupported,
1524}
1525
1526impl<'lean> TryFromLean<'lean> for ModuleQueryBatchCachedOutcome {
1527    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1528        match sum_tag(&obj)? {
1529            0 => {
1530                let [result, imports, facts] = take_ctor_objects::<3>(obj, 0, "ModuleQueryBatchCachedOutcome::ok")?;
1531                Ok(Self::Ok {
1532                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
1533                    imports: Vec::<String>::try_from_lean(imports)?,
1534                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
1535                })
1536            }
1537            1 => {
1538                let [result, imports, missing, facts] =
1539                    take_ctor_objects::<4>(obj, 1, "ModuleQueryBatchCachedOutcome::missingImports")?;
1540                Ok(Self::MissingImports {
1541                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
1542                    imports: Vec::<String>::try_from_lean(imports)?,
1543                    missing: Vec::<String>::try_from_lean(missing)?,
1544                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
1545                })
1546            }
1547            2 => {
1548                let [diagnostics, facts] =
1549                    take_ctor_objects::<2>(obj, 2, "ModuleQueryBatchCachedOutcome::headerParseFailed")?;
1550                Ok(Self::HeaderParseFailed {
1551                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
1552                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
1553                })
1554            }
1555            3 => Ok(Self::Unsupported),
1556            other => Err(conversion_error(format!(
1557                "expected Lean ModuleQueryBatchCachedOutcome ctor (tag 0..=3), found tag {other}"
1558            ))),
1559        }
1560    }
1561}
1562
1563/// Result of clearing the Lean-side module snapshot cache.
1564#[derive(Clone, Debug, Eq, PartialEq)]
1565pub struct ModuleSnapshotCacheClearResult {
1566    pub entries_cleared: u64,
1567    pub approx_bytes_cleared: u64,
1568}
1569
1570impl<'lean> TryFromLean<'lean> for ModuleSnapshotCacheClearResult {
1571    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1572        let ctor = view(&obj).ctor_shape(0, 0, "ModuleSnapshotCacheClearResult")?;
1573        Ok(Self {
1574            entries_cleared: ctor.uint64(0, "ModuleSnapshotCacheClearResult.entriesCleared")?,
1575            approx_bytes_cleared: ctor.uint64(8, "ModuleSnapshotCacheClearResult.approxBytesCleared")?,
1576        })
1577    }
1578}
1579
1580fn option_nat_u64(obj: Obj<'_>) -> lean_rs::LeanResult<Option<u64>> {
1581    match sum_tag(&obj)? {
1582        0 => Ok(None),
1583        1 => {
1584            let [value] = take_ctor_objects::<1>(obj, 1, "Option::some Nat")?;
1585            Ok(Some(nat::try_to_u64(value)?))
1586        }
1587        other => Err(conversion_error(format!(
1588            "expected Lean Option Nat ctor (tag 0..=1), found tag {other}"
1589        ))),
1590    }
1591}
1592
1593fn bool_tail(obj: &Obj<'_>, offset: u32, label: &str) -> lean_rs::LeanResult<bool> {
1594    let ctor = view(obj).ctor()?;
1595    if ctor.tag() != 0 {
1596        return Err(conversion_error(format!(
1597            "expected Lean {label} constructor tag 0, found tag {}",
1598            ctor.tag()
1599        )));
1600    }
1601    ctor.bool(offset, label)
1602}
1603
1604fn sum_tag(obj: &Obj<'_>) -> lean_rs::LeanResult<u8> {
1605    view(obj).sum_tag()
1606}
lean_rs_host/host/process/query.rs

lean_rs_host/host/process/
query.rs
