diff --git a/docs/plans/0114-mir.1a-mir-infrastructure.md b/docs/plans/0114-mir.1a-mir-infrastructure.md new file mode 100644 index 0000000..0a971aa --- /dev/null +++ b/docs/plans/0114-mir.1a-mir-infrastructure.md @@ -0,0 +1,950 @@ +# mir.1a — MIR infrastructure (additive) — Implementation Plan + +> **Parent spec:** `docs/specs/0060-typed-mir.md` +> +> **For agentic workers:** REQUIRED SUB-SKILL: use the `implement` +> skill to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Land the typed-MIR types (`ailang-mir`), the post-mono +lowering walk (`ailang-check::lower_to_mir`), and the front-end entry +(`ailang-check::elaborate_workspace`) as a **purely additive** layer — +nothing consumes MIR yet, codegen is untouched, the whole existing +suite stays green, and new tests pin that `lower_to_mir` fills `ty` +correctly on the three boundary witnesses. + +**Architecture:** This is the first half of spec iteration mir.1. The +spec's mir.1 row ("structural MIR + `ty` + delete `synth_with_extras`") +is reached across two plans: **mir.1a** (this one) builds the MIR +producer additively; **mir.1b** (next plan) flips codegen to consume +MIR and deletes `synth_with_extras`/`synth_arg_type`. The split is +forced by the compile graph: the codegen walk switch from `&Term` to +`&MTerm` is atomic (no compiling intermediate, dual-path is +spec-forbidden), whereas the producer side compiles and tests in +isolation. `lower_to_mir` carries **no** second type engine: it calls +check's canonical `synth` per node (with throwaway inference +scaffolding) and maintains `locals`/`loop_stack` during descent exactly +as `synth` does, so the type on every MIR node is the checker's own. + +**Tech Stack:** new leaf crate `ailang-mir` (depends only on +`ailang-core`); new module + entry in `ailang-check`; new integration +test in `ailang-check/tests/`. No change to `ailang-codegen`, +`crates/ail`, or any authoring/hash surface. + +--- + +## Design decisions baked into this plan (orchestrator, from spec + recon) + +- **Str split (spec line 195 made literal).** `MTerm` has a dedicated + `Str { lit, rep }` variant *distinct from* `Lit { lit, ty }`. + `lower_to_mir` routes `Term::Lit { Literal::Str }` → `MTerm::Str` + with `rep: StrRep::Static`; every other `Literal` → `MTerm::Lit`. + This installs the mir.4 hook at the exact node mir.4 needs (the #49 + loop seed `"x"` is a `Str` literal whose `rep` flips to `Heap`). +- **Structurally complete from mir.1a.** Every MIR field that later + iterations *fill* already *exists* now, at a mir.1 default: + `App.callee = Callee::Indirect()` (→ `Static` in + mir.2), `MArg.mode = Owned`, `MArg.consume_count = 1` (→ filled + mir.3), `Str.rep = Static` (→ `Heap` for loop-carried seeds in + mir.4), `New.elem = None` (→ filled mir.5). The MIR *struct shape* + does not change across mir.2–mir.5; only the values do. +- **One engine.** `lower_to_mir` never re-derives a type. It calls + `crate::synth` (canonical, `pub(crate)`, `lib.rs:3223`) on each node + with **fresh throwaway** `subst`/`counter`/`residuals`/`free_fn_calls`/ + `effects`/`warnings`, and applies the resulting `subst` before + reading the type — so no node pollutes another and the real check + state is never touched. The only state `lower_to_mir` threads is the + lexical `locals`/`loop_stack`, maintained by the same push/pop rules + `synth` uses (`Term::Let` arm template at `lib.rs:3703-3715`). +- **`elaborate_workspace` env construction mirrors mono.** Per-def + scaffolding (env, per-module `imports`, `locals` from + `params.zip(param_tys)`) is built exactly as + `crates/ailang-check/src/mono.rs:771-816` already does for its + post-typecheck synth re-entry. + +**Files this plan creates or modifies:** + +- Create: `crates/ailang-mir/Cargo.toml` — new leaf crate manifest. +- Create: `crates/ailang-mir/src/lib.rs` — MIR types + `MTerm::ty()`. +- Create: `crates/ailang-check/src/lower_to_mir.rs` — the post-mono + lowering walk. +- Modify: `Cargo.toml:3-10` — add `crates/ailang-mir` to members. +- Modify: `crates/ailang-check/Cargo.toml:7-9` — add `ailang-mir` dep. +- Modify: `crates/ailang-check/src/lib.rs:372-379` — `pub mod + lower_to_mir;`; add `elaborate_workspace`; widen `type_check_pattern` + to `pub(crate)`. +- Create: `examples/new_rawbuf_size_only.ail` — #51 witness fixture. +- Create: `examples/new_counter_user_adt.ail` — #53 witness fixture. + (#49 reuses the existing `examples/loop_recur_str_binder_no_leak_pin.ail`.) +- Test: `crates/ailang-check/tests/lower_to_mir_ty.rs` — `ty`-fill + correctness on the #51 / #53 / #49 witnesses + the Str-split rep. + +--- + +## Task 1: `ailang-mir` crate — the bridge types + +**Files:** +- Create: `crates/ailang-mir/Cargo.toml` +- Create: `crates/ailang-mir/src/lib.rs` +- Modify: `Cargo.toml:3-10` + +- [ ] **Step 1: Create the crate manifest** + +Create `crates/ailang-mir/Cargo.toml`: + +```toml +[package] +name = "ailang-mir" +version = "0.1.0" +edition = "2021" + +[dependencies] +ailang-core = { path = "../ailang-core" } +``` + +- [ ] **Step 2: Add the crate to the workspace members list** + +In `Cargo.toml`, the `members` array (lines 3-10) — add the new member +after `"crates/ailang-core"` so the leaf sorts near its only dep: + +```toml +members = [ + "crates/ailang-core", + "crates/ailang-mir", + "crates/ailang-check", + "crates/ailang-codegen", + "crates/ailang-kernel", + "crates/ailang-surface", + "crates/ailang-prose", + "crates/ail", +] +``` + +- [ ] **Step 3: Write the MIR types** + +Create `crates/ailang-mir/src/lib.rs`. Every `Term` variant +(`ailang-core/src/ast.rs:436`) gets one `MTerm` counterpart, plus the +`Str` split. Each node carries `ty` (the checker's type) and the +later-iteration annotation fields at their mir.1 defaults: + +```rust +//! Typed mid-level IR — the single artefact that crosses the +//! `check` → `codegen` boundary. Produced by +//! `ailang_check::lower_to_mir` from a monomorphised, typechecked +//! `Workspace`; consumed by `ailang_codegen`. Every node carries the +//! facts codegen used to re-derive: its type (`ty`), the resolved +//! callee (`Callee`, filled mir.2), parameter modes / consume counts +//! (`Mode` / `consume_count`, filled mir.3), and string representation +//! (`StrRep`, filled mir.4). MIR is never authored, never hashed, +//! never round-tripped — it is a compiler-internal derived form. + +use ailang_core::ast::{Literal, Pattern, Type}; +use std::collections::BTreeMap; + +/// A whole monomorphised program, lowered to MIR. +#[derive(Debug, Clone)] +pub struct MirWorkspace { + pub entry: String, + pub modules: BTreeMap, +} + +#[derive(Debug, Clone)] +pub struct MirModule { + pub name: String, + pub defs: Vec, +} + +/// One lowered top-level fn. `sig` is the declared signature; `body` +/// is the lowered fn body with `ty` on every node. +#[derive(Debug, Clone)] +pub struct MirDef { + pub name: String, + pub sig: Type, + pub params: Vec, + pub export: bool, + pub body: MTerm, +} + +/// One MIR node — structural counterpart of `ast::Term`, plus the +/// `Str` split. `ty` is the checker-proved type at this node. +#[derive(Debug, Clone)] +pub enum MTerm { + Lit { lit: Literal, ty: Type }, + /// String literal — the `Str`-representation carrier. `rep` is + /// `Static` for every literal at mir.1; mir.4 flips loop-carried + /// seeds to `Heap`. Split out of `Lit` so the rep annotation has a + /// home (spec §"Str split"). + Str { lit: String, rep: StrRep }, + Var { name: String, ty: Type }, + /// `callee` is `Indirect()` at mir.1; mir.2 + /// resolves static targets to `Callee::Static`. + App { callee: Callee, args: Vec, tail: bool, ty: Type }, + Let { name: String, mode: Mode, init: Box, body: Box, ty: Type }, + LetRec { + name: String, + sig: Type, + params: Vec, + body: Box, + in_term: Box, + ty: Type, + }, + If { cond: Box, then: Box, else_: Box, ty: Type }, + Do { op: String, args: Vec, tail: bool, ty: Type }, + Ctor { type_name: String, ctor: String, args: Vec, ty: Type }, + Match { scrutinee: Box, arms: Vec, ty: Type }, + Lam { + params: Vec, + param_tys: Vec, + ret_ty: Type, + effects: Vec, + body: Box, + ty: Type, + }, + Seq { lhs: Box, rhs: Box, ty: Type }, + Clone { value: Box, ty: Type }, + ReuseAs { source: Box, body: Box, ty: Type }, + Loop { binders: Vec, body: Box, ty: Type }, + Recur { args: Vec, ty: Type }, + /// `elem` is `None` at mir.1; mir.5 carries the element type. + New { type_name: String, elem: Option, args: Vec, ty: Type }, + Intrinsic { ty: Type }, +} + +/// A match arm. Patterns stay structural (`ast::Pattern`) — they carry +/// no type annotation the boundary re-derives. +#[derive(Debug, Clone)] +pub struct MArm { + pub pat: Pattern, + pub body: MTerm, +} + +#[derive(Debug, Clone)] +pub struct MLoopBinder { + pub name: String, + pub ty: Type, + pub init: MTerm, +} + +#[derive(Debug, Clone)] +pub enum MNewArg { + Type(Type), + Value(MTerm), +} + +/// A call/ctor/recur argument with its mode and consume count. Both +/// fields are mir.1 defaults (`Owned` / `1`); mir.3 fills them. +#[derive(Debug, Clone)] +pub struct MArg { + pub term: MTerm, + pub mode: Mode, + pub consume_count: u32, +} + +#[derive(Debug, Clone)] +pub enum Callee { + Static { module: String, fn_name: String }, + Indirect(Box), +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum StrRep { + Heap, + Static, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Mode { + Owned, + Borrow, +} + +impl MTerm { + /// The checker-proved type at this node. `Str` is always `Str`. + pub fn ty(&self) -> Type { + match self { + MTerm::Lit { ty, .. } + | MTerm::Var { ty, .. } + | MTerm::App { ty, .. } + | MTerm::Let { ty, .. } + | MTerm::LetRec { ty, .. } + | MTerm::If { ty, .. } + | MTerm::Do { ty, .. } + | MTerm::Ctor { ty, .. } + | MTerm::Match { ty, .. } + | MTerm::Lam { ty, .. } + | MTerm::Seq { ty, .. } + | MTerm::Clone { ty, .. } + | MTerm::ReuseAs { ty, .. } + | MTerm::Loop { ty, .. } + | MTerm::Recur { ty, .. } + | MTerm::New { ty, .. } + | MTerm::Intrinsic { ty } => ty.clone(), + MTerm::Str { .. } => Type::str_(), + } + } +} +``` + +- [ ] **Step 4: Build the new crate in isolation** + +Run: `cargo build -p ailang-mir` +Expected: compiles, 0 errors. (If `Type::str_()` is not a `Type` +constructor in `ailang-core`, the build errors here — resolve by using +the same constructor `synth`'s `Lit` arm uses at `lib.rs:3254`, which +is `Type::str_()`; this step is the gate that confirms it.) + +--- + +## Task 2: `ailang-check::lower_to_mir` — the post-mono walk + +**Files:** +- Create: `crates/ailang-check/src/lower_to_mir.rs` +- Modify: `crates/ailang-check/Cargo.toml:7-9` +- Modify: `crates/ailang-check/src/lib.rs:372-379` + +- [ ] **Step 1: Add the `ailang-mir` dependency to `ailang-check`** + +In `crates/ailang-check/Cargo.toml`, under `[dependencies]` (the block +at lines 7-9, currently `ailang-core` + `ailang-surface`), add: + +```toml +ailang-mir = { path = "../ailang-mir" } +``` + +- [ ] **Step 2: Declare the module** + +In `crates/ailang-check/src/lib.rs`, in the `pub mod` / `pub use` block +around lines 372-379 (where `lift`, `mono`, `diagnostic` are declared), +add: + +```rust +pub mod lower_to_mir; +``` + +- [ ] **Step 3: Write the lowering walk** + +Create `crates/ailang-check/src/lower_to_mir.rs`. The walk takes a +typechecked, **post-mono** `Module`, and for each `FnDef` builds an +`MirDef` whose body is the `Term` lowered to `MTerm` with `ty` on every +node. `synth_pure` is the single type oracle (canonical `synth`, fresh +throwaway inference state); `lower_term` maintains `locals`/`loop_stack` +by the same push/pop rules `synth` uses. + +```rust +//! Post-monomorphisation lowering from the typechecked `ast::Term` +//! to typed `MTerm`. Runs after `monomorphise_workspace`. Carries no +//! second type engine: each node's type comes from a fresh-scaffolding +//! call to the canonical `crate::synth` (lib.rs:3223). The only state +//! threaded across nodes is the lexical `locals` / `loop_stack`, +//! maintained exactly as `synth` maintains it (e.g. the `Term::Let` +//! push/pop at lib.rs:3703-3715). + +use ailang_core::ast::{Literal, Module, Term, Type}; +use ailang_mir::{ + Callee, MArg, MArm, MLoopBinder, MNewArg, MTerm, MirDef, MirModule, Mode, StrRep, +}; +use indexmap::IndexMap; +use std::collections::BTreeSet; + +use crate::{Env, Result}; + +/// Per-walk scaffolding for the canonical `synth` re-entry. `env` and +/// `in_def` are fixed per fn; `locals` / `loop_stack` are mutated as +/// the walk descends and restored on the way up, mirroring `synth`. +struct Ctx<'a> { + env: &'a Env, + in_def: &'a str, + locals: IndexMap, + loop_stack: Vec>, +} + +impl<'a> Ctx<'a> { + /// The canonical type of `t` in the current lexical scope, with no + /// side effects on real check state. Fresh inference scaffolding + /// per call; the result has its substitution applied so downstream + /// reads see a resolved type. + fn synth_pure(&mut self, t: &Term) -> Result { + let mut effects: BTreeSet = BTreeSet::new(); + let mut subst = crate::Subst::default(); + let mut counter: u32 = 0; + let mut residuals: Vec = Vec::new(); + let mut free_fn_calls: Vec = Vec::new(); + let mut warnings: Vec = Vec::new(); + let ty = crate::synth( + t, + self.env, + &mut self.locals, + &mut self.loop_stack, + &mut effects, + self.in_def, + &mut subst, + &mut counter, + &mut residuals, + &mut free_fn_calls, + &mut warnings, + )?; + Ok(subst.apply(&ty)) + } +} + +/// Default arg wrapper — mode/consume_count are mir.1 placeholders +/// (mir.3 fills them). +fn arg(term: MTerm) -> MArg { + MArg { term, mode: Mode::Owned, consume_count: 1 } +} + +/// Lower one term to `MTerm`, filling `ty` from `synth_pure`. +fn lower_term(ctx: &mut Ctx, t: &Term) -> Result { + let ty = ctx.synth_pure(t)?; + Ok(match t { + // ---- String literal: the rep carrier (Static at mir.1) ---- + Term::Lit { lit: Literal::Str { value } } => { + MTerm::Str { lit: value.clone(), rep: StrRep::Static } + } + Term::Lit { lit } => MTerm::Lit { lit: lit.clone(), ty }, + + Term::Var { name } => MTerm::Var { name: name.clone(), ty }, + + // callee is Indirect at mir.1 (mir.2 resolves Static). + Term::App { callee, args, tail } => { + let m_callee = Callee::Indirect(Box::new(lower_term(ctx, callee)?)); + let m_args = args + .iter() + .map(|a| Ok(arg(lower_term(ctx, a)?))) + .collect::>>()?; + MTerm::App { callee: m_callee, args: m_args, tail: *tail, ty } + } + + // scope-affecting: insert binder type, lower body, restore — + // exactly synth's Term::Let arm (lib.rs:3703-3715). + Term::Let { name, value, body } => { + let m_init = lower_term(ctx, value)?; + let v_ty = ctx.synth_pure(value)?; + let prev = ctx.locals.insert(name.clone(), v_ty); + let m_body = lower_term(ctx, body)?; + match prev { + Some(p) => { + ctx.locals.insert(name.clone(), p); + } + None => { + ctx.locals.shift_remove(name); + } + } + MTerm::Let { + name: name.clone(), + mode: Mode::Owned, + init: Box::new(m_init), + body: Box::new(m_body), + ty, + } + } + + Term::If { cond, then, else_ } => MTerm::If { + cond: Box::new(lower_term(ctx, cond)?), + then: Box::new(lower_term(ctx, then)?), + else_: Box::new(lower_term(ctx, else_)?), + ty, + }, + + Term::Do { op, args, tail } => { + let m_args = args + .iter() + .map(|a| Ok(arg(lower_term(ctx, a)?))) + .collect::>>()?; + MTerm::Do { op: op.clone(), args: m_args, tail: *tail, ty } + } + + Term::Ctor { type_name, ctor, args } => { + let m_args = args + .iter() + .map(|a| Ok(arg(lower_term(ctx, a)?))) + .collect::>>()?; + MTerm::Ctor { + type_name: type_name.clone(), + ctor: ctor.clone(), + args: m_args, + ty, + } + } + + // scope-affecting: each arm binds its pattern vars. Mirror + // synth's Match arm (lib.rs:3879-3896) exactly — including its + // own helper `type_check_pattern`, which resolves the binder + // types from the scrutinee's ADT. Push, lower the arm body, + // restore (innermost-first), per arm. + Term::Match { scrutinee, arms } => { + let m_scrut = Box::new(lower_term(ctx, scrutinee)?); + let s_ty = ctx.synth_pure(scrutinee)?; + let mut m_arms = Vec::with_capacity(arms.len()); + for a in arms { + let bindings = crate::type_check_pattern(&a.pat, &s_ty, ctx.env)?; + let mut pushed = Vec::new(); + for (n, t) in &bindings { + let prev = ctx.locals.insert(n.clone(), t.clone()); + pushed.push((n.clone(), prev)); + } + let m_body = lower_term(ctx, &a.body)?; + for (n, prev) in pushed.into_iter().rev() { + match prev { + Some(p) => { + ctx.locals.insert(n, p); + } + None => { + ctx.locals.shift_remove(&n); + } + } + } + m_arms.push(MArm { pat: a.pat.clone(), body: m_body }); + } + MTerm::Match { scrutinee: m_scrut, arms: m_arms, ty } + } + + // scope-affecting: params enter scope for the body. Mirror + // synth's Lam arm (lib.rs:3965): insert each param:param_ty + // into locals for the body, restore after. + Term::Lam { params, param_tys, ret_ty, effects, body } => { + let saved = ctx.locals.clone(); + for (p, pty) in params.iter().zip(param_tys.iter()) { + ctx.locals.insert(p.clone(), pty.clone()); + } + let m_body = Box::new(lower_term(ctx, body)?); + ctx.locals = saved; + MTerm::Lam { + params: params.clone(), + param_tys: param_tys.clone(), + ret_ty: (**ret_ty).clone(), + effects: effects.clone(), + body: m_body, + ty, + } + } + + Term::Seq { lhs, rhs } => MTerm::Seq { + lhs: Box::new(lower_term(ctx, lhs)?), + rhs: Box::new(lower_term(ctx, rhs)?), + ty, + }, + + Term::Clone { value } => MTerm::Clone { + value: Box::new(lower_term(ctx, value)?), + ty, + }, + + Term::ReuseAs { source, body } => MTerm::ReuseAs { + source: Box::new(lower_term(ctx, source)?), + body: Box::new(lower_term(ctx, body)?), + ty, + }, + + // scope-affecting: binders enter scope and a loop frame is + // pushed for the body so an inner Recur resolves. Mirror + // synth's Loop arm (lib.rs:4189): push the binder frame onto + // loop_stack and the binder types onto locals before lowering + // the body, pop/restore after. + Term::Loop { binders, body } => { + let mut m_binders = Vec::with_capacity(binders.len()); + for b in binders { + m_binders.push(MLoopBinder { + name: b.name.clone(), + ty: b.ty.clone(), + init: lower_term(ctx, &b.init)?, + }); + } + let saved_locals = ctx.locals.clone(); + let frame: Vec<(String, Type)> = + binders.iter().map(|b| (b.name.clone(), b.ty.clone())).collect(); + for b in binders { + ctx.locals.insert(b.name.clone(), b.ty.clone()); + } + ctx.loop_stack.push(frame); + let m_body = Box::new(lower_term(ctx, body)?); + ctx.loop_stack.pop(); + ctx.locals = saved_locals; + MTerm::Loop { binders: m_binders, body: m_body, ty } + } + + Term::Recur { args } => { + let m_args = args + .iter() + .map(|a| Ok(arg(lower_term(ctx, a)?))) + .collect::>>()?; + MTerm::Recur { args: m_args, ty } + } + + // elem is None at mir.1 (mir.5 carries the element type). + Term::New { type_name, args } => { + let m_args = args + .iter() + .map(|a| { + Ok(match a { + ailang_core::ast::NewArg::Type(t) => MNewArg::Type(t.clone()), + ailang_core::ast::NewArg::Value(v) => { + MNewArg::Value(lower_term(ctx, v)?) + } + }) + }) + .collect::>>()?; + MTerm::New { type_name: type_name.clone(), elem: None, args: m_args, ty } + } + + // scope-affecting: synth's LetRec arm (lib.rs:4029) binds + // `name: ty` for both `body` and `in_term`. Mirror it. + Term::LetRec { name, ty: rec_ty, params, body, in_term } => { + let saved = ctx.locals.clone(); + ctx.locals.insert(name.clone(), rec_ty.clone()); + let m_body = Box::new(lower_term(ctx, body)?); + let m_in = Box::new(lower_term(ctx, in_term)?); + ctx.locals = saved; + MTerm::LetRec { + name: name.clone(), + sig: rec_ty.clone(), + params: params.clone(), + body: m_body, + in_term: m_in, + ty, + } + } + + Term::Intrinsic => MTerm::Intrinsic { ty }, + }) +} +``` + +> **Implementer note for Step 3.** The Match arm calls +> `crate::type_check_pattern` — synth's own pattern-binding helper +> (`lib.rs:3880`). It is currently private to `lib.rs`; widen its +> declaration to `pub(crate) fn type_check_pattern(...)` so the +> `lower_to_mir` module can call it. That is the one-token change this +> step needs in `lib.rs` beyond the module declaration; do **not** +> otherwise touch synth or its helpers. + +- [ ] **Step 4: Write the module-lowering entry** + +Append to `crates/ailang-check/src/lower_to_mir.rs`. `lower_module` +builds one `MirDef` per `FnDef`, constructing the per-fn `Ctx` exactly +as `mono.rs:771-816` builds its synth scaffolding (env with per-module +`imports`, `locals` from `params.zip(param_tys)`): + +```rust +/// Lower one post-mono module to MIR. `env` is the workspace check +/// env (built by `build_check_env`); this fn sets `env.imports` for +/// the module and seeds per-fn `locals` from the declared params, +/// mirroring mono.rs:771-816. +pub fn lower_module(module: &Module, env: &Env) -> Result { + let mut env = env.clone(); + if let Some(im) = env.module_imports.get(&module.name).cloned() { + env.imports = im; + } + let mut defs = Vec::new(); + for def in &module.defs { + let ailang_core::ast::Def::Fn(f) = def else { continue }; + // param types from the fn signature (same source mono uses). + let param_tys = crate::fn_param_types(&f.ty); + let mut locals: IndexMap = IndexMap::new(); + for (n, t) in f.params.iter().zip(param_tys.iter()) { + locals.insert(n.clone(), t.clone()); + } + let mut ctx = Ctx { + env: &env, + in_def: &f.name, + locals, + loop_stack: Vec::new(), + }; + let body = lower_term(&mut ctx, &f.body)?; + defs.push(MirDef { + name: f.name.clone(), + sig: f.ty.clone(), + params: f.params.clone(), + export: f.export, + body, + }); + } + Ok(MirModule { name: module.name.clone(), defs }) +} +``` + +> **Implementer note for Step 4.** `crate::fn_param_types` is the +> helper that extracts a fn signature's parameter types — mono.rs uses +> the same `param_tys` at `:788`. Find what mono.rs binds `param_tys` +> from (it is in scope at `mono.rs:771-816`) and call the identical +> source; if it is a local computation rather than a shared fn, lift it +> into a `pub(crate)` helper so both sites share it. `f.export` — if +> `FnDef` has no `export: bool` field, drop that line from `MirDef` +> construction and the field from Task 1's `MirDef` (confirm against +> `ast.rs:224`). + +- [ ] **Step 5: Build the check crate** + +Run: `cargo build -p ailang-check` +Expected: compiles, 0 errors. This gates that `synth` / `Subst` / +`ResidualConstraint` / `FreeFnCall` / `Env` / `fn_param_types` are all +reachable from the new module under their referenced names (fix any +that differ by reading their declaration — they are all in +`crates/ailang-check/src/lib.rs`). + +--- + +## Task 3: `elaborate_workspace` + ty-fill pins + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs` (add `elaborate_workspace`) +- Test: `crates/ailang-check/tests/lower_to_mir_ty.rs` + +- [ ] **Step 1: Write `elaborate_workspace`** + +In `crates/ailang-check/src/lib.rs`, after `check_workspace` +(`:1145`), add the front-end entry. It runs the diagnostics gate, then +lift + mono, then lowers each post-mono module to MIR: + +```rust +/// The build-path front end: typecheck (diagnostics gate) → desugar + +/// lift → monomorphise → lower to MIR. Returns a `MirWorkspace` on +/// success, or the check diagnostics on a type error. `check_workspace` +/// stays the entry for diagnostics-only callers (`ail check`); this is +/// what the build / emit-ir paths call. +pub fn elaborate_workspace( + ws: &ailang_core::workspace::Workspace, +) -> std::result::Result> { + // 1. diagnostics gate — bail with the diagnostics on any error. + let diags = check_workspace(ws); + if diags.iter().any(|d| d.severity == crate::diagnostic::Severity::Error) { + return Err(diags); + } + // 2. desugar + lift + monomorphise — the exact sequence the CLI + // runs at main.rs:2324-2346. A lift/mono Err on a checked + // workspace is an internal compiler error → surface as a + // diagnostic, do not panic. + let mut lifted_modules = std::collections::BTreeMap::new(); + for (mname, m) in &ws.modules { + let desugared = ailang_core::desugar::desugar_module(m); + let lifted = lift_letrecs(&desugared) + .map_err(|e| vec![internal_diag(format!("lift_letrecs in `{mname}`: {e}"))])?; + lifted_modules.insert(mname.clone(), lifted); + } + let lifted = ailang_core::workspace::Workspace { + entry: ws.entry.clone(), + modules: lifted_modules, + root_dir: ws.root_dir.clone(), + registry: ws.registry.clone(), + }; + let mono = monomorphise_workspace(&lifted) + .map_err(|e| vec![internal_diag(format!("monomorphise_workspace: {e}"))])?; + // 3. lower each post-mono module to MIR. + let env = build_check_env(&mono); + let mut modules = std::collections::BTreeMap::new(); + for (name, m) in &mono.modules { + let mir = lower_to_mir::lower_module(m, &env) + .map_err(|e| vec![internal_diag(format!("lower_to_mir in `{name}`: {e}"))])?; + modules.insert(name.clone(), mir); + } + Ok(ailang_mir::MirWorkspace { entry: mono.entry.clone(), modules }) +} +``` + +> **Implementer note for Step 1.** The sequence above is transcribed +> from the CLI build path (`main.rs:2324-2346`) — `desugar_module` then +> `lift_letrecs` per module, rebuild the `Workspace`, then +> `monomorphise_workspace`. Three names to confirm against existing +> code as you wire it: +> - `build_check_env(&Workspace) -> Env` exists at `lib.rs:1632` — +> call it. (If its real signature differs, match it.) +> - `internal_diag(msg: String) -> Diagnostic` — a small new local +> helper building a `Diagnostic` with `Severity::Error` and `msg`. +> Copy the field shape from one existing `Diagnostic { … }` build +> site in this file. This is the mir.1a stand-in for the dedicated +> `MirLoweringError` the spec §"Error handling" names (introduced in +> mir.1b); "check passed but lowering failed" is that internal- +> compiler-error class. +> - `d.severity == Severity::Error` — confirm `Diagnostic` has a +> `severity: Severity` field with an `Error` variant (`Severity` +> re-exported at `:377`); adjust the predicate to the real +> field/variant names if they differ. If `check_workspace` only ever +> returns errors (no warnings in its `Vec`), the predicate can be +> `!diags.is_empty()` — verify which. + +- [ ] **Step 2: Add the two missing witness fixtures** + +The test loads the boundary witnesses as workspace fixtures (so +`load_workspace` injects the prelude — the witnesses reference +`print` / `ge` / `str_concat` / `io/print_str`, which live there). The +#49 witness already exists as +`examples/loop_recur_str_binder_no_leak_pin.ail` (reused as-is). Create +the two missing ones, each named by its module (the loader enforces +filename = module name). + +Create `examples/new_rawbuf_size_only.ail`: + +```ail +(module new_rawbuf_size_only + (fn main + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (let b (new RawBuf (con Int) 3) + (app print (app RawBuf.size b)))))) +``` + +Create `examples/new_counter_user_adt.ail`: + +```ail +(module new_counter_user_adt + (data Counter (ctor MkCounter (con Int))) + (fn new (type (fn-type (params (con Int)) (ret (con Counter)))) (params n) + (body (term-ctor Counter MkCounter n))) + (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) + (body (let c (new Counter 42) (do io/print_str "ok\n"))))) +``` + +Run (parse + check gate — confirms both fixtures load clean before the +test depends on them): +`target/debug/ail check examples/new_rawbuf_size_only.ail && target/debug/ail check examples/new_counter_user_adt.ail` +Expected: both print `ok (… symbols across 3 modules)`, exit 0. (Both +were already verified `ail check`-clean during planning; this is the +implementer's re-confirmation after writing the files.) + +- [ ] **Step 3: Write the ty-fill pins (integration test)** + +Create `crates/ailang-check/tests/lower_to_mir_ty.rs`. The test loads +each witness fixture via `ailang_surface::load_workspace` (the +established ailang-check integration-test pattern — see +`crates/ailang-check/tests/method_collision_pin.rs:15-40`), elaborates +the whole workspace (witness **plus** prelude **plus** kernel — so +`lower_to_mir` is exercised over the entire prelude, not just the tiny +witness), and asserts `ty` is filled correctly. It is an **additive** +test — it exercises the new producer without touching codegen. + +```rust +//! mir.1a: `lower_to_mir` fills `ty` on every node from the canonical +//! `synth`, and routes string literals to `MTerm::Str { rep: Static }`. +//! Loads the boundary witnesses as workspace fixtures (prelude + +//! kernel injected by `load_workspace`) and elaborates the whole +//! workspace, so the walk is exercised over the full prelude. These +//! pins protect the producer; codegen consumption arrives in mir.1b. + +use ailang_check::elaborate_workspace; +use ailang_mir::{MTerm, MirWorkspace, StrRep}; +use ailang_surface::load_workspace; +use std::path::{Path, PathBuf}; + +/// `/examples` — resolved from this crate's manifest dir, exactly +/// as `method_collision_pin.rs:19-25` does (cwd-independent). +fn examples_dir() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")) + .parent().expect("crates/ailang-check has parent crates/") + .parent().expect("crates/ has parent repo root") + .join("examples") +} + +/// Load a witness fixture (prelude injected) and elaborate it to MIR. +fn elaborate_fixture(module: &str) -> MirWorkspace { + let entry = examples_dir().join(format!("{module}.ail")); + let ws = load_workspace(&entry).expect("fixture loads (prelude injected)"); + elaborate_workspace(&ws).expect("witness elaborates to MIR") +} + +/// A def's lowered body in the elaborated workspace. +fn body<'a>(mir: &'a MirWorkspace, module: &str, def: &str) -> &'a MTerm { + &mir.modules[module] + .defs + .iter() + .find(|d| d.name == def) + .expect("def present") + .body +} + +#[test] +fn str_literal_lowers_to_static_str_node() { + // #49 witness: the loop seed "x" is a Str literal → MTerm::Str, + // rep = Static at mir.1 (mir.4 flips loop seeds to Heap). + let m = "loop_recur_str_binder_no_leak_pin"; + let mir = elaborate_fixture(m); + assert!( + find_static_str_seed(body(&mir, m, "main")), + "loop seed \"x\" must lower to MTerm::Str {{ rep: Static }}" + ); +} + +#[test] +fn new_over_user_adt_carries_node_types() { + // #53 witness: every node has a filled `ty`; the `(new Counter 42)` + // node's type is the user ADT `Counter`. + let m = "new_counter_user_adt"; + let mir = elaborate_fixture(m); + let MTerm::Let { init, .. } = body(&mir, m, "main") else { + panic!("main body is a let"); + }; + assert!( + matches!(init.as_ref(), MTerm::New { type_name, .. } if type_name == "Counter"), + "let init is the New node over Counter" + ); + let ty_str = ailang_core::pretty::type_to_string(&init.ty()); + assert!(ty_str.contains("Counter"), "New node ty is Counter, got {ty_str}"); +} + +#[test] +fn rawbuf_size_only_elaborates() { + // #51 witness: a RawBuf read only for size — must elaborate clean + // (the element type carried only by the author's annotation does + // not block lowering). + let mir = elaborate_fixture("new_rawbuf_size_only"); + assert!(mir.modules.contains_key("new_rawbuf_size_only")); +} + +/// Recursively search for a `MTerm::Str { rep: Static }` reachable +/// from a loop binder init (the seed). +fn find_static_str_seed(t: &MTerm) -> bool { + match t { + MTerm::Loop { binders, body } => { + binders.iter().any(|b| matches!( + &b.init, + MTerm::Str { rep: StrRep::Static, .. } + )) || find_static_str_seed(body) + } + MTerm::Let { init, body, .. } => { + find_static_str_seed(init) || find_static_str_seed(body) + } + _ => false, + } +} +``` + +> **Implementer note for Step 3.** `ailang_surface::load_workspace(&Path) +> -> Result` is the loader `ail check` uses (`main.rs:595`) +> and the one `method_collision_pin.rs:39` calls — it injects the +> prelude, so no hand-built single-module workspace is needed. Confirm +> `ailang-surface` is a (dev-)dependency of `ailang-check` reachable +> from `tests/` (it already is — the existing fixtures-loading pins +> import it). The `MTerm::Let`/`MTerm::New`/`MTerm::Loop` field names +> must match Task 1's type defs; if you renamed a field there, mirror +> it here. + +- [ ] **Step 4: Run the new pins** + +Run: `cargo test -p ailang-check --test lower_to_mir_ty` +Expected: PASS — all three tests green (`str_literal_lowers_to_static_str_node`, +`new_over_user_adt_carries_node_types`, `rawbuf_size_only_elaborates`). +A failure inside `elaborate_workspace` (not the assertion) means +`lower_to_mir` mishandles a `Term` shape somewhere in the prelude — +fix `lower_to_mir`, do not narrow the fixture. + +- [ ] **Step 5: Full-suite regression gate (additive ⇒ nothing breaks)** + +Run: `cargo test --workspace` +Expected: PASS — the entire existing suite stays green (mir.1a adds +code, consumes nothing; codegen, CLI, and all hash/round-trip pins are +untouched), plus the three new `lower_to_mir_ty` tests. + +--- + +## Notes for the orchestrator (commit + handoff) + +- **Commit shape:** mir.1a is one cohesive additive increment — a + single commit (`feat(check): mir.1a — typed-MIR types + post-mono + lower_to_mir + elaborate_workspace (additive)`) is appropriate; + `refs #49` (the open leg this milestone closes) in the body, not + `closes` (closure lands at mir.4). +- **Not in this plan (mir.1b, next planner run):** flipping codegen's + walk to `&MTerm`, deleting `synth_with_extras` + `synth_arg_type` + (9 call sites across lib.rs/drop.rs/match_lower.rs), threading the 18 + `lower_workspace*` callers, and the CLI build-path switch to + `elaborate_workspace`. That plan is written against the *landed* MIR + types, not this plan's projections.