a35878154b
The field-test note on the `Window` ctor claimed that bare
`(con RawBuf (con Float))` in a user ADT ctor field gives a
type-mismatch and that "the only form that checks is the
fully-qualified `raw_buf.RawBuf`". Verified against the current
tool (release at HEAD), that claim is false in every form I could
construct:
- bare `(con RawBuf a)` (type-variable element) in a non-kernel
module: checks ok
- bare `(con RawBuf (con Float))` (concrete element): checks ok
- a `(new RawBuf ...)` value stored via `term-ctor` into a
bare-declared field: checks ok
- the full rbx_1 program with the field switched to bare RawBuf:
checks ok
A ctor field is plain type position, and model 0007 §3
("kernel-module types are accessible bare in type position") already
covers it — the auto-import that makes bare `Series` work at a call
site equally makes bare `RawBuf` resolve in a user ctor field. The
only genuine constraint is that a ctor field carries no mode:
`(own (RawBuf a))` is a surface-parse-error, which model 0007 line
458 already documents.
So there is no qualification asymmetry to add to the ledger; the
ledger is correct as-is. The drift was in this checked-in comment
(a guessed rule recorded as fact), now rewritten to the verified
reality. The qualified spelling is kept in the code as the explicit
form. No ledger change.
closes #65
94 lines
3.9 KiB
Plaintext
94 lines
3.9 KiB
Plaintext
; Fieldtest raw-buf comprehensive .1 (Axes 1+2+3+4 combined — the
|
|
; "Series substrate" shape with a Float element width).
|
|
;
|
|
; Task an LLM author is naturally given: "model a fixed-size window of
|
|
; Float samples with a running total, fill it from a loop, then report
|
|
; the window mean and the window maximum through read-only helpers."
|
|
;
|
|
; The natural decomposition wraps a RawBuf<Float> together with a
|
|
; bookkeeping `count` field in a user ADT (Window), exactly the Series
|
|
; substrate the ledger (design/models/0007 §Series) describes — an ADT
|
|
; holding `(own (RawBuf a))` plus Int bookkeeping. The buffer is filled
|
|
; via a (loop ...)/recur (runtime-N, not literal indices), and the
|
|
; read-back is factored into two `borrow (Window)` helpers (`mean`,
|
|
; `wmax`) that each pattern-match the ADT and drive a read loop off the
|
|
; bookkeeping count, reading the buffer through `RawBuf.get` on a borrow.
|
|
;
|
|
; This stresses, in one program:
|
|
; - Float element width through a fill loop (not just literal sets).
|
|
; - A RawBuf stored in a user ADT field (the #50 substrate shape).
|
|
; - TWO borrow-receiver helpers composing over the same wrapped buffer
|
|
; (the #46 borrow-receiver-read fix, under composition + behind a
|
|
; match on the ADT).
|
|
; - The drop cascade: the Window ADT owns the buffer; dropping the
|
|
; Window frees the slab. Leak-clean expected under AILANG_RC_STATS.
|
|
;
|
|
; Window of 4 samples: 2.0, 4.0, 6.0, 8.0.
|
|
; mean = 20.0 / 4 = 5.0
|
|
; wmax = 8.0
|
|
; Expected stdout: two lines, "5.0" then "8.0".
|
|
|
|
(module rbx_1_float_window_stats
|
|
|
|
; NOTE (field test): a ctor-field storage type carries no mode — the
|
|
; `(own (RawBuf a))` form does NOT parse (`own` in a ctor field is a
|
|
; surface-parse-error; modes live on fn params/ret only). The element
|
|
; type itself is plain type position, so both the kernel-auto-imported
|
|
; bare `(con RawBuf (con Float))` and the fully-qualified
|
|
; `(con raw_buf.RawBuf (con Float))` check — they denote the same type.
|
|
; (The qualified form is kept here as the explicit spelling.)
|
|
(data Window
|
|
(ctor W (con raw_buf.RawBuf (con Float)) (con Int)))
|
|
|
|
(fn build_window
|
|
(doc "Allocate a 4-slot Float buffer, fill slot i with (2*(i+1)), wrap in a Window with count=4.")
|
|
(type (fn-type (params (own (con Int))) (ret (own (con Window)))))
|
|
(params n)
|
|
(body
|
|
(let buf (new RawBuf (con Float) 4)
|
|
(let filled
|
|
(loop (b (con RawBuf (con Float)) buf) (i (con Int) 0)
|
|
(if (app ge i n)
|
|
b
|
|
(recur (app RawBuf.set b i (app int_to_float (app * 2 (app + i 1))))
|
|
(app + i 1))))
|
|
(term-ctor Window W filled n)))))
|
|
|
|
(fn mean
|
|
(doc "Average of the first count slots, read through a borrow of the Window.")
|
|
(type (fn-type (params (borrow (con Window))) (ret (own (con Float)))))
|
|
(params w)
|
|
(body
|
|
(match w
|
|
(case (pat-ctor W buf count)
|
|
(app /
|
|
(loop (acc (con Float) 0.0) (i (con Int) 0)
|
|
(if (app ge i count)
|
|
acc
|
|
(recur (app + acc (app RawBuf.get buf i))
|
|
(app + i 1))))
|
|
(app int_to_float count))))))
|
|
|
|
(fn wmax
|
|
(doc "Maximum of the first count slots, read through a borrow of the Window.")
|
|
(type (fn-type (params (borrow (con Window))) (ret (own (con Float)))))
|
|
(params w)
|
|
(body
|
|
(match w
|
|
(case (pat-ctor W buf count)
|
|
(loop (mx (con Float) 0.0) (i (con Int) 0)
|
|
(if (app ge i count)
|
|
mx
|
|
(recur (if (app float_gt (app RawBuf.get buf i) mx)
|
|
(app RawBuf.get buf i)
|
|
mx)
|
|
(app + i 1))))))))
|
|
|
|
(fn main
|
|
(type (fn-type (params) (ret (own (con Unit))) (effects IO)))
|
|
(params)
|
|
(body
|
|
(let w (app build_window 4)
|
|
(seq (seq (app print (app mean w)) (do io/print_str "\n"))
|
|
(seq (app print (app wmax w)) (do io/print_str "\n")))))))
|