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

lean_rs_host/host/evidence/
status.rs
