Files

T

Brummel 832375f2ac convention: counter-prefix file naming across docs/specs/, docs/plans/, design/contracts/, design/models/

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.

2026-05-28 13:31:31 +02:00

12 KiB

Raw Permalink Blame History

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:

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:

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):

(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):

// 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):

// 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):

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:

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:

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:

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.
GREEN. Apply the write_term Term::Loop rewrite. Both snapshots pass.
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).
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:

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.
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.
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.

12 KiB Raw Permalink Blame History Unescape Escape

Prose loop binders — projection redesign — Design Spec