Keep Expr non-generic; record checked facts in side tables - #71
Open
wtholliday wants to merge 3 commits into
Open
Keep Expr non-generic; record checked facts in side tables#71wtholliday wants to merge 3 commits into
wtholliday wants to merge 3 commits into
Conversation
Record lexical bindings, solved types, and source locations in owned checked bodies. Specialization produces explicit concrete function/global instances consumed by safety, hoisting, copy elision, Cranelift, LLVM, register VM, and Stack lowering. Replace repeated name lookup, shadowing bookkeeping, and separate capture walkers with recorded identities and shared capture discovery. Retain templates across entry-point changes and specialization retries, validate publication boundaries, and keep partial editor facts separate from executable programs. Check concrete requirements in every retained function body before code motion. Preserve existing syntax and overload/coercion policies. Share borrowed-call classification and add ownership, lifecycle, safety, editor recovery, DSP state, and cancellation regressions. Document the contract in docs/CHECKED_PROGRAM.md. Validated on macOS ARM64 with LLVM 18: default and LLVM workspace builds/tests, backend golden suites, AOT integration tests, and a library check without default features all passed.
The Ubuntu LLVM job builds without the Clang-only C Stack interpreter. Three unguarded references to stack_interp_bridge prevented its library tests from compiling. Gate the C Stack portions of the hoisting and VM codegen regressions with has_stack_interp while keeping register VM coverage active on every build. Validation: reproduced all three original errors with has_stack_interp disabled locally; all 439 LLVM library tests now pass in that configuration. All 13 affected hoisting and VM codegen tests also pass with the C Stack interpreter enabled. git diff --check passes.
The checked-program boundary made `Expr` generic over its reference, binder and parameter payloads so checked bodies could carry `Reference` and `LocalId` in place of names. The repository already records derived facts in tables indexed by `ExprID`, and the checker itself built those tables before transcribing them into the generic form. `Expr` is a single non-generic type again. `CheckedBody` owns the source expression tree plus parallel tables for the solved type, the recorded `Reference` of each identifier/type application, and the `LocalId`s each declaration or lambda introduces. Consumers read identity through `reference(id)`, `binder(id)` and `binders(id)`; the checked pretty printer delegates to the source printer instead of duplicating it. Specialization, safety checking, hoisting, copy elision, Cranelift, LLVM, register VM and stack lowering read the tables. Validation checks that references and binders are recorded exactly where the expression kind requires them. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BcyQEVKmy98VkZhAnx13Tk
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #70: this branch contains #70's commits plus one commit on top (1c7294e). #70's head lives on a fork, so the PR cannot target it directly; review the last commit only, and merge after #70.
#70 made
Exprgeneric over its reference, binder and parameter payloads (Expr<R, B, P>) so checked bodies could carryReference/LocalIdin place of names. The repository's established pattern is to keep derived facts in tables indexed byExprID, and the checker already built exactly those tables before transcribing them into the generic form. This PR returns to that pattern.Expris a single non-generic enum again.CheckedBodyowns the sourceExprArenaplus parallel tables: solved type, the recordedReferenceof eachId/TypeAppnode, and theLocalIds each declaration or lambda introduces.CheckedNodeandCheckedExprare removed.reference(id),binder(id)andbinders(id). Node construction goes throughadd_id,add_local_read,add_let,add_var,add_binding,set_referenceandset_binders;replacekeeps recorded facts only when they still apply to the new expression.Id/TypeAppnodes and that binder counts match the expression kind, so the publication boundary still enforces what the generic type used to.CheckedFunction.paramsstill usesCheckedParam { local }; it is no longer required byExprbut is referenced widely in the backends, so it was left alone to keep the diff focused.Validated on macOS ARM64:
cargo test --workspace(default features, including golden CLI and LSP tests) andcargo test --features llvmwith LLVM 18 both pass.🤖 Generated with Claude Code
https://claude.ai/code/session_01BcyQEVKmy98VkZhAnx13Tk