diff --git a/docs/specs/0060-typed-mir.md b/docs/specs/0060-typed-mir.md index 1f02c7b..40884b4 100644 --- a/docs/specs/0060-typed-mir.md +++ b/docs/specs/0060-typed-mir.md @@ -78,10 +78,10 @@ exists (`crates/ailang-codegen/Cargo.toml`), so no cycle is created; `ailang-core` (for `Type`). ``` -.ail.json ─ parse ─ resolve ─ desugar ─ typecheck ─┐ - │ lower_to_mir (NEW, in ailang-check) - AST + type env ───┴──▶ MirModule ──▶ emit LLVM IR - (typed, mode/callee/rep-annotated) (codegen: reads, derives nothing) +.ail.json ─ parse ─ resolve ─ desugar ─ typecheck ─ lift ─ monomorphise ─┐ + │ lower_to_mir (NEW, in ailang-check) + monomorphised AST ─────────────────────────── ┴──▶ MirModule ──▶ emit LLVM IR + (typed, mode/callee/rep-annotated) (codegen: reads, derives nothing) ``` - The **authoring AST** (Form A, content-addressed, hashable) is @@ -89,10 +89,27 @@ exists (`crates/ailang-codegen/Cargo.toml`), so no cycle is created; authored, never hashed, never round-tripped. This preserves the authoring contract: an author writes no type the checker already infers (the feature-acceptance redundancy bar). -- `lower_to_mir` runs as the final phase of `check_workspace`, after - typecheck + lift, reusing the type environment the checker already - built. On success it yields a `MirWorkspace`; on type error it - yields the existing `Vec` and no MIR. +- `lower_to_mir` runs **after monomorphisation**, on the post-mono + workspace — the same artefact codegen lowers today. It is *not* a + phase of `check_workspace` (which stops at typecheck, pre-mono): if + MIR were built pre-mono it would not carry the monomorphic + specialisations `monomorphise_workspace` appends and codegen emits, + reintroducing the very check↔codegen gap this milestone closes. The + build path is wrapped by one front-end entry point, + `elaborate_workspace`, that runs check → lift → mono → lower_to_mir + and yields a `MirWorkspace` on success or the existing + `Vec` on a type error. +- **One type engine, not two.** `lower_to_mir` walks the post-mono AST + with check's own canonical `synth` to fill `ty` on every node. This + is still a type walk — `synth` is a pure `&Term → Type` function and + the AST carries no node-ids, so MIR cannot be a side-table read; it + is built inline by walking. What the milestone removes is not the + walk but the *second engine*: codegen's `synth_with_extras` is a + hand-copied mirror of `synth` that drifts from it (every raw-buf bug + is a drift point). Replacing the mirror with a single post-mono call + to the canonical `synth`, materialised as MIR, deletes the drift + class structurally — there is no longer a second implementation to + disagree. - `lower_workspace*` in codegen take `&MirWorkspace` instead of `&Workspace`. The `Emitter` fields and methods that re-derive (`locals`' carried `Type`, `synth_with_extras`, `type_home_module`, @@ -190,9 +207,11 @@ pub enum Mode { Owned, Borrow } // before — crates/ailang-check/src/lib.rs:1283 pub struct CheckedModule { pub symbols: IndexMap } // signatures only -// after — check_workspace yields MIR on success +// after — one front-end entry wraps check → lift → mono → lower_to_mir pub fn elaborate_workspace(ws: &Workspace) -> Result>; -// (check_workspace stays for the diagnostics-only callers; elaborate_* is the build path) +// runs the full front end and lowers the POST-mono workspace to MIR. +// (check_workspace stays for the diagnostics-only callers — `ail check`, +// which stops at typecheck; elaborate_workspace is the build path.) ``` **codegen boundary** (`ailang-codegen`): @@ -217,25 +236,37 @@ pub fn lower_workspace(mir: &MirWorkspace) -> Result; `Callee` / `Mode` / `StrRep` / `MirWorkspace`. Leaf; depends only on `ailang-core`. - **`ailang-check::lower_to_mir` (new module):** walks the - typechecked, lifted AST with the live type environment and emits + **monomorphised** AST with check's canonical `synth` and emits `MTerm`, filling `ty` on every node. Later iterations fill `callee` (mir.2), `mode` / `consume_count` (mir.3), `rep` (mir.4). +- **`ailang-check::elaborate_workspace` (new entry):** the single + front-end function — runs `check_workspace` (diagnostics gate), + `lift_letrecs`, `monomorphise_workspace`, then `lower_to_mir` on the + post-mono workspace. Returns `MirWorkspace` or the diagnostics. This + moves the mono orchestration out of the CLI and behind one boundary. - **`ailang-codegen` (rewired):** entry points take `&MirWorkspace`; the four re-derivers are removed iteration by iteration as their annotation lands in MIR. - **CLI (`crates/ail/src/main.rs`):** the build path calls - `elaborate_workspace` and threads `MirWorkspace` into - `lower_workspace*`. `check` / `emit-ir` / diagnostics paths - unchanged where they only need diagnostics. + `elaborate_workspace` (which now subsumes the explicit `lift` + `mono` + steps the CLI orchestrated) and threads `MirWorkspace` into + `lower_workspace*`. `check` / diagnostics paths stay on + `check_workspace`; the `emit-ir` path builds MIR via the same + front-end entry. ## Data flow `Workspace (AST)` → `typecheck` (unchanged) → `lift` (unchanged) → -`lower_to_mir` (type env → `MirWorkspace`) → `lower_workspace` -(`MirWorkspace` → LLVM IR text) → `clang`. The type environment that -`synth` builds inside check is consumed in-process by `lower_to_mir` -rather than discarded; nothing re-walks the AST for types after MIR -exists. +`monomorphise` (unchanged) → `lower_to_mir` (post-mono AST + canonical +`synth` → `MirWorkspace`) → `lower_workspace` (`MirWorkspace` → LLVM IR +text) → `clang`. The single type-inference engine is check's `synth`: +`lower_to_mir` calls it once over the post-mono bodies to materialise +MIR, and codegen reads the result rather than running its own +`synth_with_extras` mirror. The remaining `synth` walk inside +`typecheck` (pre-mono, for diagnostics) and the `lower_to_mir` walk +(post-mono, for MIR) are not redundant — they run on different +workspaces for different purposes, and both are the *same* canonical +engine, never a divergent copy. ## Error handling @@ -267,10 +298,10 @@ is complete ⇒ codegen cannot fall through to an `UnknownVar`). ## Iteration decomposition -Strategy: MIR is structurally complete over all 27 node kinds from -mir.1 (codegen consumes it fully — no AST/MIR dual path). Each -iteration adds **one** annotation class and deletes the matching -codegen re-derivation. +Strategy: MIR is structurally complete over all 17 `Term` variants +(`crates/ailang-core/src/ast.rs:436`) from mir.1 (codegen consumes it +fully — no AST/MIR dual path). Each iteration adds **one** annotation +class and deletes the matching codegen re-derivation. | Iter | Adds to MIR | Deletes from codegen | Acceptance | |---|---|---|---|