spec: iteration-discipline milestone — structural recursion + named loop/recur; tail-app retired
User-approved 2026-05-15 (read, probed via the sma_factory.myc streaming analysis, no D1/D2 change requested, proceed-by-/boss). Grounding-check PASS holds: spec bytes unchanged since the Step 7.5 dispatch (the non-load-bearing "34 vs 36 tail-app sites" wording left as attested rather than re-grounding for a count the agent ruled non-defect; the 21-fixture migration unit is exact). Three ordered iterations: it.1 loop/recur additive, it.2 guardedness checker + Diverge effect, it.3 tail-app/tail-do retirement + corpus migration.
This commit is contained in:
@@ -0,0 +1,437 @@
|
||||
# Iteration discipline — Design Spec
|
||||
|
||||
**Date:** 2026-05-15
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
|
||||
## Goal
|
||||
|
||||
Give AILang exactly two iteration forms and remove the third:
|
||||
|
||||
1. **Structural recursion** — a recursive call permitted *iff* it is
|
||||
structurally guarded (recurses on a constructor-smaller component
|
||||
of an algebraic argument). Under Decision 10 (ADTs are acyclic by
|
||||
construction) such recursion is **total by construction**: it
|
||||
terminates because the value it descends cannot be infinite. It
|
||||
stays a plain call, pure, effect-free, and is the most LLM-natural
|
||||
correct iteration pattern (tree / list / AST / JSON
|
||||
match-and-recurse — saturated in every FP corpus).
|
||||
|
||||
2. **Named `(loop …)` + `recur`** — the single explicit backward
|
||||
jump, lexically scoped to an enclosing named loop. Every
|
||||
repetition that is *not* structurally decreasing (accumulator
|
||||
loops that are not structural, counted iteration, state machines,
|
||||
streaming) is expressed here, and only here.
|
||||
|
||||
3. **`tail-app` / `tail-do` — retired.** The marked-tail-call concept
|
||||
(`Term::App { tail: bool }`, `Term::Do { tail: bool }`, the two
|
||||
surface keywords, `musttail` lowering, `verify_tail_positions`'s
|
||||
old role, `CheckError::TailCallNotInTailPosition`, Decision 8) is
|
||||
removed. A call is either structural recursion (a plain call,
|
||||
checked total) or it is `loop`/`recur`. No marked-tail-call
|
||||
concept survives.
|
||||
|
||||
This discharges fieldtest finding **F1** (mut-local's own stated
|
||||
motivation — "removes friction from accumulators that today need
|
||||
tail-recursive helpers" — was structurally unmet, because without a
|
||||
loop the only iteration mechanism *remained* the tail-recursive
|
||||
helper). It closes the "forgot to mark a recursive call as tail →
|
||||
silent stack overflow" trap **completely**: a non-structural
|
||||
recursion-by-call is now a named compile error, not a runtime crash.
|
||||
It unifies with Decision 10: acyclic *values* and an acyclic
|
||||
*implicit call graph* — the only cycle anywhere in a program is an
|
||||
explicit, named, typed `loop`. Fieldtest finding **F4** (DESIGN.md
|
||||
never named the tail-rec fallback) is absorbed: there is no tail-rec
|
||||
fallback to document anymore.
|
||||
|
||||
## Architecture
|
||||
|
||||
Three coupled mechanisms, shipped as three ordered iterations. The
|
||||
ordering is forced by a codegen invariant, not by convenience:
|
||||
|
||||
- The codegen block-termination invariant (`emit_call` /
|
||||
`emit_indirect_call` / `lower_effect_op` set
|
||||
`self.block_terminated = true` only on `tail: true`;
|
||||
`match_lower.rs` pre-tail-call shallow-dec and the
|
||||
`lib.rs:1238–1577` branch-termination bookkeeping depend on it)
|
||||
means `tail: true` currently *owns* the "this block ends with a
|
||||
self-terminating control transfer" seam. `recur` is precisely a
|
||||
self-terminating backward control transfer. So `recur` must occupy
|
||||
that seam **before** `tail` can vacate it.
|
||||
|
||||
Iteration order:
|
||||
|
||||
- **it.1 — `loop`/`recur`, additive.** New `Term::Loop` /
|
||||
`Term::Recur` AST + schema/canonical + Form-A surface + round-trip
|
||||
fixture + checker (scope + tail-position rules for `recur`) +
|
||||
codegen (loop-header block with phi binders; `recur` = backward
|
||||
branch occupying a *new* block-termination seam, *alongside* the
|
||||
still-present `tail` seam). Nothing is removed. End state: a
|
||||
working `loop`/`recur` and `tail-app` coexist.
|
||||
|
||||
- **it.2 — structural-guardedness checker + `Diverge` effect.** The
|
||||
recursion-guardedness analysis + `CheckError::NonStructuralRecursion`;
|
||||
and the first real implementation of the Decision-3 `Diverge`
|
||||
effect (any `FnDef` whose body contains a `Term::Loop`, or calls a
|
||||
`Diverge` callee, must declare `Diverge`). End state: structural
|
||||
recursion is pure+total; non-structural recursion-by-call is a
|
||||
compile error directing the author to `loop`; `loop`-bearing
|
||||
functions carry `!Diverge`. `tail-app` still exists but is now
|
||||
redundant with structural recursion.
|
||||
|
||||
- **it.3 — retire `tail-app`/`tail-do` + migrate corpus.** Remove the
|
||||
`tail` fields, the two keywords, the `musttail` lowering,
|
||||
`verify_tail_positions`'s old role, `TailCallNotInTailPosition`,
|
||||
Decision 8; rework the codegen block-termination invariant so the
|
||||
seam is solely `recur`'s; migrate all 21 `.ail` fixtures / 34
|
||||
`(tail-app …)` sites. Destructive; last; depends on it.1 (loop
|
||||
occupies the seam) and it.2 (the structural fixtures are *proven*
|
||||
total before their redundant tail marker is stripped).
|
||||
|
||||
First-iteration planner scope: **it.1** in full.
|
||||
|
||||
## Components
|
||||
|
||||
Per-construct touch-point set follows the mut-local milestone
|
||||
template (`docs/specs/2026-05-15-mut-local.md` §Components): AST+serde
|
||||
→ schema-drift + DESIGN.md §Data-model anchor → Form-A surface
|
||||
parse+print → round-trip fixture → check arm + diagnostics → codegen
|
||||
lower + escape → e2e example.
|
||||
|
||||
### it.1 — `loop` / `recur`
|
||||
|
||||
- **AST (`crates/ailang-core/src/ast.rs`).**
|
||||
`Term::Loop { binders: Vec<LoopBinder>, body: Box<Term> }`;
|
||||
`Term::Recur { args: Vec<Term> }`;
|
||||
`struct LoopBinder { name: String, #[serde(rename="type")] ty:
|
||||
Type, init: Box<Term> }`. Serde round-trip unit tests alongside
|
||||
the existing `Term::Mut` ones (ast.rs ~899–940). New variants
|
||||
require new anchors in `crates/ailang-core/tests/design_schema_drift.rs`
|
||||
(`Term::Loop → "loop"`, `Term::Recur → "recur"`) **and** matching
|
||||
§"Data model" entries in `docs/DESIGN.md` in the same iteration, or
|
||||
the drift test fails.
|
||||
- **Form-A surface.** No lexer change — `loop` / `recur` are
|
||||
head-idents exactly as `mut` / `var` / `assign` are (confirmed:
|
||||
mut.1 needed no `lex.rs` change). `crates/ailang-surface/src/parse.rs`:
|
||||
EBNF block, dispatch arm, `parse_loop` / `parse_recur`, keyword
|
||||
list. `crates/ailang-surface/src/print.rs`: `Term::Loop` /
|
||||
`Term::Recur` arms. `crates/ailang-prose/src/lib.rs`: read +
|
||||
rebuild arms (the prose projection is a lockstep member with
|
||||
parse/print/serde).
|
||||
- **Round-trip.** New `examples/loop_*.ail` fixture(s) —
|
||||
auto-discovered by `crates/ailang-surface/tests/round_trip.rs`
|
||||
(globs `examples/*.ail`); this is the round-trip gate.
|
||||
- **Check (`crates/ailang-check/src/lib.rs`).** `Term::Loop` typed by
|
||||
typing each binder's `init`, binding `name:ty` in a fresh frame,
|
||||
typing `body` (the loop's type is the body's type, and every
|
||||
`recur` site must unify with the binder vector). `Term::Recur`
|
||||
arity + per-position type must match the lexically-enclosing
|
||||
`Term::Loop`'s binders. New diagnostics: `RecurOutsideLoop` (a
|
||||
`recur` with no enclosing `loop`), `RecurArityMismatch`,
|
||||
`RecurTypeMismatch`. `recur` must be in **tail position** of the
|
||||
enclosing loop body — `verify_tail_positions` is repurposed: from
|
||||
it.1 on, the tail-position pass also enforces "every `recur` is in
|
||||
tail position of its enclosing loop"; the diagnostic for a
|
||||
mis-placed `recur` is `RecurNotInTailPosition` (it.3 removes the
|
||||
old `tail-app`-flavoured role of the same pass — see it.3). The
|
||||
Term-walker arms (desugar, lift, mono, the
|
||||
`MutVarCapturedByLambda`-style free-var helpers) all gain
|
||||
`Term::Loop`/`Term::Recur` cases (~25 walker sites, mirroring the
|
||||
mut.1 blast radius).
|
||||
- **Codegen (`crates/ailang-codegen/src/lib.rs`,
|
||||
`escape.rs`).** `Term::Loop` → an LLVM loop-header basic block with
|
||||
one `phi` per binder (entry edge = `init`, back edge = `recur`
|
||||
args); body lowered with the header in scope. `Term::Recur` →
|
||||
evaluate args, emit the back-edge `br` to the header, set
|
||||
`self.block_terminated = true`. This is a **new** block-termination
|
||||
seam, added *alongside* the existing `tail: true` seam (no existing
|
||||
codegen path is modified in it.1). `escape.rs` gains `Term::Loop`/
|
||||
`Term::Recur` escape-walk arms.
|
||||
- **e2e.** `examples/loop_counter.ail` (accumulator counter that
|
||||
today would be a `tail-app` helper) runs and prints the same value
|
||||
the equivalent tail-rec helper would.
|
||||
|
||||
### it.2 — guardedness checker + `Diverge`
|
||||
|
||||
- **Structural-guardedness analysis (`crates/ailang-check`).** A new
|
||||
pass over each self- or mutually-recursive `FnDef` / `LetRec`
|
||||
clause. No annotation — the structural argument position is found
|
||||
by analysis (see Design decision **D1** for why implicit, not an
|
||||
explicit `{struct}` marker). For each recursive call, the argument
|
||||
in the candidate structural position must be a *proper constructor
|
||||
sub-component* of the function's value at that position, established
|
||||
by `match`-pattern destructuring of that parameter. Accumulator
|
||||
arguments (any non-structural position) are unconstrained.
|
||||
Mutual recursion uses the conservative same-ADT-family rule (D1).
|
||||
Failure → `CheckError::NonStructuralRecursion` naming the
|
||||
unguarded call and directing the author to `(loop …)` / `recur`.
|
||||
**Transitional grandfather (it.2-only):** a recursive call that is
|
||||
not structurally guarded but *is* marked `tail: true` is exempt
|
||||
from the rejection. During the it.2→it.3 window a marked tail call
|
||||
is precisely the author's explicit "this is intended iteration, not
|
||||
accidental unbounded recursion" assertion — its original Decision-8
|
||||
purpose — so grandfathering it keeps the it.1/it.2-additive vs
|
||||
it.3-destructive split honest: the 21 corpus fixtures still
|
||||
type-check through it.2 unchanged. it.3 removes the `tail` field
|
||||
**and** this exemption in the same destructive step, by which point
|
||||
every previously-exempt site has been migrated to `loop` or to a
|
||||
now-checked structural plain call.
|
||||
- **`Diverge` effect (first implementation; Decision 3 was a
|
||||
placeholder).** The `FnDef` effect-collection site (where raised
|
||||
effects are reconciled with the declared `Type::Fn.effects` row)
|
||||
gains: if the body syntactically contains a `Term::Loop`, OR calls
|
||||
a function whose declared effect set contains `"Diverge"`, then
|
||||
`"Diverge"` must be in the declared row, else
|
||||
`CheckError::UndeclaredEffect` (existing diagnostic, existing
|
||||
machinery — `Diverge` rides the same `Vec<String>` effect row as
|
||||
`IO`). Structural recursion contributes **no** effect. See **D2**.
|
||||
- **DESIGN.md.** Decision 3 amended: `Diverge` is no longer "wired up
|
||||
in the MVP only nominally" — it is the effect of `loop`-bearing
|
||||
code. §"Feature-acceptance criterion" already carries the canonical
|
||||
worked example (the iteration story) from the 2026-05-15 edit; this
|
||||
iteration makes the prose match the implementation.
|
||||
|
||||
### it.3 — retire `tail-app` / `tail-do`
|
||||
|
||||
- **Remove.** `Term::App.tail`, `Term::Do.tail`, `is_false`;
|
||||
`tail-app` / `tail-do` dispatch + `parse_tail_app` /
|
||||
`parse_tail_do` + the keyword-list entries + the `print.rs`
|
||||
`(tail-app …)`/`(tail-do …)` arms + the prose `"tail "` projection;
|
||||
`verify_tail_positions`'s tail-app role (the pass keeps only the
|
||||
`recur`-in-tail-position role from it.1); `CheckError::
|
||||
TailCallNotInTailPosition`; the `musttail` lowering in `emit_call`
|
||||
/ `emit_indirect_call` and the `tail call` hint in
|
||||
`lower_effect_op`. DESIGN.md Decision 8 rewritten as *superseded*
|
||||
(kept as a tombstone explaining why explicit tail calls were
|
||||
retired — the schema-drift anchors and EBNF/jsonc blocks updated in
|
||||
lockstep); the Decision-3 `Diverge` line and the EBNF
|
||||
`tail-app-term` production removed.
|
||||
- **Codegen block-termination rework.** The `block_terminated = true`
|
||||
seam, currently set by `tail: true` and consumed by
|
||||
`match_lower.rs:658–913` + `lib.rs:1238–1577`, becomes solely
|
||||
`recur`'s (and the ordinary fall-through `ret`). This is the only
|
||||
non-mechanical part of it.3 and the reason it.1 ships the new seam
|
||||
first.
|
||||
- **Corpus migration (21 fixtures / 34 sites).**
|
||||
Accumulator-shaped recursions
|
||||
(`bench_compute_collatz`, `bench_compute_intsum`,
|
||||
`bench_latency_explicit`/`_implicit`, `bench_list_sum*`,
|
||||
`rc_tail_sum_explicit_leak`, `mut_counter`, `mut_sum_floats`,
|
||||
`floats_1_newton_sqrt`, `forma_1_factorial`, …) → `(loop …)` /
|
||||
`recur`. Structurally-decreasing recursions (`list_map_poly`,
|
||||
`sort`, `std_list`, `floats_2_average_int_list`) → plain calls
|
||||
(now total-checked by it.2). Each migrated fixture must still `ail
|
||||
check` clean and `ail run` to byte-identical stdout (behavioural
|
||||
pin). Bench fixtures migrate too; the milestone-close audit
|
||||
re-ratifies `bench/baseline*` if loop-header codegen diverges from
|
||||
the retired `musttail` self-call (expected equivalent-or-better: a
|
||||
header block + phi is at least as good as a `musttail` self-call,
|
||||
and removes the call-frame entirely).
|
||||
|
||||
## Data flow
|
||||
|
||||
`.ail` source → `ailang_surface::parse` → JSON-AST (`Term::Loop` /
|
||||
`Term::Recur` are first-class canonical nodes, hashable, round-trip
|
||||
gated) → `ailang-check`:
|
||||
|
||||
1. typecheck (binders typed; `recur` unified with enclosing loop) →
|
||||
2. tail-position pass (`recur`-in-tail-position; from it.3 this is
|
||||
the pass's *only* job) →
|
||||
3. structural-guardedness pass (it.2) — rejects non-structural
|
||||
recursion-by-call →
|
||||
4. effect reconciliation (it.2) — `loop`-bearing or `Diverge`-calling
|
||||
⇒ `Diverge` in declared row.
|
||||
|
||||
→ desugar / lift / mono (walker arms thread `Term::Loop`/`Recur`
|
||||
unchanged) → `ailang-codegen` (`Term::Loop` = header block + phi;
|
||||
`Term::Recur` = back-edge `br` + block-terminate) → LLVM text →
|
||||
`clang -O2`.
|
||||
|
||||
The acyclic-call-graph invariant: after it.2, the only back-edge in
|
||||
generated IR comes from a `Term::Recur` to its lexically-paired
|
||||
`Term::Loop` header. Every other call is forward and (for recursive
|
||||
defs) structurally decreasing — i.e. statically known to bottom out.
|
||||
|
||||
## Error handling
|
||||
|
||||
New `CheckError` variants (bracket-`[code]:`-free Display body, per
|
||||
the 2026-05-15 F2 bugfix convention — the CLI formatter prepends the
|
||||
`[code]`; the Display string must not embed it):
|
||||
|
||||
- `NonStructuralRecursion` — "recursive call to `f` is not on a
|
||||
structurally-smaller argument; express this iteration as `(loop …)`
|
||||
/ `recur`". Carries the call site and the offending argument.
|
||||
- `RecurOutsideLoop` — a `recur` with no lexically-enclosing `loop`.
|
||||
- `RecurArityMismatch` — `recur` arg count ≠ enclosing loop binder
|
||||
count.
|
||||
- `RecurTypeMismatch` — `recur` arg type ≠ corresponding binder type.
|
||||
- `RecurNotInTailPosition` — `recur` not in tail position of the
|
||||
enclosing loop body. (Replaces the role of the retired
|
||||
`TailCallNotInTailPosition`.)
|
||||
|
||||
`UndeclaredEffect` (existing) is reused for the
|
||||
`Diverge`-not-declared case — no new variant; `Diverge` is just
|
||||
another effect-row string.
|
||||
|
||||
it.3 removes `TailCallNotInTailPosition` and its `code()`/`ctx()`
|
||||
arms; the schema-drift / diagnostic-doc lists update in lockstep.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
- **it.1:** serde round-trip unit tests for `Term::Loop`/`Recur`;
|
||||
`round_trip.rs` auto-picks new `examples/loop_*.ail`; check-side
|
||||
pins for `RecurOutsideLoop` / `RecurArityMismatch` /
|
||||
`RecurTypeMismatch` / `RecurNotInTailPosition` (negative fixtures,
|
||||
carve-out inventory extended); a positive nested-loop +
|
||||
loop-inside-lambda fixture (mirrors the mut.3 lambda-boundary
|
||||
concern — loop allocas/phi must scope to the closure's own header);
|
||||
e2e `examples/loop_counter.ail` runs and prints the expected value.
|
||||
- **it.2:** positive pins — structural list/tree/JSON walks check
|
||||
clean and stay `Diverge`-free; accumulator-over-structural (foldl
|
||||
shape) checks clean as structural (D1); negative pins —
|
||||
non-structural recursion-by-call fires `NonStructuralRecursion`;
|
||||
a `loop`-bearing fn without `!Diverge` in its row fires
|
||||
`UndeclaredEffect`; mutual same-family recursion passes, mutual
|
||||
cross-family fails. The mut-local e2e fixtures
|
||||
(`mut_counter`/`mut_sum_floats`) are *not* migrated yet in it.2 (
|
||||
they still use `tail-app`); they migrate in it.3.
|
||||
- **it.3:** every one of the 21 migrated fixtures keeps a
|
||||
before/after stdout-equality pin; `cargo test --workspace` green;
|
||||
`design_schema_drift.rs` green with `tail` anchors removed and
|
||||
`loop`/`recur` anchors present; milestone-close `audit` runs
|
||||
`bench/` (re-ratify baseline only if loop codegen measurably
|
||||
differs from the retired `musttail` path, with the regression
|
||||
ratified as a known accepted delta the way mut.4-tidy ratified the
|
||||
typecheck-surface tax).
|
||||
|
||||
## Design decisions & rejected alternatives
|
||||
|
||||
**D1 — Structural guardedness is inferred, not annotated; the
|
||||
accumulator-carrying walk is structural; mutual recursion uses the
|
||||
conservative same-family rule.**
|
||||
|
||||
- *Inferred, not annotated.* No `{struct n}`-style marker. Rationale
|
||||
(clause 1 + clause 2): an LLM author does not annotate the
|
||||
decreasing argument — there is no FP-corpus precedent for it
|
||||
outside Coq/Agda, which are not in the LLM-natural distribution; a
|
||||
required annotation would be exactly the redundancy the language
|
||||
exists to remove (clause 2), and the analysis is local and cheap
|
||||
(walk `match`-pattern bindings of one parameter). *Rejected:*
|
||||
explicit decreasing-argument annotation — rejected because it
|
||||
fails clause 1 (LLM would not write it unprompted) and adds
|
||||
redundancy (clause 2), not because it is more work.
|
||||
- *Accumulator-carrying structural walk = structural recursion
|
||||
(plain, pure, total).* Only the structural argument must decrease;
|
||||
accumulator positions are free. Forced by coherence with D2: a
|
||||
`foldl`/`sum`-with-accumulator over a list is the single most
|
||||
LLM-natural iteration shape in the entire FP corpus; classifying it
|
||||
as non-structural would push the whole functional-iteration corpus
|
||||
through `loop`/`recur` and `!Diverge` — self-defeating. The
|
||||
accumulator is not the recursion's well-founded measure; the
|
||||
structural argument is, and Decision 10's acyclicity bounds the
|
||||
depth regardless of accumulator growth. *This resolves the
|
||||
load-bearing open question (2) from the roadmap entry.*
|
||||
- *Mutual recursion = conservative same-ADT-family rule.* A
|
||||
mutually-recursive group is total iff there is a single ADT family
|
||||
F such that every member has a structural parameter of a type in F
|
||||
and every recursive call (self or cross-group) passes, at the
|
||||
callee's structural position, a proper sub-term of the caller's
|
||||
structural parameter. *Rejected for this milestone:* a general
|
||||
lexicographic / size-measure ordering — deferred, named in the
|
||||
spec as out of scope. The same-family rule covers tree/forest,
|
||||
even/odd-over-Nat, and the mutual JSON walk (the LLM-natural set);
|
||||
anything outside it must use `loop`/`recur`. This is a deliberate,
|
||||
recorded conservative scope cut, not an oversight. *This resolves
|
||||
the load-bearing open question (1) from the roadmap entry.*
|
||||
|
||||
**D2 — `loop`/`recur` carries the `Diverge` effect; structural
|
||||
recursion stays pure+total. (The genuine fork.)**
|
||||
|
||||
- *Chosen (Option B):* non-structural recursion-by-call is a hard
|
||||
compile error (`NonStructuralRecursion`); the only way to write an
|
||||
unbounded cyclic computation is `loop`/`recur`; and any `FnDef`
|
||||
whose body contains a `Term::Loop` (or calls a `Diverge` callee)
|
||||
must declare `Diverge` in its effect row. This is the first real
|
||||
implementation of the Decision-3 `Diverge` placeholder.
|
||||
- *Rationale, from the language:* local reasoning — "every
|
||||
definition carries its full type and effect set, so a signature
|
||||
can be trusted without reading the body" — is AILang's
|
||||
load-bearing pillar after machine-readability. "Can this function
|
||||
fail to terminate?" is precisely a body-fact the effect row
|
||||
exists to lift to the signature. `!IO` already does this for
|
||||
observable effects; `!Diverge` for non-termination is the same
|
||||
move, and `loop` is the first construct that gives a *free
|
||||
syntactic hook* (no termination prover needed — the check is
|
||||
"does the body contain a `Term::Loop`"). It also makes clause 3
|
||||
self-reinforcing: structural recursion stays pure and total, so
|
||||
an LLM author who wants a clean (`!IO`-free, `!Diverge`-free)
|
||||
signature is *structurally pulled* toward structural recursion
|
||||
and pays `!Diverge` only when genuinely writing an unbounded
|
||||
loop. That behavioral nudge is the milestone's reason to exist.
|
||||
- *Rejected (Option A):* `loop`/`recur` effect-free; `Diverge`
|
||||
deleted from DESIGN.md entirely; non-termination simply localized
|
||||
to the `loop` keyword with no signature consequence. Rejected
|
||||
because it discards local reasoning about termination at exactly
|
||||
the moment `loop` makes it free to provide — a caller could no
|
||||
longer tell from a signature whether a callee may spin, violating
|
||||
the local-reasoning pillar. Effort is not the reason; the
|
||||
local-reasoning contract is.
|
||||
- *Conservativeness note:* every `loop`-bearing fn gets `!Diverge`
|
||||
even if its `recur` happens to be structurally bounded. This is a
|
||||
sound over-approximation and intentional: proving a general
|
||||
`loop` terminates is the totality analysis we deliberately do not
|
||||
build. The author who wants the pure+total guarantee writes
|
||||
structural recursion; the author who reaches for `loop` is
|
||||
telling the compiler "termination is mine to argue", and the
|
||||
signature says so.
|
||||
- *Transitional note:* the "hard compile error" lands in it.2 with a
|
||||
single, deliberately temporary exemption — a still-`tail:
|
||||
true`-marked recursive call is grandfathered until it.3 removes the
|
||||
`tail` field and the exemption together. See it.2 Components
|
||||
("Transitional grandfather"). This is what lets it.1/it.2 stay
|
||||
additive and confines all corpus breakage to the one destructive
|
||||
iteration (it.3).
|
||||
|
||||
**D3 — `loop` is Clojure-shaped (named binders + positional
|
||||
`recur`), `recur` is tail-position-only and lexically scoped.**
|
||||
`recur` re-enters the lexically-enclosing `loop` only (never an
|
||||
implicit fn head — Clojure permits the implicit form; AILang does
|
||||
not, for the same no-outward-inference reason that originally
|
||||
motivated explicit `tail-app`: the jump target must be syntactically
|
||||
present, not inferred from call position). Tail-position-only keeps
|
||||
the back-edge the *last* thing a loop iteration does, which is what
|
||||
makes the phi-node codegen well-defined and the construct a true
|
||||
constant-stack loop.
|
||||
|
||||
**D4 — One milestone, three ordered iterations; the order is forced
|
||||
by the codegen block-termination seam, not by convenience.** See
|
||||
Architecture. Recording it here so a future reader does not
|
||||
"optimise" the order and break the seam handover.
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
- it.1: `examples/loop_counter.ail` builds and runs to the expected
|
||||
value; `loop`/`recur` round-trips (parse→print→parse idempotent,
|
||||
JSON-AST hashable); all five new `Recur*` diagnostics fire on
|
||||
their negative fixtures; `tail-app` still works unchanged;
|
||||
`cargo test --workspace` green.
|
||||
- it.2: a structural list/tree/JSON walk and a foldl-shaped
|
||||
accumulator walk both check clean with **no** `Diverge` in their
|
||||
effect row; a non-structural recursion-by-call fires
|
||||
`NonStructuralRecursion`; a `loop`-bearing fn missing `!Diverge`
|
||||
fires `UndeclaredEffect`; mutual same-family recursion passes,
|
||||
cross-family fails; DESIGN.md Decision 3 + §Feature-acceptance
|
||||
prose match the implementation; `cargo test --workspace` green.
|
||||
- it.3: `Term::App.tail` / `Term::Do.tail` / both keywords /
|
||||
`musttail` lowering / `verify_tail_positions`' tail-app role /
|
||||
`TailCallNotInTailPosition` / Decision 8 all removed;
|
||||
`design_schema_drift.rs` green with `loop`/`recur` anchors and no
|
||||
`tail` anchors; all 21 migrated fixtures `ail check` clean and
|
||||
`ail run` to byte-identical pre-migration stdout; milestone-close
|
||||
`audit` clean (bench baseline pristine or regression ratified);
|
||||
`cargo test --workspace` green.
|
||||
- Milestone: the language has exactly two iteration forms; the only
|
||||
back-edge in any generated program is an explicit, named, typed,
|
||||
`!Diverge`-surfaced `loop`; F1 and F4 are discharged; the feature
|
||||
passes all three feature-acceptance clauses (recorded above and in
|
||||
DESIGN.md §"Feature-acceptance criterion").
|
||||
Reference in New Issue
Block a user