v2 emit: Bool/declared-type spelling, bare bodies, record vs refinement, Rust refinement alias - #12715
Conversation
…refusal (coproducts now emit beside functions) Side-chat ruling: heterogeneous member fold; do not classify a plain Conj member as a record (records and where-refinements share that shape after lowering, and the record fact does not reach emission); wire only the unambiguous Disj; refinement realization is a later explicit case. - v2.compiler.emit_produced: module_member_class / emit_module_member decide each DIRECT member of a module body once: bodied Arrow -> produced-decl rows (emit_produced_decl); plain Disj coproduct -> the existing v2.compiler.emit_semantic_decl emit_semantic_type_decl (first production caller); plain Conj (record or refinement) / alias / bodyless / generic / bodyless arrow / unsupported -> each its own located refusal. emit_module_body_members folds the bodies' direct members in source order and refuses on the first unrealized member -- nothing partial published. produced_module_bodies_declare_members only asks "is there a nonempty module"; the member fold is the one authority for "does it render". - v2.compiler.program_partition routes through the member fold; an empty module keeps the translate route. - closure_emit_arrow_body_refusal: the fn-beside-record row now expects the member refusal; the failure-mode row's citation follows the new function. - New v2.test.claim.emit.module_member_emission (6 rows, WARM producers, production closure_emission door). Evidence (local claim_batch): 6/6. Mutants: Conj-as-record reds refinement + record; filtering unrenderable members reds all 5 refusal rows; refusing coproducts reds the emission row. Regression: closure_emit_arrow_body_refusal 5/5, identity_cast_emission_route 2/2, produced_decl_two_target 3/3, rust_module_emission_population 8/8. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…lows (review 72631) - v2.compiler.self_host.candidate_generation generate_rust_module_emission_candidate routes through emit_module_body_members, as program_partition does, instead of emit_produced_module over the arrow-only produced_decl_conjs_in_tree, which skipped non-function members. Empty/no-body trees still refuse rust_module_emission_decl_absent. - emit_produced_module is annotated as the fold over a SUPPLIED declaration list (realization_attempt and the emit-host fixtures), not a module authority. - closure_emit_renders_an_arrow_without_its_body: prose, rung and ceiling rewritten; no receipt names the deleted produced_module_declares_bodied_members. Local claim_batch: stage0_production_target 5/5, rust_module_emission_population 8/8, module_member_emission 6/6, closure_emit_arrow_body_refusal 5/5. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…are parameter and literal bodies emit)
v2.std.compilers.target_model target_project_arrow_body_by_kind's Atom arm
accepted only an int literal and refused every other atom as
transform_shape_invalid, so `fn f(x: Int) -> Int { x }` and
`fn g() -> Bool { true }` could not be emitted although the same atom emitted as
an operand. It now calls target_value_expr_project_atom_in_arrow_scope, the
projection nested operands use: parameter binding first, then the target's
literal realizations; an unresolved name refuses body_scope_binding_invalid.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…s; refinements and undecided Conj members refuse by name
A plain Conj member is a record, a where-refinement, or neither (a
payload-bearing single variant shares the shape), and lowering erases which.
Emission now classifies it from positive facts only:
- v2.compiler.body_lowering_fold body_lower_type_decl_refinement_name_optional:
the refinement arm's own predicate (not a record block, a where host via
body_lower_find_where_host_conj), beside the record helper.
- v2.compiler.normalize refinement_declaration_capture carries it on
v2.compiler.normalized_tree NormalizedTree refinement_declarations beside
record_declarations (admit_normalized_tree_with_refinements; the old
constructor delegates with none).
- v2.compiler.emit_produced ModuleDeclarationKinds { records, refinements }
reaches emit_module_member through program_partition
emit_for_target_with_declarations; the closure door passes the member's
NormalizedTree facts, callers without them pass none.
- Classification: in records -> struct via emit_semantic_type_decl; in
refinements -> ModuleMemberRefinement (refuses not_realized until the target
realization lands); in both -> KindConflict refusal; in neither -> undecided.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…bricated spelling (Bool emits `bool`) v2.std.compilers.target_model produced_decl_type_ref_tokens bound every type atom as itself, and the serializer's interned-name fallback then printed an unmapped one raw -- `fn f(p: bool_node_symbol) -> bool_node_symbol`. - The produced-decl render chain takes a type_binding resolver (produced_decl_render_from_rows and the functions under it). - v2.compiler.emit_produced produced_type_binding resolves, in order: the target's atom realization of a kernel carrier -> that row's surface symbol (target_atom_type_spelling); an explicit binding_spellings entry for the atom; a type the module itself declares (module_declared_type_names) by its own name; otherwise refuses produced_decl_type_ref_unrealized. - v2.extdeps.languages.rust rust_binding_spellings spells the surface symbols the realization rows name: bool, char, String. - Standing, stated in the code: Int still reaches i32 through its explicit binding_spellings entry; the target has no Int atom realization (no integer value-template kind), so its route is not yet unified with Bool's. - produced_decl_support_preserved passes a resolver binding atoms as themselves (its subject is support preservation, not spelling). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d-type signatures, bare bodies
…419-emission-realizations
…ements at the parse; tighten the matrix - program_partition emit_partition passes the base target as realization_host down to emit_produced's type_binding: every atom realization row is bound to the bundle it was authored against (target_atom_realization_bundle_matches_host), and partition_derive_target_for_emit's augmented target matches none, so Bool missed on the emission path although it hits against the base target. - body_lower_type_decl_refinement_name_optional asks the PARSE for the dag_surface_where_refinement_clause production shell (the parse-level form of the by-body where arm, as the record predicate asks for the field block); it was asking for the lowered where edge, which the parse does not have yet. - module_member_emission: the record row now asserts `a: i32` and no carrier name; the payload single variant is a one-arm coproduct and asserts the enum. Matrix (local claim_batch): 9/12 -- Bool signature, bare parameter and literal bodies, refinement classification, anti-spelling record, alias/opaque/generic refusals, coproduct emission pass. Open: struct/enum field types are spelled raw by the semantic-decl emitter; a declared type in a signature is a declaration-reference Conj the signature renderer does not spell. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…target, through one resolver - Struct/enum FIELD types: v2.std.compilers.semantic_decl_emission target_semantic_decl_field_surface_from_edge bound the raw atom (`a: dag_binding_type_int`). It now takes the caller's type_binding (threaded through the struct and enum surface chains) and binds what it resolves; the serialize target lays the profile's derive rows over the HOST target's binding_spellings (semantic_decl_binding_spellings_from_rows_over), so `i32` is spelled by the map that owns it. v2.compiler.emit_semantic_decl emit_semantic_type_decl_resolving is the route the member fold uses; the resolver-less emit_semantic_type_decl stays for the routing/parity fixtures (an atom bound as itself), with no production caller. - Declared-type references: v2.compiler.emit_produced produced_type_binding spells a resolved declaration reference by the target's own DeclarationReferenceForm (target_type_expr_declaration_reference_emitted -- Rust: crate::<module>::<Name>), and every type shape now reaches the resolver. The bare-name declared_types population is deleted: resolved references never needed it. Matrix (local claim_batch, module_member_emission): 12/12. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…sparent alias), classified from their declaration - v2.extdeps.languages.rust rust_refinement_declaration_realization_node: the target-owned row (under target_model_edge_refinement_declaration) naming the four token classes of `type <Name> = <carrier>;` (new rust_token_kw_type lex rule). A transparent alias adds and drops no behaviour: the predicate is discharged at the crossing, and a crossing back to the carrier is realized as the operand unchanged. - v2.compiler.emit_produced emit_refinement_declaration: the member fold supplies the name and the carrier; the row supplies every token class; the carrier is spelled by produced_type_binding (no "i32" here). A target with no row refuses refinement_not_realized; a malformed row refuses realization_malformed (typed Outcomes over v2.std.node_query named_child_lookup, ambiguity refused). - The refinement row is realization metadata like the atom realizations, so target_model_bundle_core_keep_edge filters it from the bundle core the rows are matched against (without that, adding it broke every atom realization). - STANDING: on main a where-refinement's carrier is still its unlowered dag_surface_type_expr parse shell (the lowering gunbc#12407 adds), so the production route refuses emit_module_member_refinement_carrier_unlowered at the carrier; the supplied-carrier row exercises the alias, and the route row flips to asserting it when that lowering lands. Matrix (local claim_batch, module_member_emission): 13/13. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…419-emission-realizations # Conflicts: # src/v2/compiler/emit_produced.dag # src/v2/compiler/program_partition.dag # src/v2/compiler/self_host/candidate_generation.dag # src/v2/test/claim/emit/module_member_emission_test.dag # src/v2/workflow/floor_pure_producer_share.dag
…72955); resolve fixes from main - v2.compiler.body_lowering_fold DeclaredTypeKind = DeclaredRecord | DeclaredRefinement, decided by one predicate (body_lower_type_decl_declared_kind_optional) on the parse. NormalizedTree carries one type_declaration_kinds list in place of record_declarations + refinement_declarations, so no declaration can be named both; ModuleMemberKindConflict and emit_module_member_record_and_refinement_conflict delete. Record names are a projection (declared_record_names / normalized_tree_record_declarations), so the symbol-index fill, census and pattern-binder classifier read one authority. Undecided stays. - rust_signature_general_emit_test (landed on main) passes the resolver the renderer now takes. - type_param_binder_frame_test: the translator twins return Outcome<Node>, not ResolvedTree. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Review 72955: fixed in 79bea35. Record and refinement are now one |
…ate now sees Editing v2.lens.module_graph (record names are now a projection of the declaration kinds) brings the file under the floor's unimported-bare-provider rule. Its ends_with call already resolved to gunbc.rust_item_scan ends_with, its only definition; the import states that binding instead of leaving it to the bare channel or adding a debt row. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…419-emission-realizations
…, by importing it
v2.lens.module_graph now imports gunbc.rust_item_scan { ends_with }, and module_graph is reachable
from four files that carried an unimported bare ends_with (gitignore_emit via
generated_artifact_registry -> ... -> decl_ref_resolution -> module_graph). The floor then read
those pairs as no longer carried (RosterStale). Retiring them as ImportsFixed against unchanged files
would claim a fix that only an eight-hop transitive path supplied, so each file now imports
ends_with itself and its row retires ImportsFixed truthfully. A scan of every other ActiveDebt row
against the before/after import closures finds none newly stale (0 of 1539).
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Review 73071, the |
…ias claim The supplied-carrier refinement claim measured 379,835 eval steps against the 72,300 new-witness budget: its producer builds the Rust target model and emits one member, the same route its enrolled siblings share. It is a nullary pure producer, so it enrols beside them and the claim reads it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…s copy (review 73085) ends_with is owned by std (std.primitives ends_with_contract, std.methods ends_with_method, the std.algebra method row) as a receiver method, and v2 lenses already call it that way (v2.lens.mandatory_tag, v2.lens.machine_shape). path_matches_touched now calls file.ends_with(suffix: target), which is not a bare reference, so the touched-file gate has nothing to refuse. The borrowed import and the four imports plus ImportsFixed retirements it forced revert to main: those rows are not stale once nothing new reaches gunbc.rust_item_scan. A scratch probe confirms both suffix directions match and an unrelated path does not. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Review 73085: agreed, and fixed in da23d6e. |
…th (review 73093) - v2.compiler.emit_semantic_decl emit_semantic_type_decl(name, params, node, target, realization_host) is the only entry; the unresolved route and semantic_decl_type_as_itself delete. produced_type_binding moves here from emit_produced so production and fixtures share it. - produced_type_binding_over(target, spellings) admits an atom only if the map the declaration is SERIALIZED with spells it: the profile's rows over the target's own map, now built by one function (v2.std.compilers.semantic_decl_emission semantic_decl_profile_binding_spellings_over) that the serializer reads too. So no accepted type reaches bound_spelling_from_map's interned-name fallback. - A declaration's own type parameters are admitted by identity against its binder list. - Fixtures that asserted fabricated spellings are corrected: they supplied bare ^Int / ^Diagnostic / ^NonEmptyStr atoms production never emits, and the goldens recorded the interned names (Rust `next_id: Int`, Swift `Int` by coincidence). They now supply dag_binding_type_int: Rust `i32`, Swift `Int32` (new Swift row, the width Rust realizes; Swift's platform `Int` would be a different realization). The Rust staging fixture target carries rust_binding_spellings instead of an empty map. - New discriminating red: semantic_record_with_an_unspelled_field_type_refuses_by_name. Local: 50/50 affected claims hold across the C, Swift, Rust-staging, parity, signature and member suites. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…419-emission-realizations # Conflicts: # src/v2/std/compilers/target_model.dag
After merging main, the production route (parse, normalize, emit) emits `type Pos = i32;` for a where-refinement member, so the claim that asserted the carrier_unlowered refusal is the red it was written to flip into: it now asserts the alias on the real route, the inhabitance claim for the supplied-carrier row. The carrier guard stays (a shell carrier still refuses by name); its comment no longer says main cannot lower it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Review 73093: agreed, fixed in f5a293b.
— sent from silent-swift-419 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
APPROVE-MERGE at exact head f5a293b6fc07e96c2b1d3e4441ad590ab84306f4, contingent only on emit-build turning green on this same SHA.
The review-driven rework resolves the design concerns from the earlier draft.
-
Type spelling now has one semantic route. produced_type_binding / produced_type_binding_over first handles resolved declaration references through the target's declaration-reference form, then atom realizations, then an explicitly present binding-spelling row, else refuses produced_decl_type_ref_unrealized. Semantic declaration fields/variant payloads use this same resolver; the old "bind the type atom as itself and let interned spelling save it" route is gone. The new unspelled-field RED directly pins the fail-closed behavior. Bool now reaches Rust's surface symbol through the atom-realization row and the serializer's map spells it as bool. Int remains explicitly documented as the current exception: Rust has no Int atom-realization row, so it reaches i32 through its explicit binding spelling rather than being falsely claimed unified.
-
Bare Atom bodies now go through target_value_expr_project_atom_in_arrow_scope, the same scoped atom projection nested operands already use. The real closure-emission claims distinguish bare parameter and bare bool literal output.
-
Record/refinement classification is now one positive source fact, not two potentially conflicting sets and not a lowered-shape heuristic. body_lower_type_decl_declared_kind_optional produces exactly one DeclaredTypeKind arm per declaration; NormalizedTree carries type_declaration_kinds; record-only consumers use the projection normalized_tree_record_declarations; closure emission carries the full declaration-kind channel alongside InferredTree. The anti-spelling record control remains meaningful, and the payload-bearing single-variant case follows its actual lowered Disj form rather than being inferred as refinement from "not record".
-
Refinements are realized through a target-owned declaration row. Rust's row describes a transparent alias and leaves carrier spelling to produced_type_binding; the module fold contains no hard-coded i32 spelling. The production closure route now emits
type Pos = i32;and the supplied-lowered-carrier control independently exercises the realization arm. No newtype semantics or silent declaration erasure is introduced.
The base-vs-augmented-target distinction is also handled explicitly: emission uses the derived target for program-specific ownership/value semantics while atom/declaration realizations are looked up against the base realization_host, avoiding a false bundle-content-hash miss.
The exact-head floor selected the combined surface broadly and shows the discriminating module-member claims planned-and-passed: Bool signature, declared-type signature, bare parameter/literal bodies, record emission, refinement alias emission, anti-spelling record, coproduct/payload variant, plus the semantic unspelled-field refusal. required-CI adjudication passed. I did not independently rerun the reported per-item local mutants; their discriminators are present in the exact-head tests.
Current exact-head checks: floor=success, generated=success, witnesses=success, emit-build=queued. GitHub reports the PR mergeable. No code/design blocker remains; enqueue/land once emit-build is green and the head is unchanged.
1 participant
Combined PR for coercion follow-ups 1-4 (runners are scarce, so one PR with one commit per item).
produced_type_binding). The order is: declaration reference (DeclarationReferenceForm), then atom realization, then an explicit binding spelling, else a typed refusal. Atom rows are resolved against the base target (realization_host), because the partition's augmented bundle does not match their content hash.{ x },{ true }) emit through the arrow-scope atom projection.refinement_declarationsbesiderecord_declarations). If neither fact holds, the member refuses as undecided; if both hold, it refuses as a kind conflict.type Pos = i32;. On main the carrier is still an unlowered parse shell, so the production route refusesemit_module_member_refinement_carrier_unlowereduntil v2: coercion admits refinement-to-declared-carrier casts as Widened #12407 lands. A claim with a supplied, already-lowered carrier exercises the alias itself.Evidence:
module_member_emission_testpasses 13/13 locally (claim_batch).🤖 Generated with Claude Code