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};
11
12use crate::host::session::{LeanDeclarationFilter, LeanSourceRange};
13
14#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
15pub enum DeclarationNameMatch {
16    #[default]
17    Contains,
18    Suffix,
19}
20
21#[derive(Clone, Copy, Debug, Eq, PartialEq)]
22pub enum DeclarationSearchScope {
23    Namespace,
24    Module,
25}
26
27#[derive(Clone, Debug, Eq, PartialEq)]
28pub struct DeclarationSearchBias {
29    pub scope: DeclarationSearchScope,
30    pub prefix: String,
31    pub strict: bool,
32    pub weight: i32,
33}
34
35#[derive(Clone, Debug, Eq, PartialEq)]
36pub struct DeclarationSearchRequest {
37    pub name_fragment: Option<String>,
38    pub name_match: DeclarationNameMatch,
39    pub kind: Option<String>,
40    pub required_constants: Vec<String>,
41    pub conclusion_head: Option<String>,
42    pub scope_biases: Vec<DeclarationSearchBias>,
43    pub limit: usize,
44    pub filter: LeanDeclarationFilter,
45    pub include_source: bool,
46}
47
48impl DeclarationSearchRequest {
49    #[must_use]
50    pub fn new(name_fragment: impl Into<String>) -> Self {
51        Self {
52            name_fragment: Some(name_fragment.into()),
53            name_match: DeclarationNameMatch::Contains,
54            kind: None,
55            required_constants: Vec::new(),
56            conclusion_head: None,
57            scope_biases: Vec::new(),
58            limit: 20,
59            filter: LeanDeclarationFilter {
60                include_private: false,
61                include_generated: false,
62                include_internal: false,
63            },
64            include_source: true,
65        }
66    }
67}
68
69#[derive(Clone, Copy, Debug, Default, Eq, PartialEq)]
70pub struct DeclarationFlags {
71    pub is_private: bool,
72    pub is_generated: bool,
73    pub is_internal: bool,
74}
75
76#[derive(Clone, Debug, Eq, PartialEq)]
77pub struct DeclarationSearchRow {
78    pub name: String,
79    pub kind: String,
80    pub module: Option<String>,
81    pub source: Option<LeanSourceRange>,
82    pub match_reason: String,
83    pub score: i32,
84    pub rank: usize,
85    pub flags: DeclarationFlags,
86}
87
88#[derive(Clone, Debug, Eq, PartialEq)]
89pub struct DeclarationSearchPruning {
90    pub stage: String,
91    pub reason: String,
92    pub count: usize,
93}
94
95#[derive(Clone, Debug, Default, Eq, PartialEq)]
96pub struct DeclarationSearchTimings {
97    pub scan_micros: u64,
98    pub rank_micros: u64,
99    pub source_micros: u64,
100}
101
102#[derive(Clone, Debug, Default, Eq, PartialEq)]
103pub struct DeclarationSearchFacts {
104    pub declarations_scanned: usize,
105    pub after_name_filter: usize,
106    pub after_kind_filter: usize,
107    pub after_required_constants_filter: usize,
108    pub after_conclusion_filter: usize,
109    pub after_scope_filter: usize,
110    pub source_lookups: usize,
111    pub broad_pruning: Vec<DeclarationSearchPruning>,
112    pub truncated: bool,
113    pub timings: DeclarationSearchTimings,
114}
115
116#[derive(Clone, Debug, Eq, PartialEq)]
117pub struct DeclarationSearchResult {
118    pub declarations: Vec<DeclarationSearchRow>,
119    pub truncated: bool,
120    pub facts: DeclarationSearchFacts,
121}
122
123#[derive(Clone, Copy, Debug, Eq, PartialEq)]
124#[allow(
125    clippy::struct_excessive_bools,
126    reason = "field-selection flags mirror the Lean request shape and are clearer than five tiny enums"
127)]
128pub struct DeclarationInspectionFields {
129    pub source: bool,
130    pub statement: bool,
131    pub docstring: bool,
132    pub attributes: bool,
133    pub flags: bool,
134    /// Render `statement` notation-aware (`pp.universes false`) when `true`,
135    /// falling back to the raw term if the pretty-printer cannot render it;
136    /// the fully-elaborated raw form when `false`.
137    pub statement_pretty: bool,
138}
139
140impl Default for DeclarationInspectionFields {
141    fn default() -> Self {
142        Self {
143            source: true,
144            statement: true,
145            docstring: true,
146            attributes: true,
147            flags: true,
148            statement_pretty: true,
149        }
150    }
151}
152
153#[derive(Clone, Copy, Debug, Eq, PartialEq)]
154pub struct DeclarationInspectionBudgets {
155    pub per_field_bytes: u32,
156    pub total_bytes: u32,
157}
158
159impl Default for DeclarationInspectionBudgets {
160    fn default() -> Self {
161        Self {
162            per_field_bytes: 8 * 1024,
163            total_bytes: 64 * 1024,
164        }
165    }
166}
167
168#[derive(Clone, Debug, Eq, PartialEq)]
169pub struct DeclarationInspectionRequest {
170    pub name: String,
171    pub fields: DeclarationInspectionFields,
172    pub budgets: DeclarationInspectionBudgets,
173}
174
175impl DeclarationInspectionRequest {
176    #[must_use]
177    pub fn new(name: impl Into<String>) -> Self {
178        Self {
179            name: name.into(),
180            fields: DeclarationInspectionFields::default(),
181            budgets: DeclarationInspectionBudgets::default(),
182        }
183    }
184}
185
186#[derive(Clone, Debug, Eq, PartialEq)]
187pub struct DeclarationRenderedInfo {
188    pub value: String,
189    pub truncated: bool,
190}
191
192#[derive(Clone, Debug, Default, Eq, PartialEq)]
193#[allow(
194    clippy::struct_excessive_bools,
195    reason = "proof-search booleans are independent inspection facts, not control-flow state"
196)]
197pub struct DeclarationProofSearchFacts {
198    pub is_simp: bool,
199    pub is_rw_candidate: bool,
200    pub is_instance: bool,
201    pub is_class: bool,
202    pub class_name: Option<String>,
203}
204
205#[derive(Clone, Debug, Eq, PartialEq)]
206pub struct DeclarationInspection {
207    pub name: String,
208    pub kind: String,
209    pub module: Option<String>,
210    pub source: Option<LeanSourceRange>,
211    pub statement: Option<DeclarationRenderedInfo>,
212    pub docstring: Option<DeclarationRenderedInfo>,
213    pub attributes: Vec<String>,
214    pub proof_search: DeclarationProofSearchFacts,
215    pub flags: DeclarationFlags,
216    /// Rendering that produced `statement`: `Some(true)` = pretty, `Some(false)`
217    /// = raw, `None` when no statement was requested.
218    pub statement_pretty: Option<bool>,
219}
220
221#[derive(Clone, Debug, Eq, PartialEq)]
222pub enum DeclarationInspectionResult {
223    Found { declaration: Box<DeclarationInspection> },
224    NotFound { name: String },
225    Unsupported,
226}
227
228impl<'lean> IntoLean<'lean> for DeclarationNameMatch {
229    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
230        match self {
231            Self::Contains => nat::from_usize(runtime, 0),
232            Self::Suffix => nat::from_usize(runtime, 1),
233        }
234    }
235}
236
237impl<'lean> IntoLean<'lean> for DeclarationSearchScope {
238    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
239        match self {
240            Self::Namespace => nat::from_usize(runtime, 0),
241            Self::Module => nat::from_usize(runtime, 1),
242        }
243    }
244}
245
246fn nat_from_bool(runtime: &LeanRuntime, value: bool) -> Obj<'_> {
247    nat::from_usize(runtime, usize::from(value))
248}
249
250fn bool_from_nat(obj: Obj<'_>) -> lean_rs::LeanResult<bool> {
251    Ok(nat::try_to_usize(obj)? != 0)
252}
253
254impl<'lean> IntoLean<'lean> for DeclarationSearchBias {
255    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
256        alloc_ctor_with_objects(
257            runtime,
258            0,
259            [
260                self.scope.into_lean(runtime),
261                self.prefix.into_lean(runtime),
262                nat_from_bool(runtime, self.strict),
263                self.weight.to_string().into_lean(runtime),
264            ],
265        )
266    }
267}
268
269impl<'lean> IntoLean<'lean> for DeclarationSearchRequest {
270    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
271        alloc_ctor_with_objects(
272            runtime,
273            0,
274            [
275                self.name_fragment.into_lean(runtime),
276                self.name_match.into_lean(runtime),
277                self.kind.into_lean(runtime),
278                self.required_constants.into_lean(runtime),
279                self.conclusion_head.into_lean(runtime),
280                self.scope_biases.into_lean(runtime),
281                nat::from_usize(runtime, self.limit),
282                self.filter.into_lean(runtime),
283                nat_from_bool(runtime, self.include_source),
284            ],
285        )
286    }
287}
288
289impl<'lean> IntoLean<'lean> for DeclarationInspectionFields {
290    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
291        alloc_ctor_with_objects(
292            runtime,
293            0,
294            [
295                nat_from_bool(runtime, self.source),
296                nat_from_bool(runtime, self.statement),
297                nat_from_bool(runtime, self.docstring),
298                nat_from_bool(runtime, self.attributes),
299                nat_from_bool(runtime, self.flags),
300                nat_from_bool(runtime, self.statement_pretty),
301            ],
302        )
303    }
304}
305
306impl<'lean> IntoLean<'lean> for DeclarationInspectionBudgets {
307    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
308        alloc_ctor_with_objects(
309            runtime,
310            0,
311            [
312                nat::from_usize(runtime, self.per_field_bytes as usize),
313                nat::from_usize(runtime, self.total_bytes as usize),
314            ],
315        )
316    }
317}
318
319impl<'lean> IntoLean<'lean> for DeclarationInspectionRequest {
320    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
321        alloc_ctor_with_objects(
322            runtime,
323            0,
324            [
325                self.name.into_lean(runtime),
326                self.fields.into_lean(runtime),
327                self.budgets.into_lean(runtime),
328            ],
329        )
330    }
331}
332
333impl sealed::SealedAbi for DeclarationInspectionRequest {}
334
335impl<'lean> LeanAbi<'lean> for DeclarationInspectionRequest {
336    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
337
338    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
339        self.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            "DeclarationInspectionRequest cannot decode a Lean call result; it is an argument-only type",
345        ))
346    }
347}
348
349impl sealed::SealedAbi for &DeclarationInspectionRequest {}
350
351impl<'lean> LeanAbi<'lean> for &DeclarationInspectionRequest {
352    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
353
354    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
355        self.clone().into_lean(runtime).into_raw()
356    }
357
358    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
359        Err(conversion_error(
360            "&DeclarationInspectionRequest cannot decode a Lean call result; use DeclarationInspectionRequest for owned values",
361        ))
362    }
363}
364
365impl sealed::SealedAbi for DeclarationSearchRequest {}
366
367impl<'lean> LeanAbi<'lean> for DeclarationSearchRequest {
368    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
369
370    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
371        self.into_lean(runtime).into_raw()
372    }
373
374    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
375        Err(conversion_error(
376            "DeclarationSearchRequest cannot decode a Lean call result; it is an argument-only type",
377        ))
378    }
379}
380
381impl sealed::SealedAbi for &DeclarationSearchRequest {}
382
383impl<'lean> LeanAbi<'lean> for &DeclarationSearchRequest {
384    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
385
386    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
387        self.clone().into_lean(runtime).into_raw()
388    }
389
390    fn from_c(_c: Self::CRepr, _runtime: &'lean LeanRuntime) -> lean_rs::LeanResult<Self> {
391        Err(conversion_error(
392            "&DeclarationSearchRequest cannot decode a Lean call result; use DeclarationSearchRequest for owned values",
393        ))
394    }
395}
396
397impl<'lean> TryFromLean<'lean> for DeclarationFlags {
398    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
399        let [is_private, is_generated, is_internal] = take_ctor_objects::<3>(obj, 0, "DeclarationFlags")?;
400        Ok(Self {
401            is_private: bool_from_nat(is_private)?,
402            is_generated: bool_from_nat(is_generated)?,
403            is_internal: bool_from_nat(is_internal)?,
404        })
405    }
406}
407
408impl<'lean> TryFromLean<'lean> for DeclarationSearchRow {
409    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
410        let [name, kind, module, source, match_reason, score, rank, flags] =
411            take_ctor_objects::<8>(obj, 0, "DeclarationSearchRow")?;
412        Ok(Self {
413            name: String::try_from_lean(name)?,
414            kind: String::try_from_lean(kind)?,
415            module: Option::<String>::try_from_lean(module)?,
416            source: Option::<LeanSourceRange>::try_from_lean(source)?,
417            match_reason: String::try_from_lean(match_reason)?,
418            score: String::try_from_lean(score)?
419                .parse()
420                .map_err(|_| conversion_error("score does not fit i32"))?,
421            rank: nat::try_to_usize(rank)?,
422            flags: DeclarationFlags::try_from_lean(flags)?,
423        })
424    }
425}
426
427impl<'lean> TryFromLean<'lean> for DeclarationSearchPruning {
428    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
429        let [stage, reason, count] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchPruning")?;
430        Ok(Self {
431            stage: String::try_from_lean(stage)?,
432            reason: String::try_from_lean(reason)?,
433            count: nat::try_to_usize(count)?,
434        })
435    }
436}
437
438impl<'lean> TryFromLean<'lean> for DeclarationSearchTimings {
439    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
440        let [scan_micros, rank_micros, source_micros] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchTimings")?;
441        Ok(Self {
442            scan_micros: nat::try_to_u64(scan_micros)?,
443            rank_micros: nat::try_to_u64(rank_micros)?,
444            source_micros: nat::try_to_u64(source_micros)?,
445        })
446    }
447}
448
449impl<'lean> TryFromLean<'lean> for DeclarationSearchFacts {
450    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
451        let [
452            declarations_scanned,
453            after_name_filter,
454            after_kind_filter,
455            after_required_constants_filter,
456            after_conclusion_filter,
457            after_scope_filter,
458            source_lookups,
459            broad_pruning,
460            truncated,
461            timings,
462        ] = take_ctor_objects::<10>(obj, 0, "DeclarationSearchFacts")?;
463        Ok(Self {
464            declarations_scanned: nat::try_to_usize(declarations_scanned)?,
465            after_name_filter: nat::try_to_usize(after_name_filter)?,
466            after_kind_filter: nat::try_to_usize(after_kind_filter)?,
467            after_required_constants_filter: nat::try_to_usize(after_required_constants_filter)?,
468            after_conclusion_filter: nat::try_to_usize(after_conclusion_filter)?,
469            after_scope_filter: nat::try_to_usize(after_scope_filter)?,
470            source_lookups: nat::try_to_usize(source_lookups)?,
471            broad_pruning: Vec::<DeclarationSearchPruning>::try_from_lean(broad_pruning)?,
472            truncated: bool_from_nat(truncated)?,
473            timings: DeclarationSearchTimings::try_from_lean(timings)?,
474        })
475    }
476}
477
478impl<'lean> TryFromLean<'lean> for DeclarationSearchResult {
479    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
480        let [declarations, truncated, facts] = take_ctor_objects::<3>(obj, 0, "DeclarationSearchResult")?;
481        Ok(Self {
482            declarations: Vec::<DeclarationSearchRow>::try_from_lean(declarations)?,
483            truncated: bool_from_nat(truncated)?,
484            facts: DeclarationSearchFacts::try_from_lean(facts)?,
485        })
486    }
487}
488
489impl<'lean> TryFromLean<'lean> for DeclarationRenderedInfo {
490    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
491        let [value, truncated] = take_ctor_objects::<2>(obj, 0, "DeclarationRenderedInfo")?;
492        Ok(Self {
493            value: String::try_from_lean(value)?,
494            truncated: bool_from_nat(truncated)?,
495        })
496    }
497}
498
499impl<'lean> TryFromLean<'lean> for DeclarationProofSearchFacts {
500    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
501        let [is_simp, is_rw_candidate, is_instance, is_class, class_name] =
502            take_ctor_objects::<5>(obj, 0, "DeclarationProofSearchFacts")?;
503        Ok(Self {
504            is_simp: bool_from_nat(is_simp)?,
505            is_rw_candidate: bool_from_nat(is_rw_candidate)?,
506            is_instance: bool_from_nat(is_instance)?,
507            is_class: bool_from_nat(is_class)?,
508            class_name: Option::<String>::try_from_lean(class_name)?,
509        })
510    }
511}
512
513impl<'lean> TryFromLean<'lean> for DeclarationInspection {
514    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
515        let [
516            name,
517            kind,
518            module,
519            source,
520            statement,
521            docstring,
522            attributes,
523            proof_search,
524            flags,
525            statement_rendering,
526        ] = take_ctor_objects::<10>(obj, 0, "DeclarationInspection")?;
527        // `statementRendering : Option Nat` (1 = pretty, 0 = raw) → Option<bool>.
528        let statement_pretty = match view(&statement_rendering).sum_tag()? {
529            0 => None,
530            1 => {
531                let [nat] = take_ctor_objects::<1>(statement_rendering, 1, "DeclarationInspection.statementRendering")?;
532                Some(bool_from_nat(nat)?)
533            }
534            other => {
535                return Err(conversion_error(format!(
536                    "expected Lean Option ctor (tag 0..=1) for statementRendering, found tag {other}"
537                )));
538            }
539        };
540        Ok(Self {
541            name: String::try_from_lean(name)?,
542            kind: String::try_from_lean(kind)?,
543            module: Option::<String>::try_from_lean(module)?,
544            source: Option::<LeanSourceRange>::try_from_lean(source)?,
545            statement: Option::<DeclarationRenderedInfo>::try_from_lean(statement)?,
546            docstring: Option::<DeclarationRenderedInfo>::try_from_lean(docstring)?,
547            attributes: Vec::<String>::try_from_lean(attributes)?,
548            proof_search: DeclarationProofSearchFacts::try_from_lean(proof_search)?,
549            flags: DeclarationFlags::try_from_lean(flags)?,
550            statement_pretty,
551        })
552    }
553}
554
555impl<'lean> TryFromLean<'lean> for DeclarationInspectionResult {
556    fn try_from_lean(obj: Obj<'lean>) -> lean_rs::LeanResult<Self> {
557        match view(&obj).sum_tag()? {
558            0 => {
559                let [declaration] = take_ctor_objects::<1>(obj, 0, "DeclarationInspectionResult::found")?;
560                Ok(Self::Found {
561                    declaration: Box::new(DeclarationInspection::try_from_lean(declaration)?),
562                })
563            }
564            1 => {
565                let [name] = take_ctor_objects::<1>(obj, 1, "DeclarationInspectionResult::notFound")?;
566                Ok(Self::NotFound {
567                    name: String::try_from_lean(name)?,
568                })
569            }
570            2 => {
571                let [] = take_ctor_objects::<0>(obj, 2, "DeclarationInspectionResult::unsupported")?;
572                Ok(Self::Unsupported)
573            }
574            other => Err(conversion_error(format!(
575                "expected Lean DeclarationInspectionResult ctor (tag 0..=2), found tag {other}"
576            ))),
577        }
578    }
579}
lean_rs_host/host/declaration_search.rs

lean_rs_host/host/
declaration_search.rs
