lean_rs_host/host/
bracketed.rs

1//! Bracketed no-extension imports for one-shot lightweight queries.
2//!
3//! This module intentionally does not expose `Lean.Environment`, `Expr`,
4//! `ConstantInfo`, `Name`, or any other Lean-owned handle. The Lean shim imports
5//! with `loadExts := false`, serializes the requested declaration metadata, frees
6//! compacted regions, and only then returns these Rust-owned values.
7
8use lean_rs::Obj;
9use lean_rs::abi::structure::{alloc_ctor_with_objects, take_ctor_objects, view};
10use lean_rs::abi::traits::{IntoLean, LeanAbi, TryFromLean, conversion_error, sealed};
11use lean_rs::error::LeanResult;
12use serde::Deserialize;
13
14use crate::host::capabilities::LeanCapabilities;
15use crate::host::progress::{LeanProgressSink, ProgressBridge};
16use crate::host::session::{LeanSession, with_session_import_lock};
17use crate::host::shim_bindings::{HostShimBindings, binding_error_to_lean_error};
18
19/// Closed request for the bracketed no-extension import path.
20///
21/// The request is intentionally limited to declaration metadata lookups by
22/// name. It does not admit parser, elaborator, pretty-printer, extension, or
23/// arbitrary callback work because the imported compacted regions are freed
24/// before Rust receives the result.
25#[derive(Clone, Debug, Default, Eq, PartialEq)]
26pub struct LeanBracketedImportRequest {
27    /// Fully-qualified declaration names to inspect inside the bracket.
28    pub declaration_names: Vec<String>,
29}
30
31impl LeanBracketedImportRequest {
32    #[must_use]
33    pub fn new(declaration_names: impl IntoIterator<Item = impl Into<String>>) -> Self {
34        Self {
35            declaration_names: declaration_names.into_iter().map(Into::into).collect(),
36        }
37    }
38}
39
40impl<'lean> IntoLean<'lean> for LeanBracketedImportRequest {
41    fn into_lean(self, runtime: &'lean lean_rs::LeanRuntime) -> Obj<'lean> {
42        alloc_ctor_with_objects(runtime, 0, [self.declaration_names.into_lean(runtime)])
43    }
44}
45
46impl sealed::SealedAbi for LeanBracketedImportRequest {}
47
48impl<'lean> LeanAbi<'lean> for LeanBracketedImportRequest {
49    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
50
51    fn into_c(self, runtime: &'lean lean_rs::LeanRuntime) -> Self::CRepr {
52        self.into_lean(runtime).into_raw()
53    }
54
55    fn from_c(_c: Self::CRepr, _runtime: &'lean lean_rs::LeanRuntime) -> LeanResult<Self> {
56        Err(conversion_error(
57            "LeanBracketedImportRequest cannot decode a Lean call result; it is an argument-only type",
58        ))
59    }
60}
61
62/// Result of one bracketed no-extension import query.
63///
64/// Every field is Rust-owned data decoded from the Lean shim's serialized
65/// payload. No Lean-owned `Environment`, `Expr`, `Name`, `ConstantInfo`, or
66/// extension state escapes the `loadExts := false` / `freeRegions` bracket.
67#[derive(Clone, Debug, Eq, PartialEq)]
68pub struct LeanBracketedImportResult {
69    /// Import attribution captured before the compacted regions are freed.
70    pub import_stats: crate::host::session::LeanImportStats,
71    /// Per-request declaration metadata serialized inside the bracket.
72    pub declarations: Vec<LeanBracketedDeclarationInfo>,
73    /// Operations this path deliberately refuses because they require a normal
74    /// full session with loaded environment extensions.
75    pub rejected_operations: Vec<LeanBracketedRejectedOperation>,
76    /// Whether the Lean shim reached the `Environment.freeRegions` cleanup
77    /// point before returning the serialized result to Rust.
78    pub free_regions_ran: bool,
79}
80
81impl<'lean> TryFromLean<'lean> for LeanBracketedImportResult {
82    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
83        let free_regions_ran = {
84            let ctor = view(&obj).ctor_shape(0, 3, "BracketedImportResult")?;
85            ctor.bool(0, "BracketedImportResult.freeRegionsRan")?
86        };
87        let [import_stats, declarations, rejected_operations] =
88            take_ctor_objects::<3>(obj, 0, "BracketedImportResult")?;
89        Ok(Self {
90            import_stats: crate::host::session::LeanImportStats::try_from_lean(import_stats)?,
91            declarations: Vec::<LeanBracketedDeclarationInfo>::try_from_lean(declarations)?,
92            rejected_operations: Vec::<LeanBracketedRejectedOperation>::try_from_lean(rejected_operations)?,
93            free_regions_ran,
94        })
95    }
96}
97
98impl LeanBracketedImportResult {
99    pub(crate) fn query(
100        capabilities: &LeanCapabilities<'_, '_>,
101        imports: &[&str],
102        request: LeanBracketedImportRequest,
103        progress: Option<&dyn LeanProgressSink>,
104    ) -> LeanResult<Self> {
105        let search_paths = LeanSession::import_search_paths(capabilities)?;
106        let imports_owned: Vec<String> = imports.iter().map(|&import| import.to_owned()).collect();
107        let declaration_names = request.declaration_names;
108        with_session_import_lock(|| {
109            let shims = HostShimBindings::resolve(capabilities.shim_capability())
110                .map_err(|err| binding_error_to_lean_error(&err))?;
111            if let Some(sink) = progress {
112                let bridge = ProgressBridge::new(sink, "bracketed-import", Some(3))?;
113                let (handle, trampoline) = bridge.abi_parts();
114                let raw = shims.bracketed_import_query.call(
115                    search_paths,
116                    imports_owned,
117                    declaration_names,
118                    handle,
119                    trampoline,
120                )?;
121                Self::from_json(&bridge.decode::<String>(raw)?)
122            } else {
123                let raw = shims
124                    .bracketed_import_query
125                    .call(search_paths, imports_owned, declaration_names, 0, 0)?;
126                match Result::<String, u8>::try_from_lean(raw)? {
127                    Ok(json) => Self::from_json(&json),
128                    Err(status) => Err(lean_rs::__host_internals::host_internal(format!(
129                        "bracketed import query returned callback status {status} without a registered callback"
130                    ))),
131                }
132            }
133        })
134    }
135
136    fn from_json(raw: &str) -> LeanResult<Self> {
137        let wire: WireBracketedImportResult = serde_json::from_str(raw).map_err(|err| {
138            lean_rs::__host_internals::host_internal(format!("bracketed import query returned malformed JSON: {err}"))
139        })?;
140        Ok(wire.into())
141    }
142}
143
144/// Serialized declaration metadata produced inside the bracket.
145#[derive(Clone, Debug, Deserialize, Eq, PartialEq)]
146pub struct LeanBracketedDeclarationInfo {
147    pub name: String,
148    pub exists: bool,
149    pub kind: Option<String>,
150    pub module: Option<String>,
151    pub raw_type: Option<String>,
152}
153
154impl<'lean> TryFromLean<'lean> for LeanBracketedDeclarationInfo {
155    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
156        let exists = {
157            let ctor = view(&obj).ctor_shape(0, 4, "BracketedDeclarationInfo")?;
158            ctor.bool(0, "BracketedDeclarationInfo.existsDecl")?
159        };
160        let [name, kind, module, raw_type] = take_ctor_objects::<4>(obj, 0, "BracketedDeclarationInfo")?;
161        Ok(Self {
162            name: String::try_from_lean(name)?,
163            exists,
164            kind: Option::<String>::try_from_lean(kind)?,
165            module: Option::<String>::try_from_lean(module)?,
166            raw_type: Option::<String>::try_from_lean(raw_type)?,
167        })
168    }
169}
170
171/// Candidate operation deliberately excluded from the bracketed API.
172#[derive(Clone, Debug, Deserialize, Eq, PartialEq)]
173pub struct LeanBracketedRejectedOperation {
174    pub operation: String,
175    pub reason: String,
176}
177
178impl<'lean> TryFromLean<'lean> for LeanBracketedRejectedOperation {
179    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
180        let [operation, reason] = take_ctor_objects::<2>(obj, 0, "BracketedRejectedOperation")?;
181        Ok(Self {
182            operation: String::try_from_lean(operation)?,
183            reason: String::try_from_lean(reason)?,
184        })
185    }
186}
187
188#[derive(Deserialize)]
189struct WireBracketedImportResult {
190    import_stats: WireImportStats,
191    declarations: Vec<LeanBracketedDeclarationInfo>,
192    rejected_operations: Vec<LeanBracketedRejectedOperation>,
193    free_regions_ran: bool,
194}
195
196impl From<WireBracketedImportResult> for LeanBracketedImportResult {
197    fn from(value: WireBracketedImportResult) -> Self {
198        Self {
199            import_stats: value.import_stats.into(),
200            declarations: value.declarations,
201            rejected_operations: value.rejected_operations,
202            free_regions_ran: value.free_regions_ran,
203        }
204    }
205}
206
207#[derive(Deserialize)]
208struct WireImportStats {
209    direct_import_names: Vec<String>,
210    effective_module_count: u64,
211    compacted_region_count: u64,
212    memory_mapped_region_count: u64,
213    compacted_region_bytes: u64,
214    memory_mapped_region_bytes: u64,
215    non_memory_mapped_region_bytes: u64,
216    imported_bytes: u64,
217    imported_constant_count: u64,
218    extension_count: u64,
219    total_imported_extension_entries: u64,
220    import_level: String,
221    import_all: bool,
222    load_exts: bool,
223}
224
225impl From<WireImportStats> for crate::host::session::LeanImportStats {
226    fn from(value: WireImportStats) -> Self {
227        Self {
228            direct_import_names: value.direct_import_names,
229            effective_module_count: value.effective_module_count,
230            compacted_region_count: value.compacted_region_count,
231            memory_mapped_region_count: value.memory_mapped_region_count,
232            compacted_region_bytes: value.compacted_region_bytes,
233            memory_mapped_region_bytes: value.memory_mapped_region_bytes,
234            non_memory_mapped_region_bytes: value.non_memory_mapped_region_bytes,
235            imported_bytes: value.imported_bytes,
236            imported_constant_count: value.imported_constant_count,
237            extension_count: value.extension_count,
238            total_imported_extension_entries: value.total_imported_extension_entries,
239            import_level: value.import_level,
240            import_all: value.import_all,
241            load_exts: value.load_exts,
242        }
243    }
244}
lean_rs_host/host/bracketed.rs

lean_rs_host/host/
bracketed.rs
