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.
26#[derive(Copy, Clone, Debug, Eq, PartialEq)]
27pub enum MetaCallStatus {
28    /// The `MetaM` action returned a typed payload.
29    Ok,
30    /// The `MetaM` action raised a non-resource-exhaustion exception
31    /// (type error, unbound metavariable, …).
32    Failed,
33    /// The heartbeat ceiling tripped before the action finished.
34    /// Equivalent to `Lean.Exception.isMaxHeartbeat` matching on the
35    /// caught exception.
36    TimeoutOrHeartbeat,
37    /// The capability does not expose this service — either the Lean
38    /// shim returned `unsupported` for the request shape, or the
39    /// loaded capability does not export the service's C symbol.
40    Unsupported,
41}
42
43/// Outcome of a bounded `MetaM` service call.
44///
45/// Carries either a typed `Resp` payload (on `Ok`) or a
46/// [`LeanElabFailure`] (on every other status) so callers can both
47/// branch on the typed status tag via [`Self::status`] and read the
48/// structured diagnostics in the failure cases.
49#[derive(Debug)]
50pub enum LeanMetaResponse<Resp> {
51    /// The `MetaM` action returned a typed payload.
52    Ok(Resp),
53    /// The `MetaM` action raised a non-resource-exhaustion exception.
54    /// The failure carries one error-severity diagnostic.
55    Failed(LeanElabFailure),
56    /// The heartbeat ceiling tripped before the action finished. The
57    /// failure carries the heartbeat-exhaustion message Lean produced.
58    TimeoutOrHeartbeat(LeanElabFailure),
59    /// The capability did not provide this service. Either the Lean
60    /// shim returned `unsupported` or the dispatcher synthesised this
61    /// branch when the service's symbol was absent at capability load.
62    Unsupported(LeanElabFailure),
63}
64
65impl<Resp> LeanMetaResponse<Resp> {
66    /// Project the variant tag without inspecting the payload.
67    #[must_use]
68    pub fn status(&self) -> MetaCallStatus {
69        match self {
70            Self::Ok(_) => MetaCallStatus::Ok,
71            Self::Failed(_) => MetaCallStatus::Failed,
72            Self::TimeoutOrHeartbeat(_) => MetaCallStatus::TimeoutOrHeartbeat,
73            Self::Unsupported(_) => MetaCallStatus::Unsupported,
74        }
75    }
76
77    /// Project to the stable [`LeanDiagnosticCode`] taxonomy.
78    ///
79    /// `Ok` returns `None` — the response carries a typed payload, not
80    /// a diagnostic. The three failure variants map to
81    /// [`LeanDiagnosticCode::Elaboration`] (the failure carries a
82    /// [`LeanElabFailure`] in every case except `Unsupported`, which
83    /// projects to [`LeanDiagnosticCode::Unsupported`]).
84    #[must_use]
85    pub const fn code(&self) -> Option<LeanDiagnosticCode> {
86        match self {
87            Self::Ok(_) => None,
88            Self::Failed(_) | Self::TimeoutOrHeartbeat(_) => Some(LeanDiagnosticCode::Elaboration),
89            Self::Unsupported(_) => Some(LeanDiagnosticCode::Unsupported),
90        }
91    }
92}
93
94impl<'lean, Resp> TryFromLean<'lean> for LeanMetaResponse<Resp>
95where
96    Resp: TryFromLean<'lean>,
97{
98    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
99        let tag = ctor_tag(&obj)?;
100        match tag {
101            0 => {
102                let [payload] = take_ctor_objects::<1>(obj, 0, "MetaResponse.ok")?;
103                Ok(Self::Ok(Resp::try_from_lean(payload)?))
104            }
105            1 => {
106                let [payload] = take_ctor_objects::<1>(obj, 1, "MetaResponse.failed")?;
107                Ok(Self::Failed(LeanElabFailure::try_from_lean(payload)?))
108            }
109            2 => {
110                let [payload] = take_ctor_objects::<1>(obj, 2, "MetaResponse.timeoutOrHeartbeat")?;
111                Ok(Self::TimeoutOrHeartbeat(LeanElabFailure::try_from_lean(payload)?))
112            }
113            3 => {
114                let [payload] = take_ctor_objects::<1>(obj, 3, "MetaResponse.unsupported")?;
115                Ok(Self::Unsupported(LeanElabFailure::try_from_lean(payload)?))
116            }
117            other => Err(conversion_error(format!(
118                "expected Lean MetaResponse ctor (tag 0..=3), found tag {other}"
119            ))),
120        }
121    }
122}
lean_rs_host/host/meta/response.rs

lean_rs_host/host/meta/
response.rs
