lean_rs_host/host/evidence/
status.rs

1//! [`EvidenceStatus`] tag enum and the [`LeanKernelOutcome`] sum type
2//! returned by [`crate::LeanSession::kernel_check`].
3//!
4//! The Lean side encodes the outcome as a four-constructor inductive
5//! (`checked | rejected | unavailable | unsupported`); each constructor
6//! carries one object payload—the [`crate::LeanEvidence`] handle for
7//! `Checked`, a [`LeanElabFailure`] for the other three. The constructor
8//! tags are 0..=3 in declaration order; the [`TryFromLean`] impl below
9//! does the dispatch.
10
11use lean_rs::Obj;
12use lean_rs::abi::structure::{take_ctor_objects, view};
13use lean_rs::abi::traits::{TryFromLean, conversion_error};
14use lean_rs::error::LeanResult;
15
16use crate::host::elaboration::LeanElabFailure;
17use crate::host::evidence::handle::LeanEvidence;
18
19/// What the kernel-check capability concluded about a piece of Lean
20/// source.
21///
22/// The tag accessor on [`LeanKernelOutcome::status`] returns values of
23/// this type, as does [`crate::LeanSession::check_evidence`] when
24/// re-validating a captured [`crate::LeanEvidence`] handle.
25#[derive(Copy, Clone, Debug, Eq, PartialEq)]
26pub enum EvidenceStatus {
27    /// The kernel accepted the declaration. A [`crate::LeanEvidence`]
28    /// handle is available on the [`LeanKernelOutcome::Checked`] branch.
29    Checked,
30    /// The declaration was well-formed enough to reach kernel checking,
31    /// and the kernel (or the elaborator's type-check pass) refused it.
32    Rejected,
33    /// The capability ran but could not produce evidence—typically a
34    /// parse failure that aborted before the kernel could see the
35    /// declaration.
36    Unavailable,
37    /// The source did not name a kind of declaration this capability
38    /// produces evidence for (for example a `#check` command, a
39    /// non-theorem definition, or a comment-only fragment).
40    Unsupported,
41}
42
43/// Outcome of [`crate::LeanSession::kernel_check`].
44///
45/// Carries either a [`crate::LeanEvidence`] handle (on `Checked`) 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 LeanKernelOutcome<'lean> {
51    /// The kernel accepted the declaration.
52    Checked(LeanEvidence<'lean>),
53    /// The declaration reached kernel checking and was refused. The
54    /// failure carries the diagnostics the elaborator and kernel
55    /// produced.
56    Rejected(LeanElabFailure),
57    /// The capability could not produce evidence (typically a parse
58    /// failure). The failure carries the diagnostics Lean produced
59    /// before aborting.
60    Unavailable(LeanElabFailure),
61    /// The source did not name a supported kind of declaration. The
62    /// failure carries any diagnostics Lean produced while classifying.
63    Unsupported(LeanElabFailure),
64}
65
66impl LeanKernelOutcome<'_> {
67    /// Project the variant tag without consuming the payload.
68    ///
69    /// Useful when the caller only needs to branch on `Checked` vs. one
70    /// of the failure tags before deciding whether to read the contained
71    /// [`LeanElabFailure`] diagnostics.
72    #[must_use]
73    pub fn status(&self) -> EvidenceStatus {
74        match self {
75            Self::Checked(_) => EvidenceStatus::Checked,
76            Self::Rejected(_) => EvidenceStatus::Rejected,
77            Self::Unavailable(_) => EvidenceStatus::Unavailable,
78            Self::Unsupported(_) => EvidenceStatus::Unsupported,
79        }
80    }
81}
82
83impl<'lean> TryFromLean<'lean> for EvidenceStatus {
84    /// Decode a nullary-only Lean `EvidenceStatus` inductive.
85    ///
86    /// Tag order is `Checked = 0`, `Rejected = 1`, `Unavailable = 2`,
87    /// `Unsupported = 3`, matching the declaration order in
88    /// `fixtures/lean/LeanRsFixture/Elaboration.lean`'s `EvidenceStatus`
89    /// inductive.
90    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
91        let obj_view = view(&obj);
92        let tag = if obj_view.is_scalar() {
93            obj_view.scalar_payload("EvidenceStatus")?
94        } else {
95            let heap_tag = obj_view.ctor()?.tag();
96            let _ = take_ctor_objects::<0>(obj, heap_tag, "EvidenceStatus")?;
97            usize::from(heap_tag)
98        };
99        match tag {
100            0 => Ok(Self::Checked),
101            1 => Ok(Self::Rejected),
102            2 => Ok(Self::Unavailable),
103            3 => Ok(Self::Unsupported),
104            other => Err(conversion_error(format!(
105                "expected Lean EvidenceStatus tag 0..=3, found {other}"
106            ))),
107        }
108    }
109}
110
111impl<'lean> TryFromLean<'lean> for LeanKernelOutcome<'lean> {
112    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
113        let tag = view(&obj).ctor()?.tag();
114        match tag {
115            0 => {
116                let [payload] = take_ctor_objects::<1>(obj, 0, "KernelOutcome.checked")?;
117                Ok(Self::Checked(LeanEvidence::try_from_lean(payload)?))
118            }
119            1 => {
120                let [payload] = take_ctor_objects::<1>(obj, 1, "KernelOutcome.rejected")?;
121                Ok(Self::Rejected(LeanElabFailure::try_from_lean(payload)?))
122            }
123            2 => {
124                let [payload] = take_ctor_objects::<1>(obj, 2, "KernelOutcome.unavailable")?;
125                Ok(Self::Unavailable(LeanElabFailure::try_from_lean(payload)?))
126            }
127            3 => {
128                let [payload] = take_ctor_objects::<1>(obj, 3, "KernelOutcome.unsupported")?;
129                Ok(Self::Unsupported(LeanElabFailure::try_from_lean(payload)?))
130            }
131            other => Err(conversion_error(format!(
132                "expected Lean KernelOutcome ctor (tag 0..=3), found tag {other}"
133            ))),
134        }
135    }
136}
lean_rs_host/host/evidence/status.rs

lean_rs_host/host/evidence/
status.rs
