lean_rs_host/host/process/mod.rs
1//! Info-tree projection capability on [`crate::LeanSession`].
2//!
3//! Two sibling entry points project a Lean source into the FFI-safe
4//! [`ProcessedFile`] structure:
5//!
6//! - [`crate::LeanSession::process_with_info_tree`] takes a body-only
7//! snippet (no `import` header). It drives `IO.processCommands`
8//! from byte 0 with an empty `ModuleParserState` — the right call
9//! for inline scratch buffers and tactic-level snippets.
10//! - [`crate::LeanSession::process_module_with_info_tree`] takes a full
11//! Lean source file (header + body). It calls `Lean.Parser.parseHeader`
12//! first, then resumes `IO.processCommands` from the parser state
13//! the header parser produced — the right call for real files
14//! beginning with `import …`. Position coordinates in the returned
15//! projection are in the original file's line/column system with no
16//! Rust-side offset arithmetic.
17//!
18//! Both shims share the projection machinery (one `Elab.InfoTree`
19//! walk that records four arrays of structurally distinct nodes plus
20//! the elaborator's diagnostics). The projection is the boundary —
21//! raw `InfoTree` never crosses the FFI line, because it carries
22//! metavariable contexts and `Lean.Expr` values that cannot be revived
23//! outside the elaboration session that produced them.
24//!
25//! Each node carries an explicit `(start_line, start_column, end_line,
26//! end_column)` source range so callers can build cursor-position
27//! queries without further Lean calls. [`ProcessedFile::term_at`],
28//! [`ProcessedFile::tactic_at`], and [`ProcessedFile::references_of`]
29//! cover the three queries downstream cursor tooling needs; new lookup
30//! shapes are pure Rust on top of the same projection.
31//!
32//! Both Lean shims are **optional**: a capability dylib forked without
33//! either shim collapses to the corresponding `Unsupported` arm at
34//! dispatch time, matching the meta-service degradation pattern.
35
36mod info_tree;
37mod outcome;
38
39pub use self::info_tree::{CommandInfoNode, NameRefNode, ProcessedFile, TacticInfoNode, TermInfoNode};
40pub use self::outcome::{ProcessFileOutcome, ProcessModuleOutcome};