Struct ResolvedProgramView 

pub struct ResolvedProgramView {
    pub entry_items: Vec<ResolvedTopLevel>,
    pub modules: Vec<ResolvedModuleFns>,
    /* private fields */
}

Canonical resolved-program view consumed by codegen.

Holds the entry-scope items (post-pipeline, post-NameResolve) plus each dep module’s resolved fn defs, with an FnId index so identity-keyed lookups don’t walk linearly.

Fields

entry_items: Vec<ResolvedTopLevel>

Entry-scope resolved items, exactly as the pipeline produced them. Includes FnDef, Module markers, and Passthrough variants (verify/decision/typedef nodes that haven’t been promoted to resolved form yet — see ResolvedTopLevel).

modules: Vec<ResolvedModuleFns>

Per-dep-module resolved fn defs. Order matches the input Vec<ModuleInfo> so existing position-keyed consumers still work during migration.

Implementations

impl ResolvedProgramView

pub fn build( entry_items: Vec<ResolvedTopLevel>, modules: &[ModuleInfo], symbol_table: &SymbolTable, ) -> Self

Build the view from a pipeline-produced entry slice and the Vec<ModuleInfo> carrying dep modules’ AST fn defs. The caller has already run pipeline::run (or equivalent) and is passing through the canonical resolved_items — we do not re-resolve the entry side. Module fn defs are resolved here (the pipeline doesn’t walk them), pinning ResolveCtx.current_module to each module’s prefix so a dotted reference inside one module’s body resolves through that module’s import set first.

pub fn entry_fns(&self) -> impl Iterator<Item = &ResolvedFnDef> + '_

Resolved entry-scope fn defs in source order — the same set CodegenContext.resolved_fn_defs projected today, just reached through the canonical view.

pub fn module_fns( &self, prefix: &str, ) -> impl Iterator<Item = &ResolvedFnDef> + '_

Resolved fn defs from one dep module, in source order. Returns an empty iterator when no module with that prefix is present — callers that need an existence check should use Self::module instead.

pub fn module(&self, prefix: &str) -> Option<&ResolvedModuleFns>

Whole module slice (prefix + resolved fns) for callsites that need the prefix alongside.

pub fn fn_by_id(&self, id: FnId) -> Option<&ResolvedFnDef>

FnId-keyed lookup. Returns the resolved fn def regardless of scope — identity-sensitive consumers (proof emitter, inliner, monomorph) reach this rather than walking entry + modules manually.

pub fn fn_by_name(&self, name: &str) -> Option<&ResolvedFnDef>

First fn (entry first, then dep modules in declaration order) whose source-level name matches. Stage 5+ of #232 uses this to bridge ad-hoc detectors that historically searched by string name (is_directly_recursive in dafny codegen) into the typed FnId-keyed ProgramShape. Returns None if no such fn exists in the resolved view.

Note: bare-name lookup is ambiguous when the same name lives in two dep modules. Entry-first ordering matches what the legacy string-name detectors already assumed.

Trait Implementations

impl Clone for ResolvedProgramView

fn clone(&self) -> ResolvedProgramView

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ResolvedProgramView

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

Formats the value using the given formatter.

impl Default for ResolvedProgramView

fn default() -> ResolvedProgramView

Returns the “default value” for a type.