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#[derive(Debug)]
31pub enum ProcessFileOutcome {
32    /// The elaborator ran and produced an `Elab.InfoTree` projection.
33    /// `ProcessedFile::diagnostics` carries every error-severity entry
34    /// the elaborator emitted; callers that need to distinguish
35    /// heartbeat exhaustion from other failures should match on the
36    /// diagnostics there.
37    Processed(ProcessedFile),
38    /// The capability dylib does not export the
39    /// `lean_rs_host_process_with_info_tree` shim. No FFI call was
40    /// made; callers can fall back or degrade as appropriate.
41    Unsupported,
42}
43
44/// Outcome of [`crate::LeanSession::process_module_with_info_tree`].
45///
46/// The Lean shim parses the header first (via `Lean.Parser.parseHeader`)
47/// and only runs `IO.processCommands` if the header parsed cleanly.
48/// `Ok` / `MissingImports` therefore both carry a populated
49/// [`ProcessedFile`] (its `diagnostics` field captures any elaboration
50/// failure of the body); `HeaderParseFailed` short-circuits with just
51/// the parser's diagnostics.
52#[derive(Debug)]
53pub enum ProcessModuleOutcome {
54    /// Header parsed; every parsed import is present in the session's
55    /// open env; the body was processed. `imports` lists the
56    /// user-written modules (Lean's auto-inserted `Init` is filtered
57    /// out by the shim).
58    Ok {
59        /// Body projection. `file.diagnostics` still records any
60        /// per-command elaboration errors the body produced.
61        file: ProcessedFile,
62        /// User-written imports from the file's header.
63        imports: Vec<String>,
64    },
65    /// Header parsed but some imports name modules the session's open
66    /// env does not have. The body was still processed against the
67    /// available env — `file` is populated and the partial projection
68    /// is useful diagnostic data. Callers typically surface `missing`
69    /// as a warning.
70    MissingImports {
71        /// Body projection (partial if some declarations depended on
72        /// the missing modules).
73        file: ProcessedFile,
74        /// User-written imports from the file's header.
75        imports: Vec<String>,
76        /// Subset of `imports` not present in the session's open env.
77        missing: Vec<String>,
78    },
79    /// `Lean.Parser.parseHeader` reported error-severity messages.
80    /// `IO.processCommands` was not invoked; only the header
81    /// diagnostics are returned.
82    HeaderParseFailed {
83        /// Header-parser diagnostics, with the same byte-budget
84        /// semantics as
85        /// [`crate::host::evidence::LeanKernelOutcome::Rejected`].
86        diagnostics: LeanElabFailure,
87    },
88    /// The capability dylib does not export the
89    /// `lean_rs_host_process_module_with_info_tree` shim. No FFI call was
90    /// made.
91    Unsupported,
92}
93
94impl<'lean> TryFromLean<'lean> for ProcessModuleOutcome {
95    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
96        // The Lean inductive has three constructors:
97        //   tag 0 = .ok               (file, imports)
98        //   tag 1 = .missingImports   (file, imports, missing)
99        //   tag 2 = .headerParseFailed(diagnostics)
100        // `Unsupported` is synthesised on the Rust side and never
101        // crosses the FFI, mirroring the existing pattern on
102        // `ProcessFileOutcome`.
103        let tag = ctor_tag(&obj)?;
104        match tag {
105            0 => {
106                let [file, imports] = take_ctor_objects::<2>(obj, 0, "ProcessModuleOutcome::ok")?;
107                Ok(Self::Ok {
108                    file: ProcessedFile::try_from_lean(file)?,
109                    imports: Vec::<String>::try_from_lean(imports)?,
110                })
111            }
112            1 => {
113                let [file, imports, missing] = take_ctor_objects::<3>(obj, 1, "ProcessModuleOutcome::missingImports")?;
114                Ok(Self::MissingImports {
115                    file: ProcessedFile::try_from_lean(file)?,
116                    imports: Vec::<String>::try_from_lean(imports)?,
117                    missing: Vec::<String>::try_from_lean(missing)?,
118                })
119            }
120            2 => {
121                let [diagnostics] = take_ctor_objects::<1>(obj, 2, "ProcessModuleOutcome::headerParseFailed")?;
122                Ok(Self::HeaderParseFailed {
123                    diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
124                })
125            }
126            other => Err(conversion_error(format!(
127                "expected Lean ProcessModuleOutcome ctor (tag 0..=2), found tag {other}"
128            ))),
129        }
130    }
131}
lean_rs_host/host/process/outcome.rs

lean_rs_host/host/process/
outcome.rs
