lean_host_mcp/
projections.rs

1//! Pure data-shuffle projections from `lean-rs-worker` types into the
2//! MCP-stable wire shapes.
3//!
4//! No Lean dependency past `Serialize + Deserialize` round-trips, no
5//! `LeanRuntime` handle—these can be called from any thread and
6//! serialise straight into the JSON envelope.
7//!
8//! All projection *types* and *helper functions* live here. Tool handlers
9//! import the wire types from this module. Worker lifecycle/error
10//! classification belongs in the runtime boundary, not in projection code.
11#![allow(clippy::needless_pass_by_value)]
12
13use lean_rs_worker_parent::{
14    LeanWorkerDeclarationFlags, LeanWorkerDeclarationInspection as WorkerDeclarationInspection,
15    LeanWorkerDeclarationInspectionResult, LeanWorkerDeclarationProofSearchFacts, LeanWorkerDeclarationRow,
16    LeanWorkerDeclarationSearchFacts, LeanWorkerDeclarationSearchPruning, LeanWorkerDeclarationSearchResult,
17    LeanWorkerDeclarationSearchRow, LeanWorkerDeclarationSearchTimings, LeanWorkerDeclarationTargetInfo,
18    LeanWorkerDeclarationVerificationFacts, LeanWorkerDeclarationVerificationResult,
19    LeanWorkerDeclarationVerificationStatus, LeanWorkerDiagnostic, LeanWorkerElabFailure, LeanWorkerElabResult,
20    LeanWorkerKernelResult, LeanWorkerKernelStatus, LeanWorkerMetaResult, LeanWorkerModuleSourceSpan,
21    LeanWorkerProofAttemptEnvelope, LeanWorkerProofAttemptResult, LeanWorkerProofAttemptRow,
22    LeanWorkerProofAttemptStatus, LeanWorkerRendered, LeanWorkerRenderedInfo, LeanWorkerRendering,
23    LeanWorkerSourceRange,
24};
25
26/// Source-range projection with public fields mirroring `LeanWorkerSourceRange`.
27#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
28pub struct SourceRange {
29    pub file: String,
30    pub start_line: u32,
31    pub start_column: u32,
32    pub end_line: u32,
33    pub end_column: u32,
34}
35
36#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
37pub struct Position {
38    pub line: u32,
39    pub column: u32,
40    pub end_line: Option<u32>,
41    pub end_column: Option<u32>,
42}
43
44/// Wire-stable severity classification. The three Lean severities map to
45/// `snake_case` strings so the field is uniform with every other status
46/// discriminant in the server.
47#[derive(Debug, Clone, Copy, serde::Serialize, schemars::JsonSchema)]
48#[serde(rename_all = "snake_case")]
49pub enum Severity {
50    Error,
51    Warning,
52    Info,
53}
54
55impl Severity {
56    /// The worker layer emits severity as a snake-case string; unknown
57    /// values map to `Info` rather than blocking the response.
58    fn from_worker(s: &str) -> Self {
59        match s {
60            "error" => Self::Error,
61            "warning" => Self::Warning,
62            _ => Self::Info,
63        }
64    }
65}
66
67#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
68pub struct Diagnostic {
69    pub severity: Severity,
70    pub message: String,
71    pub position: Option<Position>,
72    /// Real source path when Lean attached one. Omitted for the synthetic
73    /// `<elaborate>` label that elaboration-buffer calls always produce;
74    /// the caller already knows which file they asked about.
75    #[serde(skip_serializing_if = "Option::is_none")]
76    pub file: Option<String>,
77}
78
79/// Structured failure payload: the projection of `LeanWorkerElabFailure`
80/// sent over JSON. Failure is part of a successful tool call; this is never
81/// an MCP error.
82#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
83pub struct ElabFailure {
84    pub diagnostics: Vec<Diagnostic>,
85    pub truncated: bool,
86}
87
88#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
89pub struct ElabSuccess {
90    pub ok: bool,
91}
92
93#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
94pub struct KernelOutcome {
95    /// One of `Checked`, `Rejected`, `Unavailable`, or `Unsupported`.
96    pub status: String,
97    pub summary: Option<KernelSummary>,
98    pub failure: Option<ElabFailure>,
99}
100
101#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
102pub struct KernelSummary {
103    pub declaration_name: String,
104    pub kind: String,
105    /// Pretty-printed declaration type via Lean's `PrettyPrinter`
106    /// (notation-aware), as the worker's `LeanWorkerKernelSummary` reports
107    /// it.
108    pub type_signature: String,
109}
110
111#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
112pub struct MetaOutcome {
113    /// One of `Ok`, `Failed`, `TimeoutOrHeartbeat`, or `Unsupported`.
114    pub status: String,
115    pub rendered: Option<String>,
116    pub definitionally_equal: Option<bool>,
117    pub failure: Option<ElabFailure>,
118    /// Set when the worker reported `LeanWorkerRendering::Raw`: the
119    /// optional `meta_pp_expr` shim was missing or reported `Unsupported`,
120    /// and the rendering fell back to `Expr.toString`. Internal; tool
121    /// handlers translate this into an envelope warning, and the field
122    /// never serialises.
123    #[serde(skip)]
124    #[schemars(skip)]
125    pub raw_fallback_used: bool,
126}
127
128#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
129pub struct DeclarationRow {
130    pub name: String,
131    pub kind: String,
132    /// Pretty-printed type signature as the worker's
133    /// `LeanWorkerDeclarationRow` reports it. `None` only when the
134    /// declaration has no recoverable type (typically internal artifacts).
135    pub type_signature: Option<String>,
136    pub source: Option<SourceRange>,
137}
138
139#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
140pub struct RenderedText {
141    pub value: String,
142    pub truncated: bool,
143}
144
145#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
146pub struct ModuleSourceSpan {
147    pub start_line: u32,
148    pub start_column: u32,
149    pub end_line: u32,
150    pub end_column: u32,
151}
152
153#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
154pub struct ProofActionDeclarationTarget {
155    pub short_name: String,
156    pub declaration_name: String,
157    pub namespace_name: String,
158    pub declaration_kind: String,
159    pub declaration_span: ModuleSourceSpan,
160    pub name_span: ModuleSourceSpan,
161    pub body_span: ModuleSourceSpan,
162}
163
164#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
165pub struct DeclarationFlags {
166    pub is_private: bool,
167    pub is_generated: bool,
168    pub is_internal: bool,
169}
170
171#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
172pub struct DeclarationSummary {
173    pub name: String,
174    pub kind: String,
175    pub module: Option<String>,
176    pub source: Option<SourceRange>,
177    pub match_reason: String,
178    pub score: i32,
179    pub rank: usize,
180    pub flags: DeclarationFlags,
181}
182
183#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
184pub struct DeclarationSearchPruning {
185    pub stage: String,
186    pub reason: String,
187    pub count: usize,
188}
189
190#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
191pub struct DeclarationSearchTimings {
192    pub scan_micros: u64,
193    pub rank_micros: u64,
194    pub source_micros: u64,
195}
196
197#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
198pub struct DeclarationSearchFacts {
199    pub declarations_scanned: usize,
200    pub after_name_filter: usize,
201    pub after_kind_filter: usize,
202    pub after_required_constants_filter: usize,
203    pub after_conclusion_filter: usize,
204    pub after_scope_filter: usize,
205    pub source_lookups: usize,
206    pub broad_pruning: Vec<DeclarationSearchPruning>,
207    pub truncated: bool,
208    pub timings: DeclarationSearchTimings,
209}
210
211#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
212pub struct DeclarationSearchResult {
213    pub declarations: Vec<DeclarationSummary>,
214    pub truncated: bool,
215    pub facts: DeclarationSearchFacts,
216}
217
218#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
219#[allow(
220    clippy::struct_excessive_bools,
221    reason = "proof-search booleans mirror independent lean-rs wire facts"
222)]
223pub struct DeclarationProofSearchFacts {
224    pub is_simp: bool,
225    pub is_rw_candidate: bool,
226    pub is_instance: bool,
227    pub is_class: bool,
228    pub class_name: Option<String>,
229}
230
231#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
232pub struct DeclarationInspection {
233    pub name: String,
234    pub kind: String,
235    pub module: Option<String>,
236    pub source: Option<SourceRange>,
237    pub statement: Option<RenderedText>,
238    /// How `statement` was rendered: `"pretty"` (notation-aware) or `"raw"`
239    /// (fully-elaborated `Expr.toString`). `"raw"` when `Pretty` was requested
240    /// but the pretty-printer could not render the term and fell back. `None`
241    /// when no statement was requested.
242    #[serde(skip_serializing_if = "Option::is_none")]
243    pub statement_rendering: Option<String>,
244    pub docstring: Option<RenderedText>,
245    pub attributes: Vec<String>,
246    pub proof_search: DeclarationProofSearchFacts,
247    pub flags: DeclarationFlags,
248}
249
250#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
251#[serde(tag = "status", rename_all = "snake_case")]
252pub enum DeclarationInspectionResult {
253    Found {
254        declaration: Box<DeclarationInspection>,
255    },
256    NotFound {
257        name: Option<String>,
258    },
259    /// The declaration's import closure reached an unbuilt `.olean`, so the
260    /// name could not be resolved against a complete environment. Distinct from
261    /// `not_found` (which would falsely claim the declaration does not exist):
262    /// it may resolve once the project is built. The envelope carries the
263    /// `lake build` warning. Shares the `needs_build` status token with the
264    /// other resolution-bearing tools.
265    NeedsBuild,
266    Unsupported,
267}
268
269#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
270pub struct ProofAttemptCandidate {
271    pub id: String,
272    pub status: String,
273    pub snippet: RenderedText,
274    pub diagnostics: ElabFailure,
275    pub downstream_diagnostics: ElabFailure,
276    pub goals: Vec<RenderedText>,
277    pub declaration: Option<ProofActionDeclarationTarget>,
278    pub proof_position: Option<ProofPositionSummary>,
279    pub output_truncated: bool,
280}
281
282#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
283pub struct ProofPositionSummary {
284    pub index: u32,
285    pub tactic: RenderedText,
286}
287
288#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
289pub struct ProofAttemptEnvelope {
290    pub candidates: Vec<ProofAttemptCandidate>,
291    pub candidate_limit: u32,
292    pub candidates_truncated: bool,
293}
294
295#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
296#[serde(tag = "status", rename_all = "snake_case")]
297pub enum ProofAttemptResult {
298    Ok {
299        result: ProofAttemptEnvelope,
300        imports: Vec<String>,
301    },
302    MissingImports {
303        result: ProofAttemptEnvelope,
304        imports: Vec<String>,
305        missing: Vec<String>,
306    },
307    HeaderParseFailed {
308        diagnostics: ElabFailure,
309    },
310    Unsupported,
311}
312
313#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
314#[allow(
315    clippy::struct_excessive_bools,
316    reason = "verification booleans mirror independent lean-rs wire facts for proof policy decisions"
317)]
318pub struct DeclarationVerificationFacts {
319    pub target: Option<ProofActionDeclarationTarget>,
320    pub diagnostics: ElabFailure,
321    pub unresolved_goals: Vec<RenderedText>,
322    pub contains_sorry: bool,
323    pub contains_admit: bool,
324    pub contains_sorry_ax: bool,
325    pub axioms: Vec<String>,
326    pub axioms_truncated: bool,
327    /// `false` when the axiom dependency set could not be computed (target
328    /// unresolved, or `report_axioms` not requested): an empty `axioms` then
329    /// means "not computed", not "no axioms". `true` with empty `axioms` is a
330    /// genuine no-nontrivial-axioms result.
331    pub axioms_available: bool,
332    pub output_truncated: bool,
333    /// Competing declarations when `verification_status` is `ambiguous`; empty
334    /// otherwise. The fully-qualified names to disambiguate between.
335    #[serde(skip_serializing_if = "Vec::is_empty")]
336    pub candidates: Vec<ProofActionDeclarationTarget>,
337    /// `false` when the verdict was computed against an incomplete or
338    /// unresolved environment (`needs_build` or `ambiguous`). The other facts
339    /// in this block are then unreliable: a clean `contains_sorry:false` /
340    /// `unresolved_goals:[]` does not mean the declaration verified — the
341    /// environment could not be assembled, or the name did not resolve, to
342    /// check it. Always serialized; an absent trust flag is worse than present.
343    pub facts_trustworthy: bool,
344}
345
346#[derive(Debug, Clone, serde::Serialize, schemars::JsonSchema)]
347#[serde(tag = "status", rename_all = "snake_case")]
348pub enum DeclarationVerificationResult {
349    Ok {
350        verification_status: String,
351        facts: Box<DeclarationVerificationFacts>,
352        imports: Vec<String>,
353    },
354    MissingImports {
355        verification_status: String,
356        facts: Box<DeclarationVerificationFacts>,
357        imports: Vec<String>,
358        missing: Vec<String>,
359    },
360    HeaderParseFailed {
361        diagnostics: ElabFailure,
362    },
363    Unsupported,
364}
365
366// --- projection helpers -------------------------------------------------
367
368pub fn project_diagnostic(d: &LeanWorkerDiagnostic) -> Diagnostic {
369    let position = d.line.map(|line| Position {
370        line,
371        column: d.column.unwrap_or(0),
372        end_line: d.end_line,
373        end_column: d.end_column,
374    });
375    Diagnostic {
376        severity: Severity::from_worker(&d.severity),
377        message: d.message.clone(),
378        position,
379        file: meaningful_file_label(&d.file_label),
380    }
381}
382
383pub fn project_failure(failure: &LeanWorkerElabFailure) -> ElabFailure {
384    ElabFailure {
385        diagnostics: failure.diagnostics.iter().map(project_diagnostic).collect(),
386        truncated: failure.truncated,
387    }
388}
389
390pub(crate) fn project_source_range(range: LeanWorkerSourceRange) -> SourceRange {
391    SourceRange {
392        file: range.file,
393        start_line: range.start_line,
394        start_column: range.start_column,
395        end_line: range.end_line,
396        end_column: range.end_column,
397    }
398}
399
400/// Strip Lean's synthetic source label so it never reaches the wire. Every
401/// call that elaborates a string buffer (rather than a file on disk) gets
402/// labelled `<elaborate>`, which is never actionable for the caller.
403fn meaningful_file_label(label: &str) -> Option<String> {
404    if label.is_empty() || label == "<elaborate>" || label.starts_with('<') {
405        None
406    } else {
407        Some(label.to_owned())
408    }
409}
410
411/// # Errors
412///
413/// Returns the projected [`ElabFailure`] in the error arm when the
414/// upstream `LeanWorkerElabResult.success` is `false`. Never an
415/// infrastructure error.
416pub fn project_elab_result(result: LeanWorkerElabResult) -> std::result::Result<ElabSuccess, ElabFailure> {
417    if result.success {
418        Ok(ElabSuccess { ok: true })
419    } else {
420        Err(ElabFailure {
421            diagnostics: result.diagnostics.iter().map(project_diagnostic).collect(),
422            truncated: result.truncated,
423        })
424    }
425}
426
427pub fn project_kernel_result(result: LeanWorkerKernelResult) -> KernelOutcome {
428    let status = match result.status {
429        LeanWorkerKernelStatus::Checked => "Checked",
430        LeanWorkerKernelStatus::Rejected => "Rejected",
431        LeanWorkerKernelStatus::Unavailable => "Unavailable",
432        LeanWorkerKernelStatus::Unsupported => "Unsupported",
433        _ => "Unsupported",
434    };
435    let summary = result.summary.map(|s| KernelSummary {
436        declaration_name: s.declaration_name,
437        kind: s.kind,
438        type_signature: s.type_signature,
439    });
440    let failure = if matches!(result.status, LeanWorkerKernelStatus::Checked) {
441        None
442    } else {
443        Some(ElabFailure {
444            diagnostics: result.diagnostics.iter().map(project_diagnostic).collect(),
445            truncated: result.truncated,
446        })
447    };
448    KernelOutcome {
449        status: status.to_owned(),
450        summary,
451        failure,
452    }
453}
454
455pub fn project_meta_rendered(result: LeanWorkerMetaResult<LeanWorkerRendered>) -> MetaOutcome {
456    match result {
457        LeanWorkerMetaResult::Ok { value } => MetaOutcome {
458            status: "Ok".into(),
459            rendered: Some(value.value),
460            definitionally_equal: None,
461            failure: None,
462            raw_fallback_used: matches!(value.rendering, LeanWorkerRendering::Raw),
463        },
464        LeanWorkerMetaResult::Failed { failure } => meta_failure("Failed", &failure),
465        LeanWorkerMetaResult::TimeoutOrHeartbeat { failure } => meta_failure("TimeoutOrHeartbeat", &failure),
466        LeanWorkerMetaResult::Unsupported { failure } => meta_failure("Unsupported", &failure),
467        _ => MetaOutcome {
468            status: "Unsupported".into(),
469            rendered: None,
470            definitionally_equal: None,
471            failure: None,
472            raw_fallback_used: false,
473        },
474    }
475}
476
477pub fn project_meta_bool(result: LeanWorkerMetaResult<bool>) -> MetaOutcome {
478    match result {
479        LeanWorkerMetaResult::Ok { value } => MetaOutcome {
480            status: "Ok".into(),
481            rendered: None,
482            definitionally_equal: Some(value),
483            failure: None,
484            raw_fallback_used: false,
485        },
486        LeanWorkerMetaResult::Failed { failure } => meta_failure("Failed", &failure),
487        LeanWorkerMetaResult::TimeoutOrHeartbeat { failure } => meta_failure("TimeoutOrHeartbeat", &failure),
488        LeanWorkerMetaResult::Unsupported { failure } => meta_failure("Unsupported", &failure),
489        _ => MetaOutcome {
490            status: "Unsupported".into(),
491            rendered: None,
492            definitionally_equal: None,
493            failure: None,
494            raw_fallback_used: false,
495        },
496    }
497}
498
499fn meta_failure(status: &str, failure: &LeanWorkerElabFailure) -> MetaOutcome {
500    MetaOutcome {
501        status: status.to_owned(),
502        rendered: None,
503        definitionally_equal: None,
504        failure: Some(project_failure(failure)),
505        raw_fallback_used: false,
506    }
507}
508
509pub fn project_declaration_row(row: LeanWorkerDeclarationRow) -> DeclarationRow {
510    DeclarationRow {
511        name: row.name,
512        kind: row.kind,
513        type_signature: row.type_signature,
514        source: row.source.map(project_source_range),
515    }
516}
517
518pub(crate) fn project_rendered_info(info: LeanWorkerRenderedInfo) -> RenderedText {
519    RenderedText {
520        value: info.value,
521        truncated: info.truncated,
522    }
523}
524
525fn rendering_label(rendering: LeanWorkerRendering) -> String {
526    match rendering {
527        LeanWorkerRendering::Pretty => "pretty".to_owned(),
528        LeanWorkerRendering::Raw => "raw".to_owned(),
529        // `LeanWorkerRendering` is `#[non_exhaustive]`. An unknown future
530        // variant falls back to "raw" (least surprising to a reader expecting
531        // elaborated output); re-check this label when bumping lean-rs.
532        _ => "raw".to_owned(),
533    }
534}
535
536pub(crate) fn project_module_source_span(span: LeanWorkerModuleSourceSpan) -> ModuleSourceSpan {
537    ModuleSourceSpan {
538        start_line: span.start_line,
539        start_column: span.start_column,
540        end_line: span.end_line,
541        end_column: span.end_column,
542    }
543}
544
545pub(crate) fn project_proof_action_target(info: LeanWorkerDeclarationTargetInfo) -> ProofActionDeclarationTarget {
546    ProofActionDeclarationTarget {
547        short_name: info.short_name,
548        declaration_name: info.declaration_name,
549        namespace_name: info.namespace_name,
550        declaration_kind: info.declaration_kind,
551        declaration_span: project_module_source_span(info.declaration_span),
552        name_span: project_module_source_span(info.name_span),
553        body_span: project_module_source_span(info.body_span),
554    }
555}
556
557pub(crate) fn project_declaration_flags(flags: LeanWorkerDeclarationFlags) -> DeclarationFlags {
558    DeclarationFlags {
559        is_private: flags.is_private,
560        is_generated: flags.is_generated,
561        is_internal: flags.is_internal,
562    }
563}
564
565fn project_declaration_summary(row: LeanWorkerDeclarationSearchRow) -> DeclarationSummary {
566    DeclarationSummary {
567        name: row.name,
568        kind: row.kind,
569        module: row.module,
570        source: row.source.map(project_source_range),
571        match_reason: row.match_reason,
572        score: row.score,
573        rank: row.rank,
574        flags: project_declaration_flags(row.flags),
575    }
576}
577
578fn project_declaration_search_pruning(row: LeanWorkerDeclarationSearchPruning) -> DeclarationSearchPruning {
579    DeclarationSearchPruning {
580        stage: row.stage,
581        reason: row.reason,
582        count: row.count,
583    }
584}
585
586fn project_declaration_search_timings(timings: LeanWorkerDeclarationSearchTimings) -> DeclarationSearchTimings {
587    DeclarationSearchTimings {
588        scan_micros: timings.scan_micros,
589        rank_micros: timings.rank_micros,
590        source_micros: timings.source_micros,
591    }
592}
593
594fn project_declaration_search_facts(facts: LeanWorkerDeclarationSearchFacts) -> DeclarationSearchFacts {
595    DeclarationSearchFacts {
596        declarations_scanned: facts.declarations_scanned,
597        after_name_filter: facts.after_name_filter,
598        after_kind_filter: facts.after_kind_filter,
599        after_required_constants_filter: facts.after_required_constants_filter,
600        after_conclusion_filter: facts.after_conclusion_filter,
601        after_scope_filter: facts.after_scope_filter,
602        source_lookups: facts.source_lookups,
603        broad_pruning: facts
604            .broad_pruning
605            .into_iter()
606            .map(project_declaration_search_pruning)
607            .collect(),
608        truncated: facts.truncated,
609        timings: project_declaration_search_timings(facts.timings),
610    }
611}
612
613pub fn project_declaration_search(result: LeanWorkerDeclarationSearchResult) -> DeclarationSearchResult {
614    DeclarationSearchResult {
615        declarations: result
616            .declarations
617            .into_iter()
618            .map(project_declaration_summary)
619            .collect(),
620        truncated: result.truncated,
621        facts: project_declaration_search_facts(result.facts),
622    }
623}
624
625pub fn project_declaration_inspection(result: LeanWorkerDeclarationInspectionResult) -> DeclarationInspectionResult {
626    match result {
627        LeanWorkerDeclarationInspectionResult::Found { declaration } => DeclarationInspectionResult::Found {
628            declaration: Box::new(project_inspection(*declaration)),
629        },
630        LeanWorkerDeclarationInspectionResult::NotFound { name } => {
631            DeclarationInspectionResult::NotFound { name: Some(name) }
632        }
633        LeanWorkerDeclarationInspectionResult::Unsupported => DeclarationInspectionResult::Unsupported,
634        // `LeanWorkerDeclarationInspectionResult` is `Found | NotFound |
635        // Unsupported` on the current worker (the enum is `#[non_exhaustive]`,
636        // hence this arm). It has no `Ambiguous`/incomplete-build variant, so
637        // unlike `verify_declaration` there is no `needs_build` case to
638        // reclassify here. If the worker gains one (see
639        // ~/Code/prompts/lean-rs/12-*.md), route it through `crate::diagnosis`.
640        _ => DeclarationInspectionResult::Unsupported,
641    }
642}
643
644pub fn project_proof_attempt(result: LeanWorkerProofAttemptResult) -> ProofAttemptResult {
645    match result {
646        LeanWorkerProofAttemptResult::Ok { result, imports } => ProofAttemptResult::Ok {
647            result: project_proof_attempt_envelope(result),
648            imports,
649        },
650        LeanWorkerProofAttemptResult::MissingImports {
651            result,
652            imports,
653            missing,
654        } => ProofAttemptResult::MissingImports {
655            result: project_proof_attempt_envelope(result),
656            imports,
657            missing,
658        },
659        LeanWorkerProofAttemptResult::HeaderParseFailed { diagnostics } => ProofAttemptResult::HeaderParseFailed {
660            diagnostics: project_failure(&diagnostics),
661        },
662        LeanWorkerProofAttemptResult::Unsupported => ProofAttemptResult::Unsupported,
663        _ => ProofAttemptResult::Unsupported,
664    }
665}
666
667pub(crate) fn project_proof_attempt_envelope(envelope: LeanWorkerProofAttemptEnvelope) -> ProofAttemptEnvelope {
668    ProofAttemptEnvelope {
669        candidates: envelope.candidates.into_iter().map(project_proof_attempt_row).collect(),
670        candidate_limit: envelope.candidate_limit,
671        candidates_truncated: envelope.candidates_truncated,
672    }
673}
674
675pub(crate) fn project_proof_attempt_row(row: LeanWorkerProofAttemptRow) -> ProofAttemptCandidate {
676    ProofAttemptCandidate {
677        id: row.id,
678        status: proof_attempt_status(row.status).to_owned(),
679        snippet: project_rendered_info(row.candidate_text),
680        diagnostics: project_failure(&row.diagnostics),
681        downstream_diagnostics: project_failure(&row.downstream_diagnostics),
682        goals: row.goals.into_iter().map(project_rendered_info).collect(),
683        declaration: row.declaration.map(project_proof_action_target),
684        proof_position: row.proof_position.map(|position| ProofPositionSummary {
685            index: position.index,
686            tactic: project_rendered_info(position.tactic),
687        }),
688        output_truncated: row.output_truncated,
689    }
690}
691
692fn proof_attempt_status(status: LeanWorkerProofAttemptStatus) -> &'static str {
693    match status {
694        LeanWorkerProofAttemptStatus::Closed => "closed",
695        LeanWorkerProofAttemptStatus::Progressed => "progressed",
696        LeanWorkerProofAttemptStatus::Failed => "failed",
697        LeanWorkerProofAttemptStatus::Timeout => "timeout",
698        LeanWorkerProofAttemptStatus::BudgetExceeded => "budget_exceeded",
699        LeanWorkerProofAttemptStatus::Unsupported => "unsupported",
700        _ => "unsupported",
701    }
702}
703
704pub fn project_declaration_verification(
705    result: LeanWorkerDeclarationVerificationResult,
706) -> DeclarationVerificationResult {
707    match result {
708        LeanWorkerDeclarationVerificationResult::Ok {
709            verification_status,
710            facts,
711            imports,
712        } => {
713            let label = verification_status_label(verification_status, &facts);
714            // `needs_build` (incomplete environment) and `ambiguous` (no single
715            // resolved target) both mean the facts describe nothing checked, so
716            // they are not trustworthy.
717            let trustworthy = label != crate::diagnosis::NEEDS_BUILD_STATUS && label != "ambiguous";
718            DeclarationVerificationResult::Ok {
719                verification_status: label.to_owned(),
720                facts: Box::new(project_declaration_verification_facts(*facts, trustworthy)),
721                imports,
722            }
723        }
724        LeanWorkerDeclarationVerificationResult::MissingImports {
725            verification_status,
726            facts,
727            imports,
728            missing,
729        } => DeclarationVerificationResult::MissingImports {
730            verification_status: verification_status_label(verification_status, &facts).to_owned(),
731            // Imports the worker could not load: the environment is incomplete,
732            // so the verdict's facts are not trustworthy.
733            facts: Box::new(project_declaration_verification_facts(*facts, false)),
734            imports,
735            missing,
736        },
737        LeanWorkerDeclarationVerificationResult::HeaderParseFailed { diagnostics } => {
738            DeclarationVerificationResult::HeaderParseFailed {
739                diagnostics: project_failure(&diagnostics),
740            }
741        }
742        LeanWorkerDeclarationVerificationResult::Unsupported => DeclarationVerificationResult::Unsupported,
743        _ => DeclarationVerificationResult::Unsupported,
744    }
745}
746
747fn project_declaration_verification_facts(
748    facts: LeanWorkerDeclarationVerificationFacts,
749    facts_trustworthy: bool,
750) -> DeclarationVerificationFacts {
751    DeclarationVerificationFacts {
752        target: facts.target.map(project_proof_action_target),
753        diagnostics: project_failure(&facts.diagnostics),
754        unresolved_goals: facts.unresolved_goals.into_iter().map(project_rendered_info).collect(),
755        contains_sorry: facts.contains_sorry,
756        contains_admit: facts.contains_admit,
757        contains_sorry_ax: facts.contains_sorry_ax,
758        axioms: facts.axioms,
759        axioms_truncated: facts.axioms_truncated,
760        axioms_available: facts.axioms_available,
761        output_truncated: facts.output_truncated,
762        candidates: facts.candidates.into_iter().map(project_proof_action_target).collect(),
763        facts_trustworthy,
764    }
765}
766
767fn verification_status_label(
768    status: LeanWorkerDeclarationVerificationStatus,
769    facts: &LeanWorkerDeclarationVerificationFacts,
770) -> &'static str {
771    match status {
772        LeanWorkerDeclarationVerificationStatus::Accepted => "verified",
773        LeanWorkerDeclarationVerificationStatus::Rejected if facts.contains_sorry => "has_sorry",
774        LeanWorkerDeclarationVerificationStatus::Rejected if !facts.unresolved_goals.is_empty() => {
775            "has_unresolved_goals"
776        }
777        LeanWorkerDeclarationVerificationStatus::Rejected if !facts.diagnostics.diagnostics.is_empty() => {
778            "has_diagnostics"
779        }
780        LeanWorkerDeclarationVerificationStatus::Rejected => "has_diagnostics",
781        LeanWorkerDeclarationVerificationStatus::NotFound => "not_found",
782        // Genuine multiple-resolution: the worker (protocol 8) attaches the
783        // competing declarations in `facts.candidates`.
784        LeanWorkerDeclarationVerificationStatus::Ambiguous => "ambiguous",
785        // The name did not resolve because the open environment is incomplete;
786        // the enclosing `MissingImports` outcome names the unbuilt modules.
787        LeanWorkerDeclarationVerificationStatus::NeedsBuild => crate::diagnosis::NEEDS_BUILD_STATUS,
788        LeanWorkerDeclarationVerificationStatus::Timeout => "timeout",
789        LeanWorkerDeclarationVerificationStatus::BudgetExceeded => "budget_exceeded",
790        LeanWorkerDeclarationVerificationStatus::Unsupported => "unsupported",
791        _ => "unsupported",
792    }
793}
794
795pub(crate) fn project_inspection(declaration: WorkerDeclarationInspection) -> DeclarationInspection {
796    DeclarationInspection {
797        name: declaration.name,
798        kind: declaration.kind,
799        module: declaration.module,
800        source: declaration.source.map(project_source_range),
801        statement: declaration.statement.map(project_rendered_info),
802        statement_rendering: declaration.statement_rendering.map(rendering_label),
803        docstring: declaration.docstring.map(project_rendered_info),
804        attributes: declaration.attributes,
805        proof_search: project_proof_search_facts(declaration.proof_search),
806        flags: project_declaration_flags(declaration.flags),
807    }
808}
809
810fn project_proof_search_facts(facts: LeanWorkerDeclarationProofSearchFacts) -> DeclarationProofSearchFacts {
811    DeclarationProofSearchFacts {
812        is_simp: facts.is_simp,
813        is_rw_candidate: facts.is_rw_candidate,
814        is_instance: facts.is_instance,
815        is_class: facts.is_class,
816        class_name: facts.class_name,
817    }
818}
819
820#[cfg(test)]
821#[allow(
822    clippy::unwrap_used,
823    clippy::panic,
824    reason = "unit tests fail directly on the wrong variant"
825)]
826mod tests {
827    use super::*;
828
829    fn clean_facts() -> LeanWorkerDeclarationVerificationFacts {
830        LeanWorkerDeclarationVerificationFacts {
831            target: None,
832            diagnostics: LeanWorkerElabFailure {
833                diagnostics: Vec::new(),
834                truncated: false,
835            },
836            unresolved_goals: Vec::new(),
837            contains_sorry: false,
838            contains_admit: false,
839            contains_sorry_ax: false,
840            axioms: Vec::new(),
841            axioms_truncated: false,
842            axioms_available: true,
843            output_truncated: false,
844            candidates: Vec::new(),
845        }
846    }
847
848    fn target_info(name: &str) -> LeanWorkerDeclarationTargetInfo {
849        let span = lean_rs_worker_parent::LeanWorkerModuleSourceSpan {
850            start_line: 0,
851            start_column: 0,
852            end_line: 0,
853            end_column: 0,
854        };
855        LeanWorkerDeclarationTargetInfo {
856            short_name: name.rsplit('.').next().unwrap_or(name).to_owned(),
857            declaration_name: name.to_owned(),
858            namespace_name: name.rsplit_once('.').map(|(ns, _)| ns.to_owned()).unwrap_or_default(),
859            declaration_kind: "theorem".to_owned(),
860            declaration_span: span.clone(),
861            name_span: span.clone(),
862            body_span: span,
863        }
864    }
865
866    #[test]
867    fn needs_build_verification_is_labeled_needs_build_with_untrustworthy_facts() {
868        let result = project_declaration_verification(LeanWorkerDeclarationVerificationResult::Ok {
869            verification_status: LeanWorkerDeclarationVerificationStatus::NeedsBuild,
870            facts: Box::new(clean_facts()),
871            imports: Vec::new(),
872        });
873        let DeclarationVerificationResult::Ok {
874            verification_status,
875            facts,
876            ..
877        } = result
878        else {
879            panic!("expected an Ok verdict");
880        };
881        assert_eq!(verification_status, "needs_build");
882        // Facts retained (not nulled) but flagged untrustworthy so a reader
883        // can't take the clean `contains_sorry:false` at face value when the
884        // environment was incomplete.
885        assert!(!facts.facts_trustworthy);
886        assert!(!facts.contains_sorry);
887    }
888
889    #[test]
890    fn ambiguous_verification_surfaces_candidates_with_untrustworthy_facts() {
891        let mut facts = clean_facts();
892        facts.candidates = vec![target_info("A.foo"), target_info("B.foo")];
893        let result = project_declaration_verification(LeanWorkerDeclarationVerificationResult::Ok {
894            verification_status: LeanWorkerDeclarationVerificationStatus::Ambiguous,
895            facts: Box::new(facts),
896            imports: Vec::new(),
897        });
898        let DeclarationVerificationResult::Ok {
899            verification_status,
900            facts,
901            ..
902        } = result
903        else {
904            panic!("expected an Ok verdict");
905        };
906        // Genuine ambiguity keeps the "ambiguous" verdict (it is actionable now
907        // that competitors are named) and is not relabeled to needs_build.
908        assert_eq!(verification_status, "ambiguous");
909        assert_eq!(facts.candidates.len(), 2);
910        assert!(!facts.facts_trustworthy);
911    }
912
913    #[test]
914    fn accepted_verification_keeps_facts_trustworthy() {
915        let result = project_declaration_verification(LeanWorkerDeclarationVerificationResult::Ok {
916            verification_status: LeanWorkerDeclarationVerificationStatus::Accepted,
917            facts: Box::new(clean_facts()),
918            imports: Vec::new(),
919        });
920        let DeclarationVerificationResult::Ok {
921            verification_status,
922            facts,
923            ..
924        } = result
925        else {
926            panic!("expected an Ok verdict");
927        };
928        assert_eq!(verification_status, "verified");
929        assert!(facts.facts_trustworthy);
930    }
931}
lean_host_mcp/projections.rs

lean_host_mcp/
projections.rs
