Show the rewrites worth reading, not all 270 of them (#28)

Sources/AngouriMath/Core/Transformations/RewriteRecording.cs

@@ -7,6 +7,7 @@
 
 using System;
 using System.Collections.Concurrent;
+using System.Collections.Generic;
 using System.Threading;
 
 namespace AngouriMath.Core.Transformations
@@ -46,6 +47,12 @@ namespace AngouriMath.Core.Transformations
     /// 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.
     /// </para>
+    /// <para>
+    /// <see cref="Steps"/> is that raw list. <see cref="Derivation"/> is the same list with the
+    /// normalisation and the repeats taken out, which is what a reader asking "how did it get
+    /// there" wants — 270 rewrites down to 6 on <c>x^(-1)/(y/z)</c>. It is still a set of
+    /// rewrites rather than a path; the paragraph above applies to both.
+    /// </para>
     /// </remarks>
     /// <example>
     /// <code>
@@ -108,6 +115,52 @@ public static RewriteRecording Start()
         /// </remarks>
         public IReadOnlyList<RewriteStep> Steps => steps.ToArray();
 
+        /// <summary>
+        /// <see cref="Steps"/> with the tidying taken out and the repeats collapsed — the rewrites
+        /// that are worth reading. <a href="https://github.com/asc-community/AngouriMath/issues/28">#28</a>
+        /// </summary>
+        /// <remarks>
+        /// <para>
+        /// Two things are dropped, and neither is a judgement about importance. Sets that declare
+        /// <see cref="RewriteRuleSet.IsNormalization"/> are the engine straightening an expression
+        /// between real rewrites. And a rewrite that has already appeared is not shown again: the
+        /// simplifier explores several candidate forms and rewrites the same subexpression the same
+        /// way in each, so the raw list repeats itself many times over.
+        /// </para>
+        /// <para>
+        /// On <c>x^(-1)/(y/z)</c> that is 270 recorded rewrites down to 6.
+        /// </para>
+        /// <para>
+        /// <b>This is a set of rewrites, not a path.</b> Each entry is a real rewrite that really
+        /// fired, on the subexpression it names — but <see cref="Entity.Simplify(int)"/> searches candidate
+        /// forms and keeps the best, so these come from several branches and some belong to
+        /// candidates that were discarded. Reading them in order does not walk from the input to
+        /// the answer, and a step's <see cref="RewriteStep.Before"/> is a subexpression rather than
+        /// the whole expression at that moment. Producing a single path, with a whole expression at
+        /// each stage, needs the simplifier to record which candidate each rewrite belonged to,
+        /// which it does not do yet.
+        /// </para>
+        /// </remarks>
+        public IReadOnlyList<RewriteStep> Derivation
+        {
+            get
+            {
+                var seen = new HashSet<(string, string, string)>();
+                var derivation = new List<RewriteStep>();
+                foreach (var step in steps)
+                {
+                    if (step.RuleSet.IsNormalization)
+                        continue;
+                    // Keyed on what the reader sees — which rewrite, from what, to what — so that
+                    // the same rewrite found down two candidate branches is shown once.
+                    if (seen.Add((step.Rule?.Name ?? step.RuleSet.Name,
+                                  step.Before.Stringize(), step.After.Stringize())))
+                        derivation.Add(step);
+                }
+                return derivation;
+            }
+        }
+
         /// <summary>Closes the recording. <see cref="Steps"/> stays readable afterwards.</summary>
         public void Dispose()
         {

Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs

@@ -29,9 +29,9 @@ public sealed class RewriteRuleSet
     {
         private readonly Func<Entity, Entity> rules;
 
-        internal RewriteRuleSet(string name, string description, TransformationRelation relation, Soundness soundness, Func<Entity, Entity> rules, IReadOnlyList<RewriteRule>? addressable = null)
-            => (Name, Description, Relation, Soundness, this.rules, Rules)
-                = (name, description, relation, soundness, rules, addressable ?? Array.Empty<RewriteRule>());
+        internal RewriteRuleSet(string name, string description, TransformationRelation relation, Soundness soundness, Func<Entity, Entity> rules, IReadOnlyList<RewriteRule>? addressable = null, bool isNormalization = false)
+            => (Name, Description, Relation, Soundness, this.rules, Rules, IsNormalization)
+                = (name, description, relation, soundness, rules, addressable ?? Array.Empty<RewriteRule>(), isNormalization);
 
         /// <summary>A stable identity for this set.</summary>
         public string Name { get; }
@@ -45,6 +45,24 @@ internal RewriteRuleSet(string name, string description, TransformationRelation
         /// <summary>How well justified that claim is. See <see cref="Soundness"/> on what a tier here is and is not.</summary>
         public Soundness Soundness { get; }
 
+        /// <summary>
+        /// Whether this set only puts an expression into a canonical shape, rather than moving it
+        /// towards an answer.
+        /// </summary>
+        /// <remarks>
+        /// Declared by the set rather than inferred, because it is a statement about intent that
+        /// no amount of looking at a rewrite settles: reordering <c>y + x</c> to <c>x + y</c> and
+        /// collapsing <c>x + x</c> to <c>2 * x</c> are both equivalences that change the tree, and
+        /// only the author knows which one was meant as tidying.
+        /// <para/>
+        /// What it is for: a reader following a derivation wants the rewrites that got somewhere,
+        /// and normalisation is the engine straightening the expression between them. On
+        /// <c>x^(-1)/(y/z)</c> it is 251 of the 270 recorded rewrites. See
+        /// <see cref="RewriteRecording.Derivation"/> and
+        /// <a href="https://github.com/asc-community/AngouriMath/issues/28">#28</a>.
+        /// </remarks>
+        public bool IsNormalization { get; }
+
         /// <summary>
         /// The individual rewrites this set is made of, in the order they are tried.
         /// </summary>

Sources/AngouriMath/Core/Transformations/RewriteRules.cs

@@ -51,7 +51,8 @@ public static class RewriteRules
             // same value wherever the divisor is not zero.
             Soundness.SoundUnderAssumptions,
             Patterns.SortRules(TreeAnalyzer.SortLevel.HIGH_LEVEL),
-            Patterns.SortRulesArms(TreeAnalyzer.SortLevel.HIGH_LEVEL));
+            Patterns.SortRulesArms(TreeAnalyzer.SortLevel.HIGH_LEVEL),
+            isNormalization: true);
 
         /// <summary>
         /// <see cref="CanonicalOrder"/>, counting constants as well, so that terms differing
@@ -63,7 +64,8 @@ public static class RewriteRules
             TransformationRelation.Equivalence,
             Soundness.SoundUnderAssumptions,
             Patterns.SortRules(TreeAnalyzer.SortLevel.MIDDLE_LEVEL),
-            Patterns.SortRulesArms(TreeAnalyzer.SortLevel.MIDDLE_LEVEL));
+            Patterns.SortRulesArms(TreeAnalyzer.SortLevel.MIDDLE_LEVEL),
+            isNormalization: true);
 
         /// <summary>
         /// <see cref="CanonicalOrder"/> over the whole subtree, so that only structurally
@@ -75,7 +77,8 @@ public static class RewriteRules
             TransformationRelation.Equivalence,
             Soundness.SoundUnderAssumptions,
             Patterns.SortRules(TreeAnalyzer.SortLevel.LOW_LEVEL),
-            Patterns.SortRulesArms(TreeAnalyzer.SortLevel.LOW_LEVEL));
+            Patterns.SortRulesArms(TreeAnalyzer.SortLevel.LOW_LEVEL),
+            isNormalization: true);
 
         /// <summary>
         /// Turns a negative power into a quotient: <c>a * b ^ (-1)</c> becomes <c>a / b</c>.

Sources/Tests/UnitTests/Common/PublicApi.txt

@@ -117,6 +117,7 @@ AngouriMath.Core.ReasonOfFailureWhileParsing.ctor()
 AngouriMath.Core.ReasonOfFailureWhileParsing.ctor(AngouriMath.Core.ReasonOfFailureWhileParsing)
 AngouriMath.Core.ReasonOfFailureWhileParsing.op_Equality(AngouriMath.Core.ReasonOfFailureWhileParsing, AngouriMath.Core.ReasonOfFailureWhileParsing) : System.Boolean
 AngouriMath.Core.ReasonOfFailureWhileParsing.op_Inequality(AngouriMath.Core.ReasonOfFailureWhileParsing, AngouriMath.Core.ReasonOfFailureWhileParsing) : System.Boolean
+AngouriMath.Core.Transformations.RewriteRecording.Derivation { } : System.Collections.Generic.IReadOnlyList<AngouriMath.Core.Transformations.RewriteStep>
 AngouriMath.Core.Transformations.RewriteRecording.Dispose() : System.Void
 AngouriMath.Core.Transformations.RewriteRecording.Start() : AngouriMath.Core.Transformations.RewriteRecording
 AngouriMath.Core.Transformations.RewriteRecording.Steps { } : System.Collections.Generic.IReadOnlyList<AngouriMath.Core.Transformations.RewriteStep>
@@ -139,6 +140,7 @@ AngouriMath.Core.Transformations.RewriteRuleGrowth.value__ : System.Int32
 AngouriMath.Core.Transformations.RewriteRuleSet.ApplyOnce(AngouriMath.Entity) : AngouriMath.Entity
 AngouriMath.Core.Transformations.RewriteRuleSet.AsTransformation() : AngouriMath.Core.Transformations.Transformation
 AngouriMath.Core.Transformations.RewriteRuleSet.Description { } : System.String
+AngouriMath.Core.Transformations.RewriteRuleSet.IsNormalization { } : System.Boolean
 AngouriMath.Core.Transformations.RewriteRuleSet.Name { } : System.String
 AngouriMath.Core.Transformations.RewriteRuleSet.Relation { } : AngouriMath.Core.Transformations.TransformationRelation
 AngouriMath.Core.Transformations.RewriteRuleSet.RuleFiringAt(AngouriMath.Entity) : AngouriMath.Core.Transformations.RewriteRule

Sources/Tests/UnitTests/Core/Transformations/RewriteRecordingTest.cs

@@ -42,6 +42,70 @@ public void ARecordingCollectsTheRewritesThatFired()
             }
         }
 
+        /// <summary>
+        /// The reporter's expression on
+        /// <a href="https://github.com/asc-community/AngouriMath/issues/28">#28</a>, and the rule
+        /// they wrote out by hand — <c>any1 / (any2 / any3) -> any1 * any3 / any2</c> — is in the
+        /// derivation, named.
+        /// </summary>
+        [Fact]
+        public void TheDerivationNamesTheRewritesTheReporterAskedFor()
+        {
+            using var recording = RewriteRecording.Start();
+            Parse("x^(-1)/(y/z)").Simplify();
+
+            var derivation = recording.Derivation;
+            Assert.NotEmpty(derivation);
+            Assert.Contains(derivation, step =>
+                step.Rule?.PatternSource == "Divf(var any1, Divf(var any2, var any3))"
+                && step.Rule?.ReplacementSource == "any1 * any3 / any2");
+        }
+
+        /// <summary>
+        /// The point of the view: the raw list is dominated by the engine tidying up between
+        /// rewrites, and by the same rewrite recurring down every candidate branch.
+        /// </summary>
+        [Fact]
+        public void TheDerivationIsFarShorterThanTheRawRecording()
+        {
+            using var recording = RewriteRecording.Start();
+            Parse("x^(-1)/(y/z)").Simplify();
+
+            Assert.True(recording.Steps.Count > 100,
+                $"the raw recording is only {recording.Steps.Count} steps, so this proves nothing");
+            Assert.True(recording.Derivation.Count < 15,
+                $"the derivation is {recording.Derivation.Count} steps: "
+                + string.Join("; ", recording.Derivation.Select(s => s.Rule?.Name ?? s.RuleSet.Name)));
+        }
+
+        /// <summary>Normalisation is what the view drops, so none of it may survive.</summary>
+        [Fact]
+        public void TheDerivationHasNoNormalisation()
+        {
+            using var recording = RewriteRecording.Start();
+            Parse("x^(-1)/(y/z)").Simplify();
+
+            // Stated rather than assumed: if the raw recording had no normalisation in it the
+            // assertion below would hold while testing nothing.
+            Assert.Contains(recording.Steps, step => step.RuleSet.IsNormalization);
+            Assert.DoesNotContain(recording.Derivation, step => step.RuleSet.IsNormalization);
+        }
+
+        /// <summary>
+        /// A rewrite that takes one step is reported as one step, with the rule that did it.
+        /// </summary>
+        [Theory]
+        [InlineData("x + x", "2 * any1")]
+        [InlineData("sin(x)^2 + cos(x)^2", "1")]
+        public void AOneStepRewriteIsOneStep(string expr, string replacement)
+        {
+            using var recording = RewriteRecording.Start();
+            Parse(expr).Simplify();
+
+            var step = Assert.Single(recording.Derivation);
+            Assert.Equal(replacement, step.Rule?.ReplacementSource);
+        }
+
         [Fact]
         public void AStepSaysWhatItClaimsAndHowWellJustifiedItIs()
         {