fix(codegen): replay loop binders in synth_with_extras (closes #47)
A `let`-bound `loop` whose body references one of its own loop binders on the non-recur exit passed `ail check` but failed `ail build` with `unknown variable`. The fieldtest surfaced this with an owned RawBuf loop binder, but the trigger is element-type-independent. Root cause: the Term::Loop arm of synth_with_extras (the type-replay walk the let-lowering runs via synth_arg_type on every let value) descended into the loop body WITHOUT adding the loop binders to `extras`, unlike the Term::Let arm which pushes its binder. A loop binder referenced on the non-recur exit then resolved to UnknownVar during the type replay. Fix: clone `extras`, push each loop binder's (name, ty), and thread the augmented extras into the recursive synth of the body — mirroring the Term::Let arm exactly. General fix; a plain Int let-bound loop that references its binder also builds now. This restores check<->codegen agreement for the natural fill-loop (thread an owned buffer of runtime length through a loop/recur, one RawBuf.set per iteration) — the way to populate a buffer whose length is not a fixed set of literal indices. Surfaced by the raw-buf fieldtest (finding B2, docs/specs/0058). RED-first: loop_let_bound_binder_reference_builds.
This commit is contained in:
@@ -0,0 +1,30 @@
|
||||
; RED for fieldtest finding B2 (raw-buf milestone, Gitea #7).
|
||||
;
|
||||
; Property: a `loop` whose result is `let`-bound, and whose body
|
||||
; references one of its own loop binders on the non-recur exit, must
|
||||
; BUILD — not only `check`. The let-lowering in codegen calls
|
||||
; `synth_arg_type` on every let value to replay its AILang type; that
|
||||
; type-replay walk must descend through `Term::Loop` with the loop's
|
||||
; binders in scope, exactly as it already does for `Term::Let`.
|
||||
;
|
||||
; The fieldtest surfaced this with an owned `RawBuf` loop binder, but
|
||||
; the trigger is element-type-independent: it is the `let`-bound loop
|
||||
; with a binder reference reachable through the synth body-walk. A
|
||||
; plain `Int` binder is the minimal autonomous reproduction.
|
||||
;
|
||||
; Pre-fix symptom: `ail check` ok, `ail build` ->
|
||||
; Error: module `loop_let_bound_binder_ref`: def `main`:
|
||||
; unknown variable: `b`
|
||||
;
|
||||
; Expected stdout: 3 (loop counts i 0,1,2 and returns binder b == i).
|
||||
(module loop_let_bound_binder_ref
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(let r
|
||||
(loop (b (con Int) 0) (i (con Int) 0)
|
||||
(if (app ge i 3)
|
||||
b
|
||||
(recur (app + i 1) (app + i 1))))
|
||||
(app print r)))))
|
||||
Reference in New Issue
Block a user