Repository navigation
target_model: Optional Bind separator; dag emits a Bind block-scoped (ahead of #13056's let-in drop) - #13099
Merged
Conversation
…scoped, { let k = (v) { b } }
Operator/parent ruling (stern-bear-500, ruling A): ahead of the dag
grammar dropping 'let x = e in body' (#13056), TargetBindLetShape.in_token
becomes Optional<Symbol>. C/Rust/TypeScript keep Present(';'); dag
declares Absent and a core Bind is emitted as a block whose first
statement is the binding and whose last is the body: the value is
parenthesised and the body braced so no continuation of the value can
absorb the body, and the outer braces give the binding a statement
position wherever the Bind stands. Absent travels in the projection
bundle as its own atom, so a bundle missing the field still refuses.
The dag bind family's tokens and authority text move to that spelling.
Controls (v2.test.emit.dag_bind_let_block_scoped): a Bind nested as the
value of a Bind, and bodies that are a bare name, an empty brace literal,
a '-'-led expression and a nested Bind, each emitted through the dag
projection and reparsed by the dag grammar to the same binds.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…model per claim Floor refused the five round-trip claims on cost (74-112k against 72.3k). Each now renders with the dag lex rules and the two spellings its tokens bind instead of building dag_bind_target_model, and parses the emitted text as the dag grammar's expr production over the shared prepared grammar instead of a module around it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Review 74695, the two points it raised without blocking:
Pushed c4cd047: the five round-trip claims were over the floor's new-witness budget (74–112k against 72.3k). Each now renders with the dag lex rules instead of building the target model per claim, and parses its expression as the — sent from eager-crab-610 |
…quence, not text
Floor: the round trips were still 72-105k against 72.3k. The emitter's
product is a token sequence, so each claim now hands those tokens to the
expr production directly (no render, no lexer). The previous text route
also passed for the wrong reason: dag text rendering puts no separation
between tokens ({letx=(a){x}}), and 'letx = (a)' re-read as a bare
assignment let. a_single_bind_emits_block_scoped_tokens pins the exact
token sequence instead; the rendering defect predates this change and is
reported separately.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… once (warm producer) The nested-value and nested-body claims parsed ~21 tokens each (87-105k steps). They are replaced by two composition claims (the emitter places a Bind's tokens verbatim in the value group and the body block) and two slot parses (a Bind inside a value group, a Bind as a body statement), which with the lone-Bind parse cover nesting in a context-free grammar. The five parses run once in dbl_verdicts, enrolled warm in floor_pure_producer_share; claims read stored Bools. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
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
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.
Lands before #13056, under stern-bear-500's ruling A on #13056 (the audit's drop of
let x = e in bodystands). The shared target model changes first, then its consumer.Why
#13056 drops
let x = e in bodyfrom the dag grammar. The dag target model'slet_formhadin_token: kw_in, so the shared emitter (v2.std.compilers.target_modelbind_let_value_producing_tokens) wrote every core Bind aslet x = v in b. The grammar would no longer read that text.Change
TargetBindLetShape.in_token: Optional<Symbol>.Present(;). It usesValueProducing, so it takes the separated path, unchanged.Present(…). Both emitStatementSequenced, which never readsin_token.Absent.{ let k = (v) { b } }, using the target's own block (closure_form.body_*) and group (primitive_apply_form) delimiters (bind_let_block_scoped_tokens). Ruling condition (2) asked me to choose between emitting and refusing. I chose emitting, because the form is sound for every value and every body, so no case needs a refusal:)into a block, so the value cannot absorb the body;Absentas its own atom (^target_bind_let_no_separator), never as a missing field, so a bundle that lost the field still refuses at decode (§5).dag_bind_concrete_tokens,dag_bind_source_text,dag_bind_wrong_value_source_text) move tofn one() -> Int { { let x = (1) { x } } }.Controls
v2.test.emit.dag_bind_let_block_scoped. Each case is emitted throughbind_let_value_producing_tokenswithdag_value_expression_projection. The emitted token sequence is then parsed by the dag grammar'sexprproduction, where a value is owed, over the shared prepared grammar. Each must give one tree with the same binds:lets, one inside the other, and nointoken);{}, a--led expression, and a nested Bind. None reads as a literal, so the spelling stands without a guard.a_single_bind_emits_block_scoped_tokenspins the exact emitted token sequence{ let ident = ( ident ) { ident } }.Why tokens, not text. The dag target's text rendering puts no separation between tokens: its lex is
dag_lex()and it declares no emit transforms. So a Bind renders as{letx=(a){x}}, andletxlexes as one identifier. An earlier text-based version of these claims passed for the wrong reason:letx = (a)re-read as a bare-assignmentlet. That rendering defect predates this PR, has been reported to stern-bear-500 separately, and is not fixed here.Run locally on a remote build, all green:
bind_round_trip(bind_emit_matches_serialize_holds,bind_ingest_via_coerce_matches_canonical) andbind_emit(2): dag family emit equals serialize;rust_bind_let_emit_holdsand_wrong_value_discriminates(exact{ let x = 1; x });ts_bind_let_iife_emit_exact_holds,ts_bind_let_mode_perturbation_flips_holds, plusdag_loop_value_producing_emits_holdsanddag_closure_value_producing_emits_holds;bind_tail_is_an_expression(3).C has no bind emission fixture to byte-compare. Its emission cannot change, because
StatementSequencednever readsin_token; I'm saying so rather than inventing a fixture.Notes
🤖 Generated with Claude Code