fieldtest: loop-recur — 10 examples, 6 findings (milestone CLOSE, clean on all axes)
Post-audit downstream-LLM-author field test of the shipped loop/recur surface (DESIGN.md + public examples only). 3 real iterative programs (Newton isqrt, Collatz, Euclidean gcd) + 5 plausible-mistake negatives + 2 no-termination probes, all run through the public ail CLI. 0 bugs. 4 working findings on the milestone's own axes: rejection diagnostics point-exact AND self-fixing; recur tail-position threads through match/let/outer-if (spec only showed if); loop composes as a value sub-expression + byte-stable round-trip; no-termination boundary exact. This empirically substantiates the "LLM author can now write iterative programs" claim. Two orthogonal non-blocking findings, neither in loop/recur scope, both routed to P2 todos (refused the scope creep into a loop/recur tidy): niladic (app f) spec_gap independently re-confirms the existing mut-local-F3 roadmap item (the design-fork decision deliberately NOT auto-ratified under /boss — parked, priority-strengthened); module-level (doc) diagnostic-hint friction (one-line tidy). Boss-verified independently (gcd->27; recur-outside-loop fires exact). The standalone loop/recur milestone is fully ratified and CLOSED: 3 iterations + tidy shipped, audit clean (drift resolved, bench pristine carry-on), fieldtest clean on every axis. Roadmap P0 marked closed.
This commit is contained in:
@@ -85,3 +85,4 @@
|
||||
- 2026-05-17 — iter loop-recur.2: standalone-`loop`/`recur` milestone (2 of 3) — Component 4 typecheck semantics. The iter-1 `synth` `CheckError::Internal` stub for `Term::Loop`/`Term::Recur` is replaced with real binder typing (each init synthed in outer scope + already-declared binder names of THIS loop via ordinary `locals` save/restore mirroring `Term::Let` verbatim; loop's static type = body type) + positional `recur` arity/per-arg-type checking via a new `loop_stack: &mut Vec<Vec<Type>>` frame threaded exactly as mut.2's `mut_scope_stack` (every recursive + cross-module + test synth caller, compile-swept). New private `verify_loop_body(t,in_loop_tail)` pass — a SIBLING of the byte-frozen `verify_tail_positions` (0 deletions, tail-app role untouched), invoked in `check_fn` after it so synth-raised codes take precedence by pass ordering. Four `Recur*` `CheckError` variants (`RecurOutsideLoop`, `RecurArityMismatch{expected,got}`, `RecurTypeMismatch{position,expected,got}`, `RecurNotInTailPosition`) + `code()` + 2 `ctx()` arms, bracket-`[code]`-free Display (F2); four negative `.ail.json` fixtures fire their codes point-exactly (`assert_eq!`, non-vacuous) via a new `loop_recur_typecheck_pin.rs` (7 tests) + a ct1 F2 human-mode sibling; `carve_out_inventory` 13→17 with the pre-existing mut.4-tidy "Twelve"-vs-13 stale-header drift corrected in passing. iter-1's `loop_sum_to.ail` round-trip fixture now ALSO typechecks clean (one fixture, two properties — no near-duplicate); `loop_forever.ail` (loop whose only path is `recur`) typechecks clean, asserting the spec "no termination claim is made or enforced". Three binding Boss design calls (mirrored into the journal): (1) `RecurTypeMismatch` is an Assign-style `subst.apply`-both-then-structural-`!=` pre-check, NOT a `unify`-propagate (a propagate would surface generic `type-mismatch` and fail the point-exact-code acceptance); (2) `loop_stack` element type is positional `Vec<Type>` NOT name-keyed `IndexMap` (recur rebinds by position; binder names live in `locals`); (3) diagnostic-code precedence is by pass ordering (synth before verify_loop_body), no explicit logic. NO codegen (iter-1 `lower_term` `CodegenError::Internal` stub stays — iter 3); NO `Diverge`/`verify_structural_recursion`/guardedness (spec deliberate boundary). Two DONE_WITH_CONCERNS, both Task 2, both journalled: (a) a plan-ordering defect — Task 2's `cargo build` 0-errors gate is unsatisfiable while `check_fn` (deferred by the plan to Task 4) is an unthreaded caller; orchestrator pulled the byte-identical declaration+threading forward to Task 2, left only the `verify_loop_body` invocation in Task 4 (no semantic change, only sequencing); (b) recon-undercount of cross-module synth callers (`builtins.rs`×2, `lift.rs:746`, `mono.rs:720`/`:1361`), the recurring mut.2-class, resolved via the plan's own designated compile-sweep oracle. Boss systemic fix folded into this commit: planner SKILL.md Step-5 self-review gains item 7 (compile-gate vs. deferred-caller ordering) so the Concern-(a) class is scrubbed at plan time, not discovered at execution. `cargo test --workspace` 608→616 / 0 red (Boss-reran independently); `verify_tail_positions`/tail-app byte-frozen confirmed by diff-hunk inspection. Component 5 (codegen loop-header/phi/back-edge) + the positive RUN-to-value / deep-`n` E2E = iteration 3 → 2026-05-17-iter-loop-recur.2.md
|
||||
- 2026-05-17 — iter loop-recur.3: standalone-`loop`/`recur` milestone (3 of 3, TERMINAL) — Component 5 codegen + run-to-value E2E. The iter-1 `lower_term` `CodegenError::Internal` stub for `Term::Loop`/`Term::Recur` is replaced with real LLVM-IR lowering: loop binders are loop-carried values lowered as entry-block allocas (the mut.3 `pending_entry_allocas` mechanism) registered in the EXISTING `mut_var_allocas` map so the EXISTING `Term::Var` load path resolves them with zero new Var code (representation-sharing only — Var-lowering byte-unchanged); a fresh `loop.header.<id>` block reached by an unconditional `br` from the pre-header; `recur` lowers ALL args to SSA BEFORE any store (simultaneous positional rebind), stores into the binder allocas, back-edges `br` to the header, and sets the SINGLE existing `block_terminated` field at its OWN new emit site (a parallel SET call-site) so the loop's exit value is the emergent product of the existing `if`/`match` join — no separate loop-result phi/exit-block. A new `loop_frames` codegen stack lets `recur` find its target header+slots; saved/reset/restored at the single lambda-lowering boundary exactly as mut.3's `mut_var_allocas` triple. `clang -O2` mem2reg promotes the binder allocas to the phi nodes the spec's secondary implementation-shape describes. Four binding Boss design calls (mirrored into the journal), all on architectural-consistency / spec-pinned-invariant grounds (NOT effort): (1) alloca+mem2reg NOT hand-emitted phi (the linear-emit architecture has no phi-with-body-discovered-back-edge-predecessor precedent; the `if` arm sidesteps by opening its join last — a loop header cannot be opened last; mem2reg yields identical optimized output; spec's "phi" is the explicitly-secondary impl-shape the spec subordinates to the planner's exact-bytes authority); (2) reuse `mut_var_allocas` + the existing `Term::Var` load path (byte-unchanged; representation-sharing, the iter-2 AST/typecheck binder distinction is post-typecheck-irrelevant to codegen); (3) emergent loop-exit via the existing if/match join once recur terminates its block, no separate result phi; (4) reuse the single `block_terminated` field, recur sets it at its own emit site, ZERO edits to any existing SET/READ site (a second field would force editing every READ site — the opposite of the spec-pinned "tail-app's use byte-unchanged"). Diff confirmed surgical by hunk-header inspection: codegen/lib.rs = exactly 3 hunks (field + init + the stub→2-arms replacement), codegen/lambda.rs = exactly 2 hunks (save + restore); NO hunk at any existing `block_terminated` SET/READ site, at tail-app/tail-do lowering, or at `verify_tail_positions`. Three new `.ail` fixtures: `loop_sum_to_run.ail`→`55` (run-to-value), `loop_sum_to_deep.ail`→`500000500000` (1e6 iterations via the back-edge, no stack growth — the spec clause-2 correctness claim made executable), `loop_forever_build.ail` (infinite loop, no non-recur exit, `ail build` exit 0 — "typechecks AND compiles, no termination claim"; never executed). Codegen-ONLY iteration: no schema/AST/serde/typecheck change; hash pins (`loop_recur` + iter13a) + drift trio + `carve_out_inventory` confirmed green UNTOUCHED (not modified); the 3 new `.ail` fixtures are round-trip-auto-covered, NOT carve-outs. One DONE_WITH_CONCERNS (T3): the plan's literal `cargo test --workspace tail` filter resolves to ZERO tests (real guards are `*_tail_position_*`/`*musttail*`); orchestrator ran the gate via real names + the authoritative full-suite 619/0 which subsumes it — recurring `feedback_plan_pseudo_vs_reality` class, no behaviour change. Boss systemic fix folded into this commit: planner SKILL.md Step-5 gains item 8 (verification-command filter strings must resolve to ≥1 named test, or use the unfiltered suite + a count assertion) — the SECOND planner-meta-gap this milestone surfaced (iter-2 added item 7). `cargo test --workspace` 616→619 / 0 red (Boss-reran independently); the 3 loop/recur e2e explicitly green (55 / 500000500000 / infinite-compiles). **All three components shipped — the loop/recur milestone is structurally complete; milestone-close (mandatory `audit`, then `fieldtest` since loop/recur is user-visible Form-A surface) is the Boss's next pipeline step.** → 2026-05-17-iter-loop-recur.3.md
|
||||
- 2026-05-18 — iter loop-recur.tidy: milestone-close audit resolution (RED `39380d3` + this GREEN). Architect drift review found a `[high]` correctness defect: a `(lam ...)` body capturing an enclosing `Term::Loop` binder passed `ail check` (exit 0) then panicked `unreachable!()` at `crates/ailang-codegen/src/lambda.rs:102` on type-correct input — a DESIGN.md "Robustness against hallucinations" violation. Root cause (debugger-confirmed RED-first): the `Term::Lam` escape guard at `crates/ailang-check/src/lib.rs:3608` iterated only `mut_scope_stack`; loop binders live in the ordinary `locals` (iter-2 design) and never entered any escape-checked scope, so the mut.4-tidy `MutVarCapturedByLambda`-class rejection had no loop-binder counterpart. Fix (GREEN, implement mini-mode): new `CheckError::LoopBinderCapturedByLambda { name }` (bracket-`[code]`-free F2 Display) + `code()` `loop-binder-captured-by-lambda` + `ctx() {name}`, symmetric to `MutVarCapturedByLambda`; the `Term::Lam` escape guard gained a parallel pass over `loop_stack` (gate widened to `!mut_scope_stack.is_empty() || !loop_stack.is_empty()`). Minimal-mechanism design call: `loop_stack`'s frame element extended `Vec<Type>` → `Vec<(String, Type)>` so the already-threaded per-loop scope frame also carries binder names (`Term::Recur` still reads `.1` BY POSITION — Boss-call-2's positional-recur invariant preserved verbatim, the name is a second field consumed only by the escape guard, a consumer iter-2 did not anticipate; the parallel-stack alternative would touch all 35 `synth` call sites, strictly larger). Codegen byte-unchanged (typecheck-only fix; the lambda.rs:102 `unreachable!()` is now genuinely unreachable, kept as a defensive assertion). Two mut.4-tidy-mirrored in-source unit tests; lockstep `carve_out_inventory` 17→18 + `ct1_check_cli` mut-F2 sibling `cases`; DESIGN.md one-line symmetric-rule note. Boss folded into this GREEN commit: the two `[medium]` doc-honesty edits the audit also surfaced (`mut_var_allocas` rustdoc now states its mut-var+loop-binder dual use truthfully; `Term::Loop` doc-comment now describes the real shipped iter-2/3 typecheck+alloca+mem2reg state, not iter-1's stale "per-binder phi" stub forward-look) + a `[low]` P2 roadmap `[todo]` (the recon-undercount 3×-pattern → an `ailang-plan-recon` agent-definition countermeasure; pairs with planner Step-5 items 7+8). Bench gate (audit Step 2): `check.py`/`compile_check.py`/`cross_lang.py` all exit 0, 25 metrics 0 regressed — **pristine** (strictly-additive surface, no hot-path; the pre-existing P2 `*.bump_s` hardware-staleness drift did not trip) → carry-on, no baseline/ratify. `cargo test --workspace` 619→622 / 0 red (Boss-reran independently incl. hash_pin 11/0 — the ast.rs/codegen doc-comment edits moved no canonical-JSON hash). **The loop/recur milestone is audit-clean** — architect drift cleared, bench pristine; the only remaining pipeline step before full close is `fieldtest` (loop/recur is user-visible Form-A surface) → 2026-05-17-iter-loop-recur.tidy.md
|
||||
- 2026-05-18 — fieldtest loop-recur (milestone CLOSE, clean on all milestone axes): post-audit downstream-LLM-author field test of the shipped loop/recur surface. The fieldtester (DESIGN.md + public examples only, never compiler source) wrote 3 real iterative programs — integer Newton sqrt (multi-binder, recur buried in if/let/if, loop result into let/seq), Collatz length (recur in match-arm tails), Euclidean gcd (loop as a value sub-expression in argument position) — plus 5 plausible-mistake negatives and 2 no-termination probes, all run through the public `ail` CLI. **0 bugs; 4 working findings, all on the milestone's own axes**: the five rejection diagnostics (recur-outside-loop / -arity / -type / -not-in-tail / loop-binder-captured-by-lambda) are point-exact AND self-fixing (name the fn, describe the fix, no false positives, no crash — the clause-2 silent-failure-class-becomes-compile-error claim made real); recur tail-position threads correctly through match-arm/let/outer-if (the spec only demonstrated `if` — generalises exactly as an author assumes); loop composes as a value sub-expression everywhere + every loop/recur fixture is `ail parse|render|parse` byte-identical (Roundtrip Invariant holds in practice); the no-termination boundary is exactly as specified (infinite loop check+build clean, zero spurious diagnostics — the precise difference from the reverted Iteration-discipline milestone). This empirically substantiates the milestone's "an LLM author can now write iterative programs with loop/recur" claim — the gate fieldtest exists to provide. Two ORTHOGONAL non-blocking findings surfaced incidentally while probing the no-termination/negative axes, neither in loop/recur scope, both routed to P2 todos (not a loop/recur tidy — refusing the scope creep): (spec_gap) niladic `(app f)` is unrepresentable in Form A and DESIGN.md's `Term::App args:[Term...]` states no minimum — INDEPENDENTLY re-confirms the existing mut-local-F3 roadmap todo (two fieldtests now hit it; the accept-`(app f)`-vs-ratify-DESIGN.md decision is a genuine design fork deliberately NOT auto-ratified under autonomous /boss — parked, priority-strengthened); (friction) the module-level `(doc …)` rejection lists valid def heads but omits that doc attaches inside fn/data — a one-line diagnostic-hint tidy. Independent Boss verification: `loop_recur_4_gcd_value_pos.ail` re-run → stdout `27`; `loop_recur_3a` re-run → `ail check` exit 1 `[recur-outside-loop] countdown: …`. **The standalone loop/recur milestone is fully ratified and CLOSED**: 3 iterations + a tidy shipped, audit clean (architect drift resolved, bench pristine carry-on), fieldtest clean on every milestone axis. Fixtures `examples/fieldtest/loop_recur_*.ail` + spec `docs/specs/2026-05-18-fieldtest-loop-recur.md` committed; roadmap P0 entry marked closed; the two orthogonal findings tracked as P2 todos → 2026-05-18-fieldtest-loop-recur.md
|
||||
|
||||
+39
-18
@@ -35,20 +35,22 @@ work progresses.
|
||||
|
||||
## P0 — In flight
|
||||
|
||||
- [~] **\[milestone\]** Standalone `loop` / `recur` — strictly-additive
|
||||
iteration surface, `recur` valid only in tail position. All three
|
||||
iterations + a tidy shipped: iter 1 `a179ec3` (additive AST nodes),
|
||||
- [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),
|
||||
iter 2 `1566ce0` (typecheck), iter 3 `edd2558` (codegen + run-to-value
|
||||
E2E), tidy (lambda-captures-loop-binder rejected at check, symmetric
|
||||
to mut.4-tidy). Milestone-close `audit` clean: architect drift
|
||||
resolved (the `[high]` codegen crash fixed in the tidy + two
|
||||
`[medium]` doc-honesty edits folded in), bench pristine (25 metrics,
|
||||
0 regressed — strictly-additive surface, no hot-path touched).
|
||||
**Remaining: `fieldtest`** (loop/recur is user-visible Form-A
|
||||
surface) — the only step before full close.
|
||||
- context: `docs/specs/2026-05-17-loop-recur.md`; principles entry
|
||||
`docs/specs/2026-05-17-llm-surface-discipline.md` §6.2; revert
|
||||
rationale `docs/specs/2026-05-16-iteration-discipline-revert.md`.
|
||||
E2E), tidy `39380d3`/`2ee9794` (lambda-captures-loop-binder rejected
|
||||
at check). Milestone-close `audit` clean (architect drift resolved,
|
||||
bench pristine 25/0 carry-on); `fieldtest` 2026-05-18 clean on all
|
||||
four milestone axes (0 bugs; diagnostics point-exact+self-fixing,
|
||||
recur-tail through match/let, loop-as-value-subexpr byte-stable,
|
||||
no-termination exact). Two orthogonal non-blocking findings routed
|
||||
to P2 todos (niladic `(app f)` — re-confirms mut-local F3; module
|
||||
`(doc)` diagnostic hint). Stays here briefly for context; remove
|
||||
once stale (full record in `docs/journals/INDEX.md`).
|
||||
- context: `docs/specs/2026-05-17-loop-recur.md`;
|
||||
`docs/specs/2026-05-18-fieldtest-loop-recur.md`; principles entry
|
||||
`docs/specs/2026-05-17-llm-surface-discipline.md` §6.2.
|
||||
|
||||
## P1 — Next
|
||||
|
||||
@@ -294,11 +296,30 @@ work progresses.
|
||||
- [ ] **\[todo\]** Zero-arg `(app f)` rejected at parse — the Form-A
|
||||
parser refuses an application with an empty argument list, so a
|
||||
nullary call has no surface form. Surfaced by the mut-local
|
||||
fieldtest (F3). Decide: accept `(app f)` as the nullary-call
|
||||
surface, or ratify in DESIGN.md that nullary functions are
|
||||
expressed differently (and say how). Not a blocker; no current
|
||||
corpus program needs it, but an LLM author reaches for it.
|
||||
- context: `docs/specs/2026-05-15-fieldtest-mut-local.md` finding F3.
|
||||
fieldtest (F3) AND **independently re-confirmed by the loop/recur
|
||||
fieldtest** (2026-05-18, finding spec_gap): the maximally-natural
|
||||
infinite-event-loop shape is a niladic `run_forever : fn() -> Int`
|
||||
called `(app run_forever)`, which dies at parse before reaching
|
||||
loop/recur semantics. Two independent fieldtests hitting the same
|
||||
gap raises the priority signal. Decide: accept `(app f)` as the
|
||||
nullary-call surface, or ratify in DESIGN.md that nullary functions
|
||||
are expressed differently (and say how). DESIGN.md's `Term::App`
|
||||
`args:[Term...]` states no minimum, so the surface "expected at
|
||||
least one argument" rule is unbacked by spec — a genuine design
|
||||
fork, deliberately NOT auto-ratified under autonomous orchestration.
|
||||
Not a blocker; no current corpus program needs it, but an LLM
|
||||
author reaches for it.
|
||||
- context: `docs/specs/2026-05-15-fieldtest-mut-local.md` finding F3;
|
||||
`docs/specs/2026-05-18-fieldtest-loop-recur.md` spec_gap.
|
||||
- [ ] **\[todo\]** Module-level `(doc …)` diagnostic omits where `doc`
|
||||
belongs — a `(module NAME (doc "…") (fn …))` is correctly rejected
|
||||
(`unknown def head \`doc\``) but the message lists valid def heads
|
||||
without saying doc strings attach *inside* `fn`/`data` defs; an
|
||||
author can read it and conclude doc strings are unsupported. One-line
|
||||
tidy: append a hint like "(doc strings attach inside `fn`/`data`
|
||||
defs, not at module level)". Low cost; verbose-diagnostic-philosophy
|
||||
gap, not a bug.
|
||||
- context: `docs/specs/2026-05-18-fieldtest-loop-recur.md` friction.
|
||||
- [ ] **\[todo\]** Workspace search beyond entry-module's directory —
|
||||
`load_workspace` only finds sibling `.ail.json` files in the same
|
||||
directory as the entry module, so any consumer of prelude/std in a
|
||||
|
||||
@@ -0,0 +1,233 @@
|
||||
# Fieldtest — loop-recur — 2026-05-18
|
||||
|
||||
**Status:** Draft — awaiting orchestrator triage
|
||||
**Author:** ailang-fieldtester (dispatched by skills/fieldtest)
|
||||
|
||||
## Scope
|
||||
|
||||
The `loop-recur` milestone shipped a standalone strict-iteration
|
||||
surface: the Form-A `(loop (NAME TYPE INIT)* BODY)` block and
|
||||
`(recur ARG*)` re-entry. `loop` is an expression whose value is the
|
||||
body's value on the iteration that exits via a non-`recur` branch;
|
||||
`recur` re-enters the lexically-innermost enclosing `loop`, rebinding
|
||||
its binders positionally. The single closed rule is that `recur` must
|
||||
be in tail position of its enclosing loop body. No totality is
|
||||
claimed — an infinite loop is legal and compiles. Four rejection
|
||||
diagnostics (`recur-outside-loop`, `recur-arity-mismatch`,
|
||||
`recur-type-mismatch`, `recur-not-in-tail-position`) plus the
|
||||
symmetric `loop-binder-captured-by-lambda` enforce the contract. The
|
||||
surface is fully shipped (parse + typecheck + native codegen + run +
|
||||
Roundtrip Invariant).
|
||||
|
||||
## Examples
|
||||
|
||||
### `examples/fieldtest/loop_recur_1_isqrt_newton.ail` — integer sqrt via Newton's method
|
||||
- Computes `floor(sqrt(152399025))` = 12345, then prints `r` and
|
||||
`r - 12345`. Two binders (`x` current guess, `prev` previous
|
||||
guess); the `recur` is buried two levels deep: inside an `if`,
|
||||
inside a `let next ...`, inside another `if`. The whole `(loop …)`
|
||||
is itself wrapped in an outer `if (< n 2)` guard, and its result
|
||||
feeds a `let r … (seq (print r) (print (- r 12345)))`.
|
||||
- Fits scope: axis 1 (multi-binder, non-trivial body, `recur` in a
|
||||
branch tail not at body toplevel) **and** axis 4 (`loop` result
|
||||
consumed by an enclosing `let`/`seq`, not as a whole fn body).
|
||||
- Outcome: `ail check` ok, `ail build` ok, runs, stdout `12345\n0` —
|
||||
matches expected on first try.
|
||||
|
||||
### `examples/fieldtest/loop_recur_2_collatz.ail` — Collatz step counter
|
||||
- `collatz_len(27)=111`, `collatz_len(97)=118`, `collatz_len(1)=0`.
|
||||
Two binders (`n` current value, `steps` accumulator). Parity
|
||||
dispatch is a `match (% n 2)` with `pat-lit 0` / `_` arms; the
|
||||
`recur` lives in the **tail of each `match` arm**, and the `match`
|
||||
is itself the tail of an `if (== n 1)`.
|
||||
- Fits scope: axis 1 — exercises `recur` tail-position through a
|
||||
`match` (the spec only spells out `if`; this confirms `match`-arm
|
||||
tails are handled identically).
|
||||
- Outcome: `ail check` ok, `ail build` ok, runs, stdout
|
||||
`111\n118\n0` — matches expected on first try.
|
||||
|
||||
### `examples/fieldtest/loop_recur_4_gcd_value_pos.ail` — Euclidean gcd as a value sub-expression
|
||||
- `gcd(48,18)=6`, `gcd(1071,462)=21`; prints their sum `27`. Two
|
||||
binders (`a`, `b`); `recur` in the tail of the else branch. The
|
||||
two `(loop …)`-bearing `gcd` calls are nested inside
|
||||
`(app print (app + (app gcd …) (app gcd …)))` — `loop` results
|
||||
flow as function arguments.
|
||||
- Fits scope: axis 4 — `loop` as a value sub-expression in
|
||||
argument position, two independent loop instantiations composed
|
||||
arithmetically.
|
||||
- Outcome: `ail check` ok, `ail build` ok, runs, stdout `27` —
|
||||
matches expected on first try.
|
||||
|
||||
### `examples/fieldtest/loop_recur_3a..3e` — the five rejection diagnostics
|
||||
Each is the *plausible wrong program an LLM author would actually
|
||||
write*, not a contrived minimal repro:
|
||||
- `3a_recur_outside_loop` — a self-recursive `countdown` helper that
|
||||
reaches for `recur` as a generic self-tail-call with no enclosing
|
||||
`loop`. → `[recur-outside-loop] countdown: …`
|
||||
- `3b_recur_arity` — a two-binder `(acc, i)` loop where the author
|
||||
writes `(recur (+ acc i))` and forgets to advance `i`. →
|
||||
`[recur-arity-mismatch] sum_to: passes 1 argument(s) but … 2
|
||||
binder(s)`
|
||||
- `3c_recur_type` — the author passes the `Bool` comparison result
|
||||
into the first `Int` binder slot. → `[recur-type-mismatch]
|
||||
count_down: argument 0 has type \`Bool\` but … is \`Int\``
|
||||
- `3d_recur_not_tail` — factorial written as `n * recur(n-1)`,
|
||||
treating `recur` as value-returning. → `[recur-not-in-tail-
|
||||
position] factorial: it is a back-jump, not a value-producing
|
||||
sub-expression`
|
||||
- `3e_binder_captured` — inside the loop body the author builds a
|
||||
`\d. acc + d` adder closing over loop binder `acc` and applies it.
|
||||
→ `[loop-binder-captured-by-lambda] sum_to: … Either move the
|
||||
lambda outside the loop, or restructure to pass \`acc\` as a lambda
|
||||
parameter …`
|
||||
- Fits scope: axes 2 and 3. Outcome: all five `ail check` exit 1
|
||||
with **exactly** the promised code; the function is named and the
|
||||
fix is described in the message text.
|
||||
|
||||
### `examples/fieldtest/loop_recur_5b_event_loop_noterm.ail` — non-terminating event loop (loop-axis-covering)
|
||||
- A two-binder tick/parity event loop with **no non-`recur` branch**.
|
||||
`ail check` ok, `ail build` ok. **Not executed** (infinite by
|
||||
design).
|
||||
- Fits scope: axis 5 — the no-termination boundary. Confirms an
|
||||
infinite `loop` typechecks and compiles cleanly with zero
|
||||
diagnostics, exactly as the spec promises.
|
||||
|
||||
### `examples/fieldtest/loop_recur_5_event_loop_noterm.ail` — friction artefact (kept, not worked around)
|
||||
- Same algorithm written the maximally-natural way for an infinite
|
||||
loop: a **niladic** `run_forever : fn() -> Int`, invoked as
|
||||
`(app run_forever)`. This is the LLM-natural shape — an event
|
||||
loop has no seed to thread — but it never reaches loop/recur
|
||||
semantics: it fails at parse with `surface-parse-error: parse
|
||||
error in app-term: expected at least one argument`. Retained
|
||||
verbatim as the finding artefact; `5b` is the variant that adds
|
||||
an honest `start` parameter so the no-termination *loop* axis is
|
||||
still genuinely exercised.
|
||||
|
||||
## Findings
|
||||
|
||||
### [working] All five rejection diagnostics are point-exact and self-fixing
|
||||
- Examples: `loop_recur_3a` … `loop_recur_3e`.
|
||||
- What happened: each plausible-mistake program produced exactly the
|
||||
promised code with no false positives and no crash. The wording
|
||||
goes beyond naming the rule — `3b` says "recur must rebind every
|
||||
binder positionally", `3d` says "it is a back-jump, not a
|
||||
value-producing sub-expression", `3e` spells out two concrete
|
||||
remediations. Every message names the enclosing function.
|
||||
- Why working: this is the milestone's clause-2 correctness claim
|
||||
(an entire silent-failure class becomes a compile error) made
|
||||
real. An author who makes the natural mistake is told what is
|
||||
wrong, where, and how to fix it, without reading DESIGN.md.
|
||||
- Recommended downstream action: carry-on. These diagnostics are a
|
||||
feature-defining strength; protect them against future
|
||||
rewording drift (a snapshot test on the message bodies, if not
|
||||
already present, would be cheap insurance — but that is an
|
||||
internal call, not a fieldtest demand).
|
||||
|
||||
### [working] `recur` tail-position threads correctly through `match`, nested `let`, and outer `if`
|
||||
- Examples: `loop_recur_1_isqrt_newton` (recur inside `if`/`let`/`if`,
|
||||
loop inside an outer `if`), `loop_recur_2_collatz` (recur in
|
||||
`match`-arm tails).
|
||||
- What happened: DESIGN.md and the §"Concrete code shapes" only
|
||||
demonstrate `recur` in `if` branches. I reached for `match`-arm
|
||||
tails and a `let`-then-`if` nest unprompted (both are the natural
|
||||
shapes for parity dispatch and Newton's fixpoint test). All
|
||||
compiled and ran correctly on the first try. The tail-position
|
||||
analysis correctly treats a `match` arm body and a `let` body as
|
||||
tail when the enclosing form is tail.
|
||||
- Why working: confirms the closed rule generalises exactly as an
|
||||
author would assume from the `if` examples — no surprise, no
|
||||
special-casing needed in author-side mental model.
|
||||
- Recommended downstream action: carry-on.
|
||||
|
||||
### [working] `loop` composes as a value sub-expression and round-trips
|
||||
- Examples: `loop_recur_1` (loop result into `let`/`seq`),
|
||||
`loop_recur_4` (two loop results into `(+ … …)` into `print`).
|
||||
- What happened: `loop` used purely as an expression — fed to a
|
||||
binding, summed with another `loop`, passed as a call argument —
|
||||
worked with no ceremony. Separately, `ail parse | ail render |
|
||||
ail parse` is canonical-JSON byte-identical for every
|
||||
loop/recur-bearing fixture (1, 2, 4, 5b), so the spec's Roundtrip
|
||||
Invariant acceptance criterion holds in practice.
|
||||
- Why working: the spec's "loop is an expression" claim is not just
|
||||
true for the whole-fn-body case the reference corpus shows; it
|
||||
holds in arbitrary expression position.
|
||||
- Recommended downstream action: carry-on.
|
||||
|
||||
### [working] No-termination boundary is exactly as specified
|
||||
- Example: `loop_recur_5b_event_loop_noterm`.
|
||||
- What happened: an infinite `loop` (every branch a `recur`)
|
||||
`ail check`s and `ail build`s with zero diagnostics. No spurious
|
||||
"unreachable", no "loop never exits", no totality complaint.
|
||||
- Why working: this is the precise difference from the reverted
|
||||
Iteration-discipline milestone, and it behaves as the spec's
|
||||
deliberate-boundary section promises.
|
||||
- Recommended downstream action: carry-on.
|
||||
|
||||
### [spec_gap] A niladic application `(app f)` is unrepresentable in Form A; DESIGN.md does not constrain it
|
||||
- Example: `loop_recur_5_event_loop_noterm` (kept as the artefact).
|
||||
- What happened: the maximally-natural infinite-loop shape is a
|
||||
zero-argument `run_forever : fn() -> Int` called as
|
||||
`(app run_forever)`. The surface parser rejects this with
|
||||
`error: [surface-parse-error] parse error in app-term: expected
|
||||
at least one argument`. DESIGN.md's `Term::App` schema is
|
||||
`{ "t":"app", "fn":Term, "args":[Term...] }` — `[Term...]` does
|
||||
not state a minimum, and the entire public `examples/*.ail`
|
||||
corpus contains **no** AIL-level call of a niladic function
|
||||
(`main` is the only zero-arg fn and is never called from source;
|
||||
`loop_forever_build.ail` deliberately gave `spin` an `Int`
|
||||
parameter to sidestep exactly this). So two readings are equally
|
||||
plausible from the spec alone: (a) `args:[]` is legal AST that
|
||||
the surface should be able to express, or (b) niladic application
|
||||
is forbidden by design and DESIGN.md should say so. The compiler
|
||||
picked (b) at the surface layer; I could not tell which reading
|
||||
is intended without reading `crates/`.
|
||||
- Why spec_gap: DESIGN.md neither permits nor forbids the empty-args
|
||||
application; the surface diagnostic ("expected at least one
|
||||
argument") states a rule that appears nowhere in DESIGN.md, and a
|
||||
downstream author writing an event loop / `unit -> a` thunk hits
|
||||
it with no spec guidance. It is orthogonal to loop/recur but was
|
||||
surfaced *by* the loop/recur no-termination axis, because an
|
||||
infinite loop is the canonical case with no state worth a
|
||||
parameter.
|
||||
- Recommended downstream action: ratify a decision and tighten
|
||||
DESIGN.md — either (a) state that niladic applications are
|
||||
forbidden in Form A and document the `unit`-param convention as
|
||||
the workaround, or (b) extend the surface to accept `(app f)`
|
||||
for `fn() -> a`. Until then, an author cannot express a
|
||||
niladic-call thunk and the diagnostic gives no DESIGN-backed
|
||||
remedy.
|
||||
|
||||
### [friction] Module-level `(doc …)` is rejected with a diagnostic that omits the actual location of `doc`
|
||||
- Examples: surfaced on the first draft of `loop_recur_3a..3e`
|
||||
(corrected in the committed fixtures to a leading `;` comment).
|
||||
- What happened: I wrote a module-level
|
||||
`(module NAME (doc "…") (fn …))` — a natural reach, since `fn`
|
||||
and `data` both accept a `doc` child, so an author reasonably
|
||||
assumes the module node does too. The diagnostic is
|
||||
`error: [surface-parse-error] parse error in module: unknown def
|
||||
head \`doc\`; expected \`data\`, \`fn\`, \`const\`, \`class\`,
|
||||
\`instance\`, or \`import\``. It correctly rejects, but the
|
||||
message lists the valid def heads **without** mentioning that
|
||||
`doc` is valid *inside* `fn`/`data` — an author can read this
|
||||
message and still not know where the doc string should go, and
|
||||
may conclude doc strings are unsupported entirely.
|
||||
- Why friction: it compiles-or-rejects correctly (no bug), but the
|
||||
verbose-by-design AILang diagnostic philosophy is not met here:
|
||||
the message names what is expected but not the one thing the
|
||||
author needs (move `doc` inside the def). Orthogonal to
|
||||
loop/recur; surfaced while writing the negative fixtures.
|
||||
- Recommended downstream action: plan a one-line tidy — append to
|
||||
the message a hint such as "(doc strings attach inside `fn`/`data`
|
||||
defs, not at module level)". Low cost, removes a dead-end for the
|
||||
author.
|
||||
|
||||
## Recommendation summary
|
||||
|
||||
| Finding | Class | Action |
|
||||
|---|---|---|
|
||||
| Five rejection diagnostics point-exact & self-fixing | working | carry-on |
|
||||
| `recur` tail-position threads through `match`/`let`/outer-`if` | working | carry-on |
|
||||
| `loop` composes as a value sub-expression & round-trips | working | carry-on |
|
||||
| No-termination boundary exactly as specified | working | carry-on |
|
||||
| Niladic `(app f)` unrepresentable; DESIGN.md silent | spec_gap | ratify + tighten DESIGN.md |
|
||||
| Module-level `(doc …)` diagnostic omits where `doc` belongs | friction | plan (one-line tidy) |
|
||||
@@ -0,0 +1,23 @@
|
||||
(module loop_recur_1_isqrt_newton
|
||||
(fn main
|
||||
(doc "Integer square root of 152399025 (= 12345^2) via Newton's method, then a sanity-difference. Expected stdout: 12345 then 0.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(let r (app isqrt 152399025)
|
||||
(seq (app print r)
|
||||
(app print (app - r 12345))))))
|
||||
(fn isqrt
|
||||
(doc "Newton's method for floor(sqrt(n)). Two binders: x (current guess) and prev (previous guess, to detect the fixpoint/2-cycle). The recur is buried inside a nested if, not at body toplevel.")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body
|
||||
(if (app < n 2)
|
||||
n
|
||||
(loop (x (con Int) n) (prev (con Int) 0)
|
||||
(if (app == x prev)
|
||||
x
|
||||
(let next (app / (app + x (app / n x)) 2)
|
||||
(if (app == next x)
|
||||
next
|
||||
(recur next x)))))))))
|
||||
@@ -0,0 +1,20 @@
|
||||
(module loop_recur_2_collatz
|
||||
(fn main
|
||||
(doc "Collatz step counts. collatz_len(27)=111, collatz_len(97)=118, collatz_len(1)=0. Expected stdout (per line): 111, 118, 0.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(seq (app print (app collatz_len 27))
|
||||
(seq (app print (app collatz_len 97))
|
||||
(app print (app collatz_len 1))))))
|
||||
(fn collatz_len
|
||||
(doc "Number of Collatz steps to reach 1. Two binders: n (current value) and steps (accumulator). Parity dispatch is a `match` on n%2; the recur lives in the tail of each match arm, not at body toplevel.")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params start)
|
||||
(body
|
||||
(loop (n (con Int) start) (steps (con Int) 0)
|
||||
(if (app == n 1)
|
||||
steps
|
||||
(match (app % n 2)
|
||||
(case (pat-lit 0) (recur (app / n 2) (app + steps 1)))
|
||||
(case _ (recur (app + (app * 3 n) 1) (app + steps 1)))))))))
|
||||
@@ -0,0 +1,16 @@
|
||||
; NEGATIVE FIXTURE. The LLM-natural mistake: author writes a
|
||||
; self-recursive helper and reaches for `recur` as if it were a
|
||||
; generic self-tail-call, but there is no enclosing `loop`.
|
||||
; Expected: `ail check` exits 1 with code recur-outside-loop.
|
||||
(module loop_recur_3a_recur_outside_loop
|
||||
(fn countdown
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
0
|
||||
(recur (app - n 1)))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app countdown 5)))))
|
||||
@@ -0,0 +1,17 @@
|
||||
; NEGATIVE FIXTURE. The LLM-natural mistake: a two-binder loop
|
||||
; (acc, i) but the author writes `(recur (app + acc i))` forgetting
|
||||
; to also advance `i` — passes 1 arg for 2 binders.
|
||||
; Expected: `ail check` exits 1 with code recur-arity-mismatch.
|
||||
(module loop_recur_3b_recur_arity
|
||||
(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))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app sum_to 10)))))
|
||||
@@ -0,0 +1,17 @@
|
||||
; NEGATIVE FIXTURE. The LLM-natural mistake: the author intends to
|
||||
; recur with the updated Int accumulator but accidentally passes a
|
||||
; Bool (the comparison result) into the first binder position.
|
||||
; Expected: `ail check` exits 1 with code recur-type-mismatch.
|
||||
(module loop_recur_3c_recur_type
|
||||
(fn count_down
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params start)
|
||||
(body
|
||||
(loop (i (con Int) start)
|
||||
(if (app == i 0)
|
||||
i
|
||||
(recur (app > i 0))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app count_down 5)))))
|
||||
@@ -0,0 +1,18 @@
|
||||
; NEGATIVE FIXTURE. The LLM-natural mistake: the author treats
|
||||
; `recur` like a value-returning recursive call and multiplies its
|
||||
; result, computing factorial as `n * recur(n-1)`. recur is an
|
||||
; argument to *, not in tail position.
|
||||
; Expected: `ail check` exits 1 with code recur-not-in-tail-position.
|
||||
(module loop_recur_3d_recur_not_tail
|
||||
(fn factorial
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body
|
||||
(loop (i (con Int) n)
|
||||
(if (app == i 1)
|
||||
1
|
||||
(app * i (recur (app - i 1)))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app factorial 5)))))
|
||||
@@ -0,0 +1,23 @@
|
||||
; NEGATIVE FIXTURE. The LLM-natural mistake: inside the loop body
|
||||
; the author builds a closure that closes over the loop binder
|
||||
; `acc` (a `\delta. acc + delta` adder) and applies it. Loop
|
||||
; binders are alloca-resident and may not be captured.
|
||||
; Expected: `ail check` exits 1 with code loop-binder-captured-by-lambda.
|
||||
(module loop_recur_3e_binder_captured
|
||||
(fn apply_int
|
||||
(type (fn-type (params (fn-type (params (con Int)) (ret (con Int))) (con Int)) (ret (con Int))))
|
||||
(params f x)
|
||||
(body (app f x)))
|
||||
(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 apply_int (lam (params (typed d (con Int))) (ret (con Int)) (body (app + acc d))) i)
|
||||
(app + i 1))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app sum_to 10)))))
|
||||
@@ -0,0 +1,24 @@
|
||||
; Two things at once:
|
||||
; (1) `loop` used as a sub-expression in argument position — the
|
||||
; (loop ...) result of `gcd` is passed straight into another
|
||||
; call (`app print (app + (app gcd 48 18) (app gcd 1071 462)))`),
|
||||
; not used as a whole fn body. Expected stdout: 27 (gcd(48,18)=6
|
||||
; plus gcd(1071,462)=21).
|
||||
; (2) Euclid's algorithm is a textbook real iterative algorithm an
|
||||
; LLM author reaches for `loop`/`recur` to write; single-binder
|
||||
; pair? no — two binders (a, b), recur swaps/reduces.
|
||||
(module loop_recur_4_gcd_value_pos
|
||||
(fn gcd
|
||||
(doc "Euclidean gcd via loop/recur. Two binders a,b; recur in the tail of the else branch.")
|
||||
(type (fn-type (params (con Int) (con Int)) (ret (con Int))))
|
||||
(params x y)
|
||||
(body
|
||||
(loop (a (con Int) x) (b (con Int) y)
|
||||
(if (app == b 0)
|
||||
a
|
||||
(recur b (app % a b))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(app print (app + (app gcd 48 18) (app gcd 1071 462))))))
|
||||
@@ -0,0 +1,19 @@
|
||||
; NO-TERMINATION BOUNDARY fixture. An LLM-natural shape: a "tick"
|
||||
; event loop that never exits (no non-recur branch). Per the
|
||||
; loop-recur spec this MUST `ail check` AND `ail build` cleanly —
|
||||
; AILang makes no termination claim. BUILD-ONLY: by design this
|
||||
; binary never returns, so it is never executed.
|
||||
(module loop_recur_5_event_loop_noterm
|
||||
(fn run_forever
|
||||
(doc "Infinite event loop. Two binders: tick counter and a running parity flag. No branch ever exits via a non-recur term.")
|
||||
(type (fn-type (params) (ret (con Int))))
|
||||
(params)
|
||||
(body
|
||||
(loop (tick (con Int) 0) (parity (con Int) 0)
|
||||
(if (app == (app % tick 2) 0)
|
||||
(recur (app + tick 1) 1)
|
||||
(recur (app + tick 1) 0)))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app run_forever)))))
|
||||
@@ -0,0 +1,21 @@
|
||||
; NO-TERMINATION BOUNDARY fixture (loop-axis-covering sibling of
|
||||
; loop_recur_5_event_loop_noterm.ail, which surfaced the orthogonal
|
||||
; niladic-call obstacle). An LLM-natural shape: a "tick" event loop
|
||||
; seeded from a start value that never exits (no non-recur branch).
|
||||
; Per the loop-recur spec this MUST `ail check` AND `ail build`
|
||||
; cleanly — AILang makes no termination claim. BUILD-ONLY: by
|
||||
; design this binary never returns, so it is never executed.
|
||||
(module loop_recur_5b_event_loop_noterm
|
||||
(fn run_forever
|
||||
(doc "Infinite event loop. Two binders: tick counter and a running parity flag. No branch ever exits via a non-recur term.")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params start)
|
||||
(body
|
||||
(loop (tick (con Int) start) (parity (con Int) 0)
|
||||
(if (app == (app % tick 2) 0)
|
||||
(recur (app + tick 1) 1)
|
||||
(recur (app + tick 1) 0)))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app run_forever 0)))))
|
||||
Reference in New Issue
Block a user