Skip to main content

aver/ir/hir/
mod.rs

1//! Resolved AST / High-level IR — typed-identity layer between
2//! [`crate::ast`] and the backends.
3//!
4//! ## Why this layer exists
5//!
6//! Pre-Phase-E backends consumed `crate::ast::Expr` directly. That
7//! shape carries source-level names everywhere: `Expr::FnCall(Ident
8//! "foo")` for a call, `Expr::Constructor("Result.Ok", arg)` for a
9//! variant, `Expr::RecordCreate { type_name: "Shape", … }` for a
10//! record. Every backend (VM compiler, Rust codegen, wasm-gc, Lean,
11//! Dafny, self-host) re-derived identity from those strings — six
12//! independent resolvers each guessing the same answer, drifting
13//! whenever a corner case touched only one of them. The proof IR
14//! layer (PRs #141–#146) moved the proof flow onto opaque `FnId` /
15//! `TypeId` / `CtorId`; Phase B (#148) did the same for the
16//! typechecker's internal `fn_sigs` + matcher. Phase E generalises
17//! the move to a shared resolved AST every backend reads.
18//!
19//! ## Contract
20//!
21//! [`ResolvedExpr`] is a mechanical translation of `Expr` — same
22//! shape, same operator precedence, same evaluation order. The only
23//! difference is that every name that referred to a declared symbol
24//! is replaced by its opaque ID:
25//!
26//! - `FnCall(Box<Spanned<Expr>>, …)` → [`ResolvedExpr::Call`] with
27//!   a [`ResolvedCallee`] discriminating user fn / builtin namespace
28//!   method / local lambda / ambient operator.
29//! - `Constructor(String, …)` → [`ResolvedExpr::Ctor`] with a
30//!   [`ResolvedCtor`] discriminating user `CtorId` / built-in
31//!   variant (`Result.Ok` / `Result.Err` / `Option.Some` /
32//!   `Option.None`).
33//! - `RecordCreate { type_name, fields }` → [`ResolvedExpr::RecordCreate`]
34//!   with a `TypeId` (always `Some` for user records — built-in
35//!   record types stay `Type::Named { id: None, … }` everywhere,
36//!   including here).
37//! - `RecordUpdate` → [`ResolvedExpr::RecordUpdate`] same.
38//! - `TailCall(TailCallData)` → [`ResolvedExpr::TailCall`] with a
39//!   `FnId` for the target.
40//! - `Pattern::Constructor(name, bindings)` → [`ResolvedPattern::Ctor`]
41//!   with a [`ResolvedCtor`].
42//! - `Stmt::Binding(name, Option<String>, expr)` →
43//!   [`ResolvedStmt::Binding`] with a resolved
44//!   [`crate::ast::Type`] annotation instead of a string.
45//!
46//! Anything that doesn't reference a declared symbol passes through
47//! structurally — literals, binops, neg, list / tuple / map
48//! literals, interpolation, independent products, error-prop, slot
49//! resolutions (`Expr::Resolved`), match arms (recursively
50//! resolved).
51//!
52//! ## What this layer does NOT do
53//!
54//! - **No semantic information added** beyond identity. Refinement
55//!   subtype decisions, recursion contracts, law theorems — all of
56//!   that stays in [`crate::ir::ProofIR`]. Resolved HIR is the
57//!   universal substrate, not a proof IR.
58//! - **No optimization**. The lowering is one-to-one; the same
59//!   number of expressions land on the other side.
60//! - **No effect propagation rewriting**. Effects stay on the
61//!   resolved fn signature exactly as the typechecker classified
62//!   them.
63//!
64//! ## What's NOT in this PR
65//!
66//! This module ships the shape only — definitions + smoke tests.
67//! Future PRs in the Phase E stack:
68//!
69//! - **PR 2** (`name_resolve` pass): builds [`ResolvedExpr`] from
70//!   `Expr` by walking the AST against a `SymbolTable` +
71//!   typechecker result.
72//! - **PR 3+** (one per backend): each backend migrates from
73//!   consuming `Expr` to [`ResolvedExpr`]. Old paths stay as
74//!   fallback during migration.
75//! - **PR N** (cleanup): drop pre-resolve consumers, remove the
76//!   bare-string lookups that the resolved layer subsumes (Phase D
77//!   in #147 terminology).
78
79use crate::ast::{AnnotBool, BinOp, FnResolution, Literal, Module, Spanned, Type};
80use crate::ir::identity::{CtorId, FnId, TypeId};
81
82pub mod classify;
83pub mod dump;
84pub mod resolve;
85pub use classify::{
86    ForwardSlot, ResolvedBodyBindingPlan, ResolvedBodyExprPlan, ResolvedBodyPlan,
87    ResolvedBoolSubjectPlan, ResolvedForwardCallPlan, ResolvedLeafOp, ResolvedThinBodyPlan,
88    ThinKind, call_plan_from_resolved_callee, classify_body_expr_plan_resolved,
89    classify_body_plan_resolved, classify_bool_match_shape_resolved,
90    classify_bool_subject_plan_resolved, classify_dispatch_pattern_resolved,
91    classify_dispatch_table_shape_resolved, classify_forward_call_resolved,
92    classify_leaf_op_resolved, classify_list_match_shape_resolved,
93    classify_match_dispatch_plan_resolved, classify_thin_fn_def_resolved, resolved_to_dotted,
94    semantic_constructor_from_resolved_ctor,
95};
96pub use dump::{dump_resolved_expr, dump_resolved_program};
97pub use resolve::{ResolveCtx, resolve_fn_def_external, resolve_program, resolve_top_level};
98
99/// Count every `ResolvedCallee::Unresolved` and
100/// `ResolvedCtor::Unresolved` reachable from `fd`'s body. The Phase E
101/// contract for `resolved_items` is **zero unresolved for well-typed
102/// programs** — non-zero means either the typechecker already
103/// rejected the program (resolver bailed to recovery) or there's a
104/// resolver gap. CI invariants compare this count against typecheck
105/// errors to catch silent regressions.
106pub fn count_unresolved_in_fn(fd: &ResolvedFnDef) -> usize {
107    let mut count = 0;
108    count_unresolved_in_body(&fd.body, &mut count);
109    count
110}
111
112fn count_unresolved_in_body(body: &ResolvedFnBody, out: &mut usize) {
113    match body {
114        ResolvedFnBody::Block(stmts) => {
115            for stmt in stmts {
116                count_unresolved_in_stmt(stmt, out);
117            }
118        }
119    }
120}
121
122fn count_unresolved_in_stmt(stmt: &ResolvedStmt, out: &mut usize) {
123    match stmt {
124        ResolvedStmt::Binding { value, .. } | ResolvedStmt::Expr(value) => {
125            count_unresolved_in_expr(&value.node, out)
126        }
127    }
128}
129
130fn count_unresolved_in_expr(expr: &ResolvedExpr, out: &mut usize) {
131    match expr {
132        ResolvedExpr::Literal(_) | ResolvedExpr::Ident(_) | ResolvedExpr::Resolved { .. } => {}
133        ResolvedExpr::Attr(obj, _) => count_unresolved_in_expr(&obj.node, out),
134        ResolvedExpr::Call(callee, args) => {
135            if let ResolvedCallee::Unresolved { callee } = callee {
136                *out += 1;
137                count_unresolved_in_expr(&callee.node, out);
138            }
139            for a in args {
140                count_unresolved_in_expr(&a.node, out);
141            }
142        }
143        ResolvedExpr::BinOp(_, l, r) => {
144            count_unresolved_in_expr(&l.node, out);
145            count_unresolved_in_expr(&r.node, out);
146        }
147        ResolvedExpr::Neg(inner) | ResolvedExpr::ErrorProp(inner) => {
148            count_unresolved_in_expr(&inner.node, out)
149        }
150        ResolvedExpr::Match { subject, arms } => {
151            count_unresolved_in_expr(&subject.node, out);
152            for arm in arms {
153                count_unresolved_in_pattern(&arm.pattern, out);
154                count_unresolved_in_expr(&arm.body.node, out);
155            }
156        }
157        ResolvedExpr::Ctor(ctor, args) => {
158            if matches!(ctor, ResolvedCtor::Unresolved { .. }) {
159                *out += 1;
160            }
161            for a in args {
162                count_unresolved_in_expr(&a.node, out);
163            }
164        }
165        ResolvedExpr::InterpolatedStr(parts) => {
166            for p in parts {
167                if let ResolvedStrPart::Parsed(inner) = p {
168                    count_unresolved_in_expr(&inner.node, out);
169                }
170            }
171        }
172        ResolvedExpr::List(items)
173        | ResolvedExpr::Tuple(items)
174        | ResolvedExpr::IndependentProduct(items, _) => {
175            for i in items {
176                count_unresolved_in_expr(&i.node, out);
177            }
178        }
179        ResolvedExpr::MapLiteral(pairs) => {
180            for (k, v) in pairs {
181                count_unresolved_in_expr(&k.node, out);
182                count_unresolved_in_expr(&v.node, out);
183            }
184        }
185        ResolvedExpr::RecordCreate { fields, .. } => {
186            for (_, e) in fields {
187                count_unresolved_in_expr(&e.node, out);
188            }
189        }
190        ResolvedExpr::RecordUpdate { base, updates, .. } => {
191            count_unresolved_in_expr(&base.node, out);
192            for (_, e) in updates {
193                count_unresolved_in_expr(&e.node, out);
194            }
195        }
196        ResolvedExpr::TailCall { args, .. } => {
197            for a in args {
198                count_unresolved_in_expr(&a.node, out);
199            }
200        }
201    }
202}
203
204fn count_unresolved_in_pattern(pat: &ResolvedPattern, out: &mut usize) {
205    match pat {
206        ResolvedPattern::Wildcard
207        | ResolvedPattern::Literal(_)
208        | ResolvedPattern::Ident(_)
209        | ResolvedPattern::EmptyList
210        | ResolvedPattern::Cons(_, _) => {}
211        ResolvedPattern::Tuple(items) => {
212            for p in items {
213                count_unresolved_in_pattern(p, out);
214            }
215        }
216        ResolvedPattern::Ctor(ctor, _) => {
217            if matches!(ctor, ResolvedCtor::Unresolved { .. }) {
218                *out += 1;
219            }
220        }
221    }
222}
223
224/// Resolved expression — the mechanical mirror of [`crate::ast::Expr`].
225///
226/// Every variant that referenced a declared symbol by string in
227/// `Expr` now carries its opaque ID. Variants that didn't reference
228/// any declaration pass through unchanged in shape.
229#[derive(Debug, Clone, PartialEq)]
230pub enum ResolvedExpr {
231    /// Literal — untouched.
232    Literal(Literal),
233    /// Source-level identifier that the resolver pass could NOT
234    /// classify into a `Resolved` slot, a fn ref, or a constructor.
235    /// Typically a top-level / global binding name; backends look it
236    /// up in the post-resolve global table.
237    ///
238    /// After full Phase E + D, this variant should rarely survive —
239    /// every name has either a slot, an `FnId`, a `CtorId`, or
240    /// fails to type-check. Kept here as the safety hatch during
241    /// migration.
242    Ident(String),
243    /// Compiled local-slot reference. Identical to `Expr::Resolved`
244    /// — the slot resolver runs before name-resolve and its output
245    /// is already typed identity.
246    Resolved {
247        slot: u16,
248        name: String,
249        last_use: AnnotBool,
250    },
251    /// Field / namespace projection. The object is recursively
252    /// resolved; the field name stays as source text because record
253    /// fields are scoped under their owning `TypeId`, not in a
254    /// global namespace.
255    Attr(Box<Spanned<ResolvedExpr>>, String),
256    /// Function call — `Expr::FnCall(callee, args)` lifted into a
257    /// [`ResolvedCallee`].
258    Call(ResolvedCallee, Vec<Spanned<ResolvedExpr>>),
259    /// Binary operator.
260    BinOp(
261        BinOp,
262        Box<Spanned<ResolvedExpr>>,
263        Box<Spanned<ResolvedExpr>>,
264    ),
265    /// Unary minus.
266    Neg(Box<Spanned<ResolvedExpr>>),
267    /// `match subject { arm, … }`.
268    Match {
269        subject: Box<Spanned<ResolvedExpr>>,
270        arms: Vec<ResolvedMatchArm>,
271    },
272    /// Constructor call — `Result.Ok(v)`, `Shape.Circle(r)`, etc.
273    Ctor(ResolvedCtor, Vec<Spanned<ResolvedExpr>>),
274    /// Result-error propagation: `expr?`.
275    ErrorProp(Box<Spanned<ResolvedExpr>>),
276    /// Interpolated string `"a${x}b"`.
277    InterpolatedStr(Vec<ResolvedStrPart>),
278    /// `[a, b, c]` list literal.
279    List(Vec<Spanned<ResolvedExpr>>),
280    /// `(a, b, c)` tuple literal.
281    Tuple(Vec<Spanned<ResolvedExpr>>),
282    /// `{"a" => 1, "b" => 2}` map literal.
283    MapLiteral(Vec<(Spanned<ResolvedExpr>, Spanned<ResolvedExpr>)>),
284    /// `Shape(name = "...", count = 0)` record-create form. The
285    /// `type_id` is `Some` for user records resolved through the
286    /// symbol table, `None` for built-in record types (`HttpResponse`,
287    /// `Header`, `Tcp.Connection`, `Buffer`, …) which don't carry
288    /// `TypeId`s by design.
289    RecordCreate {
290        type_id: Option<TypeId>,
291        /// Source-level type name kept verbatim for diagnostics +
292        /// backend codegen mangling. Mirrors `Type::Named { name }`.
293        type_name: String,
294        fields: Vec<(String, Spanned<ResolvedExpr>)>,
295    },
296    /// `Shape.update(base, field = newVal, …)` record-update.
297    RecordUpdate {
298        type_id: Option<TypeId>,
299        type_name: String,
300        base: Box<Spanned<ResolvedExpr>>,
301        updates: Vec<(String, Spanned<ResolvedExpr>)>,
302    },
303    /// Tail-position call (SCC peer). `target` is the `FnId` the
304    /// TCO transform pass committed to.
305    TailCall {
306        target: FnId,
307        args: Vec<Spanned<ResolvedExpr>>,
308    },
309    /// Independent product `(a, b)!` or `(a, b)?!`. `unwrap` toggles
310    /// the `?!` form.
311    IndependentProduct(Vec<Spanned<ResolvedExpr>>, bool),
312}
313
314/// Callee classification for [`ResolvedExpr::Call`]. Replaces the
315/// pre-Phase-E `FnCall(Box<Spanned<Expr>>, …)` shape where the
316/// callee was an arbitrary `Expr` subtree that every backend re-
317/// parsed.
318#[derive(Debug, Clone, PartialEq)]
319pub enum ResolvedCallee {
320    /// User-defined fn (entry module or any dep). Resolved by name-
321    /// resolve against the program's `SymbolTable`.
322    Fn(FnId),
323    /// Built-in namespace method — `Int.add`, `Console.print`,
324    /// `Vector.fromList`, etc. These don't have `FnId`s in the
325    /// program symbol table; carrier is the canonical
326    /// `"Namespace.method"` string. The lookup table for these is
327    /// flat and global, so a string key is enough — and stable
328    /// across compiler versions.
329    Builtin(String),
330    /// Compiler-synthesised intrinsic emitted by the
331    /// `interp_lower` / `buffer_build` deforestation passes.
332    /// Source-illegal names (`__buf_*`, `__to_str`) that only ever
333    /// appear after lowering. Carrying them as a typed variant
334    /// instead of `Unresolved { Ident("__buf_*") }` keeps the
335    /// "well-typed → zero unresolved" invariant honest — see
336    /// [`BuiltinIntrinsic`] for the enumerated set and the
337    /// `name_resolve_invariant_zero_unresolved_*` tests in
338    /// [`crate::ir::pipeline`].
339    Intrinsic(BuiltinIntrinsic),
340    /// First-class fn value bound to a local slot (lambda / fn ref
341    /// passed as an argument). The slot resolver already mapped
342    /// the binding; we just thread the slot through.
343    LocalSlot {
344        slot: u16,
345        name: String,
346        last_use: AnnotBool,
347    },
348    /// Callee shape the resolver couldn't classify — typically a
349    /// type error the typechecker already reported. Backends bail
350    /// out cleanly when they see this; pass exists so resolve can
351    /// emit a placeholder instead of panicking.
352    Unresolved {
353        /// The source-faithful expression the resolver gave up on,
354        /// kept for diagnostics. Resolved recursively into the same
355        /// IR so the surrounding tree still walks cleanly.
356        callee: Box<Spanned<ResolvedExpr>>,
357    },
358}
359
360/// The enumerated set of compiler-synthesised call intrinsics. New
361/// variants are added only when a lowering pass introduces a new
362/// `Expr::Ident("__…")` shape — there is no user-source mapping.
363#[derive(Debug, Clone, Copy, PartialEq, Eq)]
364pub enum BuiltinIntrinsic {
365    /// `__buf_new(<cap_hint>)` — allocate a fresh buffer slot.
366    BufNew,
367    /// `__buf_append(<buf>, <str>)` — concatenate a string fragment
368    /// onto the host-side buffer pool entry.
369    BufAppend,
370    /// `__buf_append_sep_unless_first(<buf>, <sep>)` — emit the
371    /// separator before every fragment except the first.
372    BufAppendSepUnlessFirst,
373    /// `__buf_finalize(<buf>)` — materialise the buffer pool entry
374    /// into an Aver `String` value and free the slot.
375    BufFinalize,
376    /// `__to_str(<value>)` — coerce any value to its display string
377    /// (used by interpolation lowering before `__buf_append`).
378    ToStr,
379    /// `__int_div_euclid(<a>, <k>)` — unchecked Euclidean (flooring)
380    /// `(Int, Int) -> Int` division. Synthesised by the MIR `const_fold`
381    /// pass when `Int.div(a, k)`'s divisor `k` is a literal `Int` outside
382    /// `{0, -1}` (the partial cases that would `Err`), so the surrounding
383    /// `Result` wrap collapses to bare division. Never produced by the
384    /// resolver — there is no `from_name` mapping; it appears only in MIR.
385    IntDivEuclid,
386    /// `__int_mod_euclid(<a>, <k>)` — unchecked Euclidean modulo
387    /// `(Int, Int) -> Int`, partner of `IntDivEuclid` so that
388    /// `div(a,k)*k + mod(a,k) == a` for every sign. Synthesised by the
389    /// MIR `const_fold` pass for `Int.mod(a, k)` with a non-zero literal
390    /// divisor `k`.
391    IntModEuclid,
392}
393
394impl BuiltinIntrinsic {
395    /// Canonical source-level name. Used by diagnostic dumps and as
396    /// the bridge into the resolver / VM dispatch tables.
397    pub const fn name(self) -> &'static str {
398        match self {
399            Self::BufNew => "__buf_new",
400            Self::BufAppend => "__buf_append",
401            Self::BufAppendSepUnlessFirst => "__buf_append_sep_unless_first",
402            Self::BufFinalize => "__buf_finalize",
403            Self::ToStr => "__to_str",
404            Self::IntDivEuclid => "__int_div_euclid",
405            Self::IntModEuclid => "__int_mod_euclid",
406        }
407    }
408
409    /// Recognise a bare identifier as one of the known intrinsics.
410    /// Returns `None` for anything else — the resolver then falls
411    /// through to its regular fn / Unresolved classification.
412    ///
413    /// `IntDivEuclid` / `IntModEuclid` are deliberately absent: they are
414    /// MIR-synthesis-only (emitted by `const_fold`), never recognised
415    /// from a source / resolver identifier.
416    pub fn from_name(name: &str) -> Option<Self> {
417        match name {
418            "__buf_new" => Some(Self::BufNew),
419            "__buf_append" => Some(Self::BufAppend),
420            "__buf_append_sep_unless_first" => Some(Self::BufAppendSepUnlessFirst),
421            "__buf_finalize" => Some(Self::BufFinalize),
422            "__to_str" => Some(Self::ToStr),
423            _ => None,
424        }
425    }
426}
427
428/// Constructor classification for [`ResolvedExpr::Ctor`] and
429/// [`ResolvedPattern::Ctor`].
430#[derive(Debug, Clone, PartialEq)]
431pub enum ResolvedCtor {
432    /// User-defined sum-type variant or record constructor.
433    User {
434        ctor_id: CtorId,
435        /// Owning type identity — kept on the callsite so backends
436        /// that pattern-match on (type, variant) don't need to walk
437        /// the symbol table on every emit.
438        type_id: TypeId,
439        /// Source name of the variant (`"Circle"`, `"Triangle"`,
440        /// the record name itself for product types). Kept for
441        /// diagnostic display + backend codegen mangling.
442        name: String,
443    },
444    /// `Result.Ok` / `Result.Err` / `Option.Some` / `Option.None`.
445    /// These are language-level rather than user-defined so they
446    /// don't carry `CtorId`s — discriminated by the variant.
447    Builtin(BuiltinCtor),
448    /// Constructor expression the resolver couldn't classify —
449    /// typechecker already reported the error. Kept as a
450    /// passthrough so the surrounding tree walks cleanly.
451    Unresolved {
452        /// Source name (`"Foo.Bar"`) preserved for diagnostics.
453        name: String,
454    },
455}
456
457/// Identity of the four built-in algebraic constructors. Mirror of
458/// the `Result` / `Option` types that the language exposes
459/// implicitly — these never get a user-program `CtorId` because
460/// they're not user-declared.
461#[derive(Debug, Clone, Copy, PartialEq, Eq)]
462pub enum BuiltinCtor {
463    ResultOk,
464    ResultErr,
465    OptionSome,
466    OptionNone,
467}
468
469/// Interpolated string piece — mirror of [`crate::ast::StrPart`].
470#[derive(Debug, Clone, PartialEq)]
471pub enum ResolvedStrPart {
472    Literal(String),
473    Parsed(Box<Spanned<ResolvedExpr>>),
474}
475
476/// One arm of a `match` — mirror of [`crate::ast::MatchArm`] with
477/// the pattern lifted to [`ResolvedPattern`].
478#[derive(Debug)]
479pub struct ResolvedMatchArm {
480    pub pattern: ResolvedPattern,
481    pub body: Box<Spanned<ResolvedExpr>>,
482    /// Per-arm slot table — same role as
483    /// [`crate::ast::MatchArm::binding_slots`]. Populated by the
484    /// resolver pass; backends read it instead of re-doing the
485    /// name → slot lookup.
486    pub binding_slots: std::sync::OnceLock<Vec<u16>>,
487}
488
489impl Clone for ResolvedMatchArm {
490    fn clone(&self) -> Self {
491        let binding_slots = std::sync::OnceLock::new();
492        if let Some(v) = self.binding_slots.get() {
493            let _ = binding_slots.set(v.clone());
494        }
495        Self {
496            pattern: self.pattern.clone(),
497            body: self.body.clone(),
498            binding_slots,
499        }
500    }
501}
502
503impl PartialEq for ResolvedMatchArm {
504    fn eq(&self, other: &Self) -> bool {
505        // `binding_slots` is filled by a later pass and isn't part
506        // of structural identity — same rule [`MatchArm`] uses.
507        self.pattern == other.pattern && self.body == other.body
508    }
509}
510
511/// Pattern shape — mirror of [`crate::ast::Pattern`].
512#[derive(Debug, Clone, PartialEq)]
513pub enum ResolvedPattern {
514    Wildcard,
515    Literal(Literal),
516    Ident(String),
517    EmptyList,
518    Cons(String, String),
519    Tuple(Vec<ResolvedPattern>),
520    /// Constructor pattern — `Result.Ok(x)`, `Shape.Circle(r)`,
521    /// `Shape.Point`. Resolved to a [`ResolvedCtor`] +
522    /// pattern-binding names.
523    Ctor(ResolvedCtor, Vec<String>),
524}
525
526/// Statement form — mirror of [`crate::ast::Stmt`] with the
527/// optional type annotation lifted to [`Type`] (already canonicalised
528/// against the resolver's symbol table) instead of a source string.
529#[derive(Debug, Clone, PartialEq)]
530pub enum ResolvedStmt {
531    Binding {
532        name: String,
533        ty_ann: Option<Type>,
534        value: Spanned<ResolvedExpr>,
535    },
536    Expr(Spanned<ResolvedExpr>),
537}
538
539/// Function body — mirror of [`crate::ast::FnBody`].
540#[derive(Debug, Clone, PartialEq)]
541pub enum ResolvedFnBody {
542    Block(Vec<ResolvedStmt>),
543}
544
545impl ResolvedFnBody {
546    pub fn stmts(&self) -> &[ResolvedStmt] {
547        match self {
548            Self::Block(stmts) => stmts,
549        }
550    }
551}
552
553/// Resolved fn definition. Mirrors [`crate::ast::FnDef`] but with
554/// signature types parsed to [`Type`] (and resolved through the
555/// owner module's resolver context, see #148 round 6) instead of
556/// source strings, plus the body lifted to [`ResolvedFnBody`].
557#[derive(Debug, Clone, PartialEq)]
558pub struct ResolvedFnDef {
559    /// Stable opaque identity of this fn. The pre-resolve `FnDef`
560    /// only carried a source name; here we promote identity to a
561    /// first-class field.
562    pub fn_id: FnId,
563    /// Source-level fn name. Kept for diagnostics + backend
564    /// codegen mangling.
565    pub name: String,
566    pub line: usize,
567    /// Parameters: `(binding_name, resolved_param_type)`. The
568    /// resolver canonicalises each annotation through the
569    /// declaring module's own resolver context.
570    pub params: Vec<(String, Type)>,
571    pub return_type: Type,
572    pub effects: Vec<Spanned<String>>,
573    pub desc: Option<String>,
574    pub body: std::sync::Arc<ResolvedFnBody>,
575    /// Slot-resolver output — see [`FnResolution`]. Carried through
576    /// unchanged.
577    pub resolution: Option<FnResolution>,
578}
579
580/// Resolved top-level item — mirror of [`crate::ast::TopLevel`].
581/// `Verify`, `Decision`, `TypeDef` items pass through with their
582/// original AST representation: they aren't on the runtime hot
583/// path, and their internal expressions get resolved lazily by
584/// proof-export passes that already consume `Expr`. Future PRs may
585/// promote them.
586#[derive(Debug, Clone, PartialEq)]
587pub enum ResolvedTopLevel {
588    Module(Module),
589    FnDef(ResolvedFnDef),
590    /// Verify / Decision / TypeDef items: passthrough for now.
591    /// Each carries its original AST node — the resolver lifts only
592    /// what runtime backends consume. See module doc for the
593    /// rationale + the future PR that promotes these.
594    Passthrough(crate::ast::TopLevel),
595}
596
597#[cfg(test)]
598mod tests {
599    use super::*;
600    use crate::ir::identity::TypeId;
601
602    #[test]
603    fn resolved_callee_user_fn_carries_typed_identity() {
604        let callee = ResolvedCallee::Fn(FnId(7));
605        let call = ResolvedExpr::Call(
606            callee,
607            vec![Spanned::new(ResolvedExpr::Literal(Literal::Int(42)), 3)],
608        );
609        // Smoke check: shape constructs and the FnId survives clone.
610        let clone = call.clone();
611        assert_eq!(clone, call);
612        match clone {
613            ResolvedExpr::Call(ResolvedCallee::Fn(id), args) => {
614                assert_eq!(id, FnId(7));
615                assert_eq!(args.len(), 1);
616            }
617            _ => panic!("expected ResolvedExpr::Call(Fn, _)"),
618        }
619    }
620
621    #[test]
622    fn resolved_ctor_user_carries_ctor_and_type_id() {
623        let ctor = ResolvedCtor::User {
624            ctor_id: CtorId(2),
625            type_id: TypeId(5),
626            name: "Circle".to_string(),
627        };
628        let expr = ResolvedExpr::Ctor(
629            ctor,
630            vec![Spanned::new(ResolvedExpr::Literal(Literal::Float(1.0)), 1)],
631        );
632        let ResolvedExpr::Ctor(
633            ResolvedCtor::User {
634                ctor_id,
635                type_id,
636                name,
637            },
638            ..,
639        ) = expr
640        else {
641            panic!("expected User ctor variant")
642        };
643        assert_eq!(ctor_id, CtorId(2));
644        assert_eq!(type_id, TypeId(5));
645        assert_eq!(name, "Circle");
646    }
647
648    #[test]
649    fn resolved_ctor_builtin_variants_distinguish() {
650        // Round-trip every builtin variant — guard against an
651        // accidental rename / collapse.
652        let variants = [
653            BuiltinCtor::ResultOk,
654            BuiltinCtor::ResultErr,
655            BuiltinCtor::OptionSome,
656            BuiltinCtor::OptionNone,
657        ];
658        for v in variants {
659            let c = ResolvedCtor::Builtin(v);
660            match c {
661                ResolvedCtor::Builtin(got) => assert_eq!(got, v),
662                _ => panic!("builtin ctor lost variant kind"),
663            }
664        }
665    }
666
667    #[test]
668    fn resolved_pattern_ctor_round_trips_through_clone() {
669        let pat = ResolvedPattern::Ctor(
670            ResolvedCtor::User {
671                ctor_id: CtorId(11),
672                type_id: TypeId(3),
673                name: "Square".to_string(),
674            },
675            vec!["side".to_string()],
676        );
677        assert_eq!(pat.clone(), pat);
678    }
679
680    #[test]
681    fn resolved_match_arm_equality_ignores_binding_slots() {
682        // Mirror of `MatchArm`'s structural equality rule — two
683        // arms with the same pattern + body must compare equal
684        // regardless of whether the slot table has been filled in.
685        let body = Box::new(Spanned::new(ResolvedExpr::Literal(Literal::Int(0)), 1));
686        let a = ResolvedMatchArm {
687            pattern: ResolvedPattern::Wildcard,
688            body: body.clone(),
689            binding_slots: std::sync::OnceLock::new(),
690        };
691        let b = ResolvedMatchArm {
692            pattern: ResolvedPattern::Wildcard,
693            body,
694            binding_slots: {
695                let lock = std::sync::OnceLock::new();
696                let _ = lock.set(vec![3, 4]);
697                lock
698            },
699        };
700        assert_eq!(a, b);
701    }
702
703    #[test]
704    fn resolved_fn_def_carries_fn_id_and_resolved_param_types() {
705        let body = ResolvedFnBody::Block(vec![ResolvedStmt::Expr(Spanned::new(
706            ResolvedExpr::Literal(Literal::Int(1)),
707            1,
708        ))]);
709        let def = ResolvedFnDef {
710            fn_id: FnId(0),
711            name: "id".to_string(),
712            line: 1,
713            params: vec![("x".to_string(), Type::Int)],
714            return_type: Type::Int,
715            effects: vec![],
716            desc: None,
717            body: std::sync::Arc::new(body),
718            resolution: None,
719        };
720        assert_eq!(def.fn_id, FnId(0));
721        assert_eq!(def.params[0].1, Type::Int);
722        assert_eq!(def.return_type, Type::Int);
723        assert_eq!(def.body.stmts().len(), 1);
724    }
725
726    #[test]
727    fn resolved_stmt_binding_threads_optional_resolved_type_ann() {
728        // `Stmt::Binding(name, Option<String>, …)` in the pre-Phase-E
729        // AST stored the annotation as a source string. Resolved
730        // form lifts to `Option<Type>`.
731        let stmt_with = ResolvedStmt::Binding {
732            name: "n".to_string(),
733            ty_ann: Some(Type::Int),
734            value: Spanned::new(ResolvedExpr::Literal(Literal::Int(0)), 1),
735        };
736        let stmt_without = ResolvedStmt::Binding {
737            name: "n".to_string(),
738            ty_ann: None,
739            value: Spanned::new(ResolvedExpr::Literal(Literal::Int(0)), 1),
740        };
741        assert_ne!(stmt_with, stmt_without);
742    }
743
744    #[test]
745    fn resolved_callee_unresolved_passes_through_inner_expr() {
746        // The Unresolved escape hatch lets the resolver emit a
747        // placeholder when it can't classify the callee — every
748        // backend uses the same bail-out path. This test just
749        // verifies it constructs and clones.
750        let inner = Spanned::new(ResolvedExpr::Ident("dynamic".to_string()), 1);
751        let call = ResolvedExpr::Call(
752            ResolvedCallee::Unresolved {
753                callee: Box::new(inner.clone()),
754            },
755            vec![],
756        );
757        let clone = call.clone();
758        assert_eq!(clone, call);
759    }
760
761    // Compile-time documentation: the structural mapping
762    // `Expr → ResolvedExpr` is exhaustive — every variant `Expr`
763    // can produce maps to a counterpart here. Asserting this in
764    // code keeps reviewers honest: when a new `Expr` variant lands,
765    // either this list gains a row or the compiler stops building.
766    #[test]
767    fn variant_coverage_matches_expr() {
768        use crate::ast::Expr;
769        fn cover(expr: &Expr) -> &'static str {
770            match expr {
771                Expr::Literal(_) => "Literal → Literal",
772                Expr::Ident(_) => "Ident → Ident",
773                Expr::Resolved { .. } => "Resolved → Resolved",
774                Expr::Attr(_, _) => "Attr → Attr",
775                Expr::FnCall(_, _) => "FnCall → Call",
776                Expr::BinOp(_, _, _) => "BinOp → BinOp",
777                Expr::Neg(_) => "Neg → Neg",
778                Expr::Match { .. } => "Match → Match",
779                Expr::Constructor(_, _) => "Constructor → Ctor",
780                Expr::ErrorProp(_) => "ErrorProp → ErrorProp",
781                Expr::InterpolatedStr(_) => "InterpolatedStr → InterpolatedStr",
782                Expr::List(_) => "List → List",
783                Expr::Tuple(_) => "Tuple → Tuple",
784                Expr::MapLiteral(_) => "MapLiteral → MapLiteral",
785                Expr::RecordCreate { .. } => "RecordCreate → RecordCreate",
786                Expr::RecordUpdate { .. } => "RecordUpdate → RecordUpdate",
787                Expr::TailCall(_) => "TailCall → TailCall",
788                Expr::IndependentProduct(_, _) => "IndependentProduct → IndependentProduct",
789            }
790        }
791        // Trivial probe — the real assertion is the `match`'s
792        // exhaustiveness check at compile time.
793        let probe = Expr::Literal(Literal::Int(0));
794        assert!(cover(&probe).contains("Literal"));
795        // Mirror sentinel — touching every `ResolvedExpr` variant
796        // here keeps the symmetry honest from the other side too.
797        let _: ResolvedExpr = ResolvedExpr::Literal(Literal::Int(0));
798        let _: ResolvedExpr = ResolvedExpr::Ident(String::new());
799        let _: ResolvedExpr = ResolvedExpr::Resolved {
800            slot: 0,
801            name: String::new(),
802            last_use: AnnotBool(false),
803        };
804        let dummy = || Box::new(Spanned::new(ResolvedExpr::Literal(Literal::Int(0)), 1));
805        let _: ResolvedExpr = ResolvedExpr::Attr(dummy(), String::new());
806        let _: ResolvedExpr = ResolvedExpr::Call(ResolvedCallee::Fn(FnId(0)), vec![]);
807        let _: ResolvedExpr = ResolvedExpr::BinOp(BinOp::Add, dummy(), dummy());
808        let _: ResolvedExpr = ResolvedExpr::Neg(dummy());
809        let _: ResolvedExpr = ResolvedExpr::Match {
810            subject: dummy(),
811            arms: vec![],
812        };
813        let _: ResolvedExpr =
814            ResolvedExpr::Ctor(ResolvedCtor::Builtin(BuiltinCtor::OptionNone), vec![]);
815        let _: ResolvedExpr = ResolvedExpr::ErrorProp(dummy());
816        let _: ResolvedExpr = ResolvedExpr::InterpolatedStr(vec![]);
817        let _: ResolvedExpr = ResolvedExpr::List(vec![]);
818        let _: ResolvedExpr = ResolvedExpr::Tuple(vec![]);
819        let _: ResolvedExpr = ResolvedExpr::MapLiteral(vec![]);
820        let _: ResolvedExpr = ResolvedExpr::RecordCreate {
821            type_id: None,
822            type_name: String::new(),
823            fields: vec![],
824        };
825        let _: ResolvedExpr = ResolvedExpr::RecordUpdate {
826            type_id: None,
827            type_name: String::new(),
828            base: dummy(),
829            updates: vec![],
830        };
831        let _: ResolvedExpr = ResolvedExpr::TailCall {
832            target: FnId(0),
833            args: vec![],
834        };
835        let _: ResolvedExpr = ResolvedExpr::IndependentProduct(vec![], false);
836    }
837}