Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

spec: prose-loop-binders — loop binders out of the body block

Browse Source 
Form-B prose renders loop binders as bare `name = init;` statements
inside the `loop { … }` body, which reads as C/Rust re-init-every-
iteration semantics — a lie about a body the projection exists to
let the reader trust. Redesign: parenthesised init-list on the
keyword, `loop(acc = 0, i = 1) { … }`, positionally isomorphic to
`recur(...)`. Projection-only; loop/recur AST, Form A, JSON-AST,
typecheck, codegen, and the Form-A↔JSON round-trip invariant are
untouched. Step-7.5 grounding-check PASS. Roadmap entry opened P0
in-flight.
This commit is contained in:
Brummel
2026-05-18 00:55:46 +02:00
parent 6cbd0fe6b1
commit c657e74f9c
2 changed files with 355 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/roadmap.md
+14
View File
@@ -35,6 +35,20 @@ work progresses.
## P0 — In flight
- [~] **\[milestone\]** Prose `loop` binders — projection redesign.
Form-B prose currently renders loop binders as `name = init;`
statements *inside* the `loop { … }` body, which misreads as
C/Rust re-init-every-iteration semantics. Move them to a
parenthesised init-list on the keyword — `loop(acc = 0, i = 1)
{ … }` — positionally isomorphic to `recur(...)`. Projection-only:
one `ailang-prose` `write_term` `Term::Loop` arm + 2 snapshot
fixtures/tests; loop/recur AST, Form A, JSON-AST, typecheck,
codegen, and the Form-A↔JSON round-trip invariant all unchanged.
Spec'd + approved 2026-05-18; Step-7.5 grounding-check PASS. Plan
next.
- context: `docs/specs/2026-05-18-prose-loop-binders.md`;
surfaced from the loop/recur prose review (2026-05-18 chat).
- [x] **\[milestone\]** Standalone `loop` / `recur` — CLOSED 2026-05-18.
Strictly-additive strict-iteration surface, `recur` tail-position-only,
no totality claim. Shipped: iter 1 `a179ec3` (additive AST nodes),
docs/specs/2026-05-18-prose-loop-binders.md
+341
View File
@@ -0,0 +1,341 @@
# 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.