Skip to content

Collect the rewrites that fire, for a caller who asks (#28) - #819

Merged
Rafael-SOWNet merged 10 commits into
masterfrom
feat/rewrite-step-recording
Aug 8, 2026
Merged

Collect the rewrites that fire, for a caller who asks (#28)#819
Rafael-SOWNet merged 10 commits into
masterfrom
feat/rewrite-step-recording

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Collaborator

Addresses #28. Stacked on #818, which is stacked on #816 — merge those first.

What it does

using var recording = RewriteRecording.Start();
var simplified = ((Entity)"a / (b / c)").Simplify();
foreach (var step in recording.Steps)
    Console.WriteLine(step);      // Common: a / (b / c) -> a * c / b

A RewriteStep is the rule set, the subexpression it matched, and what replaced it — plus the relation and soundness tier that set declares. This is only possible because #818 gave every rule set the simplifier applies a name; a rewrite reached through Patterns directly has nothing to be attributed to.

The subexpression rather than the whole expression: a pass walks bottom-up and rewrites nodes as it goes, so there is no moment at which a partly-rewritten whole expression exists to photograph. #28's example shows whole-expression snapshots; producing those would mean constructing something the engine never held.

Free when off — measured, not asserted

Against b2e3c428 (the parent), net10.0/Release, with no recording open:

parent this branch
SimplifyEasy 125.8 KB 125.8 KB
SimplifyCommon 6867.8 KB 6867.6 KB
Limit 7516.4 KB 7516.0 KB
Expand / Factorize / Differentiate / ParseEasy unchanged unchanged

The first version of this was not free, and the benchmark is what caught it. The recording path's closure captures the rule set and the recording; the compiler allocates the object holding them where they come into scope, so writing it inline behind an early return still allocated on every rewrite in the library whether or not anyone was recording. It cost Simplify a fifth of its allocation — 125.8 → 151.3 KB — while the code read as though the fast path returned before any of it. The recording path is a separate method now, and the ordinary path is a thread-static read and a branch.

That is the reason this is a scope rather than a MathS.Settings entry: a setting is something a caller can leave on.

Threading

Per thread, like MathS.Settings. A synchronous scope: do not await inside one. The recording follows the thread, not the call, so yielding lets whatever else that thread picks up be recorded as if it were the caller's — which is precisely what the parallel test runner did to the first version of the thread-isolation test, and it is worth knowing that it fails that way rather than loudly.

Closing is written to survive being done from another thread: it restores only its own thread's chain, and a closed recording ignores whatever it is still handed. So a stray reference left on a thread does nothing, rather than growing a list nobody will read or appending to a result already handed back. There is a test for exactly that, driven through the public API with two threads and a pair of events.

Recordings nest; an inner one hides the outer until it closes.

What this is not

These are the rewrites, not everything Simplify did, and the type's own documentation says so. Simplification also expands, factorises, divides polynomials, minimises boolean expressions, and then chooses among the candidates by a complexity metric. The steps are every rewrite that fired across every candidate that was generated — including the candidates that lost. Reading them as a route from the input to the returned answer would be reading in something that is not there. That route is the derivation work in #746's v5.0 tier, and it needs the candidate search to be attributable, not just the rewrites.

So #28 gets a comment, not a close: it asks for per-rule attribution (any1 / (any2 / any3) -> any1 * any3 / any2) and this gives per-rule-set. The finer grain is item 50 on #746 and wants a design document first, because splitting each switch case into an object trades one dispatch per node for one delegate call per rule per node on the hottest path there is.

Tests

5784 passing, 0 failed, 15 skipped. F# 130 passing.

The new tests cover: that rewrites are collected and every step is a real change by a registered set; that a step carries its set's relation and tier; that recording does not change the answer; determinism across two identical runs; closing; double disposal; nesting not feeding the outer recording; thread isolation; and a recording closed from a different thread going inert.

Two notes on how they are written, both learned the hard way here:

  • The parse cache is off in these tests. An Entity memoises InnerSimplified on itself, so a cached tree handed back a second time has already done part of the work and records fewer steps for the same input.
  • The thread-isolation test joins a real thread instead of awaiting a task, for the reason in Threading above.

🤖 Generated with Claude Code

Rafael-SOWNet and others added 5 commits August 8, 2026 12:45
…n it

The top-level operations are procedures you invoke: `Simplify`, `Expand`,
`Factorize`, `Differentiate`, `Integrate`, `Limit`. There is nowhere to say what
one of them claims about its output, how well justified the claim is, or that it
could not settle the question -- and nowhere to compose two of them, because a
`Func<Entity, Entity>` carries none of that. That is the first layer #746 asks
for, and this adds the smallest version of it that has real consumers.

`AngouriMath.Core.Transformations` is:

  Transformation        Name, Relation, Soundness, Apply -- plus Then, Repeat and
                        UntilStable, all bounded by the caller
  TransformationResult  input, output-or-nothing, which transformation ran; a
                        struct, so routing an ordinary call allocates nothing
  RewriteRuleSet        a named, attributed group of rewrites
  RewriteRules          the registry: ten shipped sets, explicitly listed,
                        enumerable in a fixed order

Relation is `Equivalence` or `Derivation`, because "sound" is only a statement
about some relation and a derivative is not another way of writing its
integrand. Soundness is declared, not checked, so every shipped rule set is
`SoundUnderAssumptions` and a test over `RewriteRules.All` holds it there. No
answer is `null`, the same distinction AGENTS.md draws between an unevaluated
node and NaN -- which is where this layer is more honest than the method it
backs: `Transformation.Integration` has no answer for `e^(x^2)` where
`Entity.Integrate` returns an unevaluated `Integralf`.

Two real ports, not wrappers. `Factorize` no longer names its own rules: it is
PerfectSquare, then Factorization, then a tidying pass, repeated `level` times,
composed out of the registry. `SimplifyChildren` -- run by every stage of the
simplification pipeline -- is a chain built once, statically, from four registry
entries. The other five entry points are thin adapters over the algorithm that
was already there; nothing that worked was rewritten.

`Solve` is deliberately absent. It consumes a goal and produces a solution set,
and belongs in a tactic layer that does not exist yet; `Entity.Set` being an
`Entity` means it would type-check here, which is the reason to keep it out. No
inverse machinery either -- Expand and Factor are not inverses.

Registration is static and explicit, so the layer stays trimmable and
NativeAOT-publishable, and `RewriteRules.All` is in an order that does not depend
on hashing or type-load order. `RewriteRuleSet` builds its transformation on
demand: doing it eagerly makes the registry and the catalogue depend on each
other's static initialisation, and whichever is touched second reads null fields.

Measured on net7.0/Release against master 21f0d16, two samples each, same
expressions as DotnetBenchmark/CommonFunctionsInterVersion: every timing range
overlaps the baseline's, and allocation -- which is deterministic -- is identical
or lower (SimplifyEasy 158.6 -> 157.6 KB, SimplifyCommon 6976.8 -> 6973.6 KB,
SimplifyHard 3616232 -> 3616197 KB). `Patterns.SortRules` used to build a fresh
closure on every `SimplifyChildren` call and is now built once, which is where
the difference comes from.

Tests: 5551 -> 5699 passing, 0 failed, the same 14 skipped; F# 130 passing. The
149 new tests cover the abstraction, that each 1.x method answers what its
transformation answers, determinism, that an equivalence transformation does not
change the value of the expression, that unsupported cases stay honest, and that
no registered rule set rewrites in a cycle.

No behavioural change, so no BREAKING-CHANGES.md entry. The new surface is
additive and marked experimental in its own documentation.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…them

The registry held ten sets; `Simplificator` applied twenty-two, reaching most of
them through `Patterns` directly. A set reachable only by its method has no name
to report and nothing to attribute a step to, so any account of what `Simplify`
did to an expression would have quietly omitted most of what actually fired --
which is the wrong kind of answer to give, and the reason this comes before #28
rather than after it.

All twenty-two are registered now, and `Simplificator` reaches all of them
through `RewriteRules`. Two are parameterised by sort level, so each is
registered once per level with an internal chooser beside it
(`CanonicalOrderAt`, `CommonDenominatorAt`) -- the alternative is an entry that
cannot be enumerated, which defeats the list. `Entity.Expand` is routed too, so
that it is not the one catalogue transformation still naming its own rules.
Thirty entries in total; `Rewrite(ruleSet)` is an internal extension so a
sequence of them still reads in the order it runs.

This is a rename at every call site: `ApplyOnce` *is* `Replace(rules)`. Nothing
about the order, the guards or the candidate selection moved.

Measured against d1c4a4d on net10.0/Release, two samples each. Allocation is
deterministic and reproduces exactly:

  SimplifyEasy     157.6 -> 125.8 KB   (-20%)
  SimplifyCommon  6971.1 -> 6867.8 KB
  Limit           7658.0 -> 7516.4 KB
  Integrate       1774.5 -> 1759.5 KB

`Patterns.SortRules(level)` builds a fresh closure on every call and so does the
common-denominator lambda; both ran once per pass inside the simplification
loop and are now cached registry entries. Timings are unchanged within noise.

The tests over `RewriteRules.All` now cover thirty sets rather than ten, and the
corpus gained boolean, comparison, set, factorial and totient expressions so
that those sets are exercised rather than passed over. Every registered set
still reaches a fixed point within 32 passes and is deterministic.

Two things the widened corpus turned up:

`Expand` throws `AngouriBugException` on `(x + 1)! / x!` -- a public method
crashing on an ordinary expression that `Simplify` answers as `1 + x`. It
reproduces on d1c4a4d, where `Expand`'s logic is untouched, so it is
pre-existing: filed as #817, with a skipped regression test.

The equivalence property test was wrong twice over, and both are fixed. Sets
subtract elementwise, so the difference of two equal sets is the set of pairwise
differences rather than zero; set-valued results are now compared by simplifying
both sides. And simplifying a difference to zero proves agreement while failing
to do so proves nothing -- `x! * (x + 1)` expands to `(x + 1)!`, correctly, and
the difference does not reduce. The test now looks for an actual counterexample
at sample points before reporting a defect, with a relative tolerance, and has
its own test: it must separate `sqrt(x)` from `-sqrt(x)` and must not separate
`x! * (x + 1)` from `(x + 1)!`.

Tests: 5773 passing, 0 failed, 15 skipped (the new one is #817's); F# 130.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`Simplify` returns a value and there is nothing else to ask it. #28 has wanted the
intermediate replacements since the early days, and the registry makes them
available: every rule set the simplifier applies now has a name, so a rewrite that
fires has something to be attributed to.

    using var recording = RewriteRecording.Start();
    var simplified = ((Entity)"a / (b / c)").Simplify();
    foreach (var step in recording.Steps)
        Console.WriteLine(step);      // Common: a / (b / c) -> a * c / b

A step is the rule set, the subexpression it matched, and what replaced it --
plus the relation and soundness tier that set declares. The subexpression rather
than the whole expression: a pass walks bottom-up and rewrites nodes as it goes,
so there is no moment at which a partly-rewritten whole expression exists to
photograph, and #28's example of whole-expression snapshots would mean building
something the engine never held.

Free when off, and measured rather than asserted. Against b2e3c42 on
net10.0/Release, allocation with no recording open is the same to the tenth of a
kilobyte: SimplifyEasy 125.8 KB both sides, SimplifyCommon 6867.6 against 6867.8,
Limit 7516.0 against 7516.4, Expand and Factorize identical.

Getting there needed one thing that is not obvious, and the first version had it
wrong: the recording path's closure captures the rule set and the recording, and
the compiler allocates the object holding them where they come into scope -- so
written inline behind an early return it still allocated on every rewrite in the
library, recording or not. It cost `Simplify` a fifth of its allocation
(125.8 -> 151.3 KB) and the benchmark is what caught it. The recording path is a
separate method now, so the ordinary path is a thread-static read and a branch.

Per thread, like MathS.Settings, and a synchronous scope: do not await inside one.
The recording follows the thread rather than the call, so yielding lets whatever
else that thread picks up be recorded as if it were the caller's -- which is
exactly what the parallel test runner did to the first version of the thread test.
Closing is written to survive being done from another thread: it restores only its
own thread's chain, and a closed recording ignores what it is still handed, so a
stray reference does nothing rather than growing a list nobody reads.

What this is not, and the type says so: these are the rewrites, not everything
`Simplify` did. Simplification also expands, factorises, divides polynomials,
minimises boolean expressions and then chooses among candidates by a complexity
metric. The steps are every rewrite that fired across every candidate generated,
including the ones that lost. Reading them as a route from input to answer would
be reading in something that is not there -- that route is the derivation work in
#746's v5.0 tier, and it needs the candidate search to be attributable too.

So #28 gets a comment rather than a close: it asks for per-rule attribution and
this gives per-rule-set.

Tests: 5784 passing, 0 failed, 15 skipped; F# 130. The new ones cover collection,
that a step carries its set's relation and tier, that recording does not change
the answer, determinism, closing, double disposal, nesting, thread isolation, and
that a recording closed from another thread goes inert.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Rafael-SOWNet and others added 4 commits August 8, 2026 15:38
…e-set sweep

# Conflicts:
#	Sources/AngouriMath/Core/Transformations/RewriteRules.cs
#	Sources/AngouriMath/Docs/Contributing/Transformations.md
#	Sources/Tests/UnitTests/Core/Transformations/TransformationTest.cs
FactorizationAtLevel was swept across levels and the other two were compared
against the legacy API at the default only -- three tests of the same shape,
written three different ways, which is the inconsistency AGENTS.md calls a bug in
its own right.

All three are swept now, including negative levels, which Simplify passes itself
when it re-simplifies a candidate, and levels outside the -4..4 range the
catalogue keeps built: those are constructed on the spot, and the test says they
behave the same rather than merely not throwing.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… miss

Every number reported about this layer so far came from a throwaway harness, so
nothing stood behind them and a regression would have been silent. Two of the
claims had already been broken once each during development.

DotnetBenchmark gains a TransformationLayer class: the 1.x entry points that now
route through the layer, the layer reached directly, a single rewrite pass, and
Simplify with and without a recording open. Registered in Program.cs, reporting
Allocated as well as Mean -- allocation is deterministic and reproduces to the
tenth of a kilobyte, where the timings on an ordinary machine vary by ten percent
and hide exactly the regressions this exists to catch.

Benchmarks are not run in CI, so the claim that a rewrite costs nothing when
nobody is recording gets a test of its own. It applies a rule set to a leaf, which
no rule matches and which rebuilds no nodes, so a stray per-call allocation
dominates the measurement instead of hiding inside it. Verified by putting the
closure back: 640000 bytes over 20000 calls, exactly 32 per call, four times the
budget, and the message names the cause and the fix. A second test asserts that
recording does allocate, so the budget cannot pass because the measurement is
broken.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@Rafael-SOWNet

Copy link
Copy Markdown
Collaborator Author

Two things added since the description above, both from the same question: are there benchmarks for any of this?

There were not. Every number reported about this layer came from a throwaway harness outside the repo, so nothing stood behind the claims and a regression would have been silent — despite two of them having already been broken once each while it was being written.

DotnetBenchmark gains a TransformationLayer class covering the 1.x entry points that now route through the layer, the layer reached directly, a single rewrite pass, and Simplify with and without a recording open. Registered in Program.cs, reporting Allocated alongside Mean — allocation is deterministic and reproduces to the tenth of a kilobyte, where timings on an ordinary machine vary by ten percent and hide exactly what this exists to catch.

Benchmarks are not run in CI, so the "free when off" claim gets a test. RewriteAllocationTest applies a rule set to a leaf — no rule matches, no nodes are rebuilt — so a stray per-call allocation dominates the measurement rather than hiding inside it, which is what makes the budget safe to assert across runtimes instead of a source of flakes.

It was verified by putting the bug back: 640000 bytes over 20000 calls, exactly 32 per call, four times the budget, with a failure message naming the cause and the fix. A second test asserts that recording does allocate, so the budget cannot be passing because the measurement is broken.

Also, on the base branch: FactorizationAtLevel was swept across levels while the other two levelled transformations were checked at the default only — three tests of one shape written three ways. All three are swept now, including negative levels and levels outside the -4..4 range the catalogue keeps built.

…rder

# Conflicts:
#	Sources/AngouriMath/Docs/Contributing/Transformations.md
@Rafael-SOWNet
Rafael-SOWNet changed the base branch from feat/transformation-layer-rule-registry to master August 8, 2026 16:01
@Rafael-SOWNet
Rafael-SOWNet merged commit daec065 into master Aug 8, 2026
25 checks passed
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