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 experimental bracketed import path.
20#[derive(Clone, Debug, Default, Eq, PartialEq)]
21pub struct LeanBracketedImportRequest {
22    pub declaration_names: Vec<String>,
23}
24
25impl LeanBracketedImportRequest {
26    #[must_use]
27    pub fn new(declaration_names: impl IntoIterator<Item = impl Into<String>>) -> Self {
28        Self {
29            declaration_names: declaration_names.into_iter().map(Into::into).collect(),
30        }
31    }
32}
33
34impl<'lean> IntoLean<'lean> for LeanBracketedImportRequest {
35    fn into_lean(self, runtime: &'lean lean_rs::LeanRuntime) -> Obj<'lean> {
36        alloc_ctor_with_objects(runtime, 0, [self.declaration_names.into_lean(runtime)])
37    }
38}
39
40impl sealed::SealedAbi for LeanBracketedImportRequest {}
41
42impl<'lean> LeanAbi<'lean> for LeanBracketedImportRequest {
43    type CRepr = <Obj<'lean> as LeanAbi<'lean>>::CRepr;
44
45    fn into_c(self, runtime: &'lean lean_rs::LeanRuntime) -> Self::CRepr {
46        self.into_lean(runtime).into_raw()
47    }
48
49    fn from_c(_c: Self::CRepr, _runtime: &'lean lean_rs::LeanRuntime) -> LeanResult<Self> {
50        Err(conversion_error(
51            "LeanBracketedImportRequest cannot decode a Lean call result; it is an argument-only type",
52        ))
53    }
54}
55
56/// Result of one bracketed no-extension import query.
57#[derive(Clone, Debug, Eq, PartialEq)]
58pub struct LeanBracketedImportResult {
59    pub import_stats: crate::host::session::LeanImportStats,
60    pub declarations: Vec<LeanBracketedDeclarationInfo>,
61    pub rejected_operations: Vec<LeanBracketedRejectedOperation>,
62    pub free_regions_ran: bool,
63}
64
65impl<'lean> TryFromLean<'lean> for LeanBracketedImportResult {
66    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
67        let free_regions_ran = {
68            let ctor = view(&obj).ctor_shape(0, 3, "BracketedImportResult")?;
69            ctor.bool(0, "BracketedImportResult.freeRegionsRan")?
70        };
71        let [import_stats, declarations, rejected_operations] =
72            take_ctor_objects::<3>(obj, 0, "BracketedImportResult")?;
73        Ok(Self {
74            import_stats: crate::host::session::LeanImportStats::try_from_lean(import_stats)?,
75            declarations: Vec::<LeanBracketedDeclarationInfo>::try_from_lean(declarations)?,
76            rejected_operations: Vec::<LeanBracketedRejectedOperation>::try_from_lean(rejected_operations)?,
77            free_regions_ran,
78        })
79    }
80}
81
82impl LeanBracketedImportResult {
83    pub(crate) fn query(
84        capabilities: &LeanCapabilities<'_, '_>,
85        imports: &[&str],
86        request: LeanBracketedImportRequest,
87        progress: Option<&dyn LeanProgressSink>,
88    ) -> LeanResult<Self> {
89        let search_paths = LeanSession::import_search_paths(capabilities)?;
90        let imports_owned: Vec<String> = imports.iter().map(|&import| import.to_owned()).collect();
91        let declaration_names = request.declaration_names;
92        with_session_import_lock(|| {
93            let shims = HostShimBindings::resolve(capabilities.shim_capability())
94                .map_err(|err| binding_error_to_lean_error(&err))?;
95            if let Some(sink) = progress {
96                let bridge = ProgressBridge::new(sink, "bracketed-import", Some(3))?;
97                let (handle, trampoline) = bridge.abi_parts();
98                let raw = shims.bracketed_import_query.call(
99                    search_paths,
100                    imports_owned,
101                    declaration_names,
102                    handle,
103                    trampoline,
104                )?;
105                Self::from_json(&bridge.decode::<String>(raw)?)
106            } else {
107                let raw = shims
108                    .bracketed_import_query
109                    .call(search_paths, imports_owned, declaration_names, 0, 0)?;
110                match Result::<String, u8>::try_from_lean(raw)? {
111                    Ok(json) => Self::from_json(&json),
112                    Err(status) => Err(lean_rs::__host_internals::host_internal(format!(
113                        "bracketed import query returned callback status {status} without a registered callback"
114                    ))),
115                }
116            }
117        })
118    }
119
120    fn from_json(raw: &str) -> LeanResult<Self> {
121        let wire: WireBracketedImportResult = serde_json::from_str(raw).map_err(|err| {
122            lean_rs::__host_internals::host_internal(format!("bracketed import query returned malformed JSON: {err}"))
123        })?;
124        Ok(wire.into())
125    }
126}
127
128/// Serialized declaration metadata produced inside the bracket.
129#[derive(Clone, Debug, Deserialize, Eq, PartialEq)]
130pub struct LeanBracketedDeclarationInfo {
131    pub name: String,
132    pub exists: bool,
133    pub kind: Option<String>,
134    pub module: Option<String>,
135    pub raw_type: Option<String>,
136}
137
138impl<'lean> TryFromLean<'lean> for LeanBracketedDeclarationInfo {
139    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
140        let exists = {
141            let ctor = view(&obj).ctor_shape(0, 4, "BracketedDeclarationInfo")?;
142            ctor.bool(0, "BracketedDeclarationInfo.existsDecl")?
143        };
144        let [name, kind, module, raw_type] = take_ctor_objects::<4>(obj, 0, "BracketedDeclarationInfo")?;
145        Ok(Self {
146            name: String::try_from_lean(name)?,
147            exists,
148            kind: Option::<String>::try_from_lean(kind)?,
149            module: Option::<String>::try_from_lean(module)?,
150            raw_type: Option::<String>::try_from_lean(raw_type)?,
151        })
152    }
153}
154
155/// Candidate operation deliberately excluded from the bracketed API.
156#[derive(Clone, Debug, Deserialize, Eq, PartialEq)]
157pub struct LeanBracketedRejectedOperation {
158    pub operation: String,
159    pub reason: String,
160}
161
162impl<'lean> TryFromLean<'lean> for LeanBracketedRejectedOperation {
163    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
164        let [operation, reason] = take_ctor_objects::<2>(obj, 0, "BracketedRejectedOperation")?;
165        Ok(Self {
166            operation: String::try_from_lean(operation)?,
167            reason: String::try_from_lean(reason)?,
168        })
169    }
170}
171
172#[derive(Deserialize)]
173struct WireBracketedImportResult {
174    import_stats: WireImportStats,
175    declarations: Vec<LeanBracketedDeclarationInfo>,
176    rejected_operations: Vec<LeanBracketedRejectedOperation>,
177    free_regions_ran: bool,
178}
179
180impl From<WireBracketedImportResult> for LeanBracketedImportResult {
181    fn from(value: WireBracketedImportResult) -> Self {
182        Self {
183            import_stats: value.import_stats.into(),
184            declarations: value.declarations,
185            rejected_operations: value.rejected_operations,
186            free_regions_ran: value.free_regions_ran,
187        }
188    }
189}
190
191#[derive(Deserialize)]
192struct WireImportStats {
193    direct_import_names: Vec<String>,
194    effective_module_count: u64,
195    compacted_region_count: u64,
196    memory_mapped_region_count: u64,
197    compacted_region_bytes: u64,
198    memory_mapped_region_bytes: u64,
199    non_memory_mapped_region_bytes: u64,
200    imported_bytes: u64,
201    imported_constant_count: u64,
202    extension_count: u64,
203    total_imported_extension_entries: u64,
204    import_level: String,
205    import_all: bool,
206    load_exts: bool,
207}
208
209impl From<WireImportStats> for crate::host::session::LeanImportStats {
210    fn from(value: WireImportStats) -> Self {
211        Self {
212            direct_import_names: value.direct_import_names,
213            effective_module_count: value.effective_module_count,
214            compacted_region_count: value.compacted_region_count,
215            memory_mapped_region_count: value.memory_mapped_region_count,
216            compacted_region_bytes: value.compacted_region_bytes,
217            memory_mapped_region_bytes: value.memory_mapped_region_bytes,
218            non_memory_mapped_region_bytes: value.non_memory_mapped_region_bytes,
219            imported_bytes: value.imported_bytes,
220            imported_constant_count: value.imported_constant_count,
221            extension_count: value.extension_count,
222            total_imported_extension_entries: value.total_imported_extension_entries,
223            import_level: value.import_level,
224            import_all: value.import_all,
225            load_exts: value.load_exts,
226        }
227    }
228}
lean_rs_host/host/bracketed.rs

lean_rs_host/host/
bracketed.rs
