diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRecording.cs b/Sources/AngouriMath/Core/Transformations/RewriteRecording.cs index de67ccfea..fb85733c8 100644 --- a/Sources/AngouriMath/Core/Transformations/RewriteRecording.cs +++ b/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. /// + /// + /// is that raw list. 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 x^(-1)/(y/z). It is still a set of + /// rewrites rather than a path; the paragraph above applies to both. + /// /// /// /// @@ -108,6 +115,52 @@ public static RewriteRecording Start() /// public IReadOnlyList Steps => steps.ToArray(); + /// + /// with the tidying taken out and the repeats collapsed — the rewrites + /// that are worth reading. #28 + /// + /// + /// + /// Two things are dropped, and neither is a judgement about importance. Sets that declare + /// 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. + /// + /// + /// On x^(-1)/(y/z) that is 270 recorded rewrites down to 6. + /// + /// + /// This is a set of rewrites, not a path. Each entry is a real rewrite that really + /// fired, on the subexpression it names — but 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 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. + /// + /// + public IReadOnlyList Derivation + { + get + { + var seen = new HashSet<(string, string, string)>(); + var derivation = new List(); + 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; + } + } + /// Closes the recording. stays readable afterwards. public void Dispose() { diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs b/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs index fffab36b9..14916aa47 100644 --- a/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs +++ b/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs @@ -29,9 +29,9 @@ public sealed class RewriteRuleSet { private readonly Func rules; - internal RewriteRuleSet(string name, string description, TransformationRelation relation, Soundness soundness, Func rules, IReadOnlyList? addressable = null) - => (Name, Description, Relation, Soundness, this.rules, Rules) - = (name, description, relation, soundness, rules, addressable ?? Array.Empty()); + internal RewriteRuleSet(string name, string description, TransformationRelation relation, Soundness soundness, Func rules, IReadOnlyList? addressable = null, bool isNormalization = false) + => (Name, Description, Relation, Soundness, this.rules, Rules, IsNormalization) + = (name, description, relation, soundness, rules, addressable ?? Array.Empty(), isNormalization); /// A stable identity for this set. public string Name { get; } @@ -45,6 +45,24 @@ internal RewriteRuleSet(string name, string description, TransformationRelation /// How well justified that claim is. See on what a tier here is and is not. public Soundness Soundness { get; } + /// + /// Whether this set only puts an expression into a canonical shape, rather than moving it + /// towards an answer. + /// + /// + /// Declared by the set rather than inferred, because it is a statement about intent that + /// no amount of looking at a rewrite settles: reordering y + x to x + y and + /// collapsing x + x to 2 * x are both equivalences that change the tree, and + /// only the author knows which one was meant as tidying. + /// + /// 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 + /// x^(-1)/(y/z) it is 251 of the 270 recorded rewrites. See + /// and + /// #28. + /// + public bool IsNormalization { get; } + /// /// The individual rewrites this set is made of, in the order they are tried. /// diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRules.cs b/Sources/AngouriMath/Core/Transformations/RewriteRules.cs index e801db050..8ed2f01ee 100644 --- a/Sources/AngouriMath/Core/Transformations/RewriteRules.cs +++ b/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); /// /// , 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); /// /// 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); /// /// Turns a negative power into a quotient: a * b ^ (-1) becomes a / b. diff --git a/Sources/Tests/UnitTests/Common/PublicApi.txt b/Sources/Tests/UnitTests/Common/PublicApi.txt index d0f9730c7..083ba5429 100644 --- a/Sources/Tests/UnitTests/Common/PublicApi.txt +++ b/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.RewriteRecording.Dispose() : System.Void AngouriMath.Core.Transformations.RewriteRecording.Start() : AngouriMath.Core.Transformations.RewriteRecording AngouriMath.Core.Transformations.RewriteRecording.Steps { } : System.Collections.Generic.IReadOnlyList @@ -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 diff --git a/Sources/Tests/UnitTests/Core/Transformations/RewriteRecordingTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RewriteRecordingTest.cs index 395c77125..1f8f1d154 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RewriteRecordingTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RewriteRecordingTest.cs @@ -42,6 +42,70 @@ public void ARecordingCollectsTheRewritesThatFired() } } + /// + /// The reporter's expression on + /// #28, and the rule + /// they wrote out by hand — any1 / (any2 / any3) -> any1 * any3 / any2 — is in the + /// derivation, named. + /// + [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"); + } + + /// + /// 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. + /// + [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))); + } + + /// Normalisation is what the view drops, so none of it may survive. + [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); + } + + /// + /// A rewrite that takes one step is reported as one step, with the rule that did it. + /// + [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() {