lean_rs_host/host/process/
info_tree.rs

1//! [`ProcessedFile`] and its four node types — the FFI-safe projection
2//! of `Lean.Elab.InfoTree` returned by
3//! [`crate::LeanSession::process_with_info_tree`].
4//!
5//! All fields are public: the projection is a value type, not a handle,
6//! and the encoding is part of the contract with Lean (see
7//! `LeanRsHostShims/InfoTree.lean`). Owned `String`s and primitive
8//! integers only — the whole structure is `Send + Sync + 'static` so
9//! it crosses worker-thread channels cleanly.
10
11// SAFETY DOC: the single `unsafe { ... }` block in this file carries
12// its own `// SAFETY:` comment; the blanket allow keeps the scope
13// minimal per `docs/architecture/01-safety-model.md`.
14#![allow(unsafe_code)]
15
16use lean_rs::Obj;
17use lean_rs::abi::structure::{ctor_tag, take_ctor_objects};
18use lean_rs::abi::traits::{TryFromLean, conversion_error};
19use lean_rs::error::LeanResult;
20use lean_rs_sys::ctor::lean_ctor_get_uint8;
21
22use crate::host::elaboration::LeanElabFailure;
23
24/// One `Lean.Elab.TermInfo` projection.
25///
26/// `expr_str` / `type_str` use Lean's raw `Expr.toString` projection
27/// (same shape as [`crate::LeanSession::expr_to_string_raw`]); for the
28/// notation-aware rendering call the optional
29/// [`crate::host::meta::pp_expr`] service against the original `Expr`.
30#[derive(Clone, Debug, Eq, PartialEq)]
31pub struct TermInfoNode {
32    /// 1-based start line.
33    pub start_line: u32,
34    /// 1-based start column.
35    pub start_column: u32,
36    /// 1-based end line.
37    pub end_line: u32,
38    /// 1-based end column.
39    pub end_column: u32,
40    /// `Expr.toString` of the elaborated expression.
41    pub expr_str: String,
42    /// `Expr.toString` of the inferred type, or empty if inference
43    /// failed at the recorded site.
44    pub type_str: String,
45    /// `Expr.toString` of the expected type when the elaborator recorded
46    /// one (e.g., a coercion site).
47    pub expected_type_str: Option<String>,
48}
49
50impl<'lean> TryFromLean<'lean> for TermInfoNode {
51    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
52        let [sl, sc, el, ec, expr, ty, exp_ty] = take_ctor_objects::<7>(obj, 0, "TermInfoNode")?;
53        Ok(Self {
54            start_line: u32::try_from_lean(sl)?,
55            start_column: u32::try_from_lean(sc)?,
56            end_line: u32::try_from_lean(el)?,
57            end_column: u32::try_from_lean(ec)?,
58            expr_str: String::try_from_lean(expr)?,
59            type_str: String::try_from_lean(ty)?,
60            expected_type_str: Option::<String>::try_from_lean(exp_ty)?,
61        })
62    }
63}
64
65/// One `Lean.Elab.TacticInfo` projection.
66///
67/// `goals_before` / `goals_after` are already pretty-printed by the
68/// Lean shim inside the elaboration's `MetaM` context. Empty arrays
69/// mean the elaborator recorded the tactic without an enclosing goals
70/// list (rare). The strings carry no metavariable identity that the
71/// Rust side can reuse — they are diagnostic text only.
72#[derive(Clone, Debug, Eq, PartialEq)]
73pub struct TacticInfoNode {
74    /// 1-based start line.
75    pub start_line: u32,
76    /// 1-based start column.
77    pub start_column: u32,
78    /// 1-based end line.
79    pub end_line: u32,
80    /// 1-based end column.
81    pub end_column: u32,
82    /// Goals as the user would see them before this tactic ran.
83    pub goals_before: Vec<String>,
84    /// Goals as the user would see them after this tactic ran.
85    pub goals_after: Vec<String>,
86}
87
88impl<'lean> TryFromLean<'lean> for TacticInfoNode {
89    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
90        let [sl, sc, el, ec, gb, ga] = take_ctor_objects::<6>(obj, 0, "TacticInfoNode")?;
91        Ok(Self {
92            start_line: u32::try_from_lean(sl)?,
93            start_column: u32::try_from_lean(sc)?,
94            end_line: u32::try_from_lean(el)?,
95            end_column: u32::try_from_lean(ec)?,
96            goals_before: Vec::<String>::try_from_lean(gb)?,
97            goals_after: Vec::<String>::try_from_lean(ga)?,
98        })
99    }
100}
101
102/// One identifier occurrence the elaborator recorded.
103///
104/// `is_binder` distinguishes binding sites from use sites — the same
105/// distinction Lean's LSP uses to answer "go to definition" vs. "find
106/// references". `name` is the fully-qualified name when the reference
107/// resolved to a constant; for binder occurrences it is the raw bound
108/// identifier.
109#[derive(Clone, Debug, Eq, PartialEq)]
110pub struct NameRefNode {
111    /// 1-based start line.
112    pub start_line: u32,
113    /// 1-based start column.
114    pub start_column: u32,
115    /// 1-based end line.
116    pub end_line: u32,
117    /// 1-based end column.
118    pub end_column: u32,
119    /// Fully-qualified name when resolved to a constant; raw identifier
120    /// for binder occurrences.
121    pub name: String,
122    /// `true` for binding sites, `false` for use-site references.
123    pub is_binder: bool,
124}
125
126impl<'lean> TryFromLean<'lean> for NameRefNode {
127    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
128        // Lean packs the `Bool isBinder` field into the scalar tail of
129        // the constructor (one byte at offset 0 past the five object
130        // slots), mirroring `ElabFailure.truncated`. Read the scalar
131        // before consuming the object slots.
132        let tag = ctor_tag(&obj)?;
133        if tag != 0 {
134            return Err(conversion_error(format!(
135                "expected Lean NameRefNode ctor (tag 0), found tag {tag}"
136            )));
137        }
138        let ptr = obj.as_raw_borrowed();
139        // SAFETY: ctor validated above; the first scalar-tail byte holds
140        // the `Bool isBinder` value (0 = false, 1 = true).
141        let is_binder_byte = unsafe { lean_ctor_get_uint8(ptr, 0) };
142        let is_binder = match is_binder_byte {
143            0 => false,
144            1 => true,
145            other => {
146                return Err(conversion_error(format!(
147                    "Lean NameRefNode.isBinder byte {other} is not in {{0, 1}}"
148                )));
149            }
150        };
151        let [sl, sc, el, ec, nm] = take_ctor_objects::<5>(obj, 0, "NameRefNode")?;
152        Ok(Self {
153            start_line: u32::try_from_lean(sl)?,
154            start_column: u32::try_from_lean(sc)?,
155            end_line: u32::try_from_lean(el)?,
156            end_column: u32::try_from_lean(ec)?,
157            name: String::try_from_lean(nm)?,
158            is_binder,
159        })
160    }
161}
162
163/// One top-level command the elaborator processed.
164///
165/// `decl_name` is set only for commands that introduce a named
166/// declaration (`def`, `theorem`, `instance`, …); other commands such
167/// as `#check` carry `None`.
168#[derive(Clone, Debug, Eq, PartialEq)]
169pub struct CommandInfoNode {
170    /// 1-based start line.
171    pub start_line: u32,
172    /// 1-based start column.
173    pub start_column: u32,
174    /// 1-based end line.
175    pub end_line: u32,
176    /// 1-based end column.
177    pub end_column: u32,
178    /// Declared name when the command introduces one.
179    pub decl_name: Option<String>,
180}
181
182impl<'lean> TryFromLean<'lean> for CommandInfoNode {
183    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
184        let [sl, sc, el, ec, dn] = take_ctor_objects::<5>(obj, 0, "CommandInfoNode")?;
185        Ok(Self {
186            start_line: u32::try_from_lean(sl)?,
187            start_column: u32::try_from_lean(sc)?,
188            end_line: u32::try_from_lean(el)?,
189            end_column: u32::try_from_lean(ec)?,
190            decl_name: Option::<String>::try_from_lean(dn)?,
191        })
192    }
193}
194
195/// FFI-safe projection of a processed Lean source string's
196/// `Elab.InfoTree`.
197///
198/// Four arrays of structurally distinct nodes plus the diagnostics
199/// payload the elaborator emitted. The projection is a value type:
200/// no Lean references survive on the Rust side, so a `ProcessedFile`
201/// crosses thread boundaries cleanly.
202#[derive(Clone, Debug)]
203pub struct ProcessedFile {
204    /// One entry per top-level command.
205    pub commands: Vec<CommandInfoNode>,
206    /// One entry per `Elab.TermInfo` node the elaborator emitted.
207    pub terms: Vec<TermInfoNode>,
208    /// One entry per `Elab.TacticInfo` node the elaborator emitted.
209    pub tactics: Vec<TacticInfoNode>,
210    /// Every identifier occurrence (binding sites and use sites).
211    pub names: Vec<NameRefNode>,
212    /// Diagnostics from the elaborator's `MessageLog`, with the same
213    /// byte-budget semantics as
214    /// [`crate::host::evidence::LeanKernelOutcome::Rejected`].
215    pub diagnostics: LeanElabFailure,
216}
217
218impl ProcessedFile {
219    /// Return the innermost [`TermInfoNode`] whose source range contains
220    /// the position `(line, column)`. `None` if no recorded term covers
221    /// the position. Ties on range area are broken by encounter order
222    /// (the elaborator's outer-to-inner traversal).
223    #[must_use]
224    pub fn term_at(&self, line: u32, column: u32) -> Option<&TermInfoNode> {
225        smallest_containing(&self.terms, line, column, |n| {
226            (n.start_line, n.start_column, n.end_line, n.end_column)
227        })
228    }
229
230    /// Return the innermost [`TacticInfoNode`] whose source range
231    /// contains the position.
232    #[must_use]
233    pub fn tactic_at(&self, line: u32, column: u32) -> Option<&TacticInfoNode> {
234        smallest_containing(&self.tactics, line, column, |n| {
235            (n.start_line, n.start_column, n.end_line, n.end_column)
236        })
237    }
238
239    /// Return every [`NameRefNode`] whose `name` exactly matches `name`,
240    /// in encounter order. No normalisation: the caller is responsible
241    /// for matching the fully-qualified form Lean records (e.g.,
242    /// `"Nat.succ"`, not `"succ"`).
243    #[must_use]
244    pub fn references_of<'a>(&'a self, name: &str) -> Vec<&'a NameRefNode> {
245        self.names.iter().filter(|n| n.name == name).collect()
246    }
247}
248
249impl<'lean> TryFromLean<'lean> for ProcessedFile {
250    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
251        let [commands, terms, tactics, names, diagnostics] = take_ctor_objects::<5>(obj, 0, "ProcessedFile")?;
252        Ok(Self {
253            commands: Vec::<CommandInfoNode>::try_from_lean(commands)?,
254            terms: Vec::<TermInfoNode>::try_from_lean(terms)?,
255            tactics: Vec::<TacticInfoNode>::try_from_lean(tactics)?,
256            names: Vec::<NameRefNode>::try_from_lean(names)?,
257            diagnostics: LeanElabFailure::try_from_lean(diagnostics)?,
258        })
259    }
260}
261
262fn smallest_containing<T>(
263    nodes: &[T],
264    line: u32,
265    column: u32,
266    range: impl Fn(&T) -> (u32, u32, u32, u32),
267) -> Option<&T> {
268    let mut best: Option<(&T, u64)> = None;
269    for node in nodes {
270        let (sl, sc, el, ec) = range(node);
271        if !range_contains(sl, sc, el, ec, line, column) {
272            continue;
273        }
274        let area = range_area(sl, sc, el, ec);
275        match best {
276            None => best = Some((node, area)),
277            Some((_, best_area)) if area < best_area => best = Some((node, area)),
278            _ => {}
279        }
280    }
281    best.map(|(node, _)| node)
282}
283
284fn range_contains(sl: u32, sc: u32, el: u32, ec: u32, line: u32, column: u32) -> bool {
285    if line < sl || line > el {
286        return false;
287    }
288    if line == sl && column < sc {
289        return false;
290    }
291    if line == el && column > ec {
292        return false;
293    }
294    true
295}
296
297fn range_area(sl: u32, sc: u32, el: u32, ec: u32) -> u64 {
298    // Treat lines as worth a large constant so cross-line ranges always
299    // dominate single-line ranges. Columns break ties on the same line.
300    let line_span = u64::from(el.saturating_sub(sl));
301    let col_span = u64::from(ec).saturating_sub(u64::from(sc));
302    line_span.saturating_mul(1_000_000).saturating_add(col_span)
303}
lean_rs_host/host/process/info_tree.rs

lean_rs_host/host/process/
info_tree.rs
