feat(series): ship the kernel-tier Series library extension (#61)
Series a is a bounded ring buffer with financial-style indexing (index 0 = newest), shipped as a PURE AILang library extension over RawBuf — zero Rust codegen, zero intercepts, zero (intrinsic) markers. It is the first kernel-tier module that depends on another kernel-tier module (raw_buf). This turns the committed SMA headline pin (6b7ee45) green and closes the step-1 scope of #61. The module lives at crates/ailang-kernel/src/series/{source.ail, mod.rs} and is auto-injected by the loader exactly like raw_buf (parse_series + injection in ailang-surface/src/loader.rs, re-export in lib.rs). Five real-bodied ops: new / push / at / len / total_count, all built on RawBuf.{new,set,get}. The source is the model-0007 sketch with every defect corrected and each correction verified against the live tool: - param-in narrowed to (a Int Float); Bool deferred per #61. - inner alloc is `(new RawBuf lookback)` with no element type-arg — the element is solved from the `(con RawBuf a)` ctor-field context, which the base-tier mono fix (b11a6d9) carries through to the caller's concrete type. This is the capability that lets Series be pure AILang. - element-typed params/rets are bare `a`, not `(con a)` (a type variable, not a nullary ctor). - op signatures bind `a` via `(forall (vars a) ...)`. - comparison uses the named helper `lt`, not the non-existent `<`. - the at-index formula is `(head - 1 - i + 2*lookback) mod lookback` (0007 had the sign on i wrong, walking the wrong direction). Cross-kernel-module visibility — the flagged risk — needed ZERO mechanism change: the loader derives its implicit-import set from every kernel module, so series's body resolves `RawBuf.*` and `(con RawBuf a)` via the existing kernel auto-visibility. Both CLAUDE.md lockstep pairs stay intact: - INTERCEPTS <-> (intrinsic) markers: unchanged. Series is pure-AILang, adds neither; intercepts_bijection_with_intrinsic_ markers still green. - Term::New typecheck/reject <-> pre_desugar_validation.rs: untouched; the new/Series construction exercises existing paths. Test-surface ripple, all verified: - workspace module-count pins 4 -> 5 (e2e.rs, workspace_pin.rs), with a `series` membership assertion added — the kernel set grew by one deliberate module. - two mono-identity tests (typeclass_22b3.rs) now skip `prelude` and `series`: series is the first auto-imported real-bodied consumer of the prelude polyfns `lt`/`compare` over Int, so mono legitimately materialises `lt__Int`/`compare__Int` into prelude for every workspace. That is a concrete call site, not gratuitous mutation; the tests' real invariant (mono leaves work-free modules untouched) still holds for every other module. - five IR snapshots refreshed; the deltas are strictly additive (zero IR deletions) — the same series-driven Int specialisations. Verified: full `cargo test --workspace` green; SMA binary built via `ail build --alloc=rc` prints `3.0 / 5.33333 / 5.66667 / 5.33333`. refs #61
This commit is contained in:
@@ -9,5 +9,7 @@
|
||||
//! crate carries zero parser code.
|
||||
|
||||
mod raw_buf;
|
||||
mod series;
|
||||
|
||||
pub use raw_buf::SOURCE as RAW_BUF_AIL;
|
||||
pub use series::SOURCE as SERIES_AIL;
|
||||
|
||||
@@ -0,0 +1,18 @@
|
||||
//! Series submodule — the Form-A source of the `series` kernel-tier
|
||||
//! library-extension module (Series: a bounded ring buffer over
|
||||
//! RawBuf with financial-style indexing, index 0 = newest). Parsed by
|
||||
//! `ailang_surface::parse_series`.
|
||||
//!
|
||||
//! Unlike `raw_buf`, `series` is a PURE AILang library extension: its
|
||||
//! five ops (new/push/at/len/total_count) carry real `.ail` bodies
|
||||
//! built on the `RawBuf.*` intrinsics, so it adds NO intercept entries
|
||||
//! and NO `(intrinsic)` markers. It is the first kernel-tier module
|
||||
//! that depends on another kernel-tier module (`raw_buf`); cross-
|
||||
//! kernel-module visibility comes from the kernel auto-import set the
|
||||
//! loader derives from every `kernel: true` module.
|
||||
|
||||
/// Source-of-truth Form-A text for the `series` kernel module.
|
||||
/// Declares the `Series` TypeDef (`param-in (a Int Float)`) and the
|
||||
/// five real-bodied ops `new`/`push`/`at`/`len`/`total_count`, all
|
||||
/// implemented over the `raw_buf` kernel module's `RawBuf.*` ops.
|
||||
pub const SOURCE: &str = include_str!("source.ail");
|
||||
@@ -0,0 +1,49 @@
|
||||
(module series
|
||||
(kernel)
|
||||
(data Series (vars a)
|
||||
(doc "Bounded ring buffer with financial-style indexing (index 0 = newest). Pure AILang library extension over RawBuf: the buffer holds the elements, the four Int fields are lookback (capacity), head (next write slot), count (live elements, saturates at lookback), and total (monotone count of all pushes ever). Element type restricted to {Int, Float} via param-in; Bool deferred (#61).")
|
||||
(param-in (a Int Float))
|
||||
(ctor S (con RawBuf a)
|
||||
(con Int)
|
||||
(con Int)
|
||||
(con Int)
|
||||
(con Int)))
|
||||
(fn new
|
||||
(doc "Allocate an empty Series of capacity `lookback`. The inner RawBuf is allocated via `(new RawBuf lookback)` with NO element type-arg — the element type is solved from the expected ctor-field type `(con RawBuf a)`, which the base-tier mono fix (b11a6d9) carries through to the caller's concrete type.")
|
||||
(type (forall (vars a) (fn-type (params (own (con Int))) (ret (own (con Series a))))))
|
||||
(params lookback)
|
||||
(body
|
||||
(term-ctor Series S
|
||||
(new RawBuf lookback) lookback 0 0 0)))
|
||||
(fn push
|
||||
(doc "Append `v`, evicting the oldest element when full. own-in/own-out linear threading: mutates the buffer at head, advances head mod lookback, saturates count at lookback, increments total.")
|
||||
(type (forall (vars a) (fn-type (params (own (con Series a)) (own a)) (ret (own (con Series a))))))
|
||||
(params s v)
|
||||
(body
|
||||
(match s
|
||||
(case (pat-ctor S buf lookback head count total)
|
||||
(term-ctor Series S
|
||||
(app RawBuf.set buf head v)
|
||||
lookback
|
||||
(app % (app + head 1) lookback)
|
||||
(if (app lt count lookback) (app + count 1) count)
|
||||
(app + total 1))))))
|
||||
(fn at
|
||||
(doc "Read the element `i` positions back from newest (i=0 is the most recent push). Financial indexing: slot = (head - 1 - i + 2*lookback) mod lookback. UB if i >= len; caller checks via len/total_count.")
|
||||
(type (forall (vars a) (fn-type (params (borrow (con Series a)) (own (con Int))) (ret (own a)))))
|
||||
(params s i)
|
||||
(body
|
||||
(match s
|
||||
(case (pat-ctor S buf lookback head count total)
|
||||
(app RawBuf.get buf
|
||||
(app % (app + (app - (app - head 1) i) (app * lookback 2)) lookback))))))
|
||||
(fn len
|
||||
(doc "Number of live elements (saturates at lookback).")
|
||||
(type (forall (vars a) (fn-type (params (borrow (con Series a))) (ret (own (con Int))))))
|
||||
(params s)
|
||||
(body (match s (case (pat-ctor S buf lookback head count total) count))))
|
||||
(fn total_count
|
||||
(doc "Monotone count of all pushes ever (does not saturate). Drives the SMA emit gate.")
|
||||
(type (forall (vars a) (fn-type (params (borrow (con Series a))) (ret (own (con Int))))))
|
||||
(params s)
|
||||
(body (match s (case (pat-ctor S buf lookback head count total) total)))))
|
||||
Reference in New Issue
Block a user