Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module gunbc.recurring_failure_mode.a_wildcard_match_arm_resolves_as_an_unbound_name

import std.types { NonEmptyStr }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data a_wildcard_match_arm_resolves_as_an_unbound_name: RecurringFailureMode = RecurringFailureMode {
Expand All @@ -12,7 +13,15 @@ data a_wildcard_match_arm_resolves_as_an_unbound_name: RecurringFailureMode = Re
"HOW IT SURFACED: the XL-2 if-arm repair (`v2.compiler.body_lowering_fold` `body_lower_if_arm_lowered`) made a match inside an if-arm reach resolve for the first time. On main such a match was dropped whole by the operand reader, so `if c { s } else { match s { BlgA => .. _ => .. } }` resolved; after the repair it refuses at `_`, the verdict the same match already had at the top level of a fn body. The repair did not create the refusal; it stopped hiding it.",
"CLASS: a resolve defect, not a lowering one: a wildcard pattern binds nothing and names nothing, and a resolver that looks it up as a symbol has conflated a pattern form with a reference. RUNG FOUND AT: a located refusal (mitigation) -- the wrong answer is loud, never silent, but a correct program is refused. CEILING: structurally guaranteed -- the wildcard is a distinct pattern constructor in the lowered tree, so the resolver can decline to look it up by construction. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: the lowered pattern carries the wildcard as its own form that resolve does not treat as a reference, with a witness whose red is this specimen on main and whose control is a match exhaustive through named arms only.",
"REPAIRED AT THE RESOLVE LINK, TRIGGER NOT MET (2026-09-25, on 69e0bb7566e): the earliest wrong link was `v2.compiler.resolve` `resolve_pattern_node_walk`, which recognized `_` only as a constructor FIELD's target and sent a bare arm pattern to `resolve_node_walk` as a reference; it now recognizes `_` at every pattern depth. Witness `v2.test.claim.namespace_xl0.wildcard_arm_resolve`: `a_match_exhaustive_through_a_wildcard_arm_resolves` and `an_undeclared_name_in_a_wildcard_arm_body_is_the_sole_refusal_at_its_atom` false on main, true on head; the field-wildcard and named-binder controls true on both. MEASURED CENSUS BEHAVIOUR: on main the `_` refusal refused the whole module as its own chain ahead of any body refusal (`first=_ +wc_undeclared_body`), with observation COMPLETE -- it never marked the match or module incomplete, it added a spurious chain; on head the body name is the sole chain, observation complete. THE ROW STAYS OPEN because its trigger names a capability not delivered: the lowered pattern still carries the wildcard as an ATOM SPELLED `_`, recognized by `pattern_wildcard_name` at resolve, not as its own pattern form; that construction lives in `v2.compiler.body_lowering_fold`, which this repair did not touch.",
"THE WILDCARD NO LONGER SHARES A SPELLING WITH ANY NAME; THE TRIGGER IS STILL NOT MET (XL-2, gunbc#12597). `v2.compiler.body_lowering_fold` `body_lower_pattern_atom_form` lowers an authored `_` pattern, whether a bare arm or a constructor field's target, to `v2.std.node_query` `wildcard_pattern_identity`, at the `_`'s own occurrence. That is an Atom whose identity `<wildcard-pattern>` no authored name can spell, because `<` is not an identifier character; this follows the `v2.std.anonymous_binder` precedent. `is_wildcard_pattern` is the one recogniser, and three readers consult it: `v2.compiler.resolve` (`resolve_pattern_node_walk`, `resolve_pattern_binders`), `v2.compiler.reference_conservation` `occurrence_spelling_conserved`, and `v2.std.compilers.target_model` `bound_spelling_from_map`. `pattern_wildcard_name` is now the AUTHORED spelling only. WHAT THIS ESTABLISHES: no authored name can collide with the wildcard, and on the resolve path it is kept and never looked up. That is mechanically preventable, with the rung held at the readers that call the recogniser and executed by the witnesses below. WHAT IT DOES NOT ESTABLISH: the form is still an Atom connective distinguished by its identity, so a reader that does not call `is_wildcard_pattern` still receives a named atom. The rung is the minimum across paths, so it is not structurally guaranteed. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: the lowered pattern is read through a typed pattern carrier whose wildcard is its own variant, so that EVERY reader of a match arm's pattern matches that carrier exhaustively and none can receive the wildcard as a name. A new core connective is not the route, because the six-connective vocabulary is closed (DESIGN section 4). WITNESS `v2.test.claim.body_lowering.wildcard_pattern_form`: the bare-arm and field-wildcard claims are false with main's lowering and true on head, and the nullary-constructor and binder controls are true on both. MUTATION: head's lowering with main's resolve reds `wildcard_arm_resolve` `a_match_exhaustive_through_a_wildcard_arm_resolves`. The field-wildcard resolve claim stays green under that mutation, because main's resolve bound an unrecognised field atom as a binder, so the lowering witness is that case's discriminator.",
],

evidence: [],
evidence: [
DeclarationRef { module_path: "v2.test.claim.body_lowering.wildcard_pattern_form", decl_name: "a_bare_wildcard_arm_lowers_to_the_wildcard_form", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.claim.body_lowering.wildcard_pattern_form", decl_name: "a_wildcard_constructor_field_lowers_to_the_wildcard_form", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.claim.body_lowering.wildcard_pattern_form", decl_name: "a_nullary_constructor_arm_stays_its_named_atom", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.claim.body_lowering.wildcard_pattern_form", decl_name: "a_binder_arm_stays_its_named_atom", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.claim.namespace_xl0.wildcard_arm_resolve", decl_name: "a_match_exhaustive_through_a_wildcard_arm_resolves", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.claim.namespace_xl0.wildcard_arm_resolve", decl_name: "an_undeclared_name_in_a_wildcard_arm_body_is_the_sole_refusal_at_its_atom", field: WholeDeclaration },
],
}
22 changes: 9 additions & 13 deletions src/v2/compiler/03_resolve.dag
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,7 @@ import v2.std.node_query {
construct_field_edges,
construct_tag_optional,
find_named_child,
is_wildcard_pattern,
pattern_wildcard_name
}
import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceId }
Expand Down Expand Up @@ -1526,7 +1527,7 @@ fn resolve_pattern_binders(ctx: ResolveContext, pat: Node, acc: Map<Symbol, Symb
fold(construct_field_edges(n: pat), init: acc, f: fn(m, e) {
match e.target.kind {
TypeNode { connective: Atom { identity: id } } =>
if id == pattern_wildcard_name() {
if is_wildcard_pattern(pattern: e.target) {
m
} else if resolve_pattern_atom_names_constructor(ctx: ctx, id: id) {
m
Expand All @@ -1540,7 +1541,7 @@ fn resolve_pattern_binders(ctx: ResolveContext, pat: Node, acc: Map<Symbol, Symb
}

// The pat resolves under the ARM frame: the tag and any nested constructor resolve as
// references, a binder answers BoundInFrame and stays itself, and `_` is kept as it is.
// references, a binder answers BoundInFrame and stays itself, and the wildcard is kept as it is.
//
// THESE ARE WALKS, ON gunbc#12116's CHILD WALK (XL-2 P4). A pattern, an arm and a match each fold
// their children through child_walk_step and close with child_walk_node, so every independent
Expand All @@ -1550,18 +1551,13 @@ fn resolve_pattern_binders(ctx: ResolveContext, pat: Node, acc: Map<Symbol, Symb
// come from resolve_pattern_binders over the pattern's SYNTAX and the symbol index, before the
// fold runs, so a refused pattern does not leave the body under an invented scope and no site is
// marked unobservable (P4's one exception, a Bind's binder, has no counterpart here).
fn resolve_pattern_is_wildcard(pat: Node) -> Bool {
match pat.kind {
TypeNode { connective: Atom { identity: id } } => id == pattern_wildcard_name()
_ => false
}
}

// A pattern is the arm's whole `pat` or a constructor field's target, and `_` is the same pattern
// form in both: it binds nothing and names nothing, so it is kept as it is at every depth rather
// than looked up as a reference to a symbol spelled `_`.
//
// A pattern is the arm's whole `pat` or a constructor field's target, and the wildcard is the same
// pattern FORM in both (v2.std.node_query is_wildcard_pattern): it binds nothing and names nothing,
// so it is kept as it is at every depth. Lowering mints it, so it is recognised by form, never by
// comparing an atom's spelling to `_`.
fn resolve_pattern_node_walk(ctx: ResolveContext, pat: Node) -> ResolveNodeWalk {
if resolve_pattern_is_wildcard(pat: pat) {
if is_wildcard_pattern(pattern: pat) {
ResolveWalkAccepted { value: pat, diagnostics: None }
} else {
match construct_tag_optional(n: pat) {
Expand Down
22 changes: 20 additions & 2 deletions src/v2/compiler/body_lowering_fold.dag
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,8 @@ import v2.std.node_query {
field_projection_optional,
find_named_child,
positional_payload_field_name,
pattern_wildcard_name,
wildcard_pattern_identity,
repeated_name_edges,
variant_declaration_node
}
Expand Down Expand Up @@ -5593,7 +5595,7 @@ fn body_lower_pattern_lowered(pattern_capture: Node) -> Outcome<Node> {
Present { value: pair } =>
if is_empty_conj_root(n: body_lower_deep_unwrap_optional(node: pair.right)) {
match body_lower_pattern_atom_optional(pattern_capture: pair.left) {
Present { value: atom } => outcome_accepted(value: atom)
Present { value: atom } => outcome_accepted(value: body_lower_pattern_atom_form(atom: atom))
Absent => body_lower_pattern_reject(pattern_capture: pattern_capture)
}
} else {
Expand All @@ -5605,12 +5607,28 @@ fn body_lower_pattern_lowered(pattern_capture: Node) -> Outcome<Node> {
}
Absent =>
match body_lower_pattern_atom_optional(pattern_capture: captured) {
Present { value: atom } => outcome_accepted(value: atom)
Present { value: atom } => outcome_accepted(value: body_lower_pattern_atom_form(atom: atom))
Absent => body_lower_pattern_reject(pattern_capture: pattern_capture)
}
}
}

// A BARE PATTERN ATOM IS A NAME OR THE WILDCARD, and only the wildcard changes form here: an authored
// `_` lowers to the minted wildcard pattern (v2.std.node_query wildcard_pattern_identity) at the `_`'s
// own occurrence, so no reader downstream sees a name it would look up. A name stays the atom it is,
// a constructor or a binder for the resolver to decide.
fn body_lower_pattern_atom_form(atom: Node) -> Node {
match node_atom_identity_optional(node: atom) {
Present { value: id } =>
if id == pattern_wildcard_name() {
body_lower_param_ref_atom(source: atom, identity: wildcard_pattern_identity())
} else {
atom
}
Absent => atom
}
}

// THE ARM BODY IS A VALUE, READ BY THE VALUE READER AND BY NOTHING ELSE. It was read by an operand
// reader (body_lower_match_arm_body_optional, deleted) that answered a nested `match` or `if` in arm
// position with that form's first atom -- how every arm of std.content_hash compare_content_hash lost
Expand Down
8 changes: 6 additions & 2 deletions src/v2/compiler/reference_conservation.dag
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ import v2.compiler.occurrence_role {
occurrence_role_index
}
import v2.std.anonymous_binder { anonymous_param_label, is_anonymous_param_label }
import v2.std.node_query { pattern_wildcard_name }
import v2.std.node_query { is_wildcard_pattern_identity, pattern_wildcard_name }

// REFERENCE CONSERVATION ACROSS LOWERING (XL-2).
//
Expand Down Expand Up @@ -846,8 +846,12 @@ fn absent_cause(declared: ItemDeclarationStanding) -> DroppedReferenceCause {
// `dag_binding_type_int`) at that same occurrence. That is the single authority the spelling pool
// below already consults, so it is asked here too: the locus is held and the spelling is the one
// the rewrite derives. Any other spelling at the occurrence is still RespelledInNormalizedTree.
// An authored `_` pattern is conserved by the wildcard pattern form lowering mints at its occurrence
// (v2.std.node_query is_wildcard_pattern_identity); the form is the `_`'s lowering, not a different atom.
fn occurrence_spelling_conserved(found: Symbol, identity: Symbol) -> Bool {
found == identity || found == kernel_type_spelling_of(sym: identity)
found == identity
|| found == kernel_type_spelling_of(sym: identity)
|| ((identity == pattern_wildcard_name()) && is_wildcard_pattern_identity(sym: found))
}

// WHERE AN ERASED ATOM IS COUNTED. The module header first (its item is -1), then an atom whose
Expand Down
5 changes: 4 additions & 1 deletion src/v2/std/compilers/target_model.dag
Original file line number Diff line number Diff line change
Expand Up @@ -154,6 +154,7 @@ import v2.std.node_query {
node_labeled_child_edges,
node_positional_child_targets,
nullary_inhabitant_by_discriminant,
is_wildcard_pattern_identity,
pattern_wildcard_name
}
import v2.std.qualified_name {
Expand Down Expand Up @@ -1122,6 +1123,8 @@ fn lex_rules_literal(target: TargetModel, token_class: Symbol) -> Outcome<String
// (v2.std.anonymous_binder anonymous_binder_mint_parameter_list). A target that admits only one `_` per
// signature receives two and its own compiler refuses them; no target row carries a per-target
// anonymous-parameter spelling yet.
// The minted wildcard pattern (v2.std.node_query wildcard_pattern_identity) is spelled `_` the same way,
// the inverse of its own mint in pattern lowering.
fn bound_spelling_from_map(
binding_spellings: Map<Symbol, String>,
binding: Symbol
Expand All @@ -1130,7 +1133,7 @@ fn bound_spelling_from_map(
Accepted { value: opt, diagnostics: pending } => match opt {
Present { value: spelling } => Accepted { value: spelling, diagnostics: pending }
Absent =>
if is_anonymous_param_label(sym: binding) {
if is_anonymous_param_label(sym: binding) || is_wildcard_pattern_identity(sym: binding) {
symbol_interned_spelling(binding: pattern_wildcard_name())
} else {
symbol_interned_spelling(binding: binding)
Expand Down
34 changes: 33 additions & 1 deletion src/v2/std/node_query.dag
Original file line number Diff line number Diff line change
Expand Up @@ -197,11 +197,43 @@ fn positional_payload_field_name() -> Symbol {
symbol_intern_lexeme(lexeme: "0")
}

// The wildcard pattern `_` binds nothing and names nothing (v1.compiler.parse parse_pattern).
// THE AUTHORED SPELLING of the wildcard: the `_` a source writes in a pattern or as a parameter.
// It binds nothing and names nothing (v1.compiler.parse parse_pattern). It is the SPELLING only:
// lowering never leaves it in a pattern, it mints the wildcard pattern form below instead.
fn pattern_wildcard_name() -> Symbol {
symbol_intern_lexeme(lexeme: "_")
}

// A WILDCARD PATTERN IS ITS OWN FORM, NOT AN ATOM SPELLED `_`. A pattern atom is otherwise a
// constructor or a binder, both names, so a `_` atom was a name to every reader that did not
// special-case its spelling -- resolve looked it up as a reference
// (gunbc.recurring_failure_mode a_wildcard_match_arm_resolves_as_an_unbound_name). Lowering
// (v2.compiler.body_lowering_fold body_lower_pattern_lowered) mints this identity for an authored `_`
// pattern, and `<` is not an identifier character, so no authored name can spell it -- the
// anonymous-slot precedent (v2.std.anonymous_binder anonymous_param_label). It is still an Atom told
// apart by identity, so a reader that must not treat it as a name asks is_wildcard_pattern; a typed
// pattern carrier with a wildcard variant is the next rung (the row above). THE ONE MINT;
// is_wildcard_pattern is the one recogniser.
fn wildcard_pattern_identity() -> Symbol {
symbol_intern_lexeme(lexeme: "<wildcard-pattern>")
}

// THE ONE RECOGNISER, AT TWO GRAINS. A reader holding a Symbol (a conserved atom's identity, an
// emitted binding) asks is_wildcard_pattern_identity; a reader holding a pattern Node asks
// is_wildcard_pattern, which is that same question plus the form's structure (an Atom with no
// children). No reader compares against wildcard_pattern_identity() itself.
fn is_wildcard_pattern_identity(sym: Symbol) -> Bool {
sym == wildcard_pattern_identity()
}

fn is_wildcard_pattern(pattern: Node) -> Bool {
match pattern.kind {
TypeNode { connective: Atom { identity: id } } =>
is_wildcard_pattern_identity(sym: id) && (count(pattern.children) == 0)
_ => false
}
}


fn declared_field_cardinality_of_target(target: Node) -> Cardinality {
match target.kind {
Expand Down
Loading
Loading