lean_rs_host/host/
declaration_search.rs

1//! Structured declaration search bridge for the bundled host shim.
2//!
3//! Lean owns the environment scan because it can inspect `ConstantInfo`
4//! without rendering types. Rust only encodes the request policy and decodes
5//! bounded rows plus fanout facts.
6
7use lean_rs::abi::nat;
8use lean_rs::abi::structure::{alloc_ctor_with_objects, take_ctor_objects, view};
9use lean_rs::abi::traits::{IntoLean, LeanAbi, TryFromLean, conversion_error, sealed};
10use lean_rs::{LeanRuntime, Obj};
11use lean_toolchain::LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX;
12
13use crate::host::session::{LeanDeclarationFilter, LeanSourceRange};
14
15#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
16pub enum DeclarationNameMatch {
17    #[default]
18    Contains,
19    Suffix,
20}
21
22#[derive(Clone, Copy, Debug, Eq, PartialEq)]
23pub enum DeclarationSearchScope {
24    Namespace,
25    Module,
26}
27
28#[derive(Clone, Debug, Eq, PartialEq)]
29pub struct DeclarationSearchBias {
30    pub scope: DeclarationSearchScope,
31    pub prefix: String,
32    pub strict: bool,
33    pub weight: i32,
34}
35
36#[derive(Clone, Debug, Eq, PartialEq)]
37pub struct DeclarationSearchRequest {
38    pub name_fragment: Option<String>,
39    pub name_match: DeclarationNameMatch,
40    pub kind: Option<String>,
41    pub required_constants: Vec<String>,
42    pub conclusion_head: Option<String>,
43    pub scope_biases: Vec<DeclarationSearchBias>,
44    pub limit: usize,
45    pub filter: LeanDeclarationFilter,
46    pub include_source: bool,
47}
48
49impl DeclarationSearchRequest {
50    #[must_use]
51    pub fn new(name_fragment: impl Into<String>) -> Self {
52        Self {
53            name_fragment: Some(name_fragment.into()),
54            name_match: DeclarationNameMatch::Contains,
55            kind: None,
56            required_constants: Vec::new(),
57            conclusion_head: None,
58            scope_biases: Vec::new(),
59            limit: 20,
60            filter: LeanDeclarationFilter {
61                include_private: false,
62                include_generated: false,
63                include_internal: false,
64            },
65            include_source: true,
66        }
67    }
68}
69
70#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
71pub struct DeclarationFlags {
72    pub is_private: bool,
73    pub is_generated: bool,
74    pub is_internal: bool,
75}
76
77#[derive(Clone, Debug, Eq, PartialEq)]
78pub struct DeclarationSearchRow {
79    pub name: String,
80    pub kind: String,
81    pub module: Option<String>,
82    pub source: Option<LeanSourceRange>,
83    pub match_reason: String,
84    pub score: i32,
85    pub rank: usize,
86    pub flags: DeclarationFlags,
87}
88
89#[derive(Clone, Debug, Eq, PartialEq)]
90pub struct DeclarationSearchPruning {
91    pub stage: String,
92    pub reason: String,
93    pub count: usize,
94}
95
96#[derive(Clone, Debug, Default, Eq, PartialEq)]
97pub struct DeclarationSearchTimings {
98    pub scan_micros: u64,
99    pub rank_micros: u64,
100    pub source_micros: u64,
101}
102
103#[derive(Clone, Debug, Default, Eq, PartialEq)]
104pub struct LeanDerivedWorkFacts {
105    pub source_range_lookups: u64,
106    pub docstring_lookups: u64,
107    pub raw_type_renderings: u64,
108    pub pretty_prints: u64,
109    pub proof_search_fact_collections: u64,
110    pub simp_extension_lookups: u64,
111    pub parser_elaborator_runs: u64,
112    pub module_snapshot_builds: u64,
113    pub lazy_discr_tree_import_initialization_observed: bool,
114}
115
116#[derive(Clone, Debug, Default, Eq, PartialEq)]
117pub struct DeclarationSearchFacts {
118    pub declarations_scanned: usize,
119    pub after_name_filter: usize,
120    pub after_kind_filter: usize,
121    pub after_required_constants_filter: usize,
122    pub after_conclusion_filter: usize,
123    pub after_scope_filter: usize,
124    pub source_lookups: usize,
125    pub broad_pruning: Vec<DeclarationSearchPruning>,
126    pub truncated: bool,
127    pub timings: DeclarationSearchTimings,
128    pub derived_work: LeanDerivedWorkFacts,
129}
130
131#[derive(Clone, Debug, Eq, PartialEq)]
132pub struct DeclarationSearchResult {
133    pub declarations: Vec<DeclarationSearchRow>,
134    pub truncated: bool,
135    pub facts: DeclarationSearchFacts,
136}
137
138#[derive(Clone, Copy, Debug, Eq, PartialEq)]
139#[allow(
140    clippy::struct_excessive_bools,
141    reason = "field-selection flags mirror the Lean request shape and are clearer than five tiny enums"
142)]
143pub struct DeclarationInspectionFields {
144    pub source: bool,
145    pub statement: bool,
146    pub docstring: bool,
147    pub attributes: bool,
148    pub flags: bool,
149    /// Render `statement` notation-aware (`pp.universes false`) when `true`,
150    /// falling back to the raw term if the pretty-printer cannot render it;
151    /// the fully-elaborated raw form when `false`.
152    pub statement_pretty: bool,
153    /// Include proof-search-oriented facts such as simp/rw/instance/class.
154    /// Defaults off because these facts may touch persistent extensions and
155    /// lazy derived search indexes.
156    pub proof_search: bool,
157}
158
159impl Default for DeclarationInspectionFields {
160    fn default() -> Self {
161        Self {
162            source: true,
163            statement: true,
164            docstring: true,
165            attributes: true,
166            flags: true,
167            statement_pretty: true,
168            proof_search: false,
169        }
170    }
171}
172
173#[derive(Clone, Copy, Debug, Eq, PartialEq)]
174pub struct DeclarationInspectionBudgets {
175    /// Maximum UTF-8 bytes for one rendered field.
176    pub per_field_bytes: u32,
177    /// Maximum UTF-8 bytes for all rendered fields in the inspection.
178    pub total_bytes: u32,
179}
180
181impl Default for DeclarationInspectionBudgets {
182    fn default() -> Self {
183        Self {
184            per_field_bytes: 8 * 1024,
185            total_bytes: 64 * 1024,
186        }
187    }
188}
189
190impl DeclarationInspectionBudgets {
191    /// Construct the default inspection budget bundle.
192    #[must_use]
193    pub fn new() -> Self {
194        Self::default()
195    }
196
197    /// Replace the per-field byte budget, saturating at
198    /// [`LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX`].
199    #[must_use]
200    pub fn per_field_bytes(mut self, bytes: u32) -> Self {
201        self.per_field_bytes = clamp_output_budget(bytes);
202        self
203    }
204
205    /// Replace the total inspection byte budget, saturating at
206    /// [`LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX`].
207    #[must_use]
208    pub fn total_bytes(mut self, bytes: u32) -> Self {
209        self.total_bytes = clamp_output_budget(bytes);
210        self
211    }
212
213    fn normalized(self) -> Self {
214        Self {
215            per_field_bytes: clamp_output_budget(self.per_field_bytes),
216            total_bytes: clamp_output_budget(self.total_bytes),
217        }
218    }
219}
220
221fn clamp_output_budget(bytes: u32) -> u32 {
222    let max = u32::try_from(LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX).unwrap_or(u32::MAX);
223    bytes.min(max)
224}
225
226#[derive(Clone, Debug, Eq, PartialEq)]
227pub struct DeclarationInspectionRequest {
228    pub name: String,
229    pub fields: DeclarationInspectionFields,
230    pub budgets: DeclarationInspectionBudgets,
231}
232
233impl DeclarationInspectionRequest {
234    #[must_use]
235    pub fn new(name: impl Into<String>) -> Self {
236        Self {
237            name: name.into(),
238            fields: DeclarationInspectionFields::default(),
239            budgets: DeclarationInspectionBudgets::default(),
240        }
241    }
242}
243
244#[derive(Clone, Debug, Eq, PartialEq)]
245pub struct DeclarationRenderedInfo {
246    pub value: String,
247    pub truncated: bool,
248}
249
250#[derive(Clone, Debug, Default, Eq, PartialEq)]
251#[allow(
252    clippy::struct_excessive_bools,
253    reason = "proof-search booleans are independent inspection facts, not control-flow state"
254)]
255pub struct DeclarationProofSearchFacts {
256    pub computed: bool,
257    pub unavailable_reason: Option<String>,
258    pub is_simp: bool,
259    pub is_rw_candidate: bool,
260    pub is_instance: bool,
261    pub is_class: bool,
262    pub class_name: Option<String>,
263}
264
265#[derive(Clone, Debug, Eq, PartialEq)]
266pub struct DeclarationInspection {
267    pub name: String,
268    pub kind: String,
269    pub module: Option<String>,
270    pub source: Option<LeanSourceRange>,
271    pub statement: Option<DeclarationRenderedInfo>,
272    pub docstring: Option<DeclarationRenderedInfo>,
273    pub attributes: Vec<String>,
274    pub proof_search: DeclarationProofSearchFacts,
275    pub flags: DeclarationFlags,
276    pub derived_work: LeanDerivedWorkFacts,
277    /// Rendering that produced `statement`: `Some(true)` = pretty, `Some(false)`
278    /// = raw, `None` when no statement was requested.
279    pub statement_pretty: Option<bool>,
280}
281
282#[derive(Clone, Debug, Eq, PartialEq)]
283pub enum DeclarationInspectionResult {
284    Found { declaration: Box<DeclarationInspection> },
285    NotFound { name: String },
286    Unsupported,
287}
288
289impl<'lean> IntoLean<'lean> for DeclarationNameMatch {
290    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
291        match self {
292            Self::Contains => nat::from_usize(runtime, 0),
293            Self::Suffix => nat::from_usize(runtime, 1),
294        }
295    }
296}
297
298impl<'lean> IntoLean<'lean> for DeclarationSearchScope {
299    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
300        match self {
301            Self::Namespace => nat::from_usize(runtime, 0),
302            Self::Module => nat::from_usize(runtime, 1),
303        }
304    }
305}
306
307fn nat_from_bool(runtime: &LeanRuntime, value: bool) -> Obj<'_> {
308    nat::from_usize(runtime, usize::from(value))
309}
310
311fn bool_from_nat(obj: Obj<'_>) -> lean_rs::LeanResult<bool> {
312    Ok(nat::try_to_usize(obj)? != 0)
313}
314
315impl<'lean> IntoLean<'lean> for DeclarationSearchBias {
316    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
317        alloc_ctor_with_objects(
318            runtime,
319            0,
320            [
321                self.scope.into_lean(runtime),
322                self.prefix.into_lean(runtime),
323                nat_from_bool(runtime, self.strict),
324                self.weight.to_string().into_lean(runtime),
325            ],
326        )
327    }
328}
329
330impl<'lean> IntoLean<'lean> for DeclarationSearchRequest {
331    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
332        alloc_ctor_with_objects(
333            runtime,
334            0,
335            [
336                self.name_fragment.into_lean(runtime),
337                self.name_match.into_lean(runtime),
338                self.kind.into_lean(runtime),
339                self.required_constants.into_lean(runtime),
340                self.conclusion_head.into_lean(runtime),
341                self.scope_biases.into_lean(runtime),
342                nat::from_usize(runtime, self.limit),
343                self.filter.into_lean(runtime),
344                nat_from_bool(runtime, self.include_source),
345            ],
346        )
347    }
348}
349
350impl<'lean> IntoLean<'lean> for DeclarationInspectionFields {
351    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
352        alloc_ctor_with_objects(
353            runtime,
354            0,
355            [
356                nat_from_bool(runtime, self.source),
357                nat_from_bool(runtime, self.statement),
358                nat_from_bool(runtime, self.docstring),
359                nat_from_bool(runtime, self.attributes),
360                nat_from_bool(runtime, self.flags),
361                nat_from_bool(runtime, self.statement_pretty),
362                nat_from_bool(runtime, self.proof_search),
363            ],
364        )
365    }
366}
367
368impl<'lean> IntoLean<'lean> for DeclarationInspectionBudgets {
369    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
370        let normalized = self.normalized();
371        alloc_ctor_with_objects(
372            runtime,
373            0,
374            [
375                nat::from_usize(runtime, normalized.per_field_bytes as usize),
376                nat::from_usize(runtime, normalized.total_bytes as usize),
377            ],
378        )
379    }
380}
381
382impl<'lean> IntoLean<'lean> for DeclarationInspectionRequest {
383    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
384        alloc_ctor_with_objects(
385            runtime,
386            0,
387            [
388                self.name.into_lean(runtime),
389                self.fields.into_lean(runtime),
390                self.budgets.into_lean(runtime),
391            ],
392        )
393    }
394}
395
396impl sealed::SealedAbi for DeclarationInspectionRequest {}
397
398impl<'lean> LeanAbi<'lean> for DeclarationInspectionRequest {
399    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
400
401    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
402        self.into_lean(runtime).into_raw()
403    }
404
405    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
406        Err(conversion_error(
407            "DeclarationInspectionRequest cannot decode a Lean call result; it is an argument-only type",
408        ))
409    }
410}
411
412impl sealed::SealedAbi for &DeclarationInspectionRequest {}
413
414impl<'lean> LeanAbi<'lean> for &DeclarationInspectionRequest {
415    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
416
417    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
418        self.clone().into_lean(runtime).into_raw()
419    }
420
421    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
422        Err(conversion_error(
423            "&DeclarationInspectionRequest cannot decode a Lean call result; use DeclarationInspectionRequest for owned values",
424        ))
425    }
426}
427
428impl sealed::SealedAbi for DeclarationSearchRequest {}
429
430impl<'lean> LeanAbi<'lean> for DeclarationSearchRequest {
431    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
432
433    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
434        self.into_lean(runtime).into_raw()
435    }
436
437    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
438        Err(conversion_error(
439            "DeclarationSearchRequest cannot decode a Lean call result; it is an argument-only type",
440        ))
441    }
442}
443
444impl sealed::SealedAbi for &DeclarationSearchRequest {}
445
446impl<'lean> LeanAbi<'lean> for &DeclarationSearchRequest {
447    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
448
449    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
450        self.clone().into_lean(runtime).into_raw()
451    }
452
453    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
454        Err(conversion_error(
455            "&DeclarationSearchRequest cannot decode a Lean call result; use DeclarationSearchRequest for owned values",
456        ))
457    }
458}
459
460impl<'lean> TryFromLean<'lean> for DeclarationFlags {
461    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
462        let [is_private, is_generated, is_internal] = take_ctor_objects::<3>(obj, 0, "DeclarationFlags")?;
463        Ok(Self {
464            is_private: bool_from_nat(is_private)?,
465            is_generated: bool_from_nat(is_generated)?,
466            is_internal: bool_from_nat(is_internal)?,
467        })
468    }
469}
470
471impl<'lean> TryFromLean<'lean> for DeclarationSearchRow {
472    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
473        let [name, kind, module, source, match_reason, score, rank, flags] =
474            take_ctor_objects::<8>(obj, 0, "DeclarationSearchRow")?;
475        Ok(Self {
476            name: String::try_from_lean(name)?,
477            kind: String::try_from_lean(kind)?,
478            module: Option::<String>::try_from_lean(module)?,
479            source: Option::<LeanSourceRange>::try_from_lean(source)?,
480            match_reason: String::try_from_lean(match_reason)?,
481            score: String::try_from_lean(score)?
482                .parse()
483                .map_err(|_| conversion_error("score does not fit i32"))?,
484            rank: nat::try_to_usize(rank)?,
485            flags: DeclarationFlags::try_from_lean(flags)?,
486        })
487    }
488}
489
490impl<'lean> TryFromLean<'lean> for DeclarationSearchPruning {
491    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
492        let [stage, reason, count] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchPruning")?;
493        Ok(Self {
494            stage: String::try_from_lean(stage)?,
495            reason: String::try_from_lean(reason)?,
496            count: nat::try_to_usize(count)?,
497        })
498    }
499}
500
501impl<'lean> TryFromLean<'lean> for DeclarationSearchTimings {
502    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
503        let [scan_micros, rank_micros, source_micros] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchTimings")?;
504        Ok(Self {
505            scan_micros: nat::try_to_u64(scan_micros)?,
506            rank_micros: nat::try_to_u64(rank_micros)?,
507            source_micros: nat::try_to_u64(source_micros)?,
508        })
509    }
510}
511
512impl<'lean> TryFromLean<'lean> for LeanDerivedWorkFacts {
513    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
514        let [
515            source_range_lookups,
516            docstring_lookups,
517            raw_type_renderings,
518            pretty_prints,
519            proof_search_fact_collections,
520            simp_extension_lookups,
521            parser_elaborator_runs,
522            module_snapshot_builds,
523            lazy_discr_tree_import_initialization_observed,
524        ] = take_ctor_objects::<9>(obj, 0, "DerivedWorkFacts")?;
525        Ok(Self {
526            source_range_lookups: nat::try_to_u64(source_range_lookups)?,
527            docstring_lookups: nat::try_to_u64(docstring_lookups)?,
528            raw_type_renderings: nat::try_to_u64(raw_type_renderings)?,
529            pretty_prints: nat::try_to_u64(pretty_prints)?,
530            proof_search_fact_collections: nat::try_to_u64(proof_search_fact_collections)?,
531            simp_extension_lookups: nat::try_to_u64(simp_extension_lookups)?,
532            parser_elaborator_runs: nat::try_to_u64(parser_elaborator_runs)?,
533            module_snapshot_builds: nat::try_to_u64(module_snapshot_builds)?,
534            lazy_discr_tree_import_initialization_observed: bool_from_nat(
535                lazy_discr_tree_import_initialization_observed,
536            )?,
537        })
538    }
539}
540
541impl<'lean> TryFromLean<'lean> for DeclarationSearchFacts {
542    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
543        let [
544            declarations_scanned,
545            after_name_filter,
546            after_kind_filter,
547            after_required_constants_filter,
548            after_conclusion_filter,
549            after_scope_filter,
550            source_lookups,
551            broad_pruning,
552            truncated,
553            timings,
554            derived_work,
555        ] = take_ctor_objects::<11>(obj, 0, "DeclarationSearchFacts")?;
556        Ok(Self {
557            declarations_scanned: nat::try_to_usize(declarations_scanned)?,
558            after_name_filter: nat::try_to_usize(after_name_filter)?,
559            after_kind_filter: nat::try_to_usize(after_kind_filter)?,
560            after_required_constants_filter: nat::try_to_usize(after_required_constants_filter)?,
561            after_conclusion_filter: nat::try_to_usize(after_conclusion_filter)?,
562            after_scope_filter: nat::try_to_usize(after_scope_filter)?,
563            source_lookups: nat::try_to_usize(source_lookups)?,
564            broad_pruning: Vec::<DeclarationSearchPruning>::try_from_lean(broad_pruning)?,
565            truncated: bool_from_nat(truncated)?,
566            timings: DeclarationSearchTimings::try_from_lean(timings)?,
567            derived_work: LeanDerivedWorkFacts::try_from_lean(derived_work)?,
568        })
569    }
570}
571
572impl<'lean> TryFromLean<'lean> for DeclarationSearchResult {
573    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
574        let [declarations, truncated, facts] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchResult")?;
575        Ok(Self {
576            declarations: Vec::<DeclarationSearchRow>::try_from_lean(declarations)?,
577            truncated: bool_from_nat(truncated)?,
578            facts: DeclarationSearchFacts::try_from_lean(facts)?,
579        })
580    }
581}
582
583impl<'lean> TryFromLean<'lean> for DeclarationRenderedInfo {
584    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
585        let [value, truncated] = take_ctor_objects::<2>(obj, 0, "DeclarationRenderedInfo")?;
586        Ok(Self {
587            value: String::try_from_lean(value)?,
588            truncated: bool_from_nat(truncated)?,
589        })
590    }
591}
592
593impl<'lean> TryFromLean<'lean> for DeclarationProofSearchFacts {
594    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
595        let [
596            computed,
597            unavailable_reason,
598            is_simp,
599            is_rw_candidate,
600            is_instance,
601            is_class,
602            class_name,
603        ] = take_ctor_objects::<7>(obj, 0, "DeclarationProofSearchFacts")?;
604        Ok(Self {
605            computed: bool_from_nat(computed)?,
606            unavailable_reason: Option::<String>::try_from_lean(unavailable_reason)?,
607            is_simp: bool_from_nat(is_simp)?,
608            is_rw_candidate: bool_from_nat(is_rw_candidate)?,
609            is_instance: bool_from_nat(is_instance)?,
610            is_class: bool_from_nat(is_class)?,
611            class_name: Option::<String>::try_from_lean(class_name)?,
612        })
613    }
614}
615
616impl<'lean> TryFromLean<'lean> for DeclarationInspection {
617    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
618        let [
619            name,
620            kind,
621            module,
622            source,
623            statement,
624            docstring,
625            attributes,
626            proof_search,
627            flags,
628            derived_work,
629            statement_rendering,
630        ] = take_ctor_objects::<11>(obj, 0, "DeclarationInspection")?;
631        // `statementRendering : Option Nat` (1 = pretty, 0 = raw) → Option<bool>.
632        let statement_pretty = match view(&statement_rendering).sum_tag()? {
633            0 => None,
634            1 => {
635                let [nat] = take_ctor_objects::<1>(statement_rendering, 1, "DeclarationInspection.statementRendering")?;
636                Some(bool_from_nat(nat)?)
637            }
638            other => {
639                return Err(conversion_error(format!(
640                    "expected Lean Option ctor (tag 0..=1) for statementRendering, found tag {other}"
641                )));
642            }
643        };
644        Ok(Self {
645            name: String::try_from_lean(name)?,
646            kind: String::try_from_lean(kind)?,
647            module: Option::<String>::try_from_lean(module)?,
648            source: Option::<LeanSourceRange>::try_from_lean(source)?,
649            statement: Option::<DeclarationRenderedInfo>::try_from_lean(statement)?,
650            docstring: Option::<DeclarationRenderedInfo>::try_from_lean(docstring)?,
651            attributes: Vec::<String>::try_from_lean(attributes)?,
652            proof_search: DeclarationProofSearchFacts::try_from_lean(proof_search)?,
653            flags: DeclarationFlags::try_from_lean(flags)?,
654            derived_work: LeanDerivedWorkFacts::try_from_lean(derived_work)?,
655            statement_pretty,
656        })
657    }
658}
659
660impl<'lean> TryFromLean<'lean> for DeclarationInspectionResult {
661    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
662        match view(&obj).sum_tag()? {
663            0 => {
664                let [declaration] = take_ctor_objects::<1>(obj, 0, "DeclarationInspectionResult::found")?;
665                Ok(Self::Found {
666                    declaration: Box::new(DeclarationInspection::try_from_lean(declaration)?),
667                })
668            }
669            1 => {
670                let [name] = take_ctor_objects::<1>(obj, 1, "DeclarationInspectionResult::notFound")?;
671                Ok(Self::NotFound {
672                    name: String::try_from_lean(name)?,
673                })
674            }
675            2 => {
676                let [] = take_ctor_objects::<0>(obj, 2, "DeclarationInspectionResult::unsupported")?;
677                Ok(Self::Unsupported)
678            }
679            other => Err(conversion_error(format!(
680                "expected Lean DeclarationInspectionResult ctor (tag 0..=2), found tag {other}"
681            ))),
682        }
683    }
684}
685
686#[cfg(test)]
687mod tests {
688    use super::*;
689
690    #[test]
691    fn declaration_inspection_budget_defaults_match_policy() {
692        let budgets = DeclarationInspectionBudgets::new();
693        assert_eq!(budgets.per_field_bytes, 8 * 1024);
694        assert_eq!(budgets.total_bytes, 64 * 1024);
695    }
696
697    #[test]
698    fn declaration_inspection_budget_setters_saturate() {
699        let budgets = DeclarationInspectionBudgets::new()
700            .per_field_bytes(u32::MAX)
701            .total_bytes(u32::MAX);
702        let max = clamp_output_budget(u32::MAX);
703        assert_eq!(budgets.per_field_bytes, max);
704        assert_eq!(budgets.total_bytes, max);
705    }
706
707    #[test]
708    fn declaration_inspection_budget_normalization_clamps_struct_literals() {
709        let budgets = DeclarationInspectionBudgets {
710            per_field_bytes: u32::MAX,
711            total_bytes: u32::MAX,
712        }
713        .normalized();
714        let max = clamp_output_budget(u32::MAX);
715        assert_eq!(budgets.per_field_bytes, max);
716        assert_eq!(budgets.total_bytes, max);
717    }
718}
lean_rs_host/host/declaration_search.rs

lean_rs_host/host/
declaration_search.rs
