Struct ProcessedFile 

pub struct ProcessedFile {
    pub commands: Vec<CommandInfoNode>,
    pub terms: Vec<TermInfoNode>,
    pub tactics: Vec<TacticInfoNode>,
    pub names: Vec<NameRefNode>,
    pub diagnostics: LeanElabFailure,
}

FFI-safe projection of a processed Lean source string’s Elab.InfoTree.

Four arrays of structurally distinct nodes plus the diagnostics payload the elaborator emitted. The projection is a value type: no Lean references survive on the Rust side, so a ProcessedFile crosses thread boundaries cleanly.

Fields

commands: Vec<CommandInfoNode>

One entry per top-level command.

terms: Vec<TermInfoNode>

One entry per Elab.TermInfo node the elaborator emitted.

tactics: Vec<TacticInfoNode>

One entry per Elab.TacticInfo node the elaborator emitted.

names: Vec<NameRefNode>

Every identifier occurrence (binding sites and use sites).

diagnostics: LeanElabFailure

Diagnostics from the elaborator’s MessageLog, with the same byte-budget semantics as crate::host::evidence::LeanKernelOutcome::Rejected.

Implementations

impl ProcessedFile

pub fn term_at(&self, line: u32, column: u32) -> Option<&TermInfoNode>

Return the innermost TermInfoNode whose source range contains the position (line, column). None if no recorded term covers the position. Ties on range area are broken by encounter order (the elaborator’s outer-to-inner traversal).

pub fn tactic_at(&self, line: u32, column: u32) -> Option<&TacticInfoNode>

Return the innermost TacticInfoNode whose source range contains the position.

pub fn references_of<'a>(&'a self, name: &str) -> Vec<&'a NameRefNode>

Return every NameRefNode whose name exactly matches name, in encounter order. No normalisation: the caller is responsible for matching the fully-qualified form Lean records (e.g., "Nat.succ", not "succ").

Trait Implementations

impl Clone for ProcessedFile

fn clone(&self) -> ProcessedFile

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ProcessedFile

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'lean> TryFromLean<'lean> for ProcessedFile

fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self>

Decode obj into Self, returning a LeanError::Host with stage [HostStage::Conversion] if the object’s kind or payload is outside the type’s representable range.