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

lean_rs_host/host/process/
query.rs
