crates.sage_ir.checking.body
5 anchors
| Anchor | Implementation | Tests |
|---|---|---|
| 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. | ||