Skip to content

Make each rewrite rule addressable, generated from the switch that defines it (#825, #746 item 50) - #951

Merged
Rafael-SOWNet merged 2 commits into
masterfrom
feat/addressable-rewrite-rules
Aug 15, 2026
Merged

Rafael-SOWNet merged 2 commits into
masterfrom
feat/addressable-rewrite-rules

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

Implements the design in #825 — item 50 of #746, "the rule registry: turn the pattern set into enumerable, attributable data without regressing Simplify performance".

#825 is still labelled Design document and has no Accepted label, so this is offered for review rather than on an assumed go-ahead — hence Early PR. If the design is wanted in a different shape, the generator is the part to argue about and it is one file.

What it does

A source generator (Sources/Analyzers/RuleRegistryGenerator) turns each arm of a rewrite-rule switch into an individually addressable RewriteRule. 347 rules across 16 rule sets. A RewriteStep now names which rewrite fired, not just which set, which is the grain #28 asks for.

The switch is untouched as the thing a human edits and the thing the simplifier calls, so nothing on the hot path changes.

Why a generator and not forty objects

#825's measurement disposed of the performance objection but explicitly did not dispose of this one:

Splitting forty arms by hand into forty objects is forty chances to change a pattern silently. This is the serious objection, and it is not addressed by any of the above.

The generator addresses it by construction: each arm's pattern, when clause and result expression are copied verbatim as syntax into the generated apply lambda. Nothing is retyped, nothing is re-derived, and the registry is rebuilt from the switch on every compile, so the two cannot drift. If a copied arm did not mean the same thing in the generated context it would fail to compile rather than diverge silently.

Only two things are derived, and both are documented as what they are: NodeTypes is a necessary, not sufficient condition (empty where the pattern's shape does not say), and Growth is an explicitly crude syntactic proxy. A method carrying the attribute that is not an expression-bodied parameter switch { ... } emits #error, not an empty list — a rule set that silently has no rules reads exactly like one that has been checked.

The part to review most carefully: four arms are deleted

Patterns.Common.cs loses three and Patterns.Power.cs one. These are unreachable duplicates, and removing them changes no answer. Each appeared exactly twice with byte-identical pattern, guard and result; under first-match-wins the second could never fire. Verified mechanically rather than by eye — each survivor is the earlier occurrence:

removed identical arm that survives, and still wins
Minusf(Mulf(any1, any2), Mulf(any1a, any3)) Patterns.Common.cs, was line 132
Minusf(any1, Mulf(any2, any1a)) Patterns.Common.cs, was line 137
Minusf(any1, Mulf(any1a, any2)) Patterns.Common.cs, was line 136
Divf(Powf(any1, any2), Powf(any1a, any3)) Patterns.Power.cs, was line 59

The compiler cannot warn about these: a guarded arm never marks a later arm unreachable, so CS8510 does not fire. The generator found them because it names rules by pattern and suffixes repeats — and NoArmIsShadowedByAnIdenticalOneAboveIt now fails the build if another appears. There are currently zero suffixed names, so these four were all of them.

Behaviour

No answer changes, so there is no BREAKING-CHANGES.md entry. The four removed arms were unreachable; everything else is additive. Measured rather than reasoned:

  • full suite 7248 passed, 0 failed, 14 skipped
  • the corpus gate 3/3
  • casbench 116/119, 0 wrong / 0 error / 0 timeout — byte-identical to its committed baseline once the timing column is normalised
  • rulecheck 30 sets, 1365 applications, 0 never-settle, 0 value changes — unchanged
  • F# wrapper builds, 130/130

The new tests are not a "how many fail without this" count, because they test API that does not exist without it — they would not compile. What binds instead is that the four harnesses above are unchanged against their baselines.

Public API

21 new members, which is a promise for the rest of 2.x. Two things done deliberately:

  • The three source-text properties are named PatternSource / GuardSource / ReplacementSource. They hold the C# the arm is written in, not anything a matcher can run. Goal: Math OS — a ten-year vision for AngouriMath as an open mathematical reasoning platform #746 tier 1 is pattern matching as data, and when a pattern becomes a value it should be able to be called Pattern without breaking someone first. Renaming was free before release and a major-version cost after.
  • PublicApi.txt is regenerated, not hand-edited.

What it does not do

  • No per-rule Soundness. A rule's tier is a claim somebody has to argue for and there is no honest way to derive one from syntax, so RewriteRuleSet.Soundness stays the declared tier. What being addressable buys is that a finer tier now has somewhere to live once the argument is made.
  • 14 of the 30 sets stay unaddressable — the sorts, polynomial division, the factorial rules. Their rewrites are not a switch over the expression, so there are no arms to generate from. RewriteRuleSet.Rules is empty for them, which is documented as "empty is not the same as no rewrites", and TheRegistryIsAddressableAsFarAsItSaysItIs pins the list by name so making one addressable is a change to that list rather than a silent improvement.
  • Not an e-graph, not equality saturation, no rewrite of the rule sets — exactly the scope Design document: individually addressable rewrite rules (#746 item 50) #825 set.

Follow-on, measured separately

work/egraph in the analysis workspace re-ran #746 item 51's honest memory measurement now that rules carry a direction. Withholding the 60 rules that expand ends the saturation blow-up inside the addressable half — every expression saturates, none above 19 e-nodes, where the same configuration with all rules reaches thousands — while still finding sin(x)^2 + cos(x)^2 = 1. Item 51's first stated precondition was this issue, and it is now met. The remaining obstacle is the 14 sets that cannot declare a direction.

That measurement lives outside this repository and nothing here depends on it.

🤖 Generated with Claude Code

…the name (#825)

RewriteRule.Pattern/Guard/Replacement hold the C# the switch arm is written in, not
anything a matcher can run. #746
tier 1 is pattern matching as data, and when a pattern becomes a value it should be
able to be called Pattern without breaking somebody first.

Renamed to PatternSource/GuardSource/ReplacementSource before any of this is public
in a release, which is the only moment it is free. The generator emits the
constructor call by named argument, so the two cannot drift apart -- a rename on one
side stops the generated code compiling rather than silently binding elsewhere.

PublicApi.txt regenerated: three members renamed, nothing else moved.
@Rafael-SOWNet
Rafael-SOWNet merged commit 8e823be into master Aug 15, 2026
25 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the feat/addressable-rewrite-rules branch August 15, 2026 20:37
Rafael-SOWNet added a commit that referenced this pull request Aug 23, 2026
…1012)

* Make the derivation a path from the input to the answer (#28, #273)

A recording held every rewrite that fired, across every candidate the simplifier generated
including the ones that lost, each on the subexpression it matched. Read in order that does not
walk from the input to the answer, and the type's own documentation said so in three places.

`RewriteRecording.PathFrom(input, result)` walks it. Every step is a whole expression turning
into another: `Steps[i].After` is `Steps[i + 1].Before`, the first starts at the input, and the
last lands on what `Simplify` returned. `DerivationPath.OfSimplifying(expression)` is the same
in one call, and prints as the stages with the identity that produced each one beside it.

Two grains in two types, because a rewrite pass walks bottom-up and no partly-rewritten whole
expression exists inside one: `DerivationStep` is the pass, and its `Rewrites` are the
`RewriteStep`s that fired in it, each naming the rule that did it.

What was missing was attribution. A rule-set pass now records what it turned into as well as
what it matched, and `Simplificator` records the stages that are not rewrite passes -- inner
simplification, the boolean minimiser, the polynomial rearrangement, expansion, factoring --
since the chain otherwise has a hole wherever the simplifier tidies up. Losing candidates are
absent rather than marked: nothing leads from one to the answer, so none can be on a path to
it, and what the search produced and did not keep is reported as `ExpressionsExplored`.

Free when nobody is recording, which is what #746 requires of anything above the tree: one
ambient read per stage against a tree walk per stage, and no allocation. `RewriteAllocationTest`
guards the new fast path the way it already guarded `ApplyOnce`.

`Simplify` returns what it returned before, and the raw recording is unchanged -- 270 rewrites
on `x^(-1)/(y/z)`, 251 of them normalisation, measured on both builds.

Corrected in passing, each re-measured: `Common` has 100 arms and not 103; `Derivation` on that
expression is 5 rewrites and not 6; and `Transformations.md` said a source generator over the
switch bodies was still for #746 item 50 to decide, which #951 shipped.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011emtnRT6EWTrxXNtqDVK3e

* Say per flow and ambient read, which is what the recording has been since #863

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011emtnRT6EWTrxXNtqDVK3e

---------

Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant