Files
Brummel a378dad0aa docs(design): ratify the check→codegen boundary (mir.5, typed-MIR close)
mir.5 is the typed-MIR milestone's closing iteration. Its CODE half had
already converged before the iteration began, so mir.5 ships no code —
it ratifies into the design/ ledger the boundary the code already holds.

Verified at iteration entry (empirically, not from the spec sketch):
  - all four named re-derivers grep-clean in codegen: synth_with_extras,
    synth_arg_type, type_home_module, the second infer_module_with_cross;
  - lower_workspace takes &MirWorkspace (codegen consumes MIR);
  - MTerm::New is unreachable!() — raw-buf.4 desugars Term::New to
    (app T.new …) before codegen, so there is no element-type
    re-derivation left to relocate;
  - #51 / #53 (the element-type / new-T codegen crashes) are closed;
    their residue was fixed by ee4107c / 420f75f plus the New-desugar,
    not by a separate raw-buf patch track.

Ledger work (the mir.5 deliverable):
  - NEW design/contracts/0018-check-codegen-boundary.md: the invariant
    "codegen re-derives nothing; MIR is total over what check proved;
    a codegen arm that recomputes a fact instead of reading MIR is
    drift." Ratifier: lower_to_mir_ty.rs::callee_classification_builtin_and_static.
  - 0013-typeclasses invariant 2 retracted: codegen no longer re-resolves
    cross-module names via an import_map fallback; lower_to_mir::classify_callee
    resolves the reference once into Callee::Static and codegen consumes it.
  - 0003-pipeline.md: the "lower to MIR" line names the real stage
    (elaborate_workspace → MirWorkspace → lower_workspace) and a new
    paragraph states the boundary, cross-referencing 0018.
  - INDEX.md: boundary contract row added; qualified-xref re-pointed at
    lower_to_mir + 0018.
  - codegen_import_map_fallback_pin.rs doc-comment made honest — it pins
    the post-mono AST precondition classify_callee relies on, not a
    codegen-side resolution that no longer exists. Assertions unchanged;
    the test stays green.
  - spec 0060 gains a mir.5 refinement note recording the early code
    convergence.

Acceptance criteria 1-7 of docs/specs/0060-typed-mir.md are all met.
Full workspace suite green (exit 0, 0 failed, 2 ignored); 708 passed
carried from mir.4 (no test added or removed).

Not done here (deliberately): the milestone #7 (raw-buf) subsumption
note is an external Gitea tracker write; the /boss auto-mode classifier
declined it as an unauthorised external write and it is surfaced to the
user rather than worked around. The end-to-end milestone fieldtest
remains the deliberate manual close-gate before the tracker milestone
is marked done.

refs #51 #53
2026-06-01 01:34:37 +02:00

5.2 KiB

Pipeline and CLI

Pipeline

.ail.json  ─┐
            ├─ load + validate schema
            ├─ resolve names + assign hashes
            ├─ desugar (AST → AST)
            ├─ typecheck (HM, effect rows; mode-strict per the memory model)
            ├─ lift_letrecs (post-typecheck AST → AST)
            ├─ lower to MIR (elaborate_workspace → MirWorkspace; ailang-check::lower_to_mir)
            ├─ emit LLVM IR (.ll)  (ailang-codegen::lower_workspace consumes &MirWorkspace)
            └─ clang -O2 *.ll -o binary
                  --alloc=rc   → emits inc/dec    (@ailang_rc_inc / _dec; canonical, default)
                  --alloc=bump → links bump-floor (@bump_malloc; raw-alloc bench-floor)

MIR (ailang-mir) is the single typed artefact crossing the check→codegen boundary: lower_to_mir re-enters check's canonical synth on the post-mono AST and attaches every fact codegen needs (node ty, resolved Callee, Mode + consume, StrRep), so codegen consumes &MirWorkspace and re-derives nothing — no type synthesis, no callee-ladder walk, no uniqueness inference. The invariant and its failure mode are check→codegen boundary.

Two allocator backends share the same MIR. --alloc=rc is the canonical backend committed to in the memory model and the CLI default; the typechecker enforces (own) / (borrow) modes, codegen emits ailang_rc_inc / _dec calls at the points dictated by linearity, and Term::Clone / Term::ReuseAs materialise into actual rc-bumps and in-place rewrites respectively. --alloc=bump selects the raw-alloc bench-floor (runtime/bump.c, no free, leak-only) and is used by bench/run.sh to measure RC overhead against the structurally cheapest allocator — it is not a production target.

The desugar pass (ailang-core::desugar::desugar_module) runs before typecheck and codegen in every entry point of ailang-check and ailang-codegen. It is a pure AST → AST rewriter — it flattens nested constructor patterns and alpha-renames any binder whose name shadows an enclosing binding to a fresh <name>$<n> (so the uniqueness side-table's (def_name, binder_name) key is injective per fn), and is the chosen home for any future surface-smoothing rewrites that should not bloat the core AST or the backends. Critical invariant: CheckedModule.symbols in the check entry point continues to hash from the original on-disk module, not the desugared one, so ail diff and ail manifest report identities that match the canonical JSON the user is editing.

The lift_letrecs pass (ailang-check::lift_letrecs) runs after typecheck and before codegen, but only on the build / run paths — the check subcommand stops at typecheck and never sees a lifted module. It eliminates every Term::LetRec that the desugar pass left in place (the case where at least one capture is Term::Let-bound, so its type is only knowable after inference). The output is a module with synthetic <hint>$lr_N top-level fns appended, ready for codegen. Synthetic FnDefs added by this pass do not appear in CheckedModule.symbols — same invariant as the desugar-pass lifts.

CLI

ail check     <module.ail.json>          — loads, validates, typechecks
ail manifest  <module.ail.json>          — table: name :: type !effects [hash]
ail describe  <module> <name>            — detail of a definition (form-A body)
ail render    <module.ail.json>          — JSON-AST  → form-A text  (exact inverse of `parse`)
ail parse     <module.ail>              — form-A text → canonical JSON-AST
ail prose     <module.ail.json>          — JSON-AST  → form-B (lossy human prose, no parser)
ail merge-prose <m.ail.json> <m.prose.txt>
                                         — compose the LLM-mediator prompt for the prose round-trip
ail deps      <module.ail.json>          — list cross-module references
ail diff      <a.ail.json> <b.ail.json>  — content-addressed def-level diff
ail workspace <entry.ail.json>           — list all modules transitively reachable from entry
                                           (`--json` for machine output;
                                           `manifest --workspace` and `diff --workspace`
                                           extend single-module subcommands to workspaces)
ail builtins                             — list built-in fns and effect ops
ail emit-ir   <module> [--emit=staticlib]  — writes .ll (staticlib: a main-free kernel's IR, no @main)
ail build     <module> [--emit=staticlib]  — full pipeline → binary (staticlib: lib<entry>.a + libailang_rt.a)
ail run       <module>                   — build + execute (tempdir), passthrough exit code

The text projections the CLI moves between are documented in authoring surface (Form-A, round-trippable) and prose projection (Form-B, lossy, no parser); ail build --emit=staticlib produces the layout fixed in embedding ABI plus frozen value layout.