A rule's own growth, tier and identity reach the registry

Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs

@@ -44,8 +44,9 @@ internal MatchedRule(
             MatchPattern right,
             Soundness soundness,
             Func<Bindings, bool>? when = null,
+            string? description = null,
             [CallerLineNumber] int line = 0)
-            : this(name, left, null, right ?? throw new ArgumentNullException(nameof(right)), soundness, null, when, line)
+            : this(name, left, null, right ?? throw new ArgumentNullException(nameof(right)), soundness, null, when, description, line)
         {
             // A name the replacement reads and the pattern never binds is a typo, and it is a
             // typo that would otherwise show up as a rule that silently never fires. Only a
@@ -76,10 +77,11 @@ internal MatchedRule(
             Soundness soundness,
             RewriteRuleGrowth? growth = null,
             Func<Bindings, bool>? when = null,
+            string? description = null,
             [CallerLineNumber] int line = 0)
             : this(name, left, right is null ? null : (_, bound) => right(bound),
                    right is null ? throw new ArgumentNullException(nameof(right)) : null,
-                   soundness, growth, when, line)
+                   soundness, growth, when, description, line)
         {
         }
 
@@ -110,9 +112,10 @@ internal MatchedRule(
             Soundness soundness,
             RewriteRuleGrowth? growth = null,
             Func<Bindings, bool>? when = null,
+            string? description = null,
             [CallerLineNumber] int line = 0)
             : this(name, left, right ?? throw new ArgumentNullException(nameof(right)), null,
-                   soundness, growth, when, line)
+                   soundness, growth, when, description, line)
         {
         }
 
@@ -124,9 +127,11 @@ private MatchedRule(
             Soundness soundness,
             RewriteRuleGrowth? declaredGrowth,
             Func<Bindings, bool>? when,
+            string? description,
             int line)
         {
             SourceLine = line;
+            Description = description;
             Name = name ?? throw new ArgumentNullException(nameof(name));
             Left = left ?? throw new ArgumentNullException(nameof(left));
             this.right = rightCode;
@@ -146,6 +151,30 @@ private MatchedRule(
         /// <summary>What to call this rule in a report, a test or a bug.</summary>
         internal string Name { get; }
 
+        /// <summary>
+        /// The identity this rule is, in the notation a mathematician would write it in — or
+        /// <see langword="null"/> where nobody has written one.
+        /// </summary>
+        /// <remarks>
+        /// <para>
+        /// <b>Not the same thing as <see cref="Name"/> or as the rendered pattern.</b>
+        /// <c>a / (b / c) = a * c / b</c> is what this says; <c>dividing-by-a-quotient-multiplies-by-its-reciprocal</c>
+        /// is what to call it, and <c>Divf(var a, Divf(var b, var c))</c> is how the matcher spells
+        /// it. #746 tier 2 wants metadata "rich enough that v5.0 can render a step as a sentence",
+        /// and of those three only this one is the sentence.
+        /// </para>
+        /// <para>
+        /// <b>It exists because the generator has one and this did not.</b>
+        /// <c>RuleRegistryGenerator</c> reads the comment written above a <c>switch</c> arm into
+        /// <see cref="RewriteRule.Description"/> — <b>95 of the registry's 407 arms</b> carry one
+        /// that way. A rule written as data has its identity in a comment too, and a comment is
+        /// not readable at run time, so until this parameter existed converting a set to data
+        /// <i>lost</i> the description rather than keeping it. That is what stands between the
+        /// registry and describing the rules it actually runs.
+        /// </para>
+        /// </remarks>
+        internal string? Description { get; }
+
         /// <summary>
         /// The line this rule is declared on, taken from the compiler rather than written down.
         /// </summary>
@@ -363,7 +392,8 @@ private RewriteRuleGrowth ClassifyGrowth(RewriteRuleGrowth? declared)
         /// </remarks>
         internal MatchedRule? Reversed
             => Reversal is RuleReversal.Reversible
-                ? reversed ??= new MatchedRule($"reversed {Name}", Right!, Left, Soundness, when)
+                ? reversed ??= new MatchedRule($"reversed {Name}", Right!, Left, Soundness, when,
+                    Description is null ? null : $"read backwards: {Description}")
                 : null;
 
         private MatchedRule? reversed;
@@ -617,19 +647,30 @@ internal IReadOnlyList<RewriteRule> AsAddressable()
                     source: Name,
                     index: i,
                     name: rule.Name,
-                    description: null,
+                    description: rule.Description,
                     nodeTypes: rule.Left.RequiredRootType is { } root
                         ? new[] { root }
                         : Array.Empty<Type>(),
                     patternSource: pattern,
                     guardSource: rule.HasCondition ? "a side condition on the bindings" : null,
                     replacementSource: replacement ?? "(built by code)",
-                    growth: replacement is null ? RewriteRuleGrowth.Unknown
-                        : replacement.Length > pattern.Length ? RewriteRuleGrowth.Expands
-                        : replacement.Length < pattern.Length ? RewriteRuleGrowth.Collects
-                        : RewriteRuleGrowth.Rearranges,
+                    // The rule's own answer, not a proxy for it. This used to compare the lengths
+                    // of the two rendered strings, which is what the generator has to do -- it
+                    // reads C# source text and has no tree to count. Here there is a tree, and
+                    // guessing from the rendering was wrong 23 times in 322 and in both
+                    // directions: `Divf(var a, Sinf(var b))` to `Mulf(var a, Cosecantf(var b))`
+                    // read as Expands because `Cosecantf` is a longer word than `Sinf`, while
+                    // DivisionPreparing's two read as Collects for the same reason reversed. Worse
+                    // for the thirteen Boolean rules that *declare* their growth on a code-built
+                    // replacement: with no string to measure, the proxy answered Unknown and threw
+                    // the author's declaration away.
+                    growth: rule.Growth,
                     sourceLine: rule.SourceLine,
-                    apply: rule.TryApply);
+                    apply: rule.TryApply,
+                    // Per rule, which is the whole point of a rule being a value. A set's tier is
+                    // the minimum over its rules, so one conditional rule makes a set of a hundred
+                    // report as conditional; 181 of these 322 are Sound.
+                    soundness: rule.Soundness);
             }
             return built;
         }

Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs

@@ -838,14 +838,16 @@ is var (divided, remainder)
                     MatchPattern.Any<Rational>("k"),
                     MatchPattern.Node<Divf>(MatchPattern.Any("value"), MatchPattern.Any<Rational>("d"))),
                 (node, _) => Functions.Patterns.GatherNumericCoefficientOverASurd(node),
-                Soundness.SoundUnderAssumptions),
+                Soundness.SoundUnderAssumptions,
+                description: "k * (value / d) = (k * value) / d"),
 
             // num / (a + b) -> num * (a - b) / (a^2 - b^2)
             new MatchedRule(
                 "a-two-term-denominator-is-multiplied-by-its-conjugate",
                 MatchPattern.Node<Divf>(MatchPattern.Any("num"), MatchPattern.Any("den")),
                 (node, _) => Functions.Patterns.MultiplyByTheConjugate(node),
-                Soundness.SoundUnderAssumptions));
+                Soundness.SoundUnderAssumptions,
+                description: "num / (a + b) = num * (a - b) / (a^2 - b^2)"));
 
         /// <summary>
         /// <see cref="Functions.Patterns.NumericNeatRules"/>, as data.

Sources/AngouriMath/Core/Transformations/RewriteRule.cs

@@ -75,11 +75,16 @@ public enum RewriteRuleGrowth
     /// <see cref="Entity.Simplify(int)"/> per rule set exchanged.
     /// </para>
     /// <para>
-    /// <b>What is not here.</b> A per-rule <see cref="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
-    /// <see cref="RewriteRuleSet.Soundness"/> remains the declared tier and this type does not
-    /// invent a finer one it cannot justify. What being addressable buys is that the finer tier
-    /// now has somewhere to live once the argument is made, which it did not before.
+    /// <b>A per-rule <see cref="Soundness"/> is here now, and it is empty for most rules on
+    /// purpose.</b> This paragraph used to say the tier was absent, on the argument that a rule's
+    /// tier is a claim somebody has to argue for and cannot be derived from syntax. That argument
+    /// is right and it is not a reason for the property to be missing: where the argument <i>has</i>
+    /// been made, the claim needs somewhere to live. A rule written as data declares one, and 181
+    /// of the 322 such rules are <see cref="Transformations.Soundness.Sound"/> against every set in
+    /// the registry declaring <see cref="Transformations.Soundness.SoundUnderAssumptions"/>. A rule
+    /// read off a <c>switch</c> arm declares nothing, so its <see cref="Soundness"/> is
+    /// <see langword="null"/> — which says the set's tier is a fallback rather than a measurement,
+    /// where silently copying the set's down would have said the opposite.
     /// </para>
     /// </remarks>
     public sealed class RewriteRule
@@ -95,7 +100,8 @@ internal RewriteRule(
             string replacementSource,
             RewriteRuleGrowth growth,
             int sourceLine,
-            Func<Entity, Entity?> apply)
+            Func<Entity, Entity?> apply,
+            Soundness? soundness = null)
         {
             Source = source;
             Index = index;
@@ -108,6 +114,7 @@ internal RewriteRule(
             Growth = growth;
             SourceLine = sourceLine;
             this.apply = apply;
+            Soundness = soundness;
         }
 
         private readonly Func<Entity, Entity?> apply;
@@ -182,6 +189,32 @@ internal RewriteRule(
         /// <summary>Which way the rewrite moves. See <see cref="RewriteRuleGrowth"/>.</summary>
         public RewriteRuleGrowth Growth { get; }
 
+        /// <summary>
+        /// How well justified <b>this one rule's</b> claim is, or <see langword="null"/> where the
+        /// rule has no tier of its own and its set's applies. See
+        /// <see cref="Transformations.Soundness"/> for what a tier is and is not.
+        /// </summary>
+        /// <remarks>
+        /// <para>
+        /// <b>A set's tier is the minimum over its rules, so reading it as every rule's tier
+        /// understates most of them.</b> All thirty sets in the registry declare
+        /// <see cref="Transformations.Soundness.SoundUnderAssumptions"/>, and one conditional rule
+        /// is enough to make that true of a set of a hundred. Asked per rule instead, <b>181 of the
+        /// 322 rules written as data are <see cref="Transformations.Soundness.Sound"/></b> — they
+        /// hold for every complex argument, with nothing assumed — and 141 are conditional. That
+        /// difference is invisible at set grain and is what a derivation needs in order to say why
+        /// a particular step was allowed.
+        /// </para>
+        /// <para>
+        /// <see langword="null"/> is the honest answer for a rule read off a <c>switch</c>: an arm
+        /// declares no tier, so it has none of its own, and inventing its set's would be a claim
+        /// the source does not make. A caller wanting the effective tier writes
+        /// <c>rule.Soundness ?? set.Soundness</c>, and the <see langword="null"/> is what tells it
+        /// that the second value is a fallback rather than a measurement.
+        /// </para>
+        /// </remarks>
+        public Soundness? Soundness { get; }
+
         /// <summary>The line of the source file the arm is written on.</summary>
         public int SourceLine { get; }
 

Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs

@@ -33,6 +33,32 @@ internal RewriteRuleSet(string name, string description, TransformationRelation
             => (Name, Description, Relation, Soundness, this.rules, Rules, IsNormalization)
                 = (name, description, relation, soundness, rules, addressable ?? Array.Empty<RewriteRule>(), isNormalization);
 
+        /// <summary>
+        /// A set whose rewrites are written as data: it both <i>runs</i>
+        /// <paramref name="source"/> and <i>describes</i> it.
+        /// </summary>
+        /// <remarks>
+        /// <para>
+        /// <b>One argument rather than two, because two could disagree.</b> The other constructor
+        /// takes what to run and what to report separately, and for most of the registry's life
+        /// those were a matcher on one side and a <c>switch</c> read by
+        /// <c>RuleRegistryGenerator</c> on the other — so a set could describe arms it no longer
+        /// executed, and 26 of them did. Passing the set itself makes that unrepresentable.
+        /// </para>
+        /// <para>
+        /// It also takes the factory call off the caller. A set built by a parameterised factory —
+        /// the common-denominator family, one definition read at three sort levels — would
+        /// otherwise be constructed twice, once for the delegate and once for the rules, and the
+        /// description would be of a different instance from the one that runs.
+        /// </para>
+        /// </remarks>
+        internal RewriteRuleSet(string name, string description, TransformationRelation relation, Soundness soundness, Matching.MatchedRuleSet source, bool isNormalization = false)
+            : this(name, description, relation, soundness,
+                   (source ?? throw new ArgumentNullException(nameof(source))).ApplyHere,
+                   source.AsAddressable(), isNormalization)
+        {
+        }
+
         /// <summary>A stable identity for this set.</summary>
         public string Name { get; }
 

Sources/AngouriMath/Core/Transformations/RewriteRules.cs

@@ -256,8 +256,7 @@ public static class RewriteRules
             "Multiplies a quotient by the conjugate of its denominator to clear a surd from it.",
             TransformationRelation.Equivalence,
             Soundness.SoundUnderAssumptions,
-            Matching.MatchedRules.RationalizeDenominator.ApplyHere,
-            Matching.MatchedRules.RationalizeDenominator.AsAddressable());
+            Matching.MatchedRules.RationalizeDenominator);
 
         /// <summary>
         /// Brings a quotient of quotients down to a single one.

Sources/Tests/UnitTests/Common/PublicApi.txt

@@ -180,6 +180,7 @@ AngouriMath.Core.Transformations.RewriteRule.Name { } : System.String
 AngouriMath.Core.Transformations.RewriteRule.NodeTypes { } : System.Collections.Generic.IReadOnlyList<System.Type>
 AngouriMath.Core.Transformations.RewriteRule.PatternSource { } : System.String
 AngouriMath.Core.Transformations.RewriteRule.ReplacementSource { } : System.String
+AngouriMath.Core.Transformations.RewriteRule.Soundness { } : System.Nullable<AngouriMath.Core.Transformations.Soundness>
 AngouriMath.Core.Transformations.RewriteRule.Source { } : System.String
 AngouriMath.Core.Transformations.RewriteRule.SourceLine { } : System.Int32
 AngouriMath.Core.Transformations.RewriteRule.ToString() : System.String