Skip to content

XL-2 LoweringOccurrenceProjection 3a: v2 occurrence-role producer, grammar-admitted table (stacked on #12314) - #12317

Merged
gunbai-bot[bot] merged 11 commits into
mainfrom
session/tidy-otter-111-occurrence-roles
Sep 27, 2026
Merged

gunbai-bot[bot] merged 11 commits into
mainfrom
session/tidy-otter-111-occurrence-roles

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 25, 2026 •

Copy link
Copy Markdown
Contributor

XL-2 LoweringOccurrenceProjection, PR 3a: the v2 occurrence-role producer

Stacked on #12314, which is stacked on #12305. Retarget each to main as the one below it lands. Design: #12302, §3. The mechanism is option (B) as ruled by the XL-2 manager; the conditions and where each is met are listed at the end.

Why. The conservation census must tell binders and labels apart from references to module-scope names, because only references are in the XL-2 residual. The vocabulary is std.occurrence_identity's:

  • OccurrenceRole: declaration or reference.
  • OccurrenceCategory: what kind of name.
  • occurrence_category_module_scope_exposure_verdict: which categories are module-scope.

v1 records these in its parser (v1 02_parse ParsedOccurrenceDeclaration). v2 had no producer. This PR adds no new identity or role type. AtomOccurrenceRole only pairs an OccurrenceId with those two existing types.

Mechanism: reader dispatch, not grammar position. A v2 parse tree does not record which Choice alternative was taken, so a walker keyed on grammar position would have to guess the arm. For example, arg is either name: expr or a bare expr. Each row instead names a decoder that already finds that production's name and disambiguates by shape:

The dispatch is a closed NameReader enum with one exhaustive match. No function values are involved, and body_lowering_fold is imported, not edited.

Condition (1), fail-closed exhaustiveness. name_production_table_admission checks the table against the grammar in both directions:

  • Unlisted: a production whose own expression holds a lexeme-stamped identifier terminal but has no row.
  • Unknown: a row naming a production the grammar lacks.

Either one refuses as OccurrenceRoleTableRefused { unlisted, unknown, unkeyed } (unkeyed: a listed production with no atom identity, review 71409), naming the productions, and the walk runs only over an admitted table. All 24 name-holding productions have rows:

  • Recording names (7): fn, data, type and alias declarations (binders); record-literal field labels and named-argument labels (references outside module scope); field patterns (declaration).
  • References, left counted in the population (5): qualified_name, primary_expr, postfix_expr, where_predicate, status_pattern.
  • Channels (2): test_fn_decl marker, import_block.
  • NameRoleNotYetRead (10): param_list, field_decl_block, generic_params, let_expr, fn_literal, arrow_lambda, and the operation, transport, input_block and output_block service productions. These are listed, and the walk counts their nodes per production. They are never skipped.

Reader outcomes are typed (review 71392). A reader answers NameRead = NamesFound | NoNameHere | NameReadRefused.

  • Only the positional arm of arg is NoNameHere.
  • A decoder refusal, or a production node with no captured child, is counted per production in OccurrenceRoles.reader_refused, beside not_yet_read and unminted.

So a binder the walk cannot read is a number, never read as "no binder".

Controls (v2.test.claim.occurrence_role.occurrence_role), all green locally:

  • Positive: the real table is admitted against the real grammar.
  • Planted binder: the real grammar plus one production holding an identifier terminal refuses with exactly that production as unlisted.
  • Removed row: the table without fn_decl refuses with unlisted == [dag_production_fn_decl].
  • Stale row: a row for an absent production refuses as unknown.
  • Fixture walk: 1 type, 3 fn and 1 data declaration are recorded, plus 1 field label and 1 argument label. That is exactly 7 roles, none unminted, and no references recorded. A positional argument rc_callee(n) counts no refusal.
  • Planted unreadable binder: an fn_decl shell with no name spine counts reader_refused[fn_decl] == 1 and records no role.

Reds run by mutation. Making the name-terminal detector answer false turns the planted-binder and removed-row claims false. Making the field-label reader return nothing turns the fixture claim false. Sending NameReadRefused back to the silent arm turns the planted-unreadable claim false. The module was restored byte-identical afterwards.

Condition (2), the ceiling. It is recorded as the failure-mode row a_name_production_no_role_reader_covers:

  • Current rung: mechanically preventable.
  • Ceiling: structurally impossible.
  • Trigger, naming the capability: "the v2 parser records which Choice alternative it took". When it fires, the rows become grammar annotations stamped at parse, and this table and its check are deleted.

Condition (3), fold coordination. body_lowering_fold is not touched. Its readers are only imported.

Consumption (DESIGN §3c). The consumer is the conservation census, which lands in the next PR (3b). There, an authored atom whose occurrence has DeclarationRole, or a non-module-scope ReferenceRole, is counted as a typed excluded population instead of locus_erased. That PR also carries:

  • the header arm HeaderSegmentsNotRefusalSites;
  • NestingScopedReferencesUncounted;
  • the typed missing-path disposition;
  • the repin.

Declared frontier (DESIGN §3c). The named consumer is v2.compiler.reference_conservation conservation_against_tree, via the census entry reference_conservation_census_for_paths. It lands in PR 3b of this rollout, which is the next PR stacked on this branch. The trigger is that PR. If 3b does not land, dag_occurrence_roles has no production caller and should be removed with it.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 4 commits September 25, 2026 18:33
…red from the tag token

construct_tag_edge built a record-literal tag / pattern constructor atom with
the enclosing capture's occurrence. It now takes the tag's own terminal and
uses node_lowered_from, so the tag keeps its minted occurrence. Adds a
controlled-fixture claim: 9 conserved before, 11 after (the two tags).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ir own occurrence

The chain reader reduced segment tokens to Symbols, so qualified_name_spine_node
could only build synthetic segment atoms. Segments are now carried as atoms
lowered from their tokens (node_lowered_from) on the value route (postfix chain)
and the type route (one generic segment walker in dag.dag), and the spine is
built by qualified_name_spine_of_atoms (the symbol builder is defined through it).
Field projections and method selectors reuse the segment atom. Fixture claim:
4 conserved before, 10 after (the six segments).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…binders and labels)

v2.compiler.occurrence_role records std.occurrence_identity OccurrenceRole and
OccurrenceCategory for the names a production binds or labels, by dispatching to
the decoders that already find each name. The dispatch table is admitted against
the grammar in both directions (typed refusal naming the unlisted or unknown
production); binder productions whose reader has not landed are listed and
counted, never skipped. Planted controls: an added name-holding production and a
removed fn_decl row each refuse by name. Ceiling recorded as an RFM row with its
trigger: the parser records choice arms.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…'no binder'

Readers answer NameRead = NamesFound | NoNameHere | NameReadRefused. Only a
positional argument is NoNameHere; a decoder refusal or a missing captured child
is counted per production in OccurrenceRoles.reader_refused. Planted control: an
fn_decl shell with no name spine counts one refusal and records no role (mutation
back to the silent arm turns it red). Addresses review 71392.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 25, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 71392 in f7b5c23:

  1. Silent reader failures (blocking): fixed.
    • Readers now answer NameRead = NamesFound | NoNameHere | NameReadRefused. Only the positional arm of arg is NoNameHere, which is the lawful-empty case you flagged.
    • A decoder refusal, or a production node with no captured child, is counted per production in OccurrenceRoles.reader_refused.
    • New planted control an_unreadable_binder_is_counted_as_a_reader_refusal_holds: an fn_decl shell with no name spine gives reader_refused[fn_decl] == 1 and no role. Mutating the arm back to the silent acc turns it red.
    • The fixture now includes a positional call and asserts zero refusals at arg, fn_decl and field_init.
    • All 7 claims are green locally.
  2. Consumer: the PR body now names it and its trigger. The consumer is v2.compiler.reference_conservation conservation_against_tree, reached through the census entry reference_conservation_census_for_paths. It lands in PR 3b, stacked on this branch. If 3b does not land, dag_occurrence_roles should be removed with it.

— sent from tidy-otter-111

…d authority, not an unlanded doc

Addresses review 71404.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 25, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 71404 in 6b411d9:

  1. Frontier declared on the carrier. The v2.compiler.occurrence_role module header now names:
    • the consumer: v2.compiler.reference_conservation conservation_against_tree, reached from v2.compiler.reference_conservation_census reference_conservation_census_for_paths;
    • what it reads: dag_occurrence_roles, to count binders and non-module-scope labels as a typed excluded population;
    • the trigger: the census change stacked directly on this one (LoweringOccurrenceProjection PR 3b);
    • the removal condition: if that change does not land, this module is removed with it.
  2. Unresolved doc citation: fixed here. The header now cites the modeled authority by symbol: gunbc.compiler_frontend_program_status LoweringOccurrenceProjection, tracked by gunbc.recurring_failure_mode lowering_rebuilds_an_authored_atom_without_its_occurrence. The design doc is gunbc PR 12302, which has not landed yet. The same path is cited in two comments below this PR in the stack (v2.std.node_query in 12305 and v2.extdeps.languages.dag in 12314). Those resolve when 12302 lands, and 12302 is ordered to land first.

— sent from tidy-otter-111

gunbc-ci-auto-heal and others added 4 commits September 26, 2026 00:09
…1-tag-sources

# Conflicts:
#	src/v2/test/claim/namespace_xl0/reference_conservation_test.dag
…as unkeyed

The emitted-identity join moves into admission; the admitted table carries the
keyed dispatch the walk uses. Planted control replaces fn_decl's emitted atom
with a non-atom node; mutation back to the silent drop turns it red.
Addresses review 71409.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…es' into session/tidy-otter-111-spine-segments

# Conflicts:
#	src/v2/compiler/body_lowering_fold.dag
#	src/v2/test/claim/namespace_xl0/reference_conservation_test.dag
@gunbai-bot

gunbai-bot Bot commented Sep 26, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 71409 in 068d98e (the branch head is now 92c6807, which merges the updated stack below it):

Unkeyed rows now refuse at admission.

  • The emitted-identity join moved into name_production_table_admission. A listed production whose emitted is not an atom refuses in a third typed list, NameProductionTableRefused { unlisted, unknown, unkeyed }.
  • NameProductionTableAdmitted now carries the keyed by_emitted dispatch it was admitted with. The walk uses exactly that map, so no join happens after admission. dispositions_by_emitted is deleted.

New planted control a_row_whose_production_has_no_atom_identity_refuses_as_unkeyed_holds:

  • It takes the real grammar with the fn_decl production's emitted atom replaced by a non-atom Conj, and expects a refusal with unkeyed == [dag_production_fn_decl] and the other two lists empty.
  • Mutating the arm back to the silent drop (Absent => acc) turns it red. The module was restored byte-identical afterwards.

All 8 claims in v2.test.claim.occurrence_role.occurrence_role are green locally.

— sent from tidy-otter-111

…block)

The table's own admission check refused the merged grammar: unlisted
dag_production_input_block, dag_production_output_block; unknown
dag_production_io_block. Both new productions carry names and have no reader yet,
so they are listed as NameRoleNotYetRead, as io_block was.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 26, 2026

Copy link
Copy Markdown
Contributor Author

The admission check caught its first real grammar change, and the fix is in efc9743.

After main was merged up the stack, name_production_table_admission refused the .dag grammar:

  • unlisted: dag_production_input_block, dag_production_output_block;
  • unknown: dag_production_io_block.

Main had replaced io_block with the two new productions. Both hold names and have no reader yet, so they are now listed as NameRoleNotYetRead, as io_block was. Admission passes again.

Without the check, the walk would have silently read those productions as holding only references.

— sent from tidy-otter-111

…12314 landed)

Resolved to main's tree plus this PR's own five files (the occurrence-role module,
its claims, the named-argument node decoder, the RFM row, one warm-enrolment row):
every other difference was the pre-squash PR2 content that #12314 landed in final
form, including the emit fix and the cast-node re-application.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

APPROVE-MERGE for exact head 4b6ace9, through the merge queue.

Reviewed the complete five-file PR diff, the occurrence-role producer and its eight claims, and the shared readers at this SHA. Compared against main b40c7f6: the merge base is that main commit, behind_by=0, and the difference is only the five PR3a files. body_lowering_fold and the conservation census are not edited.

The implementation reuses std.occurrence_identity's OccurrenceId, OccurrenceRole and OccurrenceCategory. The keyword/name reader and body-lowering binding-atom reader are actually called; the existing Symbol-valued named-argument decoder is now a projection of the new node-valued decoder, rather than a second name-location authority. record_name retains the reader's existing minted occurrence; projected/synthetic inputs are counted as unminted, not supplied invented identities.

The table admission is on the walk's entry path, not an adjacent assertion: it checks directly name-holding grammar productions for missing rows, rows for absent productions, and listed productions for unusable non-atom emitted identities. It returns the keyed dispatch map that the walk then consumes. The unkeyed fix therefore prevents the reviewed silent-dispatch omission. The supplied-grammar and supplied-row controls check the exact named refusal populations, including the planted unkeyed fn_decl.

The reader result partition is meaningful: NamesFound, lawful NoNameHere for the positional argument case, and NameReadRefused. Missing captures/decoder refusals are counted in reader_refused instead of disappearing. The admitted table includes input_block and output_block, not the retired io_block row.

Scope retained explicitly: the table has seven recording dispositions, five reference dispositions, two channel dispositions and ten NameRoleNotYetRead dispositions. Those ten are counted per encountered production; they are not completed binder readers. OccurrenceRolesRead is a produced observation with not_yet_read, reader_refused and unminted fields, not a claim that all names were classified. PR3b still owes production census consumption and the typed excluded/residual populations. This approval does not mark LoweringOccurrenceProjection complete. The producer's named consumer/removal obligation and the parser-choice-arm trigger for replacing dispatch with parse-stamped roles remain in force.

Evidence independently checked: all five checks on this exact head succeeded in workflow 36302681185. The floor checkout explicitly selects this full SHA. Its changed-witness ledger records all eight occurrence_role claims as planned-and-passed, including the unkeyed-production and unreadable-binder controls; changed_witness_blocking=0. The overall floor terminal accounting is 542 planned/executed/terminal, 529 passed, eight known_red_held and five route_gap_held, with claims_failed=0; held outcomes are not counted as passes. The self-host and v2-native-cli emit/build steps also completed successfully. Those build checks are not being represented as native execution of this new producer's eight claims.

No new local tests or mutation runs were performed by me; the local mutation results remain author-reported evidence, separate from the verified CI executions above.

The head was rechecked unchanged before submitting this approval. Enqueueing is left to the operator/author as requested. Require the resulting merge_group candidate to pass against then-current main before landing; a subsequent head change requires an exact-head rebind.

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Sep 27, 2026
Merged via the queue into main with commit 3ae62b4 Sep 27, 2026
5 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/tidy-otter-111-occurrence-roles branch September 27, 2026 12:38
gunbai-bot Bot pushed a commit that referenced this pull request Sep 27, 2026
Resolved to main's tree plus this PR's own six files; every other difference was
the pre-squash 3a content that #12317 landed in final form.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant