crates.sage_ir.checking
12 anchors
| Anchor | Implementation | Tests |
|---|---|---|
| crates.sage_ir.checking (12) | 12 Implemented3 TODO | 5 Implemented12 TODO |
| crates.sage_ir.checking.body (5) | 5 Implemented2 TODO | 3 Implemented5 TODO |
elaboration | Implemented | ImplementedTODO |
A completed body is an elaborated semantic tree. Successful output contains final types and semantic identities and materializes all type-directed operations used by the source. Method syntax, unresolved names, inference variables, pending obligations, and adjustment recipes do not survive in | ||
expected_types | ImplementedTODO | TODO |
Expected types flow into expression checking without selecting semantic candidates. A caller supplies an available expected type before checking the expression beneath that boundary. Expression forms may use it to guide local inference and explicit coercion, but trait proof, method provider discovery, and alias normalization retain their independent candidate-selection rules. | ||
interface_dependencies | Implemented | ImplementedTODO |
Body checking depends on interfaces, never other bodies. The body query reads only its own CST and signature plus the name-resolution, interface, metadata, candidate, and solver facts demanded by that body. A call may read its callee’s signature but cannot read the callee body. This is the body-phase consequence of Cross-item dependencies stop at semantic interfaces. | ||
isolated_completion | Implemented | ImplementedTODO |
Speculation is isolated and completion is quiescent. Candidate matching and other speculative relations occur in child inference versions; failure discards their equalities, wakeups, and staged obligations, while a successful operation commits them atomically. The public result is frozen only after fallback and terminal obligation processing leave no live work. Versioned egraph children are inference transactions defines the shared transaction rules. | ||
operator_calls | ImplementedTODO | TODO |
Overloadable operators remain resolved calls in Typed IR. Every non-short-circuit binary operator retains its trait operation and method result through inference; its token alone neither narrows nor equates operand types. Every proven operation completes as a resolved trait-method call, including primitive and generic cases. Ambiguity and unsupported operands cannot be represented as success, and primitive specialization occurs only at the future codegen boundary defined by the operator representation decision. | ||
identity_minting | Implemented | TODO |
Semantic identities have exactly one minting boundary. An owning query creates each generic parameter or associated-item symbol once. Every dependent query reopens or references that identity instead of reconstructing it from its name or source position. The identity family is defined by Symbols form the uniform semantic identity family. | ||
owned_products | Implemented | ImplementedTODO |
Checked products own their semantic storage. CST is immutable input; each checked signature or body allocates into a fresh output stash and returns a self-contained | ||
| crates.sage_ir.checking.signature (4) | 4 Implemented1 TODO | 1 Implemented4 TODO |
body_independence | Implemented | TODO |
A checked signature is the body-independent cross-item interface. Consumers obtain the types, generic binder, and parameter environment needed to use a definition without checking that definition’s body. No signature query reads any function body. This is the signature-phase consequence of Cross-item dependencies stop at semantic interfaces. | ||
narrow_detail | ImplementedTODO | TODO |
Interface detail is split at semantic reuse boundaries. Fields and associated-item enumeration remain independently keyed from the owner signature, and selecting one associated item reads only that item’s signature. Enumeration never checks sibling signatures or bodies eagerly. | ||
owner_binder | Implemented | ImplementedTODO |
Generic identities are minted once by their owner and reused. An owner signature creates its parameters under one binder. Associated-item, field, and body queries reopen that binder and add only genuinely new item-level parameters; they never reconstruct an existing | ||
storage | Implemented | TODO |
Checked interfaces are self-contained semantic values. Signature lowering reads CST from one stash and writes all checked types, binders, predicates, and retained alias applications into a separate result stash. No checked value points into tree-sitter state or the source CST stash. This is the signature-level ownership boundary established by Stash for type-level interning. | ||
symbol_keyed_interfaces | Implemented | TODO |
Public checking queries are symbol-keyed semantic boundaries. A caller supplies the definition symbol and the query derives scope and environment from it. Signatures are the primary cross-item interface; field, member, and other language-required interfaces may be separate narrow products. Bodies and checking temporaries are not interfaces. This is the shared query design required by Cross-item dependencies stop at semantic interfaces. | ||