A pattern reaches inside a binder, and only one node type needed it (#1074)

[Rafael-SOWNet]

Closes #1074.

The defect

{ x : x in S } is S, and the switch said so by deconstructing ConditionalSet(var v, Inf(var v, var s)) — reading the node's stored parts. A pattern could not. The matcher walked DirectChildren, where a set builder publishes one child, its predicate, with the bound name already replaced by a placeholder invented per traversal:

{ x : x in [0; 1] }   ->   DirectChildren: [ %1 in [0; 1] ]

So a two-child pattern over it never matched, and no pattern could name the bound variable at all. That rule bound the whole set and took it apart in its replacement — honest, but a rule whose shape was code again, so it could not be read backwards or checked the way its neighbours are.

The rename is load-bearing: it is what makes traversal alpha-invariant, and #1008 was about that placeholder escaping into Vars/FreeVariables. So the fix is not to stop renaming.

The fix

Matching reads the declared pair, through a new internal Entity.MatchableChildren — DirectChildren for every node but one. This is the same split VarsAndConsts and FreeVariables already make, and for the same reason: what a set builder is is read off its declared parts, and what it publishes for traversal is a capture-avoiding rewriting of them.

MatchPattern.Binder<T>(varName, body) is the spelling, and the rule becomes:

MatchPattern.Binder<Set.ConditionalSet>(
    "v", MatchPattern.Node<Set.Inf>(MatchPattern.Any("v"), MatchPattern.Any("s"))),
MatchPattern.Any("s"),

The repeated "v" is what the switch wrote as when v1 == v1a.

The issue's premise was wrong, and that shrank the fix

#1074 said "Every binder is in the same position: sum, product, integral, derivative, limit, ConditionalSet" and expected a Binder<T> family. Measured, that is false — I had generalised from the one case I had opened:

	DirectChildren
{ x : x in [0; 1] }	[1] %1 in [0; 1]
lambda(x, x + 1)	[2] x | x + 1
sum(x, x, 1, 3)	[4] x | x | 1 | 3
product(x, x, 1, 3)	[4] x | x | 1 | 3
integral(x, x)	[2] x | x
integral(x, x, 0, 1)	[4] x | x | 0 | 1
derivative(x, x)	[3] x | x | 1
limit(x, x, 0)	[3] x | x | 0

Every binder but the set builder publishes the name it binds as an ordinary child, un-renamed — so a plain Node<T> already reaches it and a repeated hole already says "the same variable". One override, not six. EveryOtherBinderPublishesTheNameItBinds puts that measurement in the build, so a binder that starts hiding its name fails here rather than going quiet.

Alpha-invariance

The name position is a hole and cannot be anything else — matching a bound name against a written one would make { x : … } and { y : … } different expressions, which they are not. What is asserted is that two occurrences are the same name, never which. Pinned by TheBoundNameIsNotWhatIsMatchedOn.

The widening also must not hand every two-child pattern in the library a new node to match. All three matching entry points check the node type first, and ATwoChildPatternOfAnotherTypeStillDoesNotMatchASetBuilder asks all three rather than the one a rewrite pass happens to use.

A binder pattern reports CanEMatch false rather than relying on never being asked: the e-graph is built from DirectChildren and has no notion of binding, which is why MatchPattern.Construct has no entry for a binder to begin with.

One test assertion was wrong in general

EveryDataRuleIsBuildableOnBothSides asserted Left.IsBuildable == (Reversal is not PatternCannotBeBuilt). Classify returns the first reason a rule is one-way, so a rule that both drops a hole and has an unbuildable left is reported as dropping the hole. This rule is the first of that shape. Stated as the two true implications instead.

Its reason for being one-way got better rather than going away: ReplacementIsCode → ReplacementDropsHoles — one-way because S does not say which name a set builder over it would bind, rather than because of how it was written.

Measured

No answer changes: MatchableChildren is internal and only the node pattern reads it, and the rule fires on exactly what it fired on before — MatchedRulesAgreeWithTheSwitchTest compares the data rules against the original switch and is unchanged. No BREAKING-CHANGES.md entry is owed.

Failed: 0, Passed: 9097, Skipped: 14 locally on net10.0.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura