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_sys::object::{lean_is_scalar, lean_unbox};
12
13use crate::host::elaboration::LeanElabFailure;
14use crate::host::evidence::handle::LeanEvidence;
15use lean_rs::Obj;
16use lean_rs::abi::structure::{ctor_tag, take_ctor_objects};
17use lean_rs::abi::traits::{TryFromLean, conversion_error};
18use lean_rs::error::LeanResult;
19
20/// What the kernel-check capability concluded about a piece of Lean
21/// source.
22///
23/// The tag accessor on [`LeanKernelOutcome::status`] returns values of
24/// this type, as does [`crate::LeanSession::check_evidence`] when
25/// re-validating a captured [`crate::LeanEvidence`] handle.
26#[derive(Copy, Clone, Debug, Eq, PartialEq)]
27pub enum EvidenceStatus {
28    /// The kernel accepted the declaration. A [`crate::LeanEvidence`]
29    /// handle is available on the [`LeanKernelOutcome::Checked`] branch.
30    Checked,
31    /// The declaration was well-formed enough to reach kernel checking,
32    /// and the kernel (or the elaborator's type-check pass) refused it.
33    Rejected,
34    /// The capability ran but could not produce evidence — typically a
35    /// parse failure that aborted before the kernel could see the
36    /// declaration.
37    Unavailable,
38    /// The source did not name a kind of declaration this capability
39    /// produces evidence for (for example a `#check` command, a
40    /// non-theorem definition, or a comment-only fragment).
41    Unsupported,
42}
43
44/// Outcome of [`crate::LeanSession::kernel_check`].
45///
46/// Carries either a [`crate::LeanEvidence`] handle (on `Checked`) 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 LeanKernelOutcome<'lean> {
52    /// The kernel accepted the declaration.
53    Checked(LeanEvidence<'lean>),
54    /// The declaration reached kernel checking and was refused. The
55    /// failure carries the diagnostics the elaborator and kernel
56    /// produced.
57    Rejected(LeanElabFailure),
58    /// The capability could not produce evidence (typically a parse
59    /// failure). The failure carries the diagnostics Lean produced
60    /// before aborting.
61    Unavailable(LeanElabFailure),
62    /// The source did not name a supported kind of declaration. The
63    /// failure carries any diagnostics Lean produced while classifying.
64    Unsupported(LeanElabFailure),
65}
66
67impl LeanKernelOutcome<'_> {
68    /// Project the variant tag without consuming the payload.
69    ///
70    /// Useful when the caller only needs to branch on `Checked` vs. one
71    /// of the failure tags before deciding whether to read the contained
72    /// [`LeanElabFailure`] diagnostics.
73    #[must_use]
74    pub fn status(&self) -> EvidenceStatus {
75        match self {
76            Self::Checked(_) => EvidenceStatus::Checked,
77            Self::Rejected(_) => EvidenceStatus::Rejected,
78            Self::Unavailable(_) => EvidenceStatus::Unavailable,
79            Self::Unsupported(_) => EvidenceStatus::Unsupported,
80        }
81    }
82}
83
84impl<'lean> TryFromLean<'lean> for EvidenceStatus {
85    /// Decode a nullary-only Lean `EvidenceStatus` inductive. Lean's
86    /// compiler emits a nullary-only inductive as a scalar-tagged
87    /// pointer (`lean_box(tag)`) at the top-level boundary rather
88    /// than a heap-allocated zero-field constructor, so the decoder
89    /// reads through `lean_unbox` on the scalar branch and falls back
90    /// to [`ctor_tag`] only if a future encoding shift starts
91    /// materialising the inductive on the heap.
92    ///
93    /// Tag order is `Checked = 0`, `Rejected = 1`, `Unavailable = 2`,
94    /// `Unsupported = 3`, matching the declaration order in
95    /// `fixtures/lean/LeanRsFixture/Elaboration.lean`'s `EvidenceStatus`
96    /// inductive.
97    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
98        let raw = obj.as_raw_borrowed();
99        // SAFETY: `lean_is_scalar` is pure pointer-bit math.
100        #[allow(unsafe_code)]
101        let tag = if unsafe { lean_is_scalar(raw) } {
102            // SAFETY: scalar branch; `lean_unbox` returns the payload
103            // `usize` (the constructor tag for a nullary-only
104            // inductive).
105            #[allow(unsafe_code)]
106            let payload = unsafe { lean_unbox(raw) };
107            // The parent `obj` (a scalar pointer) carries no heap
108            // refcount; drop is a no-op.
109            drop(obj);
110            payload
111        } else {
112            // Future-proofing: if Lean ever heap-allocates this
113            // inductive, the ctor branch decodes through the standard
114            // structure-pattern primitives.
115            let heap_tag = ctor_tag(&obj)?;
116            let _ = take_ctor_objects::<0>(obj, heap_tag, "EvidenceStatus")?;
117            usize::from(heap_tag)
118        };
119        match tag {
120            0 => Ok(Self::Checked),
121            1 => Ok(Self::Rejected),
122            2 => Ok(Self::Unavailable),
123            3 => Ok(Self::Unsupported),
124            other => Err(conversion_error(format!(
125                "expected Lean EvidenceStatus tag 0..=3, found {other}"
126            ))),
127        }
128    }
129}
130
131impl<'lean> TryFromLean<'lean> for LeanKernelOutcome<'lean> {
132    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
133        // KernelOutcome is a 4-constructor inductive; each ctor carries
134        // a single object-pointer field.
135        let tag = ctor_tag(&obj)?;
136        match tag {
137            0 => {
138                let [payload] = take_ctor_objects::<1>(obj, 0, "KernelOutcome.checked")?;
139                Ok(Self::Checked(LeanEvidence::try_from_lean(payload)?))
140            }
141            1 => {
142                let [payload] = take_ctor_objects::<1>(obj, 1, "KernelOutcome.rejected")?;
143                Ok(Self::Rejected(LeanElabFailure::try_from_lean(payload)?))
144            }
145            2 => {
146                let [payload] = take_ctor_objects::<1>(obj, 2, "KernelOutcome.unavailable")?;
147                Ok(Self::Unavailable(LeanElabFailure::try_from_lean(payload)?))
148            }
149            3 => {
150                let [payload] = take_ctor_objects::<1>(obj, 3, "KernelOutcome.unsupported")?;
151                Ok(Self::Unsupported(LeanElabFailure::try_from_lean(payload)?))
152            }
153            other => Err(conversion_error(format!(
154                "expected Lean KernelOutcome ctor (tag 0..=3), found tag {other}"
155            ))),
156        }
157    }
158}
lean_rs_host/host/evidence/status.rs

lean_rs_host/host/evidence/
status.rs
