Corpus stdlib redo (Buffer/StringBuf as CkLang), with/with mut + Size u16 locks #29
tvidal
dferreira
Loading…
Reference in a new issue
No description provided.
Delete branch "feat/029-corpus-stdlib-redo-buffer-stringbuf-as-cklang"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Corpus stdlib redo (Buffer/StringBuf as CkLang), with/with mut + Size u16 locks
Along the way:
with/with mut, redo Buffer as CkLang over the floorsizeas the record fieldTouches 17 files:
.gitignore,docs/actors.md,docs/impl/memory-model/capabilities.md,docs/impl/type-system/value-parameters.md,docs/records.md,docs/syntax.mdand 11 more.Split. The decision in
freezeis a pure function now, with its own tests intests/corpus/stdlib/Buffer.ck.Yes. The commit messages carried me through all 17 files, which is not always true.
@ -74,0 +132,4 @@// (buf dead after) is enforced by the ownership pass (M4), not by a copy.// `List<T, size>` is NOT split into empty/non-empty (the deliberate non-// uniformity with String) — an empty buffer freezes to `[]`.fn freeze<T, size: Size>(buf: Buffer<T, size>) -> List<T, size> {freezereads, decides and writes in one function. The deciding part is the piece I would want to test on its own. Worth splitting?Read it too. No objection to
tests/corpus/stdlib/Buffer.ck.The "DEFERRED — parser can't" comments were largely stale; the grammar has since grown. Verified each claim empirically, then wrote the locked surfaces as code: - Error.ck: real `trait Error { hint, site, stacktrace, cause }` (trait fields parse since slice-8; the E0040 claim was false). Resolves clean. - Buffer/StringBuf/Bytes/String: full op surfaces as `fn … { intrinsic }`, mirroring the Memory.ck floor — opaque-newtype ops are intrinsic, their storage is unspeakable in CkLang. - Arena.ck: restored the OOM bound check as the tail `match` (success in the `false` arm); its cited E0062/E0050 blockers were stale, the real one is statement-position `match` (E0036). - Span.ck: corrected stale grammar rationale to the true design blockers. - trap.md: rewritten, strict-exhaustive reconcile green. Every new trap is the same ratchet class (`intrinsic` → E0301), retiring together when codegen learns to bind `intrinsic`. Still deferred on design, not grammar: Assert::any (function type), String::slice/StrSpan (span fork), Span get/to_owned (undesigned OutOfBounds + bound fork), Panic test mock.with/with mut, redo Buffer as CkLang over the floor 14052883c2The mutation model. CkLang gets ONE mutation operator and no bare `=`: - `let x` binds `imm`, `let mut x` binds `uniq` (the capability reaching the surface without spelling the full lattice); - `x with { f: v }` copies (any binding); `x with mut { f: v }` mutates in place (uniq only, returns Unit); `x with mut <expr>` replaces the whole value. `with mut` on a non-mut binding is a compile error (M4 enforces). The split puts copy-vs-mutate cost in the source, greppable as `with mut` — never an optimizer's invisible choice. Docs: - syntax.md: new canonical "Mutation: `with` / `with mut`" section. - actors.md: fold the bare-`=` actor-state carve-out into `with mut`; state is just a `uniq` binding, not special syntax. - records.md: `with mut` documented as the in-place sibling of `with`. - capabilities.md: note the locked surface (let/let mut/with/with mut); the lattice semantics + checker stay the proposed part. Buffer redone as real CkLang (the first worked "stdlib is CkLang" example): - `newtype Buffer` -> `record Buffer { region, len }`. Rule that falls out: `newtype` is only for the irreducible floor (Region/Handle); anything implementable in CkLang is a `record` over it, opacity via field privacy. - new/push/push_all/len/clear are CkLang over the Memory floor + `with mut`; only `freeze` (the uniq->imm transition, minting an opaque List) stays `intrinsic`, and reduces to a record move once List lands. - trap.md rewritten; reconcile green. New transient gaps trapped and labelled: cross-module floor refs, `size` in value position (evidence for Size=usize), and the not-yet-parsed `with mut`.sizeas the record field d6094fb1ecStringBuf becomes the Buffer twin: `record StringBuf { region, len }` over the Memory floor; new/push/push_str/len/clear are real CkLang with `with mut`. Two ops stay `intrinsic`: `freeze` (the uniq->imm transition, reduces to a record move once String lands) and `encode_utf8` (UTF-8 encode is mask/shift bit math and CkLang has no bitwise operators yet, so the encode is below CkLang — reduces to ordinary CkLang once they land). Buffer + StringBuf both read the bound as the `buf.size` FIELD (the lowercase type param `size: Size` is itself an immutable field — five-keyword carve-up), which resolves clean; only `new` still needs the bare type-level value to size the allocation (the lone const-generic-in-value gap, ties to Size=usize, deferred). `size` is never mutated — only `len` is `with mut`-patched. trap.md reconciled green; intro rewritten — `intrinsic` is now per-reason (floor / transition / no-bitwise-ops / unlanded builtin), not "opaque newtype".