Make a rewrite rule's left-hand side data, and prove it against the switch (#248, #746 v1.0)

[Rafael-SOWNet]

#746 v1.0 asks for "pattern matching as a data structure, not a switch: matchable, enumerable, testable".

Every rewrite in the library is currently an arm of a switch expression, and three separate things tier 2 wants turn out to be blocked on that one fact:

• a rule cannot carry its own justification tier (the soundness audit on Design document: individually addressable rewrite rules (#746 item 50) #825 — a set's tier is the minimum over its arms, so one conditional arm drags eighteen unconditional ones down, which is why all 30 sets declare the same value);
• a rule cannot be addressed individually (Design document: individually addressable rewrite rules (#746 item 50) #825);
• an e-graph cannot match against an e-class because there is no pattern object to match with (measured in the Goal: Math OS — a ten-year vision for AngouriMath as an open mathematical reasoning platform #746 e-graph evaluation, where the prototype had to extract a representative term per class instead of e-matching).

What this adds

MatchPattern	a left-hand side as a value: a hole, a typed hole, a literal, a node
MatchedRule	one rule — name, pattern, side condition, builder, and its own Soundness
MatchedRuleSet	an ordered list, enumerable, whose tier is derived from its rules

Three properties the switch cannot have, each with a test:

• A repeated name binds the same subexpression both times — what the existing rules spell out by hand as when any1 == any1a. Here it falls out of the matcher.
• A set's tier is the weakest of its rules, derived rather than declared, so it cannot drift from what it describes.
• Rules are enumerable and named, so one can be listed, tested alone, or named in a bug report.

The load-bearing part is the equivalence test, not the types

DivisionPreparing is expressed as data beside the switch that already expresses it, and both are run over every expression a small grammar produces — 500+ — and required to agree on all of them. The test also asserts the rules actually fire on a fair number, so agreement cannot be two things both doing nothing.

That makes replacing a switch a mechanical step, provable one set at a time, rather than a wholesale leap.

Deliberately not here

Associativity and commutativity in the matcher — a + b does not match b + a. That is what #248 is actually about, and guessing at its shape before the plain case is proven is how a matcher gets built twice. Everything is internal for the same reason: the shape should survive a few more sets before it becomes public surface.

Measured

Suite 7075 passed / 0 failed, 5 new; casbench 116/119 with 0 wrong, 0 error, 0 timeout. No BREAKING-CHANGES.md entry — nothing existing changes behaviour, and no public surface is added.

🤖 Generated with Claude Code

[Rafael-SOWNet]

Pushed a second commit, because one rule set proves the types compile rather than that the shape generalises.

CollapseMultipleFractions is now expressed as data too, and it was chosen for being harder in three specific ways: eight rules instead of three, an order that is load-bearing — the quotient-times-quotient rule has to be tried before the general product rule or the general one swallows it — and a predicate on a hole, Integer { IsPositive: true }.

One feature was added and nothing else changed. MatchPattern.Any<T>(name, where) is the C# property pattern as data — a predicate on the node, which travels with the hole and can be read off a rule, as against a condition about the match as a whole, which belongs in the rule's when and cannot. That is the answer to the question the second set was picked to ask.

Both sets now agree with their switch on every one of the 500+ generated expressions, and two more properties have tests of their own:

• a predicate on a hole is checked — (x/y)^2 fires, (x/y)^(-2), (x/y)^0 and (x/y)^z do not;
• the order of the rules is load-bearing in the data exactly as it is in the switch — reversing the list makes the general rule match (a/b) * (c/d) first, which is the collision the written order avoids. A switch gets that ordering by accident of being written top to bottom; a list has to mean it.

Suite 7081 / 0.

[Rafael-SOWNet]

Two more commits, and the second one is #248's actual subject.

A rule-level guard over two bindings

PowerRules' (a^b)^c = a^(b*c) — true for a positive base whatever the exponents, and for any base when the outer exponent is whole. As data the guard reads c is Integer || a.Evaled is Real { IsPositive: true }: two bindings at once, which no per-hole predicate can say. This is #752, the rule that was once applied unconditionally and turned sqrt(x^2) into x.

Comparing it to the switch needed care — PowerRules is large and an earlier arm may fire first, so a case counts only where the switch either did nothing or produced exactly the power-of-a-power answer. That the rule cannot be isolated from its switch any other way is itself the argument for rules being data, and it is written into the test rather than into a commit message.

Commutative matching — and it needs backtracking

CommonRules writes k*p + k*q = k*(p+q) out four times because a C# pattern cannot say "either way round". One commutative pattern says it.

Getting there meant matching has to enumerate solutions rather than return one. b*a + c*a shares a, and a matcher that commits to the first way the left product matches binds k = b, fails on the right, and gives up — in both orders of the sum. Only backtracking finds it. Bindings are now copied rather than mutated for the same reason: a branch that fails must leave nothing behind for the branch tried next.

The finding that matters more than the rule

The commutative rule fires in exactly the cases the four arms fire — all 256 sums of products the test generates — but it does not always build the same tree. Where two factors are shared they pick different ones:

a*b + b*a     four arms -> b*(a + a)     one rule -> a*(b + b)      both 2ab

That tie-break is fixed in the switch by the order its arms happen to be written in, and was never chosen deliberately. So migrating this rule is not purely mechanical: it needs a tie-break convention, or the printed answer moves for expressions with two shared factors. The test asserts firing-agreement exactly and value-agreement where the trees differ, so the difference is pinned rather than found later by a user.

It is also the first rule here that is Soundness.Sound — distributivity needs no condition — so the tier finally distinguishes it from its neighbours, which is the argument for tiers belonging to rules.

Not here: matching across a flattened chain (a + b + c against x + y). That is the n-ary half, wants the operands gathered first, and is a larger change.

Suite 7100 / 0, 30 tests in this file.