lean_rs_host/host/meta/
response.rs

1//! `LeanMetaResponse<Resp>` and `MetaCallStatus` — typed outcome of a
2//! bounded `MetaM` service call.
3//!
4//! The Lean side encodes `MetaResponse α` as a four-constructor
5//! inductive (`ok / failed / timeoutOrHeartbeat / unsupported`); each
6//! constructor carries a single object payload — the typed response on
7//! `Ok`, a [`LeanElabFailure`] on every other branch. Tag indices are
8//! 0..=3 in declaration order; the [`TryFromLean`] impl below does the
9//! dispatch.
10//!
11//! `LeanMetaResponse<Resp>` is the value type [`crate::LeanSession::run_meta`]
12//! returns; callers can both branch on the typed tag via
13//! [`LeanMetaResponse::status`] and read the typed payload on the `Ok`
14//! branch (or the structured diagnostics on the other three).
15
16use crate::host::elaboration::LeanElabFailure;
17use lean_rs::Obj;
18use lean_rs::abi::structure::{ctor_tag, take_ctor_objects};
19use lean_rs::abi::traits::{TryFromLean, conversion_error};
20use lean_rs::error::{LeanDiagnosticCode, LeanResult};
21
22/// Classification tag for a meta-service call.
23///
24/// Returned by [`LeanMetaResponse::status`] without inspecting the
25/// payload. `#[non_exhaustive]` so future capability refinements can
26/// extend the taxonomy without breaking exhaustive matches downstream.
27#[derive(Copy, Clone, Debug, Eq, PartialEq)]
28#[non_exhaustive]
29pub enum MetaCallStatus {
30    /// The `MetaM` action returned a typed payload.
31    Ok,
32    /// The `MetaM` action raised a non-resource-exhaustion exception
33    /// (type error, unbound metavariable, …).
34    Failed,
35    /// The heartbeat ceiling tripped before the action finished.
36    /// Equivalent to `Lean.Exception.isMaxHeartbeat` matching on the
37    /// caught exception.
38    TimeoutOrHeartbeat,
39    /// The capability does not expose this service — either the Lean
40    /// shim returned `unsupported` for the request shape, or the
41    /// loaded capability does not export the service's C symbol.
42    Unsupported,
43}
44
45/// Outcome of a bounded `MetaM` service call.
46///
47/// Carries either a typed `Resp` payload (on `Ok`) or a
48/// [`LeanElabFailure`] (on every other status) so callers can both
49/// branch on the typed status tag via [`Self::status`] and read the
50/// structured diagnostics in the failure cases.
51///
52/// `#[non_exhaustive]` so the variant set tracks future toolchain
53/// classification refinements without breaking exhaustive matches.
54#[derive(Debug)]
55#[non_exhaustive]
56pub enum LeanMetaResponse<Resp> {
57    /// The `MetaM` action returned a typed payload.
58    Ok(Resp),
59    /// The `MetaM` action raised a non-resource-exhaustion exception.
60    /// The failure carries one error-severity diagnostic.
61    Failed(LeanElabFailure),
62    /// The heartbeat ceiling tripped before the action finished. The
63    /// failure carries the heartbeat-exhaustion message Lean produced.
64    TimeoutOrHeartbeat(LeanElabFailure),
65    /// The capability did not provide this service. Either the Lean
66    /// shim returned `unsupported` or the dispatcher synthesised this
67    /// branch when the service's symbol was absent at capability load.
68    Unsupported(LeanElabFailure),
69}
70
71impl<Resp> LeanMetaResponse<Resp> {
72    /// Project the variant tag without inspecting the payload.
73    #[must_use]
74    pub fn status(&self) -> MetaCallStatus {
75        match self {
76            Self::Ok(_) => MetaCallStatus::Ok,
77            Self::Failed(_) => MetaCallStatus::Failed,
78            Self::TimeoutOrHeartbeat(_) => MetaCallStatus::TimeoutOrHeartbeat,
79            Self::Unsupported(_) => MetaCallStatus::Unsupported,
80        }
81    }
82
83    /// Project to the stable [`LeanDiagnosticCode`] taxonomy.
84    ///
85    /// `Ok` returns `None` — the response carries a typed payload, not
86    /// a diagnostic. The three failure variants map to
87    /// [`LeanDiagnosticCode::Elaboration`] (the failure carries a
88    /// [`LeanElabFailure`] in every case except `Unsupported`, which
89    /// projects to [`LeanDiagnosticCode::Unsupported`]).
90    #[must_use]
91    pub const fn code(&self) -> Option<LeanDiagnosticCode> {
92        match self {
93            Self::Ok(_) => None,
94            Self::Failed(_) | Self::TimeoutOrHeartbeat(_) => Some(LeanDiagnosticCode::Elaboration),
95            Self::Unsupported(_) => Some(LeanDiagnosticCode::Unsupported),
96        }
97    }
98}
99
100impl<'lean, Resp> TryFromLean<'lean> for LeanMetaResponse<Resp>
101where
102    Resp: TryFromLean<'lean>,
103{
104    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
105        let tag = ctor_tag(&obj)?;
106        match tag {
107            0 => {
108                let [payload] = take_ctor_objects::<1>(obj, 0, "MetaResponse.ok")?;
109                Ok(Self::Ok(Resp::try_from_lean(payload)?))
110            }
111            1 => {
112                let [payload] = take_ctor_objects::<1>(obj, 1, "MetaResponse.failed")?;
113                Ok(Self::Failed(LeanElabFailure::try_from_lean(payload)?))
114            }
115            2 => {
116                let [payload] = take_ctor_objects::<1>(obj, 2, "MetaResponse.timeoutOrHeartbeat")?;
117                Ok(Self::TimeoutOrHeartbeat(LeanElabFailure::try_from_lean(payload)?))
118            }
119            3 => {
120                let [payload] = take_ctor_objects::<1>(obj, 3, "MetaResponse.unsupported")?;
121                Ok(Self::Unsupported(LeanElabFailure::try_from_lean(payload)?))
122            }
123            other => Err(conversion_error(format!(
124                "expected Lean MetaResponse ctor (tag 0..=3), found tag {other}"
125            ))),
126        }
127    }
128}
lean_rs_host/host/meta/response.rs

lean_rs_host/host/meta/
response.rs
