lean_rs_host/host/process/outcome.rs
1//! Typed outcomes for the two info-tree projection shims on
2//! [`crate::LeanSession`].
3//!
4//! - [`ProcessFileOutcome`] is what
5//! [`crate::LeanSession::process_with_info_tree`] returns: the
6//! body-only projection plus the `Unsupported` degradation arm.
7//! - [`ProcessModuleOutcome`] is what
8//! [`crate::LeanSession::process_module_with_info_tree`] returns: three
9//! real arms (`Ok`, `MissingImports`, `HeaderParseFailed`) plus the
10//! same `Unsupported` degradation. The arms distinguish a cleanly
11//! parsed header whose body elaborated, a cleanly parsed header
12//! whose imports the session's open env does not have (soft
13//! failure — the body still runs against the env), and a header
14//! that did not parse at all (the body is never elaborated).
15//!
16//! Heartbeat exhaustion during a single command's elaboration surfaces
17//! as an error-severity entry in `ProcessedFile::diagnostics`, not a
18//! separate wire arm — `IO.processCommands` catches per-command
19//! exceptions and attaches them to the message log on both shims.
20
21use lean_rs::Obj;
22use lean_rs::abi::structure::{ctor_tag, take_ctor_objects};
23use lean_rs::abi::traits::{TryFromLean, conversion_error};
24use lean_rs::error::LeanResult;
25
26use crate::host::elaboration::LeanElabFailure;
27use crate::host::process::info_tree::ProcessedFile;
28
29/// Outcome of [`crate::LeanSession::process_with_info_tree`].
30///
31/// `#[non_exhaustive]` so future capability refinements can extend the
32/// taxonomy without breaking exhaustive matches.
33#[derive(Debug)]
34#[non_exhaustive]
35pub enum ProcessFileOutcome {
36 /// The elaborator ran and produced an `Elab.InfoTree` projection.
37 /// `ProcessedFile::diagnostics` carries every error-severity entry
38 /// the elaborator emitted; callers that need to distinguish
39 /// heartbeat exhaustion from other failures should match on the
40 /// diagnostics there.
41 Processed(ProcessedFile),
42 /// The capability dylib does not export the
43 /// `lean_rs_host_process_with_info_tree` shim. No FFI call was
44 /// made; callers can fall back or degrade as appropriate.
45 Unsupported,
46}
47
48/// Outcome of [`crate::LeanSession::process_module_with_info_tree`].
49///
50/// The Lean shim parses the header first (via `Lean.Parser.parseHeader`)
51/// and only runs `IO.processCommands` if the header parsed cleanly.
52/// `Ok` / `MissingImports` therefore both carry a populated
53/// [`ProcessedFile`] (its `diagnostics` field captures any elaboration
54/// failure of the body); `HeaderParseFailed` short-circuits with just
55/// the parser's diagnostics.
56///
57/// `#[non_exhaustive]` so future capability refinements can extend the
58/// taxonomy without breaking exhaustive matches.
59#[derive(Debug)]
60#[non_exhaustive]
61pub enum ProcessModuleOutcome {
62 /// Header parsed; every parsed import is present in the session's
63 /// open env; the body was processed. `imports` lists the
64 /// user-written modules (Lean's auto-inserted `Init` is filtered
65 /// out by the shim).
66 Ok {
67 /// Body projection. `file.diagnostics` still records any
68 /// per-command elaboration errors the body produced.
69 file: ProcessedFile,
70 /// User-written imports from the file's header.
71 imports: Vec<String>,
72 },
73 /// Header parsed but some imports name modules the session's open
74 /// env does not have. The body was still processed against the
75 /// available env — `file` is populated and the partial projection
76 /// is useful diagnostic data. Callers typically surface `missing`
77 /// as a warning.
78 MissingImports {
79 /// Body projection (partial if some declarations depended on
80 /// the missing modules).
81 file: ProcessedFile,
82 /// User-written imports from the file's header.
83 imports: Vec<String>,
84 /// Subset of `imports` not present in the session's open env.
85 missing: Vec<String>,
86 },
87 /// `Lean.Parser.parseHeader` reported error-severity messages.
88 /// `IO.processCommands` was not invoked; only the header
89 /// diagnostics are returned.
90 HeaderParseFailed {
91 /// Header-parser diagnostics, with the same byte-budget
92 /// semantics as
93 /// [`crate::host::evidence::LeanKernelOutcome::Rejected`].
94 diagnostics: LeanElabFailure,
95 },
96 /// The capability dylib does not export the
97 /// `lean_rs_host_process_module_with_info_tree` shim. No FFI call was
98 /// made.
99 Unsupported,
100}
101
102impl<'lean> TryFromLean<'lean> for ProcessModuleOutcome {
103 fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
104 // The Lean inductive has three constructors:
105 // tag 0 = .ok (file, imports)
106 // tag 1 = .missingImports (file, imports, missing)
107 // tag 2 = .headerParseFailed(diagnostics)
108 // `Unsupported` is synthesised on the Rust side and never
109 // crosses the FFI, mirroring the existing pattern on
110 // `ProcessFileOutcome`.
111 let tag = ctor_tag(&obj)?;
112 match tag {
113 0 => {
114 let [file, imports] = take_ctor_objects::<2>(obj, 0, "ProcessModuleOutcome::ok")?;
115 Ok(Self::Ok {
116 file: ProcessedFile::try_from_lean(file)?,
117 imports: Vec::<String>::try_from_lean(imports)?,
118 })
119 }
120 1 => {
121 let [file, imports, missing] = take_ctor_objects::<3>(obj, 1, "ProcessModuleOutcome::missingImports")?;
122 Ok(Self::MissingImports {
123 file: ProcessedFile::try_from_lean(file)?,
124 imports: Vec::<String>::try_from_lean(imports)?,
125 missing: Vec::<String>::try_from_lean(missing)?,
126 })
127 }
128 2 => {
129 let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ProcessModuleOutcome::headerParseFailed")?;
130 Ok(Self::HeaderParseFailed {
131 diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
132 })
133 }
134 other => Err(conversion_error(format!(
135 "expected Lean ProcessModuleOutcome ctor (tag 0..=2), found tag {other}"
136 ))),
137 }
138 }
139}