diff --git a/AGENTS.md b/AGENTS.md index 92e00db57..bcb3050a3 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -242,6 +242,11 @@ input; `Derivation` means it is a different object. A derivative and an antideri verified — so promoting one means changing that test, and saying in the same change why the rewrite needs no assumptions. Loosening a tier needs nothing. +**A recording is a scope, not a setting.** `RewriteRecording.Start()` collects the rewrites that +fire while it is open, and costs one thread-static read per rule set — not per node — when nobody +opened one. Anything else added to this layer has to keep that shape: the common path may not pay +for machinery it is not using, and a switch a caller can leave on is a way of making it pay. + **Say "no answer" with `null`, here too.** `ApplyCore` returning `null` is the layer's way of saying "I could not settle this", and it is the one place where the new layer is *more* honest than the 1.x method it backs: `Transformation.Integration` has no answer where `Entity.Integrate` returns an diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRecording.cs b/Sources/AngouriMath/Core/Transformations/RewriteRecording.cs new file mode 100644 index 000000000..60c7e34d3 --- /dev/null +++ b/Sources/AngouriMath/Core/Transformations/RewriteRecording.cs @@ -0,0 +1,117 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using System; + +namespace AngouriMath.Core.Transformations +{ + /// + /// Collects the rewrites that fire while it is open, so that an answer can be asked how + /// it was reached rather than only what it is. + /// + /// + /// + /// Off unless asked for, and off is free: with no recording open, applying a rule set + /// costs one thread-static read more than it did before — per rule set, not per node — + /// and allocates nothing. That is the condition + /// #746 puts on + /// every layer above the tree, and it is why this is a scope rather than a setting that + /// something might leave on. + /// + /// + /// Per thread, like : a recording opened on one thread does + /// not see rewrites on another, so a parallel caller records its own work and nobody + /// else's. + /// + /// + /// A synchronous scope, and it has to be. Do not 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 yours, and the continuation may + /// come back on a different thread than the one holding it. Closing is written to + /// survive both — a recording closed elsewhere leaves the opening thread pointing at + /// something that ignores what it is handed rather than at a list that keeps growing — + /// but what gets collected in between is not something this can make meaningful. Record + /// around synchronous work, and await outside the scope. + /// + /// + /// What this is not. It records rewrites — which is what + /// #28 asks for — + /// and not everything does. Simplification also + /// expands, factorises, divides polynomials, minimises boolean expressions and then + /// *chooses* among the candidates by a complexity metric; the steps below are the + /// rewrites, in the order they fired, across every candidate that was generated, + /// including the ones that lost. Reading them as a route from the input to the returned + /// answer would be reading in something that is not there. + /// + /// + /// + /// + /// using AngouriMath; + /// using AngouriMath.Core.Transformations; + /// + /// using var recording = RewriteRecording.Start(); + /// var simplified = ((Entity)"a / (b / c)").Simplify(); + /// foreach (var step in recording.Steps) + /// Console.WriteLine(step); + /// + /// + public sealed class RewriteRecording : IDisposable + { + [ThreadStatic] + private static RewriteRecording? current; + + private readonly RewriteRecording? enclosing; + private readonly List steps = new(); + private bool closed; + + private RewriteRecording(RewriteRecording? enclosing) => this.enclosing = enclosing; + + /// + /// Opens a recording on this thread. Dispose it to close it — the value is meant to + /// be held in a , as values are. + /// + /// + /// Recordings nest: opening one inside another hides the outer one until the inner + /// is disposed, so a caller who records a subcomputation does not silently add its + /// steps to somebody else's list. + /// + public static RewriteRecording Start() => current = new RewriteRecording(current); + + /// + /// The rewrites that fired while this recording was open, in the order they fired. + /// + public IReadOnlyList Steps => steps; + + /// Closes the recording. stays readable afterwards. + public void Dispose() + { + if (closed) + return; + closed = true; + // Only this thread's chain is ours to put back. Disposing on a thread other than + // the one that opened it -- which is what awaiting inside a recording leads to -- + // would otherwise clear whatever that thread was recording into, and leave the + // opening thread pointing at a closed recording. Add ignores that case, so the + // worst a stray reference can do is nothing. + if (ReferenceEquals(current, this)) + current = enclosing; + } + + /// + /// The recording to report to, or where nobody is listening — + /// which is the case this has to stay free for. + /// + internal static RewriteRecording? Current => current; + + internal void Add(RewriteRuleSet ruleSet, Entity before, Entity after) + { + if (closed) + return; + steps.Add(new RewriteStep(ruleSet, before, after)); + } + } +} diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs b/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs index 70e4f8248..dc56c2112 100644 --- a/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs +++ b/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs @@ -60,9 +60,34 @@ internal RewriteRuleSet(string name, string description, TransformationRelation /// /// The expression to rewrite. public Entity ApplyOnce(Entity expression) - => expression is null - ? throw new ArgumentNullException(nameof(expression)) - : expression.Replace(rules); + { + if (expression is null) + throw new ArgumentNullException(nameof(expression)); + + // One thread-static read, per application rather than per node, and nothing + // allocated: the ordinary path must not pay for a recording nobody opened. + var recording = RewriteRecording.Current; + return recording is null + ? expression.Replace(rules) + : ApplyOnceRecording(expression, recording); + } + + /// + /// A method of its own, and that is the whole reason for it. The closure below + /// captures the rule set and the recording, and the compiler allocates the object + /// holding them where they come into scope -- so writing this inline in + /// put one allocation on every rewrite in the + /// library whether or not anybody was recording. Measured: it cost `Simplify` a + /// fifth of its allocation on the benchmark expressions. + /// + private Entity ApplyOnceRecording(Entity expression, RewriteRecording recording) + => expression.Replace(node => + { + var rewritten = rules(node); + if (rewritten != node) + recording.Add(this, node, rewritten); + return rewritten; + }); /// /// This set as a , so that it composes with the rest of diff --git a/Sources/AngouriMath/Core/Transformations/RewriteStep.cs b/Sources/AngouriMath/Core/Transformations/RewriteStep.cs new file mode 100644 index 000000000..8b10274e5 --- /dev/null +++ b/Sources/AngouriMath/Core/Transformations/RewriteStep.cs @@ -0,0 +1,43 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +namespace AngouriMath.Core.Transformations +{ + /// + /// One rewrite that actually fired: which rule set did it, the subexpression it matched, + /// and what it put there instead. + /// + /// + /// The subexpression, not the whole expression. A rewrite pass walks the tree bottom-up + /// and rewrites nodes as it goes, so there is no moment at which a partly-rewritten + /// whole expression exists to be photographed — reporting one would mean building it, + /// and it would be a picture of something the engine never held. + /// + public readonly struct RewriteStep + { + internal RewriteStep(RewriteRuleSet ruleSet, Entity before, Entity after) + => (RuleSet, Before, After) = (ruleSet, before, after); + + /// Which rule set rewrote it. + public RewriteRuleSet RuleSet { get; } + + /// The subexpression as it was matched. + public Entity Before { get; } + + /// What replaced it. Never equal to — a rule set that changed nothing records nothing. + public Entity After { get; } + + /// What the rule set claims about the rewrite. See . + public TransformationRelation Relation => RuleSet.Relation; + + /// How well justified that claim is. See on what a tier is and is not. + public Soundness Soundness => RuleSet.Soundness; + + /// + public override string ToString() => $"{RuleSet.Name}: {Before.Stringize()} -> {After.Stringize()}"; + } +} diff --git a/Sources/AngouriMath/Docs/Contributing/Transformations.md b/Sources/AngouriMath/Docs/Contributing/Transformations.md index fba4f399e..3caa022f3 100644 --- a/Sources/AngouriMath/Docs/Contributing/Transformations.md +++ b/Sources/AngouriMath/Docs/Contributing/Transformations.md @@ -37,6 +37,7 @@ same claim in the shape its callers expect, by handing back an unevaluated `Inte | `TransformationResult` | input, output-or-nothing, and which transformation ran. A struct, so routing an ordinary call through this layer allocates nothing | | `RewriteRuleSet` | a named, attributed group of rewrites — `Name`, `Description`, `Relation`, `Soundness`, `ApplyOnce` | | `RewriteRules` | the registry: every rule set the simplifier applies, explicitly listed, enumerable through `All` in a fixed order | +| `RewriteRecording` / `RewriteStep` | a scope that collects the rewrites which fired while it was open — off unless asked for, and free when off | Composition is `Then`, `Repeat(n)` and `UntilStable(max)`. All three take their bound from the caller: there is no unbounded rewrite loop anywhere in the layer, and `UntilStable` reports hitting @@ -68,6 +69,39 @@ built out of the registry. `SimplifyChildren` — which every stage of the simpl Everything else is a thin adapter over the algorithm that was already there. **Nothing that worked was rewritten to make the architecture tidier.** +## Recording what fired + +```csharp +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 +``` + +This is [#28](https://github.com/asc-community/AngouriMath/issues/28). Three things about it +are deliberate and worth keeping: + +**Free when off.** With no recording open, applying a rule set costs one thread-static read +more than it did before — per rule set, not per node — and allocates nothing. That is why it +is a scope rather than a setting: a setting is something a caller can leave on. + +**Per thread**, like `MathS.Settings`, so a parallel caller records its own work and nobody +else's. Recordings nest, and an inner one hides the outer until it closes. + +**A step is a subexpression, not a snapshot.** A rewrite 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; reporting those would mean +constructing something the engine never held. + +And the honest limit, which the type's own documentation states: **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 candidates that lost. Reading them as a route from the input to the returned answer +would be reading in something that is not there. Making that route available is the +derivation work in #746's v5.0 tier, and it needs the candidate search to be attributable +first, not just the rewrites. + ## What is deliberately not here **`Solve` is not a transformation.** It consumes a *goal* — an equation, with a variable to solve for diff --git a/Sources/Tests/DotnetBenchmark/Program.cs b/Sources/Tests/DotnetBenchmark/Program.cs index c59d0b0e4..89aef4a17 100644 --- a/Sources/Tests/DotnetBenchmark/Program.cs +++ b/Sources/Tests/DotnetBenchmark/Program.cs @@ -77,6 +77,9 @@ public static void Main(string[] args) { "RAMUsageTest" => GetReportByBenchmark(typeof(RAMUsageTest), "Gen 0", "Gen 1", "Gen 2", "Allocated"), "CommonFunctionsInterVersion" => GetReportByBenchmark(typeof(CommonFunctionsInterVersion), "Mean", "Error", "StdDev"), + // Allocated as well as Mean: the regressions this one exists to catch + // show up in allocation and are invisible in the timings. + "TransformationLayer" => GetReportByBenchmark(typeof(TransformationLayer), "Mean", "Error", "StdDev", "Allocated"), "CompiledFuncTest" => GetReportByBenchmark(typeof(CompiledFuncTest), "Mean", "Error", "StdDev"), "NumbersBenchmark" => GetReportByBenchmark(typeof(NumbersBenchmark), "Mean", "Error", "StdDev"), _ => throw new($"Unexpected benchmark {arg}") diff --git a/Sources/Tests/DotnetBenchmark/TransformationLayer.cs b/Sources/Tests/DotnetBenchmark/TransformationLayer.cs new file mode 100644 index 000000000..3f8afde21 --- /dev/null +++ b/Sources/Tests/DotnetBenchmark/TransformationLayer.cs @@ -0,0 +1,75 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using AngouriMath; +using AngouriMath.Core.Transformations; +using BenchmarkDotNet.Attributes; +using BenchmarkDotNet.Exporters.Csv; + +namespace DotnetBenchmark +{ + /// + /// The transformation layer, measured for time and allocation. + /// + /// + /// + /// Two claims are made about this layer and neither is safe without something that + /// measures them: that routing the 1.x entry points through it costs nothing, and that + /// recording rewrites costs nothing when nobody is recording. Both have already been + /// broken once during development -- the second by a closure the compiler allocated at + /// method entry regardless of the early return, which cost Simplify a fifth of + /// its allocation with the feature switched off, and which no test would have noticed. + /// + /// + /// Read the allocation column first. It is deterministic and reproduces to the tenth of + /// a kilobyte, where the timings on an ordinary machine vary by ten percent run to run + /// and hide exactly this kind of regression. + /// + /// + [ArtifactsPath(@"./benchmark_results.csv")] + [CsvExporter(CsvSeparator.Semicolon)] + [MemoryDiagnoser] + public class TransformationLayer + { + private static readonly Entity simplifyInput = "x + 3 / 3 + x ^ 0 - log(e, e2)"; + private static readonly Entity quotientInput = "(x ^ 3 + 3 * x ^ 2 * y + 3 * x * y ^ 2 + y ^ 3) / (x + y)"; + private static readonly Entity expandInput = "(x + y) ^ 6"; + private static readonly Entity factorizeInput = "x * y + y + 1 + x"; + private static readonly Entity surdInput = "1 / (sqrt(3) + 5)"; + private static readonly Entity unorderedInput = "z + y + x + sin(b) + a"; + private static readonly Entity derivativeInput = "x + 3 + arccos(x + 2) / sqrt(x2 + 1)"; + + // The 1.x surface, which now reaches its algorithm through the layer. These are the + // numbers to compare against a build from before the layer existed. + [Benchmark] public void Simplify() => simplifyInput.Simplify(); + [Benchmark] public void SimplifyQuotient() => quotientInput.Simplify(); + [Benchmark] public void Expand() => expandInput.Expand(); + [Benchmark] public void Factorize() => factorizeInput.Factorize(); + [Benchmark] public void Differentiate() => derivativeInput.Differentiate("x"); + + // The layer reached directly. + [Benchmark] public void SimplificationTransformation() => Transformation.Simplification.Apply(simplifyInput); + [Benchmark] public void Normalization() => Transformation.Normalization.Apply(unorderedInput); + [Benchmark] public void Rationalisation() => Transformation.Rationalisation.Apply(surdInput); + [Benchmark] public void Substitution() => Transformation.Substitution("x", 3).Apply(quotientInput); + + // A single rewrite pass, the unit everything above is built out of. + [Benchmark] public void OneRewritePass() => RewriteRules.Common.ApplyOnce(quotientInput); + [Benchmark] public void OneRewritePassThatMatchesNothing() => RewriteRules.PhiFunction.ApplyOnce(quotientInput); + + // The pair that matters. SimplifyWhileRecording is expected to cost more -- it + // collects a step per rewrite. Simplify above is the one that must not move: it is + // the same call with nobody listening, and if the two ever converge, the recording + // machinery has leaked into the ordinary path. + [Benchmark] + public void SimplifyWhileRecording() + { + using var recording = RewriteRecording.Start(); + simplifyInput.Simplify(); + } + } +} diff --git a/Sources/Tests/UnitTests/Core/Transformations/RewriteAllocationTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RewriteAllocationTest.cs new file mode 100644 index 000000000..fc9703437 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/RewriteAllocationTest.cs @@ -0,0 +1,93 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using System; +using AngouriMath; +using AngouriMath.Core.Transformations; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// That applying a rule set with nobody recording stays free. + /// + /// + /// + /// This is the one claim about the layer that no ordinary test can see: the code reads + /// as though the fast path returns before any of the recording machinery, and it did, + /// and it still allocated on every call — because the closure on the recording path + /// captures the rule set and the recording, and the compiler allocates the object + /// holding them where they come into scope. It cost Simplify a fifth of its + /// allocation with recording switched off, and only a benchmark caught it. + /// + /// + /// A benchmark is not run in CI, so the guard is here. It is written to be blunt rather + /// than precise: applying a rule set to a leaf, which no rule matches, rebuilds + /// no nodes and so should allocate essentially nothing. One stray per-call allocation + /// then dominates the measurement instead of hiding inside it, which is what makes the + /// threshold below safe to assert across runtimes rather than a source of flakes. + /// + /// + [Trait("Area", "Transformations")] + public sealed class RewriteAllocationTest + { + private const int Iterations = 20_000; + + /// + /// Generous on purpose. The measurement is a handful of bytes per call at most; a + /// reintroduced per-call closure costs on the order of thirty, which is roughly a + /// hundredfold over this budget. Anything in between is not something this test is + /// trying to have an opinion about. + /// + private const long BudgetBytes = 8 * Iterations; + + [Fact] + public void ApplyingARuleSetToALeafAllocatesEssentiallyNothing() + { + Entity leaf = MathS.Var("x"); + + // Warm the caches the first call fills, so that what is measured is the + // steady-state cost and not one-off construction. + for (var i = 0; i < 100; i++) + RewriteRules.Common.ApplyOnce(leaf); + + GC.Collect(); + GC.WaitForPendingFinalizers(); + GC.Collect(); + + var before = GC.GetAllocatedBytesForCurrentThread(); + for (var i = 0; i < Iterations; i++) + RewriteRules.Common.ApplyOnce(leaf); + var allocated = GC.GetAllocatedBytesForCurrentThread() - before; + + Assert.True( + allocated <= BudgetBytes, + $"applying a rule set with no recording open allocated {allocated} bytes over {Iterations} calls, " + + $"which is over the {BudgetBytes} budget. Something on the fast path is allocating per call -- " + + "a closure in the method is the usual cause, and moving it into its own method is the usual fix."); + } + + [Fact] + public void RecordingIsWhatCostsSomething() + { + // The other half of the claim: the budget above is not passing because the + // measurement is broken. With a recording open the same calls do allocate, + // because each rewrite becomes a step. + Entity expression = MathS.FromString("a / (b / c)", useCache: false); + + using var recording = RewriteRecording.Start(); + + var before = GC.GetAllocatedBytesForCurrentThread(); + for (var i = 0; i < 1_000; i++) + RewriteRules.Common.ApplyOnce(expression); + var allocated = GC.GetAllocatedBytesForCurrentThread() - before; + + Assert.True(allocated > 8 * 1_000, $"recording allocated only {allocated} bytes; the measurement is not measuring anything"); + Assert.NotEmpty(recording.Steps); + } + } +} diff --git a/Sources/Tests/UnitTests/Core/Transformations/RewriteRecordingTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RewriteRecordingTest.cs new file mode 100644 index 000000000..ae63015e6 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/RewriteRecordingTest.cs @@ -0,0 +1,209 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using System.Collections.Generic; +using System.Linq; +using System.Threading; +using AngouriMath; +using AngouriMath.Core.Transformations; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// Recording the rewrites that fire — #28. + /// + [Trait("Area", "Transformations")] + public sealed class RewriteRecordingTest + { + // Uncached, so that each expression is a fresh tree. An Entity memoises + // InnerSimplified on itself, so a cached one handed back a second time has already + // done part of the work and would record fewer steps for the same input. + private static Entity Parse(string raw) => MathS.FromString(raw, useCache: false); + + [Fact] + public void ARecordingCollectsTheRewritesThatFired() + { + using var recording = RewriteRecording.Start(); + Parse("a / (b / c)").Simplify(); + + Assert.NotEmpty(recording.Steps); + foreach (var step in recording.Steps) + { + // A rule set that changed nothing records nothing, so every step is a change. + Assert.NotEqual(step.Before, step.After); + // and every step names a set the registry knows about + Assert.Contains(step.RuleSet, RewriteRules.All); + } + } + + [Fact] + public void AStepSaysWhatItClaimsAndHowWellJustifiedItIs() + { + using var recording = RewriteRecording.Start(); + Parse("a / (b / c)").Simplify(); + + var step = recording.Steps[0]; + Assert.Equal(step.RuleSet.Relation, step.Relation); + Assert.Equal(step.RuleSet.Soundness, step.Soundness); + Assert.Equal(TransformationRelation.Equivalence, step.Relation); + Assert.Equal(Soundness.SoundUnderAssumptions, step.Soundness); + Assert.Contains("->", step.ToString()); + Assert.Contains(step.RuleSet.Name, step.ToString()); + } + + [Fact] + public void NothingIsRecordedWhenNobodyIsListening() + { + // Not an assertion about a counter -- there is nothing to count when no + // recording is open. What is pinned is that opening one afterwards starts empty, + // so the previous work left nothing behind in a static. + Parse("a / (b / c)").Simplify(); + + using var recording = RewriteRecording.Start(); + Assert.Empty(recording.Steps); + } + + [Fact] + public void RecordingDoesNotChangeTheAnswer() + { + var withoutRecording = Parse("(x ^ 3 + 3 * x ^ 2 * y + 3 * x * y ^ 2 + y ^ 3) / (x + y)").Simplify(); + + Entity withRecording; + using (var _ = RewriteRecording.Start()) + withRecording = Parse("(x ^ 3 + 3 * x ^ 2 * y + 3 * x * y ^ 2 + y ^ 3) / (x + y)").Simplify(); + + Assert.Equal(withoutRecording, withRecording); + } + + [Fact] + public void TheSameComputationRecordsTheSameStepsEveryTime() + { + static IReadOnlyList Record() + { + using var recording = RewriteRecording.Start(); + Parse("sin(x) / tan(x) + a / (b / c)").Simplify(); + return recording.Steps.Select(s => s.ToString()).ToList(); + } + + Assert.Equal(Record(), Record()); + } + + [Fact] + public void ClosingARecordingStopsIt() + { + var recording = RewriteRecording.Start(); + Parse("a / (b / c)").Simplify(); + var afterFirst = recording.Steps.Count; + recording.Dispose(); + + Parse("sin(x) / tan(x)").Simplify(); + + Assert.Equal(afterFirst, recording.Steps.Count); + } + + [Fact] + public void DisposingTwiceIsHarmless() + { + var recording = RewriteRecording.Start(); + recording.Dispose(); + recording.Dispose(); + + using var next = RewriteRecording.Start(); + Parse("a / (b / c)").Simplify(); + Assert.NotEmpty(next.Steps); + } + + [Fact] + public void AnInnerRecordingDoesNotFeedTheOuterOne() + { + using var outer = RewriteRecording.Start(); + Parse("a / (b / c)").Simplify(); + var outerBeforeInner = outer.Steps.Count; + + using (var inner = RewriteRecording.Start()) + { + Parse("sin(x) / tan(x)").Simplify(); + Assert.NotEmpty(inner.Steps); + } + + Assert.Equal(outerBeforeInner, outer.Steps.Count); + + // and the outer one is listening again once the inner has closed + Parse("u / (v / w)").Simplify(); + Assert.True(outer.Steps.Count > outerBeforeInner); + } + + [Fact] + public void ARecordingOnOneThreadDoesNotSeeAnother() + { + using var recording = RewriteRecording.Start(); + Parse("a / (b / c)").Simplify(); + var mine = recording.Steps.Count; + + // A thread joined synchronously rather than an awaited task. Awaiting would + // yield this thread while the recording is still open on it, and this thread is + // exactly where the test runner is free to start something else -- which the + // recording would then collect, because it follows the thread and not the call. + var other = new Thread(() => Parse("sin(x) / tan(x) + u / (v / w)").Simplify()); + other.Start(); + other.Join(); + + Assert.Equal(mine, recording.Steps.Count); + } + + [Fact] + public void AClosedRecordingIgnoresWhateverItIsStillHanded() + { + // Closing on a different thread than the one that opened it leaves the opening + // thread still holding the reference. It must then be inert: neither growing a + // list nobody will read, nor adding to a result already handed back. + RewriteRecording? opened = null; + using var recorded = new ManualResetEventSlim(); + using var closed = new ManualResetEventSlim(); + + var opener = new Thread(() => + { + opened = RewriteRecording.Start(); + Parse("a / (b / c)").Simplify(); + recorded.Set(); + closed.Wait(); + // This thread's `current` still points at the recording that was closed + // from elsewhere; none of this may reach it. + Parse("u / (v / w)").Simplify(); + }); + opener.Start(); + recorded.Wait(); + + var recording = Assert.IsType(opened); + var collected = recording.Steps.Count; + Assert.NotEqual(0, collected); + + recording.Dispose(); + closed.Set(); + opener.Join(); + + Assert.Equal(collected, recording.Steps.Count); + } + + [Fact] + public void EveryRecordedStepIsAnEquivalenceUnderStatedAssumptions() + { + using var recording = RewriteRecording.Start(); + Parse("sin(x) / tan(x) + a / (b / c) + (x + 1) ^ 2").Simplify(); + + Assert.NotEmpty(recording.Steps); + foreach (var step in recording.Steps) + { + // Nothing the simplifier applies may claim a proof it has not got, and + // nothing it applies may claim to have produced a different object. + Assert.Equal(TransformationRelation.Equivalence, step.Relation); + Assert.NotEqual(Soundness.Sound, step.Soundness); + } + } + } +}