lean_rs_host/host/meta/
service.rs

1//! [`LeanMetaService`] — sealed descriptor for a registered bounded
2//! `MetaM` service.
3//!
4//! Each pinned service ties together:
5//!
6//! - the Lean-side `@[export]` symbol name the dispatcher resolves;
7//! - the list of `.olean` modules that must be imported into the
8//!   session before the service can run;
9//! - the typed request / response shape (encoded as `PhantomData<fn(Req)
10//!   -> Resp>`) the [`crate::LeanSession::run_meta`] generic
11//!   parameters must agree with.
12//!
13//! The struct has no public constructor — the only `LeanMetaService`
14//! values downstream code can name are returned by the four free
15//! functions in this module, which form the closed registry. Adding a
16//! new service requires landing a Lean `@[export]` *and* a Rust-side
17//! constructor here.
18
19use core::marker::PhantomData;
20
21use lean_rs::LeanExpr;
22
23use super::LeanMetaTransparency;
24
25/// Sealed descriptor for one registered `MetaM` service.
26///
27/// `Req` is the Rust-side type the call site supplies; `Resp` is the
28/// type the typed payload decodes into on the `Ok` branch. The phantom
29/// `fn(Req) -> Resp` keeps the marker invariant in both parameters
30/// (matching how Lake's emitted signature treats them).
31#[derive(Clone, Copy)]
32pub struct LeanMetaService<Req, Resp> {
33    name: &'static str,
34    required_imports: &'static [&'static str],
35    _marker: PhantomData<fn(Req) -> Resp>,
36}
37
38impl<Req, Resp> LeanMetaService<Req, Resp> {
39    /// Crate-internal constructor. The pinned service free fns below
40    /// are the only callers.
41    pub(crate) const fn new(name: &'static str, required_imports: &'static [&'static str]) -> Self {
42        Self {
43            name,
44            required_imports,
45            _marker: PhantomData,
46        }
47    }
48
49    /// The Lean-side C-symbol name the dispatcher resolves.
50    #[must_use]
51    pub fn name(&self) -> &'static str {
52        self.name
53    }
54
55    /// The `.olean` module names that must appear in the session's
56    /// import list before this service can run. Callers can either
57    /// thread the list into [`crate::LeanCapabilities::session`] or
58    /// import the parent `LeanRsFixture` roll-up module, which
59    /// transitively imports every fixture submodule.
60    #[must_use]
61    pub fn required_imports(&self) -> &'static [&'static str] {
62        self.required_imports
63    }
64}
65
66impl<Req, Resp> core::fmt::Debug for LeanMetaService<Req, Resp> {
67    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
68        f.debug_struct("LeanMetaService")
69            .field("name", &self.name)
70            .field("required_imports", &self.required_imports)
71            .finish()
72    }
73}
74
75// -- The four pinned services ------------------------------------------
76//
77// Each constructor returns the typed descriptor `'lean`-parameterised
78// over the request/response payload. The Lean-side symbol names and
79// import strings are pinned here; the `LeanMetaService` shape is
80// otherwise sealed.
81
82const REQUIRED_IMPORTS: &[&str] = &["LeanRsHostShims.Meta"];
83
84/// Register the `Meta.inferType` service.
85///
86/// Calling [`crate::LeanSession::run_meta`] with the returned
87/// descriptor and a [`LeanExpr`] returns a typed
88/// [`super::LeanMetaResponse`] carrying the inferred type expression on
89/// `Ok`.
90#[must_use]
91pub fn infer_type<'lean>() -> LeanMetaService<LeanExpr<'lean>, LeanExpr<'lean>> {
92    LeanMetaService::new("lean_rs_host_meta_infer_type", REQUIRED_IMPORTS)
93}
94
95/// Register the `Meta.whnf` service.
96///
97/// Returns the weak-head normal form of the supplied expression under
98/// the bundle's reducibility setting.
99#[must_use]
100pub fn whnf<'lean>() -> LeanMetaService<LeanExpr<'lean>, LeanExpr<'lean>> {
101    LeanMetaService::new("lean_rs_host_meta_whnf", REQUIRED_IMPORTS)
102}
103
104/// Register the diagnostic heartbeat-burn service.
105///
106/// The Lean-side action loops on `Core.checkMaxHeartbeats`; any nonzero
107/// heartbeat budget below the loop bound trips
108/// `Lean.Exception.isMaxHeartbeat` and surfaces as
109/// `LeanMetaResponse::TimeoutOrHeartbeat`. The supplied `LeanExpr` is
110/// ignored — the request shape is uniform with the inference / whnf
111/// services so callers do not need a separate "no input" descriptor.
112#[must_use]
113pub fn heartbeat_burn<'lean>() -> LeanMetaService<LeanExpr<'lean>, LeanExpr<'lean>> {
114    LeanMetaService::new("lean_rs_host_meta_heartbeat_burn", REQUIRED_IMPORTS)
115}
116
117/// Register the `Meta.isDefEq` service.
118///
119/// The request is the Lean product `(lhs, rhs, transparency)`. The
120/// response remains a [`super::LeanMetaResponse<bool>`], so heartbeat
121/// exhaustion and Lean exceptions stay distinct from a successful
122/// `false`.
123#[must_use]
124pub fn is_def_eq<'lean>() -> LeanMetaService<(LeanExpr<'lean>, LeanExpr<'lean>, LeanMetaTransparency), bool> {
125    LeanMetaService::new("lean_rs_host_meta_is_def_eq", REQUIRED_IMPORTS)
126}
lean_rs_host/host/meta/service.rs

lean_rs_host/host/meta/
service.rs
