Repository navigation
N7 text crossings: route every bare chars/chars_to_string in the N7 closure through the declared conversion plan - #13151
Merged
Merged
Conversation
…e corpus's unicode scalar plans DESIGN section 4 (2026-09-26 ruling): an author crosses a boundary implicit coercion refuses only by selecting a named conversion plan. ConversionPlan joins the explicit-cast surface and the declared LiteralUnfolding routes; gunbc.structural_realization_bindings conversion_plan_rows declares unicode_scalar_unfold (kernel String -> FreeMonoid<Char>) and its inverse unicode_scalar_fold. judge_conversion_plan answers a site that names a plan, keyed on declarations; controls are driven by supplied plan references until the surface syntax is ruled. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…r identity readings Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…gs mirrors Copied from claim_executor --required-regen's candidate tree at bb2120c. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ode_scalar_unfold / unicode_scalar_fold Per the ruling there is no grammar change: each ConversionPlan row names an ordinary declared function by declaration identity (route), and a call is admitted as the named route because a row names the callee. The judgment is keyed on the callee's declaration. The two route functions are declared in std.coercion; their bodies realize the row's single phase. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…irrors for the route functions Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…losure through the declared conversion plan tokenize's ingress, std.source_annotation's host-lexeme convenience, the LexRule helpers (dag.dag, lexing), integer's digit reader and dag.dag's string-literal scalar readers call std.coercion unicode_scalar_unfold; the token lexeme, target_model's fixed-spelling and escape writers and its code-point Symbol call unicode_scalar_fold. Each is a crossing between a bare String (read as host text by both checker and renderer today, see test.claim.bare_imported_text_reading_witness_test) and a structural FreeMonoid<Char> position, so each now names its route instead of a bare kernel name v2 resolve cannot see. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ingHasNoImplicitRoute) Under operator ruling O5 a conversion plan is selected by calling the function its row names, so the checker's identity-keyed text-crossing refusal now carries that function as its residual: unicode_scalar_unfold when the produced side is host text, unicode_scalar_fold otherwise. Blocking, like the TypeMismatch it replaces at the two text-crossing sites. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…route consumers and TextCrossingHasNoImplicitRoute Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…KernelMinted, not a std.types declaration The floor's declarations phase refused decl_ref(std.types, String): the kernel String has no declaring module (TypeDeclarationProvenance KernelMinted). ConversionEndpoint = KernelMintedCarrier | DeclaredCarrier names each carrier the way it is actually identified. The controls' phantom citations (Int, utf8_bytes, hollow_route) now cite real declarations. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…dpoint Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…umer stated as a frontier (review 75096) A plan with no phase now has no constructor, so ConversionPlanHasNoPhase and its control are gone (DESIGN 5, construction over validation); a composite plan is the trigger for a non-empty phase sequence. The judgment's consumer -- the kernel-crossing wall in v1.compiler.infer, ruled the last step of the lane -- is stated beside the declaration with its trigger (DESIGN 3c declared frontier). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…hase plan Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…_scalar_fold's phase (calm-boar-904 ruling) Authority is now the declared route function; the .dag body stays required, because a from_code_point/concat fold is quadratic, and it lands with a linear .dag text writer. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…g.dag): keep both imports Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…phism row; identity derived from route (calm-boar-904's #13143 objection) A plan stored route, endpoints and phase independently while the judgment checked only endpoints, so an unfold route carrying the inverse phase was admitted. Now ConversionPlan is { route, phase }, a phase carries the full LiteralHomomorphism row, source/target are derived (the inverse reverses them), and the identity is route.decl_name (O5: the function IS the plan). literal_homomorphism_rows and conversion_plan_rows share one declared row, unicode_scalar_literal_homomorphism. Mutation control: the unfold route with the inverse phase refuses. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d endpoints Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…td_core mirror to be regenerated)
…xtCrossingHasNoImplicitRoute) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…oolean literal row; bindings mirror to be regenerated)
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…s to be regenerated)
…the carrier Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d the named call is admitted (review 75433) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ent (census fixtures cannot supply std.coercion's bare channel) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Addressed review 75433 in c7bc26e. Three claims were added to
Separately, three pre-existing wall claims ( |
…infer mirror to be regenerated)
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…n, no wildcard (sharp-raven-357's objection) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… (body comments do not parse) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Oct 4, 2026
Both conflicts were #13287's own changes, already on main: the generated v1_compiler_emit_rust.rs mirror and 05_emit_rust.dag now equal main's exactly, so #13294 no longer touches v1 and main's regen fixed point covers it; tokenize_prepared takes main's unicode_scalar_unfold ingress (#13151). 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.
Stacked on #13143; the base retargets to main when it lands. This is the consumer switch for operator ruling O5.
What: every bare
chars/chars_to_stringin the N7 closure (tidy-raven-393's scan of the 141 closure files, plus target_model's code-point Symbol) now calls the declared route instead of a kernel name v2 resolve cannot see:compiler.01_tokenizetokenizeingress;std.source_annotationadvance_line_prefix_indent_only_text;std.compilers.lexingphrase_to_lex_rule_set;std.integerinteger_string_to_decimal_digits_optional;extdeps.languages.dagLexRule helpers ×2 (N7 occ 1093838) anddag_string_literal_body_optional/_encoded; target_modelapply_emit_spelling_quote.01_tokenizetoken lexeme ×2 (N7 occ 506352); target_modellex_pattern_fixed_spelling×2,apply_emit_spelling_quote's escaped result, and the code-point Symbol.Why each is a genuine crossing:
test.claim.bare_imported_text_reading_witness_test(#13150) measures that a bare-importedStringreads as host text in the checker, and the renderer agrees. Every site therefore moves a host value into a qualifiedv2.std.text.String/List<Char>position, or the reverse. (#13140 is closed because deleting these calls was not an identity.)Still to do in this PR before ready:
std.source_annotation(regen running).unicode_scalar_unfold/unicode_scalar_fold, and the route call is judged throughjudge_text_conversion_plan.gunbc.primitive_egresschars_to_stringas the realization ofunicode_scalar_fold's phase.🤖 Generated with Claude Code
Exhaustive route match (sharp-raven-357's objection, zero-ambiguity ruling):
v1.compiler.infertext_crossing_or_type_mismatch_errorno longer has a wildcard arm. It matches eachTextRepresentationvariant explicitly:HostTextnamesunicode_scalar_unfold;CodePointSequencenamesunicode_scalar_fold;NotText/TextRepresentationUnidentifiedname no route and keep the plain type mismatch.A later variant now fails this match at compile time instead of being silently advised to call the fold. The seed mirror is regenerated from the
.dag.