Expand description
Canonical resolved view of the program for codegen consumers.
Single source of truth for “what does the program look like, after
name resolution, with module/entry scope preserved”. Backends that
used to walk CodegenContext.{items, fn_defs, type_defs} (raw
ast::*) should iterate this view’s resolved fn defs instead. The
AST-shape fields on CodegenContext remain available as source
metadata (spans, diagnostics, syntax-discovery), not as the
authoritative backend input.
§Current Typed HIR boundary (post epic #180)
Aver’s Typed HIR is a query layer, not a duplicate IR enum. Its two structural primitives — what backends mean when they reach for “the typed program” — are:
ResolvedProgramView(this struct). The canonical post-name- resolution program: everyFnDefprojected throughcrate::ir::hir::ResolvedFnDefwith typedparams: Vec<(String, Type)>andreturn_type: Type, indexed by opaquecrate::ir::FnId. Backends ask “what does this fn look like?” throughfn_by_idorentry_fns()/module_fns(prefix)and get typed answers.- Stamped
crate::ast::Spanned<crate::ir::hir::ResolvedExpr>. Every reachable body expression in a well-typed program has.ty().is_some()after the typechecker stamps and the resolver propagates. Backends read inferred types per node without re-running inference.
Together they answer “what name does this refer to?” (resolved
HIR via FnId / TypeId / CtorId) and “what type does this
expression have?” (typed slot via Spanned::ty()).
Conscious exceptions still walking ast::* directly (each
documented at the call site):
verify_lawhelper walkers (crate::verify_law). The helper-law / contextual-helper hint walkers operate on entry-only ASTFnDefs throughcrate::verify_law::EntryFnIndex. The parser invariant (verify <name>only accepts a singleIdent) keeps the identity-safe contract; migration to FnId keying is gated on module-scoped verify shipping.- Lean / Dafny proof + law spec emitters. Several recognisers
(
emit_*_spec_equivalence_law,direct_callAST shape match) keep walkingSpanned<Expr>source-shape because the proof IR is keyed on syntactic surfaces the user wrote, not the resolver- canonicalised form.emit_expr_legacyis the explicit adapter. - wasm-gc post-link view ([
crate::codegen::wasm_gc::view]). The wasm-gc backend collapses N modules into one emit unit viaflatten_multimodule, then rebuilds its owncrate::ir::SymbolTable+ resolver pass over the flattened slice. The post-link namespace is the identity layer in that backend; the documentedbackend-link-stagecategory covers it.
Trigger-driven follow-up (NOT scoped to #180):
- MIR / Core IR. Per-expression effects, SSA / CFG / explicit ownership / effect tracking per instruction belong to a separate epic. Typed HIR is the substrate they lower from; build the IR when an inliner / monomorphiser / cross-scope optimiser needs it.
TypedProgramViewwrapper. Combiningresolved_program’sFnIdindex with the typed expression slot into one query surface (view.fn_by_id(id).body_expr_type(span)or similar) would tighten the contract but adds no semantic value today — wait for a real consumer.- Module-scoped verify → FnId keyed
verify_law. TheEntryFnIndexnewtype is the tripwire that forces the contributor to address keying when the parser starts accepting dotted verify targets.
§Construction
Built once at the codegen boundary:
- Entry slice projects from
PipelineResult.resolved_items— the resolver pass populates this unconditionally, so we just pick out theResolvedTopLevel::FnDefvariants and clone the resolved fn defs out of them. No re-resolve. - Module slice resolves each dep module’s
&[FnDef]throughresolve_fn_def_externalunder aResolveCtxpinned to that module’s prefix. This is the only producer of resolved module bodies —CodegenContext.resolved_module_fn_defsis a projection / cache of this view, not an independent source.
§Lookups
The view exposes fn_by_id(FnId) so callsites that have an opaque
FnId in hand (typical for identity-sensitive emit) can recover
the resolved body without round-tripping through bare names.
Iteration is provided per-scope: entry_fns() walks the entry
slice; module_fns(prefix) walks one dep module’s slice.
Epic #170 Phase 1: this is the foundation every later phase builds on. Backends migrate to consuming the view as primary input in subsequent PRs; this PR only consolidates the producer side without touching backend signatures.
Structs§
- Resolved
Module Fns - Resolved-form mirror of one dep module’s fn defs, with the
module’s prefix preserved so per-scope iteration is cheap and the
view can build an
FnId-keyed lookup without losing scope. - Resolved
Program View - Canonical resolved-program view consumed by codegen.