Brummel
37ac704bf3
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).
80 lines
2.4 KiB
Plaintext
80 lines
2.4 KiB
Plaintext
; Iter 18g tidy follow-up RED-test fixture: a let-binder whose
|
|
; value is a Term::Var referencing a non-Own fn-param must
|
|
; inherit the param's mode for codegen's drop-emission gates.
|
|
;
|
|
; The carve-out documented in 18d.4's Iter A fix: the gate
|
|
; checks `scrutinee_is_owned` against `current_param_modes`,
|
|
; but only fn-params are recorded there. A let-binder aliasing
|
|
; an Implicit-mode fn-param passes the gate (its lookup
|
|
; misses, default = owned), so the arm-close drop fires on
|
|
; memory the caller still references.
|
|
;
|
|
; Pattern: `pin_aliased` takes `t` as Implicit-mode (default,
|
|
; no annotation); aliases it via `(let a t ...)`; matches `a`.
|
|
; In the TNode arm the pattern-bindings `l` / `r` would be
|
|
; dec'd at arm close because `a` looks owned to the gate —
|
|
; corrupting the caller's tree.
|
|
;
|
|
; Pre-fix under --alloc=rc: refcount underflow at the second
|
|
; iteration of `loop`, where the recursive call into
|
|
; `pin_aliased(t)` re-loads cells the previous iteration
|
|
; freed.
|
|
; Post-fix: clean exit, output `0`. Stats are not the focus
|
|
; here (the caller's tree leaks under the Implicit-mode
|
|
; back-compat lane); the test asserts only correctness.
|
|
|
|
(module rc_let_alias_implicit_param
|
|
|
|
(data Tree
|
|
(ctor TLeaf)
|
|
(ctor TNode (con Int) (con Tree) (con Tree)))
|
|
|
|
(fn build
|
|
(type
|
|
(fn-type
|
|
(params (con Int))
|
|
(ret (own (con Tree)))))
|
|
(params d)
|
|
(body
|
|
(if (app == d 0)
|
|
(term-ctor Tree TLeaf)
|
|
(term-ctor Tree TNode 1
|
|
(app build (app - d 1))
|
|
(app build (app - d 1))))))
|
|
|
|
; Pin via let-alias: the alias `a` is a Var-binding on the
|
|
; Implicit-mode (default) param `t`. Codegen's gate must
|
|
; recognise that `a` inherits `t`'s mode and skip the arm-
|
|
; close drop that would otherwise fragment the caller's
|
|
; tree.
|
|
(fn pin_aliased
|
|
(type
|
|
(fn-type
|
|
(params (con Tree))
|
|
(ret (con Int))))
|
|
(params t)
|
|
(body
|
|
(let a t
|
|
(match a
|
|
(case (pat-ctor TLeaf) 0)
|
|
(case (pat-ctor TNode v l r) 1)))))
|
|
|
|
(fn loop
|
|
(type
|
|
(fn-type
|
|
(params (con Int) (con Tree))
|
|
(ret (con Int))))
|
|
(params n t)
|
|
(body
|
|
(if (app == n 0)
|
|
0
|
|
(let _v (app pin_aliased t)
|
|
(app loop (app - n 1) t)))))
|
|
|
|
(fn main
|
|
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
|
(params)
|
|
(body
|
|
(let t (app build 2)
|
|
(app print (app loop 3 t))))))
|