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/// One selector inside a batched module-processing request.
58#[derive(Clone, Debug, Eq, PartialEq)]
59pub enum ModuleQuerySelector {
60    Diagnostics {
61        id: String,
62    },
63    ProofState {
64        id: String,
65        line: u32,
66        column: u32,
67    },
68    TypeAt {
69        id: String,
70        line: u32,
71        column: u32,
72    },
73    References {
74        id: String,
75        name: String,
76    },
77    DeclarationTarget {
78        id: String,
79        name: Option<String>,
80        line: Option<u32>,
81        column: Option<u32>,
82    },
83    SurroundingDeclaration {
84        id: String,
85        line: u32,
86        column: u32,
87    },
88}
89
90impl ModuleQuerySelector {
91    #[must_use]
92    pub fn id(&self) -> &str {
93        match self {
94            Self::Diagnostics { id }
95            | Self::ProofState { id, .. }
96            | Self::TypeAt { id, .. }
97            | Self::References { id, .. }
98            | Self::DeclarationTarget { id, .. }
99            | Self::SurroundingDeclaration { id, .. } => id,
100        }
101    }
102}
103
104impl<'lean> IntoLean<'lean> for ModuleQuery {
105    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
106        match self {
107            Self::Diagnostics => 0u8.into_lean(runtime),
108            Self::TypeAt { line, column } => {
109                alloc_ctor_with_objects(runtime, 1, [line.into_lean(runtime), column.into_lean(runtime)])
110            }
111            Self::GoalAt { line, column } => {
112                alloc_ctor_with_objects(runtime, 2, [line.into_lean(runtime), column.into_lean(runtime)])
113            }
114            Self::References { name } => alloc_ctor_with_objects(runtime, 3, [name.into_lean(runtime)]),
115        }
116    }
117}
118
119impl<'lean> IntoLean<'lean> for ModuleQueryOutputBudgets {
120    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
121        alloc_ctor_with_objects(
122            runtime,
123            0,
124            [
125                self.per_field_bytes.into_lean(runtime),
126                self.total_bytes.into_lean(runtime),
127            ],
128        )
129    }
130}
131
132impl sealed::SealedAbi for ModuleQueryOutputBudgets {}
133
134impl<'lean> LeanAbi<'lean> for ModuleQueryOutputBudgets {
135    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
136
137    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
138        self.into_lean(runtime).into_raw()
139    }
140
141    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
142        Err(conversion_error(
143            "ModuleQueryOutputBudgets cannot decode a Lean call result; it is an argument-only type",
144        ))
145    }
146}
147
148impl sealed::SealedAbi for &ModuleQueryOutputBudgets {}
149
150impl<'lean> LeanAbi<'lean> for &ModuleQueryOutputBudgets {
151    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
152
153    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
154        self.clone().into_lean(runtime).into_raw()
155    }
156
157    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
158        Err(conversion_error(
159            "&ModuleQueryOutputBudgets cannot decode a Lean call result; use ModuleQueryOutputBudgets for owned values",
160        ))
161    }
162}
163
164impl<'lean> IntoLean<'lean> for ModuleQuerySelector {
165    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
166        match self {
167            Self::Diagnostics { id } => alloc_ctor_with_objects(runtime, 0, [id.into_lean(runtime)]),
168            Self::ProofState { id, line, column } => alloc_ctor_with_objects(
169                runtime,
170                1,
171                [
172                    id.into_lean(runtime),
173                    line.into_lean(runtime),
174                    column.into_lean(runtime),
175                ],
176            ),
177            Self::TypeAt { id, line, column } => alloc_ctor_with_objects(
178                runtime,
179                2,
180                [
181                    id.into_lean(runtime),
182                    line.into_lean(runtime),
183                    column.into_lean(runtime),
184                ],
185            ),
186            Self::References { id, name } => {
187                alloc_ctor_with_objects(runtime, 3, [id.into_lean(runtime), name.into_lean(runtime)])
188            }
189            Self::DeclarationTarget { id, name, line, column } => alloc_ctor_with_objects(
190                runtime,
191                4,
192                [
193                    id.into_lean(runtime),
194                    name.into_lean(runtime),
195                    line.into_lean(runtime),
196                    column.into_lean(runtime),
197                ],
198            ),
199            Self::SurroundingDeclaration { id, line, column } => alloc_ctor_with_objects(
200                runtime,
201                5,
202                [
203                    id.into_lean(runtime),
204                    line.into_lean(runtime),
205                    column.into_lean(runtime),
206                ],
207            ),
208        }
209    }
210}
211
212impl<'lean> TryFromLean<'lean> for ModuleQuerySelector {
213    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
214        drop(obj);
215        Err(conversion_error(
216            "ModuleQuerySelector cannot decode a Lean call result; it is an argument-only type",
217        ))
218    }
219}
220
221impl sealed::SealedAbi for ModuleQuerySelector {}
222
223impl<'lean> LeanAbi<'lean> for ModuleQuerySelector {
224    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
225
226    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
227        self.into_lean(runtime).into_raw()
228    }
229
230    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
231        Err(conversion_error(
232            "ModuleQuerySelector cannot decode a Lean call result; it is an argument-only type",
233        ))
234    }
235}
236
237impl sealed::SealedAbi for ModuleQuery {}
238
239impl<'lean> LeanAbi<'lean> for ModuleQuery {
240    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
241
242    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
243        self.into_lean(runtime).into_raw()
244    }
245
246    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
247        Err(conversion_error(
248            "ModuleQuery cannot decode a Lean call result; it is an argument-only type",
249        ))
250    }
251}
252
253impl sealed::SealedAbi for &ModuleQuery {}
254
255impl<'lean> LeanAbi<'lean> for &ModuleQuery {
256    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
257
258    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
259        self.clone().into_lean(runtime).into_raw()
260    }
261
262    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
263        Err(conversion_error(
264            "&ModuleQuery cannot decode a Lean call result; use ModuleQuery for owned values",
265        ))
266    }
267}
268
269/// Source span in the original file. Positions are 1-based.
270#[derive(Clone, Debug, Eq, PartialEq)]
271pub struct ModuleSourceSpan {
272    pub start_line: u32,
273    pub start_column: u32,
274    pub end_line: u32,
275    pub end_column: u32,
276}
277
278impl<'lean> TryFromLean<'lean> for ModuleSourceSpan {
279    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
280        let [sl, sc, el, ec] = take_ctor_objects::<4>(obj, 0, "ModuleSourceSpan")?;
281        Ok(Self {
282            start_line: u32::try_from_lean(sl)?,
283            start_column: u32::try_from_lean(sc)?,
284            end_line: u32::try_from_lean(el)?,
285            end_column: u32::try_from_lean(ec)?,
286        })
287    }
288}
289
290/// Bounded rendered Lean text.
291#[derive(Clone, Debug, Eq, PartialEq)]
292pub struct RenderedInfo {
293    pub value: String,
294    pub truncated: bool,
295}
296
297impl<'lean> TryFromLean<'lean> for RenderedInfo {
298    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
299        let truncated = bool_tail(&obj, 0, "RenderedInfo.truncated")?;
300        let [value] = take_ctor_objects::<1>(obj, 0, "RenderedInfo")?;
301        Ok(Self {
302            value: String::try_from_lean(value)?,
303            truncated,
304        })
305    }
306}
307
308/// One identifier occurrence the elaborator recorded.
309#[derive(Clone, Debug, Eq, PartialEq)]
310pub struct NameRefNode {
311    pub start_line: u32,
312    pub start_column: u32,
313    pub end_line: u32,
314    pub end_column: u32,
315    pub name: String,
316    pub is_binder: bool,
317}
318
319impl<'lean> TryFromLean<'lean> for NameRefNode {
320    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
321        let is_binder = bool_tail(&obj, 0, "NameRefNode.isBinder")?;
322        let [sl, sc, el, ec, nm] = take_ctor_objects::<5>(obj, 0, "NameRefNode")?;
323        Ok(Self {
324            start_line: u32::try_from_lean(sl)?,
325            start_column: u32::try_from_lean(sc)?,
326            end_line: u32::try_from_lean(el)?,
327            end_column: u32::try_from_lean(ec)?,
328            name: String::try_from_lean(nm)?,
329            is_binder,
330        })
331    }
332}
333
334/// Result for [`ModuleQuery::TypeAt`].
335#[derive(Clone, Debug, Eq, PartialEq)]
336pub enum TypeAtResult {
337    Term {
338        span: ModuleSourceSpan,
339        expr: RenderedInfo,
340        type_str: RenderedInfo,
341        expected_type: Option<RenderedInfo>,
342    },
343    NoTerm,
344}
345
346impl<'lean> TryFromLean<'lean> for TypeAtResult {
347    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
348        match sum_tag(&obj)? {
349            0 => {
350                let [span, expr, type_str, expected_type] = take_ctor_objects::<4>(obj, 0, "TypeAtResult::term")?;
351                Ok(Self::Term {
352                    span: ModuleSourceSpan::try_from_lean(span)?,
353                    expr: RenderedInfo::try_from_lean(expr)?,
354                    type_str: RenderedInfo::try_from_lean(type_str)?,
355                    expected_type: Option::<RenderedInfo>::try_from_lean(expected_type)?,
356                })
357            }
358            1 => Ok(Self::NoTerm),
359            other => Err(conversion_error(format!(
360                "expected Lean TypeAtResult ctor (tag 0..=1), found tag {other}"
361            ))),
362        }
363    }
364}
365
366/// Result for [`ModuleQuery::GoalAt`].
367#[derive(Clone, Debug, Eq, PartialEq)]
368pub enum GoalAtResult {
369    Goal {
370        span: ModuleSourceSpan,
371        goals_before: Vec<String>,
372        goals_after: Vec<String>,
373        truncated: bool,
374    },
375    NoTacticContext,
376}
377
378impl<'lean> TryFromLean<'lean> for GoalAtResult {
379    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
380        match sum_tag(&obj)? {
381            0 => {
382                let truncated = bool_tail(&obj, 0, "GoalAtResult::goal.truncated")?;
383                let [span, before, after] = take_ctor_objects::<3>(obj, 0, "GoalAtResult::goal")?;
384                Ok(Self::Goal {
385                    span: ModuleSourceSpan::try_from_lean(span)?,
386                    goals_before: Vec::<String>::try_from_lean(before)?,
387                    goals_after: Vec::<String>::try_from_lean(after)?,
388                    truncated,
389                })
390            }
391            1 => Ok(Self::NoTacticContext),
392            other => Err(conversion_error(format!(
393                "expected Lean GoalAtResult ctor (tag 0..=1), found tag {other}"
394            ))),
395        }
396    }
397}
398
399/// Result for [`ModuleQuery::References`].
400#[derive(Clone, Debug, Eq, PartialEq)]
401pub struct ReferencesResult {
402    pub references: Vec<NameRefNode>,
403    pub truncated: bool,
404}
405
406impl<'lean> TryFromLean<'lean> for ReferencesResult {
407    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
408        let truncated = bool_tail(&obj, 0, "ReferencesResult.truncated")?;
409        let [references] = take_ctor_objects::<1>(obj, 0, "ReferencesResult")?;
410        Ok(Self {
411            references: Vec::<NameRefNode>::try_from_lean(references)?,
412            truncated,
413        })
414    }
415}
416
417/// One rendered local declaration in a proof-state result.
418#[derive(Clone, Debug, Eq, PartialEq)]
419pub struct LocalInfo {
420    pub name: String,
421    pub binder_info: String,
422    pub type_str: RenderedInfo,
423    pub value: Option<RenderedInfo>,
424}
425
426impl<'lean> TryFromLean<'lean> for LocalInfo {
427    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
428        let [name, binder_info, type_str, value] = take_ctor_objects::<4>(obj, 0, "LocalInfo")?;
429        Ok(Self {
430            name: String::try_from_lean(name)?,
431            binder_info: String::try_from_lean(binder_info)?,
432            type_str: RenderedInfo::try_from_lean(type_str)?,
433            value: Option::<RenderedInfo>::try_from_lean(value)?,
434        })
435    }
436}
437
438/// Source metadata for the declaration surrounding a proof-agent query.
439#[derive(Clone, Debug, Eq, PartialEq)]
440pub struct DeclarationTargetInfo {
441    pub short_name: String,
442    pub declaration_name: String,
443    pub namespace_name: String,
444    pub declaration_kind: String,
445    pub declaration_span: ModuleSourceSpan,
446    pub name_span: ModuleSourceSpan,
447    pub body_span: ModuleSourceSpan,
448}
449
450impl<'lean> TryFromLean<'lean> for DeclarationTargetInfo {
451    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
452        let [
453            short_name,
454            declaration_name,
455            namespace_name,
456            declaration_kind,
457            declaration_span,
458            name_span,
459            body_span,
460        ] = take_ctor_objects::<7>(obj, 0, "DeclarationTargetInfo")?;
461        Ok(Self {
462            short_name: String::try_from_lean(short_name)?,
463            declaration_name: String::try_from_lean(declaration_name)?,
464            namespace_name: String::try_from_lean(namespace_name)?,
465            declaration_kind: String::try_from_lean(declaration_kind)?,
466            declaration_span: ModuleSourceSpan::try_from_lean(declaration_span)?,
467            name_span: ModuleSourceSpan::try_from_lean(name_span)?,
468            body_span: ModuleSourceSpan::try_from_lean(body_span)?,
469        })
470    }
471}
472
473/// Result for [`ModuleQuerySelector::DeclarationTarget`].
474#[derive(Clone, Debug, Eq, PartialEq)]
475pub enum DeclarationTargetResult {
476    Target(DeclarationTargetInfo),
477    NotFound,
478    Ambiguous(Vec<DeclarationTargetInfo>),
479}
480
481impl<'lean> TryFromLean<'lean> for DeclarationTargetResult {
482    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
483        match sum_tag(&obj)? {
484            0 => {
485                let [info] = take_ctor_objects::<1>(obj, 0, "DeclarationTargetResult::target")?;
486                Ok(Self::Target(DeclarationTargetInfo::try_from_lean(info)?))
487            }
488            1 => Ok(Self::NotFound),
489            2 => {
490                let [candidates] = take_ctor_objects::<1>(obj, 2, "DeclarationTargetResult::ambiguous")?;
491                Ok(Self::Ambiguous(Vec::<DeclarationTargetInfo>::try_from_lean(
492                    candidates,
493                )?))
494            }
495            other => Err(conversion_error(format!(
496                "expected Lean DeclarationTargetResult ctor (tag 0..=2), found tag {other}"
497            ))),
498        }
499    }
500}
501
502/// Proof-state payload for one cursor.
503#[derive(Clone, Debug, Eq, PartialEq)]
504pub struct ProofStateInfo {
505    pub declaration_name: Option<String>,
506    pub namespace_name: String,
507    pub safe_edit: Option<DeclarationTargetInfo>,
508    pub span: ModuleSourceSpan,
509    pub goals_before: Vec<String>,
510    pub goals_after: Vec<String>,
511    pub locals: Vec<LocalInfo>,
512    pub expected_type: Option<RenderedInfo>,
513    pub truncated: bool,
514}
515
516impl<'lean> TryFromLean<'lean> for ProofStateInfo {
517    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
518        let truncated = bool_tail(&obj, 0, "ProofStateInfo.truncated")?;
519        let [
520            declaration_name,
521            namespace_name,
522            safe_edit,
523            span,
524            goals_before,
525            goals_after,
526            locals,
527            expected_type,
528        ] = take_ctor_objects::<8>(obj, 0, "ProofStateInfo")?;
529        Ok(Self {
530            declaration_name: Option::<String>::try_from_lean(declaration_name)?,
531            namespace_name: String::try_from_lean(namespace_name)?,
532            safe_edit: Option::<DeclarationTargetInfo>::try_from_lean(safe_edit)?,
533            span: ModuleSourceSpan::try_from_lean(span)?,
534            goals_before: Vec::<String>::try_from_lean(goals_before)?,
535            goals_after: Vec::<String>::try_from_lean(goals_after)?,
536            locals: Vec::<LocalInfo>::try_from_lean(locals)?,
537            expected_type: Option::<RenderedInfo>::try_from_lean(expected_type)?,
538            truncated,
539        })
540    }
541}
542
543/// Result for [`ModuleQuerySelector::ProofState`].
544#[derive(Clone, Debug, Eq, PartialEq)]
545pub enum ProofStateResult {
546    State(Box<ProofStateInfo>),
547    Unavailable { message: String },
548}
549
550impl<'lean> TryFromLean<'lean> for ProofStateResult {
551    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
552        match sum_tag(&obj)? {
553            0 => {
554                let [info] = take_ctor_objects::<1>(obj, 0, "ProofStateResult::state")?;
555                Ok(Self::State(Box::new(ProofStateInfo::try_from_lean(info)?)))
556            }
557            1 => {
558                let [message] = take_ctor_objects::<1>(obj, 1, "ProofStateResult::unavailable")?;
559                Ok(Self::Unavailable {
560                    message: String::try_from_lean(message)?,
561                })
562            }
563            other => Err(conversion_error(format!(
564                "expected Lean ProofStateResult ctor (tag 0..=1), found tag {other}"
565            ))),
566        }
567    }
568}
569
570/// Result for [`ModuleQuerySelector::SurroundingDeclaration`].
571#[derive(Clone, Debug, Eq, PartialEq)]
572pub enum SurroundingDeclarationResult {
573    Declaration(DeclarationTargetInfo),
574    None,
575}
576
577impl<'lean> TryFromLean<'lean> for SurroundingDeclarationResult {
578    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
579        match sum_tag(&obj)? {
580            0 => {
581                let [info] = take_ctor_objects::<1>(obj, 0, "SurroundingDeclarationResult::declaration")?;
582                Ok(Self::Declaration(DeclarationTargetInfo::try_from_lean(info)?))
583            }
584            1 => Ok(Self::None),
585            other => Err(conversion_error(format!(
586                "expected Lean SurroundingDeclarationResult ctor (tag 0..=1), found tag {other}"
587            ))),
588        }
589    }
590}
591
592/// Typed payload returned by a successful module query.
593#[derive(Clone, Debug)]
594pub enum ModuleQueryResult {
595    Diagnostics(LeanElabFailure),
596    TypeAt(TypeAtResult),
597    GoalAt(GoalAtResult),
598    References(ReferencesResult),
599}
600
601impl<'lean> TryFromLean<'lean> for ModuleQueryResult {
602    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
603        match sum_tag(&obj)? {
604            0 => {
605                let [failure] = take_ctor_objects::<1>(obj, 0, "ModuleQueryResult::diagnostics")?;
606                Ok(Self::Diagnostics(LeanElabFailure::try_from_lean(failure)?))
607            }
608            1 => {
609                let [result] = take_ctor_objects::<1>(obj, 1, "ModuleQueryResult::typeAt")?;
610                Ok(Self::TypeAt(TypeAtResult::try_from_lean(result)?))
611            }
612            2 => {
613                let [result] = take_ctor_objects::<1>(obj, 2, "ModuleQueryResult::goalAt")?;
614                Ok(Self::GoalAt(GoalAtResult::try_from_lean(result)?))
615            }
616            3 => {
617                let [result] = take_ctor_objects::<1>(obj, 3, "ModuleQueryResult::references")?;
618                Ok(Self::References(ReferencesResult::try_from_lean(result)?))
619            }
620            other => Err(conversion_error(format!(
621                "expected Lean ModuleQueryResult ctor (tag 0..=3), found tag {other}"
622            ))),
623        }
624    }
625}
626
627/// Typed payload returned by one successful batch selector.
628#[derive(Clone, Debug)]
629pub enum ModuleQueryBatchResult {
630    Diagnostics(LeanElabFailure),
631    ProofState(ProofStateResult),
632    TypeAt(TypeAtResult),
633    References(ReferencesResult),
634    DeclarationTarget(DeclarationTargetResult),
635    SurroundingDeclaration(SurroundingDeclarationResult),
636}
637
638impl<'lean> TryFromLean<'lean> for ModuleQueryBatchResult {
639    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
640        match sum_tag(&obj)? {
641            0 => {
642                let [failure] = take_ctor_objects::<1>(obj, 0, "ModuleQueryBatchResult::diagnostics")?;
643                Ok(Self::Diagnostics(LeanElabFailure::try_from_lean(failure)?))
644            }
645            1 => {
646                let [result] = take_ctor_objects::<1>(obj, 1, "ModuleQueryBatchResult::proofState")?;
647                Ok(Self::ProofState(ProofStateResult::try_from_lean(result)?))
648            }
649            2 => {
650                let [result] = take_ctor_objects::<1>(obj, 2, "ModuleQueryBatchResult::typeAt")?;
651                Ok(Self::TypeAt(TypeAtResult::try_from_lean(result)?))
652            }
653            3 => {
654                let [result] = take_ctor_objects::<1>(obj, 3, "ModuleQueryBatchResult::references")?;
655                Ok(Self::References(ReferencesResult::try_from_lean(result)?))
656            }
657            4 => {
658                let [result] = take_ctor_objects::<1>(obj, 4, "ModuleQueryBatchResult::declarationTarget")?;
659                Ok(Self::DeclarationTarget(DeclarationTargetResult::try_from_lean(result)?))
660            }
661            5 => {
662                let [result] = take_ctor_objects::<1>(obj, 5, "ModuleQueryBatchResult::surroundingDeclaration")?;
663                Ok(Self::SurroundingDeclaration(
664                    SurroundingDeclarationResult::try_from_lean(result)?,
665                ))
666            }
667            other => Err(conversion_error(format!(
668                "expected Lean ModuleQueryBatchResult ctor (tag 0..=5), found tag {other}"
669            ))),
670        }
671    }
672}
673
674/// One selector result in a batched module query.
675#[derive(Clone, Debug)]
676pub enum ModuleQueryBatchItem {
677    Ok {
678        id: String,
679        result: Box<ModuleQueryBatchResult>,
680    },
681    Unavailable {
682        id: String,
683        message: String,
684    },
685    BudgetExceeded {
686        id: String,
687        message: String,
688    },
689}
690
691impl ModuleQueryBatchItem {
692    #[must_use]
693    pub fn id(&self) -> &str {
694        match self {
695            Self::Ok { id, .. } | Self::Unavailable { id, .. } | Self::BudgetExceeded { id, .. } => id,
696        }
697    }
698}
699
700impl<'lean> TryFromLean<'lean> for ModuleQueryBatchItem {
701    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
702        match sum_tag(&obj)? {
703            0 => {
704                let [id, result] = take_ctor_objects::<2>(obj, 0, "ModuleQueryBatchItem::ok")?;
705                Ok(Self::Ok {
706                    id: String::try_from_lean(id)?,
707                    result: Box::new(ModuleQueryBatchResult::try_from_lean(result)?),
708                })
709            }
710            1 => {
711                let [id, message] = take_ctor_objects::<2>(obj, 1, "ModuleQueryBatchItem::unavailable")?;
712                Ok(Self::Unavailable {
713                    id: String::try_from_lean(id)?,
714                    message: String::try_from_lean(message)?,
715                })
716            }
717            2 => {
718                let [id, message] = take_ctor_objects::<2>(obj, 2, "ModuleQueryBatchItem::budgetExceeded")?;
719                Ok(Self::BudgetExceeded {
720                    id: String::try_from_lean(id)?,
721                    message: String::try_from_lean(message)?,
722                })
723            }
724            other => Err(conversion_error(format!(
725                "expected Lean ModuleQueryBatchItem ctor (tag 0..=2), found tag {other}"
726            ))),
727        }
728    }
729}
730
731/// Successful batch selector envelope.
732#[derive(Clone, Debug)]
733pub struct ModuleQueryBatchEnvelope {
734    pub items: Vec<ModuleQueryBatchItem>,
735    pub total_truncated: bool,
736}
737
738impl<'lean> TryFromLean<'lean> for ModuleQueryBatchEnvelope {
739    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
740        let total_truncated = bool_tail(&obj, 0, "ModuleQueryBatchEnvelope.totalTruncated")?;
741        let [items] = take_ctor_objects::<1>(obj, 0, "ModuleQueryBatchEnvelope")?;
742        Ok(Self {
743            items: Vec::<ModuleQueryBatchItem>::try_from_lean(items)?,
744            total_truncated,
745        })
746    }
747}
748
749/// Worker-side module snapshot cache status for a batched module query.
750#[derive(Clone, Copy, Debug, Eq, PartialEq)]
751pub enum ModuleQueryCacheStatus {
752    Hit,
753    Miss,
754    Rebuilt,
755    Evicted,
756}
757
758impl<'lean> TryFromLean<'lean> for ModuleQueryCacheStatus {
759    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
760        match sum_tag(&obj)? {
761            0 => Ok(Self::Hit),
762            1 => Ok(Self::Miss),
763            2 => Ok(Self::Rebuilt),
764            3 => Ok(Self::Evicted),
765            other => Err(conversion_error(format!(
766                "expected Lean ModuleQueryCacheStatus ctor (tag 0..=3), found tag {other}"
767            ))),
768        }
769    }
770}
771
772impl ModuleQueryCacheStatus {
773    fn from_scalar_tail(byte: u8) -> lean_rs::LeanResult<Self> {
774        match byte {
775            0 => Ok(Self::Hit),
776            1 => Ok(Self::Miss),
777            2 => Ok(Self::Rebuilt),
778            3 => Ok(Self::Evicted),
779            other => Err(conversion_error(format!(
780                "expected Lean ModuleQueryCacheStatus scalar tag 0..=3, found {other}"
781            ))),
782        }
783    }
784}
785
786/// Phase timings for cached batched module queries, in microseconds.
787#[derive(Clone, Debug, Eq, PartialEq)]
788pub struct ModuleQueryTimings {
789    pub header_import_micros: u64,
790    pub elaboration_micros: u64,
791    pub projection_micros: u64,
792    pub rendering_micros: u64,
793}
794
795impl<'lean> TryFromLean<'lean> for ModuleQueryTimings {
796    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
797        let ctor = view(&obj).ctor_shape(0, 0, "ModuleQueryTimings")?;
798        Ok(Self {
799            header_import_micros: ctor.uint64(0, "ModuleQueryTimings.headerImportMicros")?,
800            elaboration_micros: ctor.uint64(8, "ModuleQueryTimings.elaborationMicros")?,
801            projection_micros: ctor.uint64(16, "ModuleQueryTimings.projectionMicros")?,
802            rendering_micros: ctor.uint64(24, "ModuleQueryTimings.renderingMicros")?,
803        })
804    }
805}
806
807/// Cache and timing facts attached to cached batched module-query outcomes.
808#[derive(Clone, Debug, Eq, PartialEq)]
809pub struct ModuleQueryCacheFacts {
810    pub cache_status: ModuleQueryCacheStatus,
811    pub timings: ModuleQueryTimings,
812    pub output_bytes: u64,
813    pub cache_entry_count: Option<u64>,
814    pub cache_approx_bytes: Option<u64>,
815}
816
817impl<'lean> TryFromLean<'lean> for ModuleQueryCacheFacts {
818    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
819        let ctor = view(&obj).ctor_shape(0, 3, "ModuleQueryCacheFacts")?;
820        let output_bytes = ctor.uint64(0, "ModuleQueryCacheFacts.outputBytes")?;
821        let cache_status = ctor.uint8(8, "ModuleQueryCacheFacts.cacheStatus")?;
822        let [timings, cache_entry_count, cache_approx_bytes] = take_ctor_objects::<3>(obj, 0, "ModuleQueryCacheFacts")?;
823        Ok(Self {
824            cache_status: ModuleQueryCacheStatus::from_scalar_tail(cache_status)?,
825            timings: ModuleQueryTimings::try_from_lean(timings)?,
826            output_bytes,
827            cache_entry_count: option_nat_u64(cache_entry_count)?,
828            cache_approx_bytes: option_nat_u64(cache_approx_bytes)?,
829        })
830    }
831}
832
833/// Cache policy passed to the Lean-side module snapshot cache.
834#[derive(Clone, Debug, Eq, PartialEq)]
835pub struct ModuleQueryCachePolicy {
836    pub file_identity: String,
837    pub key: String,
838    pub max_entries: u64,
839    pub ttl_millis: u64,
840    pub max_bytes: u64,
841}
842
843/// Header-aware module-query outcome.
844#[derive(Clone, Debug)]
845pub enum ModuleQueryOutcome {
846    Ok {
847        result: ModuleQueryResult,
848        imports: Vec<String>,
849    },
850    MissingImports {
851        result: ModuleQueryResult,
852        imports: Vec<String>,
853        missing: Vec<String>,
854    },
855    HeaderParseFailed {
856        diagnostics: LeanElabFailure,
857    },
858    Unsupported,
859}
860
861impl<'lean> TryFromLean<'lean> for ModuleQueryOutcome {
862    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
863        match sum_tag(&obj)? {
864            0 => {
865                let [result, imports] = take_ctor_objects::<2>(obj, 0, "ModuleQueryOutcome::ok")?;
866                Ok(Self::Ok {
867                    result: ModuleQueryResult::try_from_lean(result)?,
868                    imports: Vec::<String>::try_from_lean(imports)?,
869                })
870            }
871            1 => {
872                let [result, imports, missing] = take_ctor_objects::<3>(obj, 1, "ModuleQueryOutcome::missingImports")?;
873                Ok(Self::MissingImports {
874                    result: ModuleQueryResult::try_from_lean(result)?,
875                    imports: Vec::<String>::try_from_lean(imports)?,
876                    missing: Vec::<String>::try_from_lean(missing)?,
877                })
878            }
879            2 => {
880                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ModuleQueryOutcome::headerParseFailed")?;
881                Ok(Self::HeaderParseFailed {
882                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
883                })
884            }
885            3 => Ok(Self::Unsupported),
886            other => Err(conversion_error(format!(
887                "expected Lean ModuleQueryOutcome ctor (tag 0..=3), found tag {other}"
888            ))),
889        }
890    }
891}
892
893/// Header-aware batched module-query outcome.
894#[derive(Clone, Debug)]
895pub enum ModuleQueryBatchOutcome {
896    Ok {
897        result: ModuleQueryBatchEnvelope,
898        imports: Vec<String>,
899    },
900    MissingImports {
901        result: ModuleQueryBatchEnvelope,
902        imports: Vec<String>,
903        missing: Vec<String>,
904    },
905    HeaderParseFailed {
906        diagnostics: LeanElabFailure,
907    },
908    Unsupported,
909}
910
911impl<'lean> TryFromLean<'lean> for ModuleQueryBatchOutcome {
912    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
913        match sum_tag(&obj)? {
914            0 => {
915                let [result, imports] = take_ctor_objects::<2>(obj, 0, "ModuleQueryBatchOutcome::ok")?;
916                Ok(Self::Ok {
917                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
918                    imports: Vec::<String>::try_from_lean(imports)?,
919                })
920            }
921            1 => {
922                let [result, imports, missing] =
923                    take_ctor_objects::<3>(obj, 1, "ModuleQueryBatchOutcome::missingImports")?;
924                Ok(Self::MissingImports {
925                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
926                    imports: Vec::<String>::try_from_lean(imports)?,
927                    missing: Vec::<String>::try_from_lean(missing)?,
928                })
929            }
930            2 => {
931                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ModuleQueryBatchOutcome::headerParseFailed")?;
932                Ok(Self::HeaderParseFailed {
933                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
934                })
935            }
936            3 => Ok(Self::Unsupported),
937            other => Err(conversion_error(format!(
938                "expected Lean ModuleQueryBatchOutcome ctor (tag 0..=3), found tag {other}"
939            ))),
940        }
941    }
942}
943
944/// Header-aware batched module-query outcome with cache/timing facts.
945#[derive(Clone, Debug)]
946pub enum ModuleQueryBatchCachedOutcome {
947    Ok {
948        result: ModuleQueryBatchEnvelope,
949        imports: Vec<String>,
950        facts: ModuleQueryCacheFacts,
951    },
952    MissingImports {
953        result: ModuleQueryBatchEnvelope,
954        imports: Vec<String>,
955        missing: Vec<String>,
956        facts: ModuleQueryCacheFacts,
957    },
958    HeaderParseFailed {
959        diagnostics: LeanElabFailure,
960        facts: ModuleQueryCacheFacts,
961    },
962    Unsupported,
963}
964
965impl<'lean> TryFromLean<'lean> for ModuleQueryBatchCachedOutcome {
966    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
967        match sum_tag(&obj)? {
968            0 => {
969                let [result, imports, facts] = take_ctor_objects::<3>(obj, 0, "ModuleQueryBatchCachedOutcome::ok")?;
970                Ok(Self::Ok {
971                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
972                    imports: Vec::<String>::try_from_lean(imports)?,
973                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
974                })
975            }
976            1 => {
977                let [result, imports, missing, facts] =
978                    take_ctor_objects::<4>(obj, 1, "ModuleQueryBatchCachedOutcome::missingImports")?;
979                Ok(Self::MissingImports {
980                    result: ModuleQueryBatchEnvelope::try_from_lean(result)?,
981                    imports: Vec::<String>::try_from_lean(imports)?,
982                    missing: Vec::<String>::try_from_lean(missing)?,
983                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
984                })
985            }
986            2 => {
987                let [diagnostics, facts] =
988                    take_ctor_objects::<2>(obj, 2, "ModuleQueryBatchCachedOutcome::headerParseFailed")?;
989                Ok(Self::HeaderParseFailed {
990                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
991                    facts: ModuleQueryCacheFacts::try_from_lean(facts)?,
992                })
993            }
994            3 => Ok(Self::Unsupported),
995            other => Err(conversion_error(format!(
996                "expected Lean ModuleQueryBatchCachedOutcome ctor (tag 0..=3), found tag {other}"
997            ))),
998        }
999    }
1000}
1001
1002/// Result of clearing the Lean-side module snapshot cache.
1003#[derive(Clone, Debug, Eq, PartialEq)]
1004pub struct ModuleSnapshotCacheClearResult {
1005    pub entries_cleared: u64,
1006    pub approx_bytes_cleared: u64,
1007}
1008
1009impl<'lean> TryFromLean<'lean> for ModuleSnapshotCacheClearResult {
1010    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
1011        let ctor = view(&obj).ctor_shape(0, 0, "ModuleSnapshotCacheClearResult")?;
1012        Ok(Self {
1013            entries_cleared: ctor.uint64(0, "ModuleSnapshotCacheClearResult.entriesCleared")?,
1014            approx_bytes_cleared: ctor.uint64(8, "ModuleSnapshotCacheClearResult.approxBytesCleared")?,
1015        })
1016    }
1017}
1018
1019fn option_nat_u64(obj: Obj<'_>) -> lean_rs::LeanResult<Option<u64>> {
1020    match sum_tag(&obj)? {
1021        0 => Ok(None),
1022        1 => {
1023            let [value] = take_ctor_objects::<1>(obj, 1, "Option::some Nat")?;
1024            Ok(Some(nat::try_to_u64(value)?))
1025        }
1026        other => Err(conversion_error(format!(
1027            "expected Lean Option Nat ctor (tag 0..=1), found tag {other}"
1028        ))),
1029    }
1030}
1031
1032fn bool_tail(obj: &Obj<'_>, offset: u32, label: &str) -> lean_rs::LeanResult<bool> {
1033    let ctor = view(obj).ctor()?;
1034    if ctor.tag() != 0 {
1035        return Err(conversion_error(format!(
1036            "expected Lean {label} constructor tag 0, found tag {}",
1037            ctor.tag()
1038        )));
1039    }
1040    ctor.bool(offset, label)
1041}
1042
1043fn sum_tag(obj: &Obj<'_>) -> lean_rs::LeanResult<u8> {
1044    view(obj).sum_tag()
1045}
lean_rs_host/host/process/query.rs

lean_rs_host/host/process/
query.rs
