docs(stdlib): session ledger §9 — progress, the arena bug (found+fixed), shortcuts, R2 wall #44
tvidal
dferreira
Loading…
Reference in a new issue
No description provided.
Delete branch "feat/044-docs-stdlib-session-ledger-9-progress-the-aren"
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?
docs(stdlib): session ledger §9 — progress, the arena bug (found+fixed), shortcuts, R2 wall
Along the way:
Touches 45 files:
.claude/commands/cleanup.md,current-state.md,docs/impl/08-diagnostics.md,docs/impl/runtime/README.md,docs/impl/type-system/TY7-exhaustive-match-and-narrowing.md,src/rust/crates/ck_driver/src/lib.rsand 39 more.Split. The decision in
dropis a pure function now, with its own tests insrc/rust/crates/ck_driver/tests/match_bool_run.rs.Pushed a fix for both. The second pass on
src/rust/crates/ck_driver/tests/match_bool_run.rsis much smaller than the first.Two things inline. The one in
src/rust/crates/ck_driver/tests/match_bool_run.rsis the one I care about.@ -0,0 +149,4 @@}impl Drop for Teardown {fn drop(&mut self) {dropreads, decides and writes in one function. The deciding part is the piece I would want to test on its own. Worth splitting?Both answered, and
src/rust/crates/ck_driver/tests/match_bool_run.rsreads right now. Merging.Second read on
src/rust/crates/ck_driver/tests/match_bool_run.rs. Nothing to add.The first crack in the R2 wall. `let <ident> = <expr>;` now lowers in run-path bodies: the block-statement walkers `emit_effect`/`emit_block_value` thread a mutable `LocalSlots`, and a new `StmtKind::Let` arm emits the initializer's word(s) and binds them under the LocalId — read back exactly like a parameter. Int locals bind one i64; String locals bind the (ptr,len) pair via emit_arg (concat vs int-add disambiguated by operand shape, since the run-path floor type table is empty). Dependent lets work (`let b = a + 22` reads the earlier `a`). Correction to the plan: arithmetic through locals required making `emit_scalar_value` locals-aware — the shared `apply_int_binop` now backs both the context-free `emit_value` and the locals-aware walker. New `codegen/binding.rs` (emit_let / let_binds_string / apply_int_binop) keeps codegen.rs at 805/809 — the R3 LoC cap was NOT raised (ratchet discipline). Out-of-scope forms stay real CodegenError::Unsupported (compound patterns, record/list lets); no silent truncation. Gates: fmt/clippy(-D warnings)/build/test --workspace all exit 0 (1117 tests). Gates: tests/corpus/let_int (fn main -> Int { let a=20; let b=a+22; b } -> exit 42, freestanding) + tests/corpus/let_log (String let -> Log::info, freestanding Sys::write), both in corpus.rs RUNTIME_TESTED; let_log in LIVE_STDLIB_APPS. if/else/match/for remain the wall — R2b is next.CkLang has no `if`; branching is value-position `match` only. New Floor IR ExprKind::Match { scrutinee, arms } with ArmPattern { Literal | Wildcard | Binder }, lowered in ck_lower::lower (a guarded arm or any out-of-frame pattern takes the WHOLE match to Unsupported — nothing half-lowered). Codegen in a new codegen/match_expr.rs: scrutinee evaluated once, sequential icmp+brif dispatch, per-arm blocks, a merge block whose param is the match value; a binder binds the scrutinee word into the R2a LocalSlots. Comparison operators </>/<=/>=/!= added to apply_int_binop so a Bool scrutinee (a > b) is producible. Exhaustiveness is the front-end's guarantee (TY7/E0719); the impossible no-catch-all fallthrough traps to keep the CFG well-formed. Bare-variant patterns DEFERRED to R2c (need a pattern-head CST tag reader — new resolver machinery). Match dispatched from emit_block_value (already &mut LocalSlots) not emit_scalar_value — match is tail-only, never a scalar operand. Gates: fmt/clippy(-D warnings)/build/test --workspace all exit 0; arch R3/R4 green (codegen.rs at 809/809 cap — NOT raised; match_expr.rs split out). Gates: tests/corpus/match_bool (match a>b {true->1 false->42} -> exit 42) + tests/corpus/match_int (match n {0->100 1->42 _->7} -> exit 42), both freestanding, in RUNTIME_TESTED. Arena.ck's true/false tail is now expressible.HIR StmtKind::Let now carries the full ck_hir::Pattern (unified with the pattern match arms bind) instead of Option<LocalId>; the resolver records it, the type stage checks irrefutability + flows binder types, ck_lower keeps R2a's simple-let runtime via a Binder->Some(local) adaptor (no floor_ir/codegen change). New E0731 (refutable pattern in let). Records destructure irrefutably via the reused match exhaustiveness core (single_arm_covers_all). ckc-check only; runtime destructure is R2c-cg. KNOWN SOUNDNESS GAP (fix commit follows immediately, before R2c-cg): the LIST irrefutability rule is UNSOUND. Under bounded-max list semantics (List<T,N> = length 0..=N, per arenas.md/types.md and match_list's Exact/Open cover), a fixed-arity `let [a,b] = xs` and a non-empty-prefix `let [head, ..rest] = xs` are REFUTABLE (they miss shorter lengths) — only pure `[..rest]` is irrefutable. This slice's arity==bound / rest-always-irrefutable rule wrongly accepts them. Latent (no R2c-cg runtime executes it yet); corrected in the next commit by reusing match_list::list_cover (irrefutable iff Open(0)). Gates: fmt/clippy(-D warnings)/build/test --workspace exit 0; ck_types 222, conformance green. New goldens tests/types/let_{destructure,refutable}_*.cktest.