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

lean_rs_host/host/meta/
response.rs
