Brummel
a378dad0aa
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
92 lines
5.2 KiB
Markdown
92 lines
5.2 KiB
Markdown
# 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`](../../crates/ailang-mir/src/lib.rs)) 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](../contracts/0018-check-codegen-boundary.md).
|
|
|
|
Two allocator backends share the same MIR. `--alloc=rc` is the
|
|
canonical backend committed to in the
|
|
[memory model](../contracts/0008-memory-model.md) 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`](../../crates/ailang-core/src/desugar.rs))
|
|
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](../contracts/0001-authoring-surface.md) (Form-A,
|
|
round-trippable) and [prose projection](0006-prose-projection.md)
|
|
(Form-B, lossy, no parser); `ail build --emit=staticlib` produces
|
|
the layout fixed in [embedding ABI](../contracts/0003-embedding-abi.md)
|
|
plus [frozen value layout](../contracts/0006-frozen-value-layout.md).
|