Brummel
832375f2ac
All 176 files in the four accumulating directories now use a zero-padded 4-digit counter prefix that reflects creation order (`NNNN-slug.md`). The counter is assigned per directory in strict git-log creation order; ties broken alphabetically by original name. The old `YYYY-MM-DD-` prefix on docs/specs/ and docs/plans/ files is dropped — the date is recoverable from git log and the counter carries the ordering. A file's counter is stable for the life of the file: never reassigned, never reused, never compacted. Deleted files retire their counter; subsequent files do not fill the gap. This is the property that lets cross-references stay literal — refs use the full filename including the counter (`design/contracts/0007-honesty-rule.md`) so they grep cleanly and resolve directly without a glob step. 313 cross-references updated across .md/.rs/.toml/.c/.json files (test pins, include_str! paths, design-INDEX entries, baseline notes, runtime C comments, inter-contract markdown links incl. bare basename and `../models/foo.md` forms). CLAUDE.md gets a new "File-naming convention" section spelling out the rule and rationale. skills/brainstorm/SKILL.md and skills/planner/SKILL.md updated so new spec/plan creation produces counter-prefixed names from the start. The full test suite (cargo test --workspace) passes.
342 lines
12 KiB
Markdown
342 lines
12 KiB
Markdown
# Prose `loop` binders — projection redesign — Design Spec
|
||
|
||
**Date:** 2026-05-18
|
||
**Status:** Draft — awaiting user spec review
|
||
**Authors:** Brummel (orchestrator) + Claude
|
||
|
||
## Goal
|
||
|
||
The Form-B prose projection of `Term::Loop` currently renders the
|
||
binder-with-initial-value list as bare `name = init;` statements
|
||
*inside* the `loop { … }` body block:
|
||
|
||
```rust
|
||
loop {
|
||
acc = 0;
|
||
i = 1;
|
||
if i > n { acc } else { recur(acc + i, i + 1) }
|
||
}
|
||
```
|
||
|
||
A reader (LLM or human) decodes `loop { x = 0; … }` with the
|
||
C/Rust mental model: *re-assign `x = 0` on every iteration, then run
|
||
the rest*. That reading is wrong. The binders are **loop entry
|
||
state**, bound once on entry and thereafter re-bound **only** by
|
||
`recur`; they are not body statements and do not re-run per iteration.
|
||
|
||
Prose exists as the reading/diffing surface. AILang's load-bearing
|
||
doctrine is "the signature tells the truth without reading the body";
|
||
the dual obligation is that *when the body is read, the projection
|
||
must not lie about it*. The current projection lies. This milestone
|
||
replaces it.
|
||
|
||
The fix is a single change to one render arm in `ailang-prose`.
|
||
The `loop`-recur AST, Form-A surface, canonical JSON-AST, typechecker
|
||
and codegen are **unchanged**. This is a projection-only milestone,
|
||
one iteration.
|
||
|
||
## Architecture
|
||
|
||
`ailang-prose` is a one-way, deliberately lossy projection
|
||
(`docs/PROSE_ROUNDTRIP.md`). There is **no Form-B parser**: edited
|
||
prose is re-integrated by an LLM mediator (`ail merge-prose`), and
|
||
that mediator is fed `ailang_surface::print` (Form-A) as the original
|
||
module — *not* the prose. Consequently the `loop` prose rendering
|
||
feeds nothing back: it is read by humans/LLMs in step 2 of the
|
||
prose cycle and nowhere else.
|
||
|
||
The byte-isomorphic round-trip invariant in this project is
|
||
**Form-A ↔ JSON-AST** (surface crate, gated by the cross-form-identity
|
||
preflight). Prose is not on that path. This milestone therefore has
|
||
**zero** interaction with the round-trip invariant — stated explicitly
|
||
here so milestone-close audit does not chase a phantom risk.
|
||
|
||
The only contract the change must preserve is *projection
|
||
determinism* (same module → same prose bytes), which any pure printer
|
||
change preserves trivially, plus the snapshot-test discipline in
|
||
`crates/ailang-prose/tests/snapshot.rs` (a renderer change requires a
|
||
deliberate, diff-visible snapshot update — exactly the RED→GREEN of
|
||
this milestone).
|
||
|
||
The chosen rendering is a parenthesised init-list on the `loop`
|
||
keyword, positionally isomorphic to `recur`'s argument list:
|
||
|
||
```rust
|
||
loop(acc = 0, i = 1) {
|
||
if i > n { acc } else { recur(acc + i, i + 1) }
|
||
}
|
||
```
|
||
|
||
Rationale (semantic, not effort):
|
||
- The body block `{ … }` now contains exactly the loop body — the
|
||
binders are physically outside it, killing the "re-init every
|
||
iteration" misreading at the syntax level.
|
||
- `loop(acc = 0, i = 1)` and `recur(acc + i, i + 1)` are the same
|
||
positional shape. The binder list *is* the parameter list that
|
||
`recur` re-supplies; making them visually isomorphic teaches the
|
||
correct model ("`recur` re-binds these, positionally") instead of
|
||
obscuring it.
|
||
- Types are stripped (`acc = 0`, not `acc: Int = 0`), consistent
|
||
with the standing prose rule that `(con T)` is dropped everywhere
|
||
— `let`, `mut`/`var`, and fn parameters all render type-free in
|
||
prose because the type is re-derivable.
|
||
|
||
Rejected alternatives:
|
||
- **`loop with acc = 0, i = 1 { … }`** — `with` already denotes the
|
||
effect set in prose (`fn main() -> Unit with IO`). Overloading one
|
||
token with two unrelated meanings reduces readability; rejected on
|
||
the token-collision ground, not on effort.
|
||
- **`loop { initially acc = 0, i = 1; <body> }`** — stays inside the
|
||
braces (still visually conflated) and invents an `initially`
|
||
keyword; weaker than the chosen form on the exact axis at issue.
|
||
|
||
## Concrete code shapes
|
||
|
||
### The AILang program (primary — clause-1 evidence)
|
||
|
||
This milestone changes **no** authoring surface, so there is no new
|
||
construct an LLM author reaches for. The clause-1 artefact is the
|
||
existing, unchanged Form-A program and its projection. The program
|
||
(`examples/loop_sum_to_run.ail`, verbatim, unchanged by this
|
||
milestone):
|
||
|
||
```lisp
|
||
(module loop_sum_to_run
|
||
(fn main
|
||
(doc "loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55.")
|
||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||
(params)
|
||
(body (app print (app sum_to 10))))
|
||
(fn sum_to
|
||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||
(params n)
|
||
(body
|
||
(loop (acc (con Int) 0) (i (con Int) 1)
|
||
(if (app > i n)
|
||
acc
|
||
(recur (app + acc i) (app + i 1)))))))
|
||
```
|
||
|
||
Its prose projection, **before** (current, misleading):
|
||
|
||
```rust
|
||
// module loop_sum_to_run
|
||
|
||
/// loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55.
|
||
fn main() -> Unit with IO {
|
||
print(sum_to(10))
|
||
}
|
||
|
||
fn sum_to(n: Int) -> Int {
|
||
loop {
|
||
acc = 0;
|
||
i = 1;
|
||
if i > n {
|
||
acc
|
||
} else {
|
||
recur(acc + i, i + 1)
|
||
}
|
||
}
|
||
}
|
||
```
|
||
|
||
**After** (this milestone):
|
||
|
||
```rust
|
||
// module loop_sum_to_run
|
||
|
||
/// loop-recur iter 3 — sum 1..10 via loop/recur. Expected stdout: 55.
|
||
fn main() -> Unit with IO {
|
||
print(sum_to(10))
|
||
}
|
||
|
||
fn sum_to(n: Int) -> Int {
|
||
loop(acc = 0, i = 1) {
|
||
if i > n {
|
||
acc
|
||
} else {
|
||
recur(acc + i, i + 1)
|
||
}
|
||
}
|
||
}
|
||
```
|
||
|
||
The empty-binder loop (`examples/loop_forever_build.ail`'s
|
||
`(loop (i (con Int) 0) (recur (app + i 1)))` has one binder; a
|
||
genuinely binder-less `(loop <body>)` is also legal) renders
|
||
`loop() { … }` — parentheses are always emitted, for regularity
|
||
and symmetry with `recur()` (which already renders the no-arg form
|
||
with empty parens). Single-binder example
|
||
(`examples/loop_forever_build.ail`):
|
||
|
||
```rust
|
||
fn spin(n: Int) -> Int {
|
||
loop(i = 0) {
|
||
recur(i + 1)
|
||
}
|
||
}
|
||
```
|
||
|
||
### Implementation shape (secondary — supporting, not the point)
|
||
|
||
One arm in `crates/ailang-prose/src/lib.rs`, the `Term::Loop` case
|
||
of `write_term` (currently lib.rs:938–954).
|
||
|
||
Before:
|
||
|
||
```rust
|
||
Term::Loop { binders, body } => {
|
||
// loop-recur iter 1: minimal-correctness Form-B render.
|
||
// Prose surface for loop is not yet designed; render the
|
||
// shape so a reader sees it without overcommitting.
|
||
out.push_str("loop {\n");
|
||
for b in binders {
|
||
indent(out, level + 1);
|
||
out.push_str(&b.name);
|
||
out.push_str(" = ");
|
||
write_term(out, &b.init, level + 1, owning_module);
|
||
out.push_str(";\n");
|
||
}
|
||
indent(out, level + 1);
|
||
write_term(out, body, level + 1, owning_module);
|
||
out.push('\n');
|
||
indent(out, level);
|
||
out.push('}');
|
||
}
|
||
```
|
||
|
||
After:
|
||
|
||
```rust
|
||
Term::Loop { binders, body } => {
|
||
out.push_str("loop(");
|
||
for (i, b) in binders.iter().enumerate() {
|
||
if i > 0 {
|
||
out.push_str(", ");
|
||
}
|
||
out.push_str(&b.name);
|
||
out.push_str(" = ");
|
||
write_term(out, &b.init, level, owning_module);
|
||
}
|
||
out.push_str(") {\n");
|
||
indent(out, level + 1);
|
||
write_term(out, body, level + 1, owning_module);
|
||
out.push('\n');
|
||
indent(out, level);
|
||
out.push('}');
|
||
}
|
||
```
|
||
|
||
The init expressions render at `level` (they are on the keyword
|
||
line, not inside the indented block) — mirrors how `recur`'s args
|
||
already render at the call-site level (lib.rs:956–965). The doc
|
||
comment that says "Prose surface for loop is not yet designed" is
|
||
removed (it is now designed). `Term::Recur` is **unchanged**: it
|
||
already renders `recur(a, b)` correctly and is now visibly
|
||
isomorphic to the loop head.
|
||
|
||
The two non-render `Term::Loop` sites — `count_free_var`
|
||
(lib.rs:~1167) and `subst_var_with_term` (lib.rs:~1341) — are
|
||
**not touched**; they implement shadowing/substitution semantics,
|
||
not rendering.
|
||
|
||
## Components
|
||
|
||
- `crates/ailang-prose/src/lib.rs` — rewrite the `Term::Loop` arm
|
||
of `write_term`. ~12 LOC in one arm. No signature change, no new
|
||
function, no new dependency.
|
||
- `examples/loop_sum_to_run.prose.txt` (new) and
|
||
`examples/loop_forever_build.prose.txt` (new) — committed snapshot
|
||
expectations carrying the Option-A bytes.
|
||
- `crates/ailang-prose/tests/snapshot.rs` — two `#[test]` functions
|
||
(`snapshot_loop_sum_to_run`, `snapshot_loop_forever_build`)
|
||
invoking the existing `check_snapshot` harness. These cover the
|
||
two structurally distinct cases: multi-binder + non-recur exit,
|
||
and single-binder + recur-only (no exit).
|
||
|
||
## Data flow
|
||
|
||
`examples/<stem>.ail` → `ailang_surface::load_module` →
|
||
`ailang_prose::module_to_prose` → byte-compare against committed
|
||
`examples/<stem>.prose.txt`. Unchanged harness; this milestone only
|
||
adds two stems to the set and changes the bytes the renderer
|
||
produces for `Term::Loop`.
|
||
|
||
No runtime, codegen, typecheck, or schema data path is touched.
|
||
|
||
## Error handling
|
||
|
||
None applicable. Prose rendering is total over a well-formed AST
|
||
(the AST is already validated by `load_module` before reaching the
|
||
renderer). The change introduces no new failure mode and no new
|
||
diagnostic. The empty-binder case is handled by the loop emitting
|
||
`loop() { … }` (the `for` loop body simply does not execute; the
|
||
`(` / `)` are emitted unconditionally).
|
||
|
||
## Testing strategy
|
||
|
||
RED-first, via the existing snapshot harness:
|
||
|
||
1. **RED.** Author `examples/loop_sum_to_run.prose.txt` and
|
||
`examples/loop_forever_build.prose.txt` with the **desired**
|
||
Option-A bytes, plus the two `#[test]` functions. Against the
|
||
current renderer these fail (it emits the old `loop { acc = 0;
|
||
… }` shape), pinning the symptom.
|
||
2. **GREEN.** Apply the `write_term` `Term::Loop` rewrite. Both
|
||
snapshots pass.
|
||
3. **No-regression.** The full `crates/ailang-prose` test suite
|
||
stays green — no other fixture contains `Term::Loop`, so no
|
||
other snapshot changes (confirmed: no existing
|
||
`examples/*.prose.txt` contains `loop`).
|
||
4. **Determinism** is covered structurally — the renderer is a pure
|
||
function of the AST; the snapshot equality check *is* the
|
||
determinism assertion.
|
||
|
||
Explicitly **out of scope for test coverage** (because untouched):
|
||
the Form-A ↔ JSON-AST cross-form-identity preflight and the
|
||
`merge-prose` cycle. The spec asserts these are not on the changed
|
||
path; no new test is added there because nothing there changes.
|
||
|
||
Multi-line wrapping of a long binder list is **out of scope**:
|
||
single-line comma-separated, consistent with how `recur` args and
|
||
fn-call args already render. If a future fixture needs wrapping it
|
||
is a separate, separately-motivated change.
|
||
|
||
## Acceptance criteria
|
||
|
||
- `cargo test -p ailang-prose` green, including the two new
|
||
`snapshot_loop_*` tests.
|
||
- `ail prose examples/loop_sum_to_run.ail` emits the **After**
|
||
block above byte-for-byte (binders on the `loop(...)` keyword
|
||
line; the `{ … }` body contains no `name = init;` lines).
|
||
- `ail prose examples/loop_forever_build.ail` emits `loop(i = 0) {`
|
||
with `recur(i + 1)` as the body.
|
||
- No diff in any other `examples/*.prose.txt`.
|
||
- No change to `examples/*.ail`, `*.ail.json` build artefacts,
|
||
typecheck, codegen, runtime, or `docs/DESIGN.md` (the loop/recur
|
||
semantics are unchanged; only their reading projection changes).
|
||
- `docs/PROSE_ROUNDTRIP.md` unchanged (the cycle it documents is
|
||
untouched; prose remains a lossy one-way projection).
|
||
|
||
### Feature-acceptance criterion (DESIGN.md gate)
|
||
|
||
This is a projection change, not an authoring feature, so clause 1
|
||
("an LLM author naturally produces code that uses it") is evaluated
|
||
against the *reading* surface, not a new construct: the program is
|
||
unchanged; the deliverable is its honest projection. The three
|
||
clauses:
|
||
|
||
1. **Naturally used:** the prose surface is the LLM/human reading
|
||
and diffing surface for every module containing a loop — it is
|
||
used by construction, not opt-in.
|
||
2. **Measurably improves correctness / removes redundancy:** yes —
|
||
it removes a projection that actively implies wrong (re-init-
|
||
every-iteration) loop semantics. A reading surface that lies
|
||
about the body it projects is a correctness defect in that
|
||
surface; the fix is the removal of that defect.
|
||
3. **Reintroduces no eliminated bug class:** none. Prose has no
|
||
parser and relaxes no semantic constraint; the Form-A surface,
|
||
typechecker, codegen, and round-trip invariant are untouched.
|
||
|
||
Passes on all three.
|