iter revert: back out the Iteration-discipline milestone (it.1 + it.2)
One forward iteration; main never rewound.1ff7e81(the pre-9973546 commit) is the per-region byte oracle — every reverted source/test file is byte-identical to it; crates/ailang-check/src/lib.rs fully so. Root cause being corrected: the Iteration-discipline milestone was an over-escalation of fieldtest finding F1 (a [friction] item whose own minimal recommendation was a DESIGN.md note). Its totality dichotomy made the maximally-LLM-natural build(d:Int)=Node(1,build(d-1), build(d-1)) inexpressible (it.3 BLOCKED); the only in-thesis escape (A1/it.2b) conceded the language's first documented-unenforced totality precondition — a purity-pillar dilution the user rejected in favour of a full revert + rebuild. Removed: Term::Loop/Term::Recur/LoopBinder; the verify_structural_ recursion guardedness pass + term_contains_loop + Diverge-injection + the transitively-it.2 module_fns plumbing; the five Recur*/ NonStructuralRecursion CheckError variants (+ code() + the 3 dedicated ctx() arms); the it.1 codegen loop-header/phi/back-edge + parallel block_terminated setter; all Loop/Recur walker arms; 16 it.1/it.2 fixtures; 2 pin files; bench/it3-oracle/. Restored: 2 RC fixtures to1ff7e81content. Surgically kept (not in1ff7e81, landed with the milestone but independently sound): feature-acceptance clause 3 in DESIGN.md and skills/brainstorm/SKILL.md, with its worked example de-claimed from "shipped" to hypothetical-illustration form; the F3 P2 todo. bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json kept as historical record (like journals/plans). Sole net addition: an honest F1/F4 documented-idiom note in DESIGN.md (the tail-recursive accumulator fallback; examples/mut_counter.ail), guarded by a doc-presence test — "a documentation note is not a reshape", asserts nothing at the typecheck level. Roadmap: the Iteration-discipline block + blocking-fork section removed; the genuine total-Int-recursion ambition preserved as a deferred P2 milestone sequenced behind a future Nat/refinement-types milestone (not abandoned — correctly sequenced after the type machinery it needs). 2026-05-15-iteration-discipline.md carries a superseded header; it.1/it.2/it.3 journals + plans stay as history. Correctness gate PRISTINE: 164 surviving 1ff7e81-era fixtures ail check/ail run byte-identical to pre-milestone behaviour (verified against a1ff7e81worktree reference compiler, zero drift); cargo test --workspace 600/0; zero residual it.1/it.2 production surface. Spec docs/specs/2026-05-16-iteration-discipline-revert.md (b3853bf), plan docs/plans/2026-05-16-iter-revert.md (abf0013).
This commit is contained in:
+15
-49
@@ -102,12 +102,17 @@ A proposed feature ships only if all three hold:
|
||||
the bug class is structurally impossible rather than merely
|
||||
discouraged. A documentation note is not a reshape; the
|
||||
discriminator is whether the wrong code fails to typecheck, not
|
||||
whether a guideline advises against it. The canonical worked
|
||||
example is the iteration story: a bare `while` over mutable state
|
||||
passes 1 and 2 yet fails 3 (it reinstates iterated-mutable-state
|
||||
reasoning); structural recursion over an acyclic ADT and a named
|
||||
loop/recur point pass all three (the bug class is closed by
|
||||
construction, not by advice).
|
||||
whether a guideline advises against it. Worked example: a bare
|
||||
`while` over mutable state would pass clauses 1 and 2 yet fail
|
||||
clause 3 (it reinstates iterated-mutable-state reasoning the pure
|
||||
core exists to remove); a hypothetical "all repetition is either
|
||||
structurally-decreasing recursion over an acyclic ADT or an
|
||||
explicit named loop" iteration story would, *if it could be built
|
||||
without a documented-unenforced precondition*, pass all three —
|
||||
and the fact that the 2026-05 attempt could not (it forced a
|
||||
silent-divergence precondition; see
|
||||
`docs/specs/2026-05-16-iteration-discipline-revert.md`) is itself
|
||||
the clause-3 mechanism working as intended.
|
||||
|
||||
This is the positive complement to the CLAUDE.md rule that
|
||||
implementation effort is not a rationale: cost is not a reason *for* a
|
||||
@@ -164,16 +169,8 @@ Advantages:
|
||||
|
||||
The default is total, pure functions. Effects are declared as a set in the
|
||||
function type: `(Int) -> Int ![IO]`. The effect set is row-polymorphic
|
||||
(`![IO | r]`). Two effects are wired up: `IO` (observable side effects,
|
||||
raised by `do`-operations), and `Diverge` (non-termination). As of iter
|
||||
it.2 (2026-05-15) `Diverge` is no longer nominal: it is the effect carried
|
||||
by any function whose body contains a `loop` (or that calls a
|
||||
`Diverge`-declaring function), surfaced through the existing
|
||||
declared-vs-raised reconciliation (an undeclared `Diverge` is the existing
|
||||
`UndeclaredEffect`, no new diagnostic). Structural recursion is pure and
|
||||
total and carries no effect — the author who wants a `!Diverge`-free
|
||||
signature is structurally pulled toward structural recursion and pays
|
||||
`!Diverge` only when genuinely writing an unbounded `loop`.
|
||||
(`![IO | r]`). In the MVP only the effects `IO` and `Diverge` (for infinite
|
||||
loops) are wired up.
|
||||
|
||||
This is the most important LLM property: when I read a function, I can trust
|
||||
its signature without reading the body.
|
||||
@@ -2418,22 +2415,6 @@ are real surface forms.
|
||||
{ "t": "assign",
|
||||
"name": "<id>",
|
||||
"value": Term }
|
||||
|
||||
// Iter it.1: named loop head. `binders` declares one or more
|
||||
// lexically-scoped, typed, initialised binders (initialised in
|
||||
// order); `body` is a single Term in scope of all binders. `recur`
|
||||
// re-enters the lexically nearest enclosing loop, rebinding the
|
||||
// binders positionally; it must be in tail position of that loop's
|
||||
// body. The loop's static type is `body`'s static type.
|
||||
{ "t": "loop",
|
||||
"binders": [ { "name": "<id>", "type": Type, "init": Term }, ... ],
|
||||
"body": Term }
|
||||
|
||||
// Iter it.1: backward jump to the lexically nearest enclosing loop;
|
||||
// tail-position-only; binds that loop's binders. The `args` array is
|
||||
// always present in canonical JSON (even when empty).
|
||||
{ "t": "recur",
|
||||
"args": [ Term, ... ] }
|
||||
```
|
||||
|
||||
In the MVP, `do` is only a direct call to a built-in effect op (no
|
||||
@@ -2449,23 +2430,6 @@ mut-var into a lambda body is rejected at typecheck via
|
||||
`CheckError::MutVarCapturedByLambda` (iter mut.4-tidy). See
|
||||
`docs/specs/2026-05-15-mut-local.md`.
|
||||
|
||||
`loop`/`recur` are additive as of iter it.1 (2026-05-15): they
|
||||
parse, print, prose-project, round-trip, typecheck (binder typing,
|
||||
recur arity/type unification, recur tail-position) and codegen
|
||||
(loop-header block with one phi per binder, `recur` as a back-edge
|
||||
`br`) without removing or modifying the existing `tail-app`/`tail-do`
|
||||
paths. As of iter it.2 (2026-05-15) the structural-recursion
|
||||
guardedness restriction and the `Diverge` effect are in effect:
|
||||
a non-structural recursion-by-call is the compile error
|
||||
`NonStructuralRecursion` (directing the author to `(loop …)` /
|
||||
`recur`), and any fn whose body contains a `Term::Loop` (or calls a
|
||||
`Diverge`-declaring callee) must declare `!Diverge` in its effect
|
||||
row — structural recursion stays pure, total, and effect-free. A
|
||||
transitional grandfather exempts still-`tail: true`-marked recursive
|
||||
calls so the corpus type-checks unchanged through it.2.
|
||||
`tail-app`/`tail-do` are retired in it.3. See
|
||||
`docs/specs/2026-05-15-iteration-discipline.md`.
|
||||
|
||||
**`Literal`**:
|
||||
|
||||
```jsonc
|
||||
@@ -2917,6 +2881,8 @@ What **is** supported (and used as the smoke test for the pipeline):
|
||||
effect), and introduce composable transducers (`Stateful a b` +
|
||||
`pipe`). Spec: `docs/specs/2026-05-15-mut-local.md`.
|
||||
|
||||
**Accumulator-over-iteration shape (documented idiom, not an enforced rule).** `mut`/`var`/`assign` removes friction from *straight-line* and *cascade-of-if* accumulators, but does **not** by itself express the "one running total updated once per loop iteration" shape: a `var` cannot be captured into a lambda (the seal) and there is no loop construct in the language. Until a future iteration-totality milestone lands (gated behind `Nat`/refinement types — see the deferred roadmap entry), the canonical pattern for the per-iteration accumulator is a tail-recursive helper that threads the running total as an explicit parameter; `examples/mut_counter.ail` is the reference. This is a documented authoring idiom, not a typecheck-enforced constraint — wrong code here does not fail to compile, it is merely less ergonomic, which is exactly why this is documentation and not a language rule.
|
||||
|
||||
Pipeline regression smoke tests:
|
||||
|
||||
- `examples/sum.ail.json` → prints 55 (recursion, arithmetic).
|
||||
|
||||
@@ -0,0 +1,174 @@
|
||||
# iter revert — Iteration-discipline milestone surgical forward revert
|
||||
|
||||
**Date:** 2026-05-16
|
||||
**Started from:** abf00131c10ff9287b419439c565480c96fa861b
|
||||
**Status:** DONE
|
||||
**Tasks completed:** 11 of 11
|
||||
|
||||
## Summary
|
||||
|
||||
The Iteration-discipline milestone (it.1 `96db54d` + it.2 `a4be1e5`)
|
||||
is fully backed out by a single forward iteration, with `1ff7e81`
|
||||
(the last commit before milestone-start `9973546`) as the per-region
|
||||
byte oracle. `main` was never rewound — every restore is a forward
|
||||
working-tree edit, net-new it.1/it.2 surface is `rm`'d, DESIGN.md is
|
||||
hunk-edited in place (clause 3 / criterion section KEPT, never
|
||||
wholesale-restored). Feature-acceptance clause 3 and the F3 todo are
|
||||
retained; the clause-3 worked example is de-claimed from "shipped" to
|
||||
hypothetical-illustration form (in DESIGN.md and brainstorm SKILL.md
|
||||
in lockstep); one honest F1/F4 documentation note is added (the only
|
||||
net addition) and guarded by a doc-presence test. The correctness
|
||||
gate (Task 11) proved compiler behaviour **pristine**: all 164
|
||||
surviving `1ff7e81`-era fixtures `ail check`/`ail run` byte-identical
|
||||
to their pre-milestone behaviour; `cargo test --workspace` 600/0;
|
||||
zero residual it.1/it.2 production surface. AILang's iteration story
|
||||
is exactly the pre-`9973546` state (structural / tail recursion;
|
||||
`tail-app` intact); the genuine total-recursion ambition is preserved
|
||||
on the roadmap as a deferred P2 milestone sequenced behind a future
|
||||
`Nat`/refinement-types milestone.
|
||||
|
||||
## Per-task notes
|
||||
|
||||
- revert.1: AST node family + drift anchors + DESIGN.md §Data-model —
|
||||
removed `Term::Loop`/`Term::Recur`/`struct LoopBinder` + 2 serde
|
||||
units (ast.rs byte-identical to oracle); loop/recur exemplars +
|
||||
match arms removed from design_schema_drift.rs / spec_drift.rs /
|
||||
schema_coverage.rs (byte-identical); DESIGN.md §Data-model
|
||||
loop/recur JSON + it.1/it.2 prose removed (region byte-identical).
|
||||
- revert.2: `CheckError` surface — 5 variants + doc comments, 5
|
||||
`code()` arms, 3 dedicated `ctx()` arms deleted; `_ =>` catch-all
|
||||
preserved; diagnostic.rs confirmed genuine no-op.
|
||||
- revert.3: it.2 guardedness pass + Diverge-injection — STOP-gate
|
||||
cleared (all 6 named helpers it.2-net-new at oracle → all delete,
|
||||
no ambiguity). Removed the entire 687-line guardedness cluster
|
||||
(verify_structural_recursion, term_contains_loop, adt_families,
|
||||
referenced_con_names, mutual_structural_group, adt_param_positions,
|
||||
RecCall, TypeUnionFind, MutualGroup, et al.) **plus** the
|
||||
transitively-it.2 `module_fns` plumbing through
|
||||
check_module/check_def/check_fn signatures (oracle proved net-new;
|
||||
resolved via the plan's Oracle convention + recon-by-name mandate —
|
||||
see Concerns). 3 Diverge-injection sites restored byte-identical;
|
||||
lib.rs `"Diverge"` count 0 == oracle.
|
||||
- revert.4: it.1 check surface — synth Loop/Recur arms +
|
||||
verify_loop_body deleted; loop_stack param + ~30 threaded calls + 9
|
||||
local decls removed; verify_tail_positions survives, it.1 arms
|
||||
removed, byte-identical to oracle; substitute_rigids_in_term +
|
||||
post-mono name arms cleaned. Result:
|
||||
`crates/ailang-check/src/lib.rs` FULLY byte-identical to `1ff7e81`.
|
||||
- revert.5: 9 remaining walker files (lift/mono/linearity/uniqueness/
|
||||
reuse_shape/pre_desugar_validation/builtins + core desugar/
|
||||
workspace) restored to oracle, all byte-identical; pre-restore diff
|
||||
classification proved every hunk it.1/it.2-only.
|
||||
- revert.6: surface + prose + form-A grammar — parse.rs/print.rs/
|
||||
prose lib.rs/form_a.md restored to oracle byte-identical; each
|
||||
touched only by 96db54d (it.1) since 1ff7e81; surface+prose build
|
||||
clean.
|
||||
- revert.7: codegen — lib.rs/escape.rs/lambda.rs + ail/main.rs
|
||||
restored to oracle byte-identical; `block_terminated = true` count
|
||||
== 8 == oracle (it.1 parallel setter gone; the 4 tail-driven + 4
|
||||
control-flow setters survive). `cargo build --workspace` clean
|
||||
(first full-build gate, lockstep clustering worked as designed).
|
||||
- revert.8: STOP-gate re-verify cleared (live `git diff --stat`
|
||||
matched plan's net-new/modified/absent classification exactly).
|
||||
Deleted 2 pin files + 16 fixtures + bench/it3-oracle via plain
|
||||
`rm` (no git-index touch). 2 RC fixtures restored byte-identical.
|
||||
e2e.rs + codegen_import_map_fallback_pin.rs + carve_out_inventory.rs
|
||||
restored byte-identical (carve = "Twelve carve-outs", last entry
|
||||
test_mut_var_captured_by_lambda.ail.json). it.{1,2,3} stats json
|
||||
KEPT. cargo test --workspace 599/0.
|
||||
- revert.9: DESIGN.md Decision 3 → 1ff7e81 placeholder (byte-identical,
|
||||
hunk-only); clause-3 worked example de-claimed to hypothetical form
|
||||
(criterion section + clause-3 discriminator KEPT); brainstorm
|
||||
SKILL.md de-claimed in lockstep; F1/F4 note added verbatim;
|
||||
doc-presence test added verbatim, PASSES.
|
||||
- revert.10: roadmap Iteration-discipline [~] block + blocking-fork
|
||||
sub-section removed; deferred "Iteration-totality story" entry
|
||||
added verbatim at top of P2 (per plan + spec sequencing); F3 +
|
||||
Stateful-islands untouched; superseded header prepended to the old
|
||||
spec; Step-4 STOP-check clean (no residual A1 amendment).
|
||||
- revert.11 (correctness gate): 1ff7e81 ref compiler built in
|
||||
throwaway worktree; 164-fixture check/run oracle captured;
|
||||
post-revert compiler diffed byte-for-byte — fail=0, ZERO DRIFT,
|
||||
behaviour PRISTINE. cargo test --workspace 600/0. Residual
|
||||
it.1/it.2 production-surface grep clean. Worktree removed; main
|
||||
HEAD never moved.
|
||||
|
||||
## Concerns
|
||||
|
||||
- revert.3: the plan's Task-3 file-map enumerated the guardedness
|
||||
helpers + call site but did NOT explicitly list the `module_fns`
|
||||
signature threading through check_module/check_def/check_fn. The
|
||||
`1ff7e81` oracle unambiguously proved that threading it.2-net-new;
|
||||
leaving it would have been dead it.2 surface referencing deleted
|
||||
helpers. Resolved correctly via the plan's own "Oracle convention"
|
||||
+ "re-locate by symbol name, oracle is authority on every byte"
|
||||
mandate + the spec §Data-flow ("restored to pure pre-it.1 role").
|
||||
This is the recon-map-drifts-but-oracle-is-authority mechanism
|
||||
working as designed, not a plan defect — no bounce. Flagged so the
|
||||
Boss is aware the plan file-map under-enumerated one signature
|
||||
edge; the end-state is verified correct (lib.rs byte-identical to
|
||||
oracle).
|
||||
- revert.9: the plan's Task-9 Step-6 single-line grep heuristic
|
||||
(`grep -c 'clauses 1 and 2 yet fail clause 3' ...`) returned 0
|
||||
because the verbatim-applied replacement text line-wraps ("yet
|
||||
fail\n clause 3"). The substantive acceptance criterion
|
||||
(clause-3 block retained, only de-claimed) is positively verified
|
||||
multiline + by the intact `## Feature-acceptance criterion` section
|
||||
and "criterion 3 is the discriminator" sentence. Not a defect;
|
||||
flagged so the Boss does not misread the heuristic.
|
||||
|
||||
## Known debt
|
||||
|
||||
(none — the revert is byte-pristine against `1ff7e81` for all
|
||||
production surface; behaviour is byte-identical over the surviving
|
||||
corpus.)
|
||||
|
||||
## Blocked detail
|
||||
|
||||
(none — DONE.)
|
||||
|
||||
## Files touched
|
||||
|
||||
90 working-tree paths (Boss commits all as one cohesive revert iter):
|
||||
|
||||
- Deleted (59): `crates/ailang-check/tests/loop_recur_pin.rs`,
|
||||
`crates/ailang-check/tests/structural_recursion_pin.rs`; 16 it.1/it.2
|
||||
fixtures under `examples/` (loop_*.ail, struct_rec_*.ail,
|
||||
test_recur_*.ail.json, test_loop_missing_diverge / test_mutual_cross_family
|
||||
/ test_non_structural_recursion .ail.json); `bench/it3-oracle/`
|
||||
(MANIFEST.tsv + 40 .out).
|
||||
- Modified — source revert to 1ff7e81 (byte-identical):
|
||||
`crates/ailang-core/src/ast.rs`, `desugar.rs`, `workspace.rs`;
|
||||
`crates/ailang-check/src/lib.rs`, `lift.rs`, `mono.rs`,
|
||||
`linearity.rs`, `uniqueness.rs`, `reuse_shape.rs`,
|
||||
`pre_desugar_validation.rs`, `builtins.rs`;
|
||||
`crates/ailang-codegen/src/lib.rs`, `escape.rs`, `lambda.rs`;
|
||||
`crates/ail/src/main.rs`; `crates/ailang-surface/src/parse.rs`,
|
||||
`print.rs`; `crates/ailang-prose/src/lib.rs`;
|
||||
`crates/ailang-core/specs/form_a.md`.
|
||||
- Modified — tests revert to 1ff7e81 (byte-identical):
|
||||
`crates/ailang-core/tests/spec_drift.rs`, `schema_coverage.rs`,
|
||||
`carve_out_inventory.rs`; `crates/ail/tests/e2e.rs`,
|
||||
`codegen_import_map_fallback_pin.rs`.
|
||||
- Modified — net-add / hunk-edit:
|
||||
`crates/ailang-core/tests/design_schema_drift.rs` (loop/recur
|
||||
anchors removed + new doc-presence test added),
|
||||
`docs/DESIGN.md` (Decision 3 placeholder + clause-3 de-claim +
|
||||
F1/F4 note; hunk-edited, clause 3 kept), `docs/roadmap.md`
|
||||
(Iteration-discipline block removed, deferred P2 entry added),
|
||||
`docs/specs/2026-05-15-iteration-discipline.md` (superseded
|
||||
header), `skills/brainstorm/SKILL.md` (worked-example de-claim).
|
||||
- Modified — fixtures restored to 1ff7e81:
|
||||
`examples/rc_pin_recurse_implicit.ail`,
|
||||
`examples/rc_let_alias_implicit_param.ail`.
|
||||
- KEPT (no-op, Boss decision):
|
||||
`bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json`.
|
||||
|
||||
E2E coverage: none (revert iteration — the Task-11 behavioural-
|
||||
equivalence sweep over all 164 surviving fixtures is a stronger
|
||||
correctness proof than new E2E; the doc-presence test guards the
|
||||
only net-new artefact).
|
||||
|
||||
## Stats
|
||||
|
||||
bench/orchestrator-stats/2026-05-16-iter-revert.json
|
||||
@@ -78,3 +78,4 @@
|
||||
- 2026-05-15 — iter it.1: iteration-discipline milestone (1 of 3) — `Term::Loop` / `Term::Recur` / `LoopBinder` added as strictly-additive first-class AST nodes end-to-end: Form-A `parse_loop`/`parse_recur` + print + prose render/free-var/subst lockstep + canonical-JSON serde/round-trip + schema/spec-drift/schema-coverage/carve-out lockstep (13→17) + typecheck (binder typing + recur arity/type unification via `loop_stack: &mut Vec<Vec<Type>>` threaded exactly as mut.2's `mut_scope_stack`; recur-tail-position via a new private `verify_loop_body`, `verify_tail_positions` public signature unchanged) + codegen (loop-header block, one phi per binder, recur back-edge `br` with a NEW parallel `block_terminated` setter, lambda-boundary `loop_frames` save/restore mirroring mut.3). Four new `CheckError` variants `Recur{OutsideLoop,ArityMismatch,TypeMismatch,NotInTailPosition}` (bracket-`[code]`-free Display per the F2 convention). Strictly additive verified — zero deletions touch `tail-app`/`tail-do`, `verify_tail_positions`' tail-app role, or the seven existing codegen `block_terminated` sites (the 32 within-iter deletions are exclusively DD-3 stub-then-fill replacements). `Term::Recur` synth returns a fresh metavar (resolves the plan's flagged `Type::unit()` open risk: recur appears in `if` branches that must unify with the sibling type). `loop_counter.ail`→`55`, `loop_in_lambda_e2e.ail`→`49`, four negatives fire exact codes, `tail-app` fixtures byte-identical, zero IR/prose snapshot drift; `cargo test --workspace` green. Two mut.1-class plan-pseudo-vs-reality substitutions recorded (prose round-trip asserting AST-equality is impossible — no Form-B parser by design; the diagnostic.rs doc-list premise was false) → 2026-05-15-iter-it.1.md
|
||||
- 2026-05-15 — iter it.2: iteration-discipline milestone (2 of 3) — structural-recursion guardedness checker + first real `Diverge` effect, strictly additive (nothing `tail`-related removed; that is it.3). New whole-body pass `verify_structural_recursion` runs as a sibling of `verify_tail_positions` in `check_fn`'s post-synth region (DD-1): the `smaller`-set algorithm with implicit candidate-position inference + unconstrained accumulator positions (DD-2 — foldl-shape accumulator classifies as structural recursion, pure+total), self/mutual identification with an inline ADT-family connected-components union-find (DD-3), and the it.2-only `tail==false` grandfather. `CheckError::NonStructuralRecursion {callee,arg}` (bracket-`[code]`-free Display per F2). `term_contains_loop` (stops at `Term::Lam` boundaries, DD-4) injects `"Diverge"` into the raised effect set so the existing `UndeclaredEffect` machinery enforces it with no new diagnostic variant; lam-arrow + `Term::LetRec` sub-effect sites wired (loop behind a lam edge carries `!Diverge` on the lam's arrow, propagating via the free callee-effect path, not leaking to the enclosing fn — exactly as `!IO` scopes). DESIGN.md Decision 3 + §Data-model hook synced present-tense. Four it.1 loop fixtures gained `!Diverge`. Two spec-premise boundary defects surfaced and resolved inside the task's invariants (corpus clean, check not weakened): (§1) the spec's "21 tail-app fixtures" grandfather premise under-counts the corpus — no-ADT-candidate counter recursions (~18, e.g. `build_tree(depth:Int)`) have no structural position to verify and are deferred to it.3 migration; (§2) two RC-regression fixtures (`rc_pin_recurse_implicit`, `rc_let_alias_implicit_param`) hold an ADT param constant while decrementing an Int — genuinely non-structural, joined the spec's transitional `tail-app` grandfather exactly as the other 20 corpus fixtures do (their RC==GC regression guards verified still green; the regression lives in the unchanged `pin`/`pin_aliased` bodies). Both recorded as corrected it.3 corpus-migration scope. `cargo test --workspace` 622 green / 0 red; all 9 acceptance pins non-vacuous (negatives `.contains(code)`); struct_rec_sum→15, loop_needs_diverge→55, the it.1 55/49 e2e still green → 2026-05-15-iter-it.2.md
|
||||
- 2026-05-15 — iter it.3 (BLOCKED, bounce-back): destructive terminal iteration of iteration-discipline. Task 1 (non-destructive: pre-migration oracle + the spec-delegated class-(b) live sweep) ran complete — 40 recursive corpus fixtures classified + oracled under `bench/it3-oracle/`; zero production code changed; HEAD clean at c992eb9. The mandated Task-1.3 sweep surfaced a **fundamental milestone-design flaw**, not a migration nuisance: 6 fixtures contain `build(d: Int) = if d==0 then Leaf else Node(1, build(d-1), build(d-1))` — a terminating, maximally-LLM-natural, **non-structural (Int param, no ADT-candidate) non-tail BRANCHING (double) recursion** that the milestone's totality dichotomy ("structural-over-ADT OR loop/recur, else error") makes **inexpressible**: not ADT-structural, and not `recur`-able (branching ≠ single tail back-edge). Post-it.3 it is a hard `NonStructuralRecursion` with no expressible alternative — the milestone as-specified would fail its own feature-acceptance criterion (clause 1: the LLM reaches for `build(d-1),build(d-1)`; clause 2: the milestone would *remove* expressivity). The orchestrator correctly refused a 4th plan-patch and bounced (`feedback_spec_over_plan_patches`). Boss verdict: the totality story overlooked a second canonical total-by-construction scheme — well-founded recursion on a strictly-decreasing non-negative Int measure. Resolution requires a new additive iteration **it.2b** (widen the it.2 guardedness checker to accept Int-bounded recursion incl. branching) BEFORE it.3 re-dispatches; the purity sub-fork (Int≠Nat: total only for non-negative entry) touches the user-co-designed purity pillar → user design decision, recommended option A1 (accept with a documented non-negative-entry obligation, analogous to array-bounds). Notify sent; loop stopped. The RC-RSS/18g.1 load-bearing risk (it.3 Task 5.5/5b) was NOT reached and must NOT be treated as resolved by the milestone-close audit → 2026-05-15-iter-it.3.md
|
||||
- 2026-05-16 — iter revert: Iteration-discipline milestone (it.1 `96db54d` + it.2 `a4be1e5`) fully backed out by one **forward** iteration (`main` sacrosanct — never rewound; `1ff7e81`, the pre-`9973546` commit, is the per-region byte oracle). Root cause: the milestone was an over-escalation of fieldtest finding F1 (a `[friction]` item whose own minimal recommendation was a DESIGN.md note); its totality dichotomy made the maximally-LLM-natural `build(d:Int)=Node(1,build(d-1),build(d-1))` inexpressible (it.3 BLOCKED), and the only in-thesis escape (A1/it.2b) conceded the language's first documented-unenforced totality precondition — a purity-pillar dilution the user rejected. `Term::Loop`/`Term::Recur`/`LoopBinder`, the `verify_structural_recursion` guardedness pass + `term_contains_loop` + `Diverge`-injection + the transitively-it.2 `module_fns` plumbing, the five `Recur*`/`NonStructuralRecursion` `CheckError` variants (+ `code()` + 3 dedicated `ctx()` arms), the it.1 codegen loop-header/phi/back-edge + parallel `block_terminated` setter, and all walker arms are removed — `crates/ailang-check/src/lib.rs` and every reverted source/test file byte-identical to `1ff7e81`. Surgical keeps: feature-acceptance **clause 3** (DESIGN.md + brainstorm SKILL.md, worked example de-claimed "shipped"→hypothetical) and the F3 P2 todo. Sole net addition: an honest F1/F4 documented-idiom note (tail-recursive accumulator fallback; `examples/mut_counter.ail`) guarded by a doc-presence test. 16 it.1/it.2 fixtures + 2 pin files + `bench/it3-oracle/` deleted; 2 RC fixtures restored to `1ff7e81`; `bench/orchestrator-stats/2026-05-15-iter-it.{1,2,3}.json` kept (historical record). Roadmap: Iteration-discipline block + blocking-fork section removed; the genuine total-Int-recursion ambition preserved as a deferred P2 milestone sequenced behind a future `Nat`/refinement-types milestone (not abandoned — correctly sequenced). Correctness gate PRISTINE: 164 surviving `1ff7e81`-era fixtures `ail check`/`ail run` byte-identical to pre-milestone behaviour (1ff7e81 worktree reference compiler, zero drift); `cargo test --workspace` 600/0; zero residual it.1/it.2 production surface. The old it.* journals/plans + the superseded-headered `2026-05-15-iteration-discipline.md` stay as historical record → 2026-05-16-iter-revert.md
|
||||
|
||||
+17
-137
@@ -40,143 +40,6 @@ clean. Pick the next milestone from P2.)_
|
||||
|
||||
## P1 — Next
|
||||
|
||||
- [~] **\[milestone\]** Iteration discipline — structural recursion +
|
||||
named `loop`/`recur`; recursion-by-call restricted; `tail-app`
|
||||
retired. Spec `docs/specs/2026-05-15-iteration-discipline.md`
|
||||
(approved fda9b78; scope-corrected 2018178/10a0595). **Status
|
||||
2026-05-15: it.1 SHIPPED (96db54d — loop/recur additive), it.2
|
||||
SHIPPED (a4be1e5 — guardedness checker + first real Diverge
|
||||
effect), it.3 BLOCKED on a surfaced fundamental design fork (see
|
||||
"The blocking fork" below — needs a user design decision + a new
|
||||
iteration it.2b before it.3 can re-dispatch).** The iteration
|
||||
story of the language, decided in principle 2026-05-15. Two
|
||||
constructs survive, one is removed:
|
||||
- **Structural recursion stays — and becomes total-by-construction.**
|
||||
A recursive call is permitted iff it is structurally guarded:
|
||||
each recursive call is on a constructor-smaller component of an
|
||||
algebraic argument. Decision 10 already guarantees ADTs are
|
||||
acyclic, so a structurally-guarded recursion terminates *by the
|
||||
invariant the language already holds* — permitting it costs
|
||||
nothing on the provability pillar and it stays locally checkable.
|
||||
This is the most LLM-natural correct pattern (tree / AST / JSON /
|
||||
list `match`-and-recurse, saturated in every FP corpus) and must
|
||||
not be amputated.
|
||||
- **All other repetition must go through a named `(loop ...)` head +
|
||||
`recur`.** `recur` is the single explicit backward jump; it
|
||||
targets a lexically-enclosing named loop, never an implicit fn
|
||||
head (Clojure permits the implicit form — AILang does not, for
|
||||
the same no-outward-inference reason that motivated explicit
|
||||
`tail-app`). Accumulator loops, counted iteration, streaming,
|
||||
state machines — none are structurally decreasing, so all are
|
||||
forced into the explicit named-loop form.
|
||||
- **`tail-app` is retired.** `Term::App { tail: bool }` and the
|
||||
`musttail`-lowering surface go away: a call is either structural
|
||||
recursion (a plain call, checked total) or it is `loop`/`recur`
|
||||
(the only loop). No marked-tail-call concept survives.
|
||||
|
||||
**Motivation.** Discharges fieldtest finding F1 — the most
|
||||
consequential mut-local finding: mut-local's own motivation
|
||||
("removes friction from accumulators that today need tail-recursive
|
||||
helpers") was structurally unmet, because without a loop the only
|
||||
iteration mechanism remained the very tail-rec helper. `loop`/`recur`
|
||||
closes that honestly without introducing an imperative construct
|
||||
(it is pure: no mutable loop variable, no effect, composes into pure
|
||||
contexts freely). It also closes the residual "forgot to mark tail"
|
||||
trap *completely* — a recursive call that is not structurally
|
||||
guarded is a compile error that names itself, not a silent
|
||||
stack-overflow. And it unifies with Decision 10: acyclic values
|
||||
*and* an acyclic implicit call graph; the only cycles anywhere in a
|
||||
program are explicit, named, typed `loop` points. Both surviving
|
||||
constructs pass all three feature-acceptance clauses including the
|
||||
2026-05-15 clause 3 (structural recursion and named loop/recur are
|
||||
LLM-natural *and* their bug class is closed by construction; a bare
|
||||
`while` is exactly what clause 3 rejects).
|
||||
|
||||
**Original open spec questions — RESOLVED in it.2 (a4be1e5).**
|
||||
(1) *mutual* structural recursion → the conservative same-ADT-family
|
||||
rule (connected-components union-find over the type-reference
|
||||
graph; admits tree/forest, even/odd-over-Nat, mutual JSON; a
|
||||
general size-measure ordering stays out of scope). (2) the
|
||||
`foldl`-shaped accumulator-carrying structural walk → **counts as
|
||||
structural recursion** (plain, pure, total — only the structural
|
||||
argument must decrease; accumulator positions are unconstrained).
|
||||
Both shipped and pinned.
|
||||
|
||||
**The blocking fork (it.3-surfaced 2026-05-15 — needs a USER
|
||||
design decision; touches the purity pillar the user co-designed).**
|
||||
The milestone's totality thesis recognised exactly ONE
|
||||
total-by-construction recursion scheme: structural-over-an-acyclic-
|
||||
ADT (Decision 10). The it.3 mandated corpus sweep proved this is
|
||||
*incomplete*. Six corpus fixtures contain the single most
|
||||
LLM-natural tree-builder shape:
|
||||
`build(d: Int) = if d==0 then Leaf else Node(1, build(d-1), build(d-1))`.
|
||||
It is provably terminating, but: **not** ADT-structural (`d` is
|
||||
`Int`, no constructor-smaller component) and **not** `loop`/`recur`-
|
||||
able (it is *branching/double* recursion; `recur` is a single
|
||||
tail-position back-edge — a balanced-tree build is not a tail
|
||||
loop; the only `loop` form is a hand-rolled explicit-stack
|
||||
worklist, which no LLM writes). So the milestone *as-specified*
|
||||
makes a trivially-total, maximally-natural function
|
||||
**inexpressible** — failing its own feature-acceptance criterion
|
||||
(clause 1: the LLM reaches for `build(d-1),build(d-1)`; clause 2:
|
||||
the milestone would *remove* expressivity). This is a real
|
||||
design-thesis gap, not a migration nuisance: there is a SECOND
|
||||
canonical total-by-construction scheme the design overlooked —
|
||||
**well-founded recursion on a strictly-decreasing non-negative
|
||||
integer measure** (`f(0)=base; f(n)=…f(n-1)…`, branching allowed).
|
||||
|
||||
**Decision the user must make** (it trades against the purity
|
||||
pillar — Int ≠ ℕ; AILang has no `Nat`/refinement types, so
|
||||
Int-bounded recursion is total only for *non-negative entry*):
|
||||
- **A1 (RECOMMENDED).** Make the totality story a *trichotomy*:
|
||||
ADT-structural | Int-bounded-well-founded | explicit `loop`/`recur`.
|
||||
Accept Int-bounded recursion (recursive call on `p - <pos-lit>`
|
||||
with a non-recursing base guard, branching allowed) as a
|
||||
*second total-by-construction class*, with one documented
|
||||
obligation: non-negative entry (a negative seed diverges — the
|
||||
same precondition class as array-bounds the language already
|
||||
lives with). Restores the entire `f(n-1)` recursion family (the
|
||||
second-most-common shape in any corpus); keeps all 6 fixtures
|
||||
verbatim; the trichotomy is *more* complete, not less principled.
|
||||
Rationale is the language's own gate: a milestone that makes
|
||||
`build(d)` inexpressible cannot pass the feature-acceptance
|
||||
criterion. *Why this is a user call:* it concedes "total by
|
||||
construction, sign nothing" → "total by construction modulo one
|
||||
documented non-negative-entry obligation" — a dilution of a
|
||||
purity pillar the user personally weighted in the original
|
||||
Socratic design dialogue.
|
||||
- **A2.** Introduce a `Nat` type; accept Int-bounded recursion
|
||||
only on `Nat` — preserves zero-precondition purity, but `Nat`
|
||||
is its own sub-milestone and an LLM writes `depth: Int` unless
|
||||
the prelude makes `Nat` the natural default (clause-1 friction).
|
||||
- **A3 / B / C (not recommended).** Strict-dichotomy +
|
||||
explicit-worklist (fails clause 1 — no LLM hand-rolls a stack
|
||||
for tree-build); a narrow carve-out predicate (the patch smell);
|
||||
reshaping the LLM-natural fixtures (forbidden —
|
||||
`feedback_dont_adapt_tests_to_bugs`).
|
||||
|
||||
**If A1 (or A2): new iteration it.2b** — additive widening of the
|
||||
it.2 guardedness checker to also accept Int-bounded (incl.
|
||||
branching) recursion as total; no removal. After it.2b the 6
|
||||
fixtures check clean with zero migration; it.3 then re-dispatches
|
||||
from c992eb9 (the `bench/it3-oracle/` 40-fixture behavioural
|
||||
oracle is preserved and reused; nothing in it.3 was destructive).
|
||||
The it.3 RC-RSS/18g.1 load-bearing risk (Task 5.5/5b) is still
|
||||
UNTESTED — must not be treated as resolved by the milestone-close
|
||||
audit.
|
||||
|
||||
**Relation to Stateful islands.** This entry owns the iteration
|
||||
story and *supersedes* the "while-loops legal" scope bullet of the
|
||||
Stateful-islands milestone below. The genuinely-escaping
|
||||
mutable-state path (`ref a` / `MutArray a` / `Stateful a b` /
|
||||
`pipe`) is unaffected and stays in Stateful-islands.
|
||||
|
||||
- context: spec `docs/specs/2026-05-15-iteration-discipline.md`;
|
||||
per-iter journals 2026-05-15-iter-it.1 (shipped), -it.2
|
||||
(shipped), -it.3 (BLOCKED — the design fork above). Next action
|
||||
is a USER decision on the blocking fork (A1 recommended), then
|
||||
iteration it.2b, then it.3 re-dispatch from c992eb9.
|
||||
|
||||
- [x] **\[milestone\]** Heap-`Str` ABI — runtime infrastructure for
|
||||
malloc-backed, refcounted `Str` values alongside the existing
|
||||
static `@.str_*` globals. Today the `Str` path is static-only
|
||||
@@ -213,6 +76,23 @@ clean. Pick the next milestone from P2.)_
|
||||
|
||||
## P2 — Medium-term
|
||||
|
||||
- [ ] **\[milestone\]** Iteration-totality story — structural +
|
||||
Int-bounded total recursion with *enforced* non-negativity.
|
||||
AILang's iteration story stays as-is (structural / tail recursion;
|
||||
`tail-app` intact). The genuine ambition — make `f(n-1)`-family
|
||||
recursion (incl. branching tree builders) total *by construction*
|
||||
with the non-negative-entry precondition **enforced**, not merely
|
||||
documented — is deferred here because doing it without a purity-
|
||||
pillar concession requires refinement/`Nat` type machinery the
|
||||
language has not built (Decision 4 keeps refinements opaque, no
|
||||
SMT). Not abandoned; correctly sequenced after the type machinery.
|
||||
- depends on: a future `Nat`/refinement-types milestone (no spec
|
||||
yet).
|
||||
- context: `docs/specs/2026-05-16-iteration-discipline-revert.md`
|
||||
(why the 2026-05 attempt was reverted) and
|
||||
`docs/journals/2026-05-15-iter-it.3.md` (the branching-builder
|
||||
counter-example that surfaced the gap).
|
||||
|
||||
- [x] **\[milestone\]** Retire `io/print_int` / `io/print_bool` /
|
||||
`io/print_float` effect-ops + migrate example corpus to `print`.
|
||||
Shipped 2026-05-14 as iter rpe.1.
|
||||
|
||||
@@ -1,3 +1,11 @@
|
||||
> **SUPERSEDED 2026-05-16 by
|
||||
> `docs/specs/2026-05-16-iteration-discipline-revert.md`.** This
|
||||
> milestone was reverted in full (it.1 + it.2 backed out forward;
|
||||
> it.3 never ran). It is retained as a historical record of the
|
||||
> attempt and the design-thesis gap it surfaced; it is **not** the
|
||||
> current iteration-story design. Do not plan or implement from this
|
||||
> file.
|
||||
|
||||
# Iteration discipline — Design Spec
|
||||
|
||||
**Date:** 2026-05-15
|
||||
|
||||
Reference in New Issue
Block a user