Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

plan: mir.1a — typed-MIR infrastructure (additive half of spec mir.1)

Browse Source 
First of two plans for spec iteration mir.1 (docs/specs/0060-typed-mir.md).
mir.1 is the project's largest iteration — a full codegen frontend
switch from walking &Term to walking &MTerm — and it does not fit one
bite-sized plan, because the switch is atomic: there is no compiling
intermediate between "all Term" and "all MTerm" (dual-path is
spec-forbidden). The MIR *producer* side, by contrast, compiles and
tests in isolation. So mir.1 is sequenced across two plans:

- mir.1a (this plan): the additive producer — new leaf crate
  ailang-mir (MTerm/MArg/Callee/Mode/StrRep, structurally complete over
  all 17 Term variants plus the Str split), ailang-check::lower_to_mir
  (post-mono walk that calls canonical synth per node and maintains
  locals/loop_stack exactly as synth does — no second type engine), and
  ailang-check::elaborate_workspace (check → desugar+lift → mono →
  lower_to_mir). Nothing consumes MIR yet; codegen untouched; whole
  suite stays green; three ty-fill pins load the #51/#53/#49 witnesses
  as fixtures and elaborate the full workspace (prelude included).

- mir.1b (next plan, against the landed types): flip codegen's walk to
  &MTerm, delete synth_with_extras + synth_arg_type (9 call sites across
  lib.rs/drop.rs/match_lower.rs), thread the 18 lower_workspace* callers,
  switch the CLI build path to elaborate_workspace.

Both together satisfy the spec's mir.1 row. The split is plan
granularity, not a spec change — the spec's mir.1 deliverable is
unchanged.

Orchestrator design calls baked in (planner judgement, no user fork):
dedicated MTerm::Str{lit,rep} variant (Str-split installs the mir.4
hook at the #49 loop seed); emit_ir keeps &Module (builds MIR
internally — minimal blast radius); lower_to_mir scaffolding mirrors
mono.rs:771-816; Match-arm binding reuses synth's own type_check_pattern.

Recon (plan-recon) mapped the full deletion blast radius for mir.1b
(9 synth_arg_type sites, not the 3 the focus-hint assumed; 18
lower_workspace* callers). The two new witness fixtures
(new_rawbuf_size_only, new_counter_user_adt) were verified ail
check-clean during planning.
This commit is contained in:
Brummel
2026-05-31 13:51:33 +02:00
parent 8bc2972594
commit 438a009b83
1 changed files with 950 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/plans/0114-mir.1a-mir-infrastructure.md
+950
View File
@@ -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(<lowered callee>)` (→ `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<String, MirModule>,
}
#[derive(Debug, Clone)]
pub struct MirModule {
pub name: String,
pub defs: Vec<MirDef>,
}
/// 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<String>,
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(<lowered callee>)` at mir.1; mir.2
/// resolves static targets to `Callee::Static`.
App { callee: Callee, args: Vec<MArg>, tail: bool, ty: Type },
Let { name: String, mode: Mode, init: Box<MTerm>, body: Box<MTerm>, ty: Type },
LetRec {
name: String,
sig: Type,
params: Vec<String>,
body: Box<MTerm>,
in_term: Box<MTerm>,
ty: Type,
},
If { cond: Box<MTerm>, then: Box<MTerm>, else_: Box<MTerm>, ty: Type },
Do { op: String, args: Vec<MArg>, tail: bool, ty: Type },
Ctor { type_name: String, ctor: String, args: Vec<MArg>, ty: Type },
Match { scrutinee: Box<MTerm>, arms: Vec<MArm>, ty: Type },
Lam {
params: Vec<String>,
param_tys: Vec<Type>,
ret_ty: Type,
effects: Vec<String>,
body: Box<MTerm>,
ty: Type,
},
Seq { lhs: Box<MTerm>, rhs: Box<MTerm>, ty: Type },
Clone { value: Box<MTerm>, ty: Type },
ReuseAs { source: Box<MTerm>, body: Box<MTerm>, ty: Type },
Loop { binders: Vec<MLoopBinder>, body: Box<MTerm>, ty: Type },
Recur { args: Vec<MArg>, ty: Type },
/// `elem` is `None` at mir.1; mir.5 carries the element type.
New { type_name: String, elem: Option<Type>, args: Vec<MNewArg>, 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<MTerm>),
}
#[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<String, Type>,
loop_stack: Vec<Vec<(String, Type)>>,
}
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<Type> {
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = crate::Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<crate::ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<crate::FreeFnCall> = Vec::new();
let mut warnings: Vec<crate::diagnostic::Diagnostic> = 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<MTerm> {
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::<Result<Vec<_>>>()?;
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::<Result<Vec<_>>>()?;
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::<Result<Vec<_>>>()?;
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::<Result<Vec<_>>>()?;
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::<Result<Vec<_>>>()?;
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<MirModule> {
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<String, Type> = 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<ailang_mir::MirWorkspace, Vec<crate::diagnostic::Diagnostic>> {
// 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};
/// `<repo>/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<Workspace>` 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.