Brummel
d5cc6e96b6
- rawbuf_1_score_table / rawbuf_2_running_max: the header OUTCOME blocks described the pre-fix breakage (does-not-check / unknown-variable). Those defects are fixed (B1 #46, B2 #47, B5); update the comments to the current state — both check, build, run to their expected values and are leak-clean under AILANG_RC_STATS. The files now serve as positive regression examples, not bug repros. - design/models/0007 §RawBuf: ratify the fieldtest's B4 spec_gap. The `own -> own` signature of RawBuf.set is a threading discipline, not runtime-enforced single-use; a double-consume of the same owned buffer aliases one slab (consistent with every owned value in the language). State that single-use is the author's responsibility and full linear enforcement is Issue #22 territory. Surfaced by the raw-buf fieldtest (docs/specs/0058).
58 lines
2.4 KiB
Plaintext
58 lines
2.4 KiB
Plaintext
; Fieldtest raw-buf.1 (Axis 1, RawBuf as mutable indexed storage).
|
|
; Task an LLM author is naturally given: "build a small score table of
|
|
; N slots, fill slot i with a computed score (i*i + 1), then read every
|
|
; slot back and total the scores." The natural shape uses RawBuf.size to
|
|
; drive the read loop rather than hard-coding the bound, which the spec's
|
|
; worked program (literal 0/1/2 indices) never exercises.
|
|
;
|
|
; Fill loop: thread the owned buffer through RawBuf.set in a (loop ...)
|
|
; with a recur per slot. Read loop: borrow the buffer, drive i from 0 to
|
|
; (RawBuf.size buf) accumulating (RawBuf.get buf i).
|
|
;
|
|
; Expected stdout: scores 1, 2, 5, 10, 17 -> sum 35.
|
|
;
|
|
; This was the fieldtest repro for two defects, both now fixed:
|
|
; - B1 (#46): the `total` helper, which takes `borrow (RawBuf Int)`
|
|
; and only calls RawBuf.size / RawBuf.get on the receiver, was
|
|
; falsely rejected with [consume-while-borrowed]. The linearity
|
|
; pass now resolves the type-scoped borrow-receiver ops, so the
|
|
; borrow helper checks clean.
|
|
; - B2 (#47): the `fill` loop, threading the owned buffer through a
|
|
; `recur`, failed codegen with `unknown variable: b`. The synth
|
|
; type-replay now descends through `loop` with the loop binders in
|
|
; scope.
|
|
; OUTCOME (current): checks, builds, runs; prints 35. Leak-clean under
|
|
; AILANG_RC_STATS (the owned buffer drops at scope close, B5).
|
|
|
|
(module rawbuf_1_score_table
|
|
|
|
(fn fill
|
|
(doc "Fill slots 0..n of buf with (i*i + 1). Linear: own in, own out.")
|
|
(type (fn-type (params (own (con RawBuf (con Int))) (con Int)) (ret (own (con RawBuf (con Int))))))
|
|
(params buf n)
|
|
(body
|
|
(loop (b (con RawBuf (con Int)) buf) (i (con Int) 0)
|
|
(if (app ge i n)
|
|
b
|
|
(recur (app RawBuf.set b i (app + (app * i i) 1))
|
|
(app + i 1))))))
|
|
|
|
(fn total
|
|
(doc "Sum every slot of buf, driving the bound off RawBuf.size.")
|
|
(type (fn-type (params (borrow (con RawBuf (con Int)))) (ret (con Int))))
|
|
(params buf)
|
|
(body
|
|
(loop (acc (con Int) 0) (i (con Int) 0)
|
|
(if (app ge i (app RawBuf.size buf))
|
|
acc
|
|
(recur (app + acc (app RawBuf.get buf i))
|
|
(app + i 1))))))
|
|
|
|
(fn main
|
|
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
|
(params)
|
|
(body
|
|
(let buf (new RawBuf (con Int) 5)
|
|
(let buf (app fill buf 5)
|
|
(app print (app total buf)))))))
|