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}