Iter 16a-aux — DESIGN.md drift audit (post-15f)

After six feature iters since the last docs sweep, DESIGN.md had
visible drift. Patched in place rather than queueing the next
codegen-heavy iter against a stale spec.

DESIGN.md changes (+72 LOC):
- Decision 6: form (A) marked shipped (Iter 14c, sole projection
  since 15e); body kept as audit trail.
- Pipeline: desugar pass added between resolve+hash and typecheck;
  invariant noted that CheckedModule.symbols hashes from the
  original module, not the desugared one (so ail diff/manifest
  preserve on-disk identity).
- CLI: added deps, diff, workspace, builtins (shipped earlier but
  never doc'd).
- "What is not (yet) supported": re-anchored from "end of Iter 13"
  to "as of Iter 16a"; removed lifted gates (cross-module ADTs,
  no-GC, flat-pattern-only); added tighter follow-up gates
  (literal sub-patterns, local recursive let).
- "What IS supported": promoted nested Ctor patterns (16a),
  cross-module ADTs (14h), form-(A) text surface (14b/14c/15e),
  Boehm GC (Decision 9 / 14f) into the smoke-test list.
- Smoke tests: added std_list_demo, std_maybe_demo, std_either_demo,
  std_pair_demo, nested_pat fixtures.

JOURNAL: 16a-aux entry recording the drift sites and what was
explicitly *not* changed (Goal, Decisions 1-5, 7-9, Mangling,
Convention, Data model, Verification — spot-checked, all current).

Tests: 93/93 unchanged (doc-only). Build clean.
This commit is contained in:
2026-05-07 19:39:44 +02:00
parent 689c445d25
commit 20b412342d
2 changed files with 168 additions and 22 deletions
+94 -22
View File
@@ -113,10 +113,20 @@ Rationale:
Trade-off: no inline optimisations through the LLVM API. We rely on
`clang -O2` as the standard pipeline.
## Decision 6: authoring surface (Iter 14b — WIP)
## Decision 6: authoring surface (Iter 14b)
**Status: design pass in progress.** Reading without skipping the JOURNAL
will leave this section ahead of the implementation.
**Status: shipped.** Form (A) was chosen in Iter 14b and implemented as
the `ailang-surface` crate (parser + printer) in Iter 14c. Form-A is
gated against drift by `ailang-surface/tests/round_trip.rs`, which
parses every `.ailx` fixture, prints it back, re-parses, and demands
canonical-byte equality. In Iter 15e, `ail render` and both branches
of `ail describe` were rewired to use `ailang_surface::print`, making
form (A) the **sole** text projection of a module — the legacy
non-round-tripping pretty-printer code in `pretty.rs` was deleted in
the same iter, leaving only diagnostic helpers (`type_to_string`,
`pattern_to_string`, `manifest`) public. The rest of this section
records the *why* of Decision 6 for the audit trail; the constraints
listed below describe the surface as shipped.
### Why this is opening up
@@ -689,23 +699,41 @@ conversion in JOURNAL). A `seq` term evaluates `lhs` for its effects
.ail.json ─┐
├─ load + validate schema
├─ resolve names + assign hashes
├─ desugar (AST → AST, Iter 16a)
├─ typecheck (HM, effect rows)
├─ lower to MIR (SSA-like, named SSA values)
├─ emit LLVM IR (.ll)
└─ clang -O2 *.ll -o binary
└─ clang -O2 *.ll -o binary (links libgc for @GC_malloc)
```
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 — currently
only flattens nested constructor patterns (16a), but 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.
## 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
ail render <module> — JSON → pretty-print
ail parse <module.ail>pretty-print → JSON (for bootstrapping)
ail emit-ir <module> — writes .ll
ail build <module> — full pipeline → binary
ail run <module> — build + execute (tempdir), passthrough exit code
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.ailx> form-A text → canonical JSON-AST
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> — writes .ll
ail build <module> — full pipeline → binary
ail run <module> — build + execute (tempdir), passthrough exit code
```
## Verification and correctness (across cycles)
@@ -723,8 +751,15 @@ ail run <module> — build + execute (tempdir), passthrough exit
## What is not (yet) supported
Snapshot of the boundary at the end of Iter 13. Items move out of this list
as iterations land; the JOURNAL records the exact iteration.
Snapshot of the boundary as of Iter 16a. Items move out of this list
as iterations land; the JOURNAL records the exact iteration. Recently
**lifted** gates that used to live here: cross-module ADTs (lifted in
Iter 14h via qualified `module.Type` / `module.Ctor` references in
both `(con ...)` and `(term-ctor ...)` / `(pat-ctor ...)` positions);
GC for ADT boxes, lambda envs, and closure pairs (Boehm conservative
collector wired up in Iter 14f, see Decision 9); nested constructor
sub-patterns inside `match` (lifted in Iter 16a via the desugar pass —
literal sub-patterns are still rejected, see below).
- No effect handlers — only the built-in IO and Diverge ops.
- No refinements / SMT escalation.
@@ -737,13 +772,15 @@ as iterations land; the JOURNAL records the exact iteration.
instantiation, deferred.
- No higher-rank polymorphism. Passing a polymorphic fn to another
polymorphic fn (`apply(id, 42)`) is not supported.
- No cross-module ADTs. ADTs are local to a module; ctor names must be
unique within their module but may collide across modules.
- No literal sub-patterns inside a Ctor pattern. `(pat-ctor Cons 0 _)`
is rejected (`nested-ctor-pattern-not-allowed` from `ailang-check`)
because the pattern-match backend has no switch-on-i64 yet.
Workaround: bind a var and test in the arm body.
- No local recursive `let`. `let f = ... in ...` only sees `f`'s
binding inside the body, not inside its own RHS — recursion needs
a top-level def.
- No visibility rules in imports. Every top-level def of an imported module
is reachable; there is no `pub` / `priv`.
- No GC. ADT boxes, lambda envs, and closure pairs all leak. Acceptable
for current example programs; required before any longer-running
program.
What **is** supported (and used as the smoke test for the pipeline):
@@ -751,10 +788,30 @@ What **is** supported (and used as the smoke test for the pipeline):
- `if`, `let`, function calls, recursion.
- Effects on function signatures, with `do op(args)` for direct effect
ops (`io/print_int`, `io/print_bool`, `io/print_str`).
- **ADTs + flat pattern matching** (Iter 3). Sub-patterns of a Ctor
pattern are restricted to `Var` / `Wild`.
- **ADTs + pattern matching** (Iter 3, extended in Iter 16a). Sub-patterns
of a Ctor pattern may be `Var`, `Wild`, **or another `Ctor`** (the
desugar pass flattens nested Ctor patterns into a chain of let + match
before typecheck/codegen — see `ailang-core::desugar` and Pipeline
above). Literal sub-patterns (`(pat-ctor Cons 0 _)`) are still rejected
by `ailang-check`.
- **Imports + qualified cross-module references** via dotted names
(Iter 5).
(Iter 5). Extends to **types and constructors** (Iter 14h): a foreign
module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as
`(term-ctor std_pair.Pair MkPair x y)` and `(pat-ctor MkPair x y)`
inside that scrutinee. Std-library demos (`examples/std_*_demo.ail.json`)
exercise this end-to-end.
- **AI-authoring text surface, form (A)** (Decision 6 / Iter 14b14c,
exclusive in 15e). The `ailang-surface` crate parses `.ailx` form-A
text into a canonical `ailang-core::ast::Module` and prints any module
back as form-A text. `ail render` and `ail describe` use it as the
sole text projection; `ail parse` is the inverse direction. Round-trip
identity (text → AST → JSON → AST → text) is gated by
`ailang-surface/tests/round_trip.rs` over every shipped fixture.
- **Memory management via Boehm conservative GC** (Decision 9 / Iter 14f).
Every ADT box, lambda env, and closure pair is allocated by `@GC_malloc`,
declared in the LLVM module preamble and linked from `libgc` at build
time. Soak-tested by `examples/gc_stress.ail.json` and the
`examples/std_list_stress.ail.json` fixture.
- **First-class function references** (Iter 7). A top-level fn name (or
qualified `prefix.def`) used as a `Term::Var` is a fn-value.
- **Anonymous lambdas with capture** (Iter 8). `Term::Lam` constructs a
@@ -802,3 +859,18 @@ Pipeline regression smoke tests:
- `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match
over `Maybe<Int>`: `or_else(Some(7), 99)` then
`or_else(None, 99)`).
- `examples/std_list_demo.ail.json` (Iter 15a/15b) → exercises
`std_list`'s combinators (length, sum, reverse, take/drop-style
uses) end-to-end against `std_list`'s `List<a>`.
- `examples/std_maybe_demo.ail.json` (Iter 15c) → exercises `std_maybe`
combinators over `Maybe<Int>`, including `from_maybe` and `map`.
- `examples/std_either_demo.ail.json` (Iter 15d) → first program with
three distinct type variables in a single fn (the `either`
eliminator), monomorphised six different ways in the IR.
- `examples/std_pair_demo.ail.json` (Iter 15f) → drives every
`std_pair` combinator (fst, snd, swap, map_first, map_second);
expected output 7, 9, 9, 7, 8, 18.
- `examples/nested_pat.ail.json` (Iter 16a) → first program to use a
nested `(pat-ctor Cons a (pat-ctor Cons b _))`; the desugar pass
flattens it into a chain that the existing flat-match codegen
consumes. Prints 30 for a 3-element input list.