From a26180d24714c0e4c08eee79e25e96ebac0ea430 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 30 Aug 2026 13:23:47 +0000 Subject: [PATCH] A rule's own growth, tier and identity reach the registry The registry runs one thing and describes another. 27 of the 30 sets execute `MatchedRuleSet.ApplyHere`, and 29 take their `Rules` from `RuleRegistryGenerator` reading the `switch` those sets no longer run -- #825's open half, and what #746 tier 2 names as gating the rest. Repointing them at `AsAddressable()` is the change that fixes it, and this is the three things that had to be true of `AsAddressable()` first. **Growth was a proxy, and wrong 23 times in 322 in both directions.** It compared the lengths of the two rendered pattern strings, which is what the generator has to do -- it reads C# source text and has no tree to count nodes on. Here there is a tree. `Divf(var a, Sinf(var b))` to `Mulf(var a, Cosecantf(var b))` read as Expands because `Cosecantf` is a longer word than `Sinf`, and DivisionPreparing's two read as Collects for that 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. `MatchedRule.Growth` is exact from `MatchPattern.NodeCount` and is now what is reported. **A tier per rule, and null where there is none.** A set's tier is the minimum over its rules, so one conditional rule makes a set of a hundred report as conditional -- which is why all thirty sets declare `SoundUnderAssumptions` and the field distinguishes nothing. Asked per rule, **181 of the 322 data rules are `Sound`** and 141 are conditional. `RewriteRule.Soundness` is `Soundness?` rather than `Soundness`: a `switch` arm declares no tier, so it has none of its own, and copying its set's down would assert a claim the source does not make. A caller wanting the effective tier writes `rule.Soundness ?? set.Soundness`, and the null is what tells it the second is a fallback. **And somewhere for the identity to live, which is what blocked the repoint.** The generator reads the comment above a `switch` arm into `RewriteRule.Description` -- `a / (b / c) = a * c / b` and its like, **95 of the registry's 407 arms**. A rule written as data has its identity in a comment too, and a comment is not readable at run time, so `AsAddressable` passed `description: null` and converting a set to data *lost* the description rather than keeping it. #746 tier 2 wants metadata "rich enough that v5.0 can render a step as a sentence", and of a rule's name, its rendered pattern and this, only this is the sentence. `MatchedRule` takes one now, a reversed rule prefixes rather than repeats it, and `RationalizeDenominator` -- the one set the registry already describes from its data form -- demonstrates it end to end: 0 of 2 rules reported an identity, now both do. `RewriteRuleSet` gains a constructor taking a `MatchedRuleSet` and reading both the runner and the rules off it, so a set cannot describe arms it does not execute. Also takes the factory call off the caller: the common-denominator family would otherwise be built twice, once for the delegate and once for the rules, and describe a different instance from the one that runs. **Not in this: the repoint itself.** It was written and measured and then taken back out. Pointing all 27 converted sets at `AsAddressable()` builds and leaves nine test failures, seven distinct, and they are informative rather than churn: the registry's arm count goes 407 -> 313 (the collapse the commutative patterns achieved -- `Common` 100 -> 62, `Boolean` 36 -> 20), rules start being named by their data names rather than by their rendered patterns, and the 95 descriptions all become null. So it changes public enumeration and needs a BREAKING-CHANGES entry, it invalidates `RuleConfluenceTest`'s index-named conflicts, and until the descriptions are ported set by set it is a net loss of metadata. That is the next change and it is one per set, with `MatchedRulesAgreeWithTheSwitchTest` as the net. Public surface: one additive property. Full suite: 8973 passed, 14 skipped, 0 failed. Part of #746 tier 2 and #825. --- .../Transformations/Matching/MatchedRule.cs | 61 +++++-- .../Transformations/Matching/MatchedRules.cs | 6 +- .../Core/Transformations/RewriteRule.cs | 45 ++++- .../Core/Transformations/RewriteRuleSet.cs | 26 +++ .../Core/Transformations/RewriteRules.cs | 3 +- Sources/Tests/UnitTests/Common/PublicApi.txt | 1 + .../Core/Transformations/RuleMetadataTest.cs | 160 ++++++++++++++++++ 7 files changed, 282 insertions(+), 20 deletions(-) create mode 100644 Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs index 96e4a89ac..123addd56 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs @@ -44,8 +44,9 @@ internal MatchedRule( MatchPattern right, Soundness soundness, Func? 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? 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? 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? 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( /// What to call this rule in a report, a test or a bug. internal string Name { get; } + /// + /// The identity this rule is, in the notation a mathematician would write it in — or + /// where nobody has written one. + /// + /// + /// + /// Not the same thing as or as the rendered pattern. + /// a / (b / c) = a * c / b is what this says; dividing-by-a-quotient-multiplies-by-its-reciprocal + /// is what to call it, and Divf(var a, Divf(var b, var 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. + /// + /// + /// It exists because the generator has one and this did not. + /// RuleRegistryGenerator reads the comment written above a switch arm into + /// — 95 of the registry's 407 arms 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 + /// lost the description rather than keeping it. That is what stands between the + /// registry and describing the rules it actually runs. + /// + /// + internal string? Description { get; } + /// /// The line this rule is declared on, taken from the compiler rather than written down. /// @@ -363,7 +392,8 @@ private RewriteRuleGrowth ClassifyGrowth(RewriteRuleGrowth? declared) /// 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 AsAddressable() source: Name, index: i, name: rule.Name, - description: null, + description: rule.Description, nodeTypes: rule.Left.RequiredRootType is { } root ? new[] { root } : Array.Empty(), 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; } diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index d7b6bcabd..f82999ba0 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -838,14 +838,16 @@ is var (divided, remainder) MatchPattern.Any("k"), MatchPattern.Node(MatchPattern.Any("value"), MatchPattern.Any("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(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)")); /// /// , as data. diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRule.cs b/Sources/AngouriMath/Core/Transformations/RewriteRule.cs index c93d3f1bd..5b1ef53c7 100644 --- a/Sources/AngouriMath/Core/Transformations/RewriteRule.cs +++ b/Sources/AngouriMath/Core/Transformations/RewriteRule.cs @@ -75,11 +75,16 @@ public enum RewriteRuleGrowth /// per rule set exchanged. /// /// - /// What is not here. A per-rule . A rule's tier is a claim - /// somebody has to argue for, and there is no honest way to derive one from syntax — so - /// 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. + /// A per-rule is here now, and it is empty for most rules on + /// purpose. 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 has + /// been made, the claim needs somewhere to live. A rule written as data declares one, and 181 + /// of the 322 such rules are against every set in + /// the registry declaring . A rule + /// read off a switch arm declares nothing, so its is + /// — 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. /// /// public sealed class RewriteRule @@ -95,7 +100,8 @@ internal RewriteRule( string replacementSource, RewriteRuleGrowth growth, int sourceLine, - Func apply) + Func 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 apply; @@ -182,6 +189,32 @@ internal RewriteRule( /// Which way the rewrite moves. See . public RewriteRuleGrowth Growth { get; } + /// + /// How well justified this one rule's claim is, or where the + /// rule has no tier of its own and its set's applies. See + /// for what a tier is and is not. + /// + /// + /// + /// A set's tier is the minimum over its rules, so reading it as every rule's tier + /// understates most of them. All thirty sets in the registry declare + /// , and one conditional rule + /// is enough to make that true of a set of a hundred. Asked per rule instead, 181 of the + /// 322 rules written as data are — 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. + /// + /// + /// is the honest answer for a rule read off a switch: 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 + /// rule.Soundness ?? set.Soundness, and the is what tells it + /// that the second value is a fallback rather than a measurement. + /// + /// + public Soundness? Soundness { get; } + /// The line of the source file the arm is written on. public int SourceLine { get; } diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs b/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs index 72e2a2bd5..d6e5815d8 100644 --- a/Sources/AngouriMath/Core/Transformations/RewriteRuleSet.cs +++ b/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(), isNormalization); + /// + /// A set whose rewrites are written as data: it both runs + /// and describes it. + /// + /// + /// + /// One argument rather than two, because two could disagree. 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 switch read by + /// RuleRegistryGenerator 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. + /// + /// + /// 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. + /// + /// + 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) + { + } + /// A stable identity for this set. public string Name { get; } diff --git a/Sources/AngouriMath/Core/Transformations/RewriteRules.cs b/Sources/AngouriMath/Core/Transformations/RewriteRules.cs index 4d7b64afe..c7fa7a587 100644 --- a/Sources/AngouriMath/Core/Transformations/RewriteRules.cs +++ b/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); /// /// Brings a quotient of quotients down to a single one. diff --git a/Sources/Tests/UnitTests/Common/PublicApi.txt b/Sources/Tests/UnitTests/Common/PublicApi.txt index 2ef6569d2..1ec2feb55 100644 --- a/Sources/Tests/UnitTests/Common/PublicApi.txt +++ b/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 AngouriMath.Core.Transformations.RewriteRule.PatternSource { } : System.String AngouriMath.Core.Transformations.RewriteRule.ReplacementSource { } : System.String +AngouriMath.Core.Transformations.RewriteRule.Soundness { } : System.Nullable AngouriMath.Core.Transformations.RewriteRule.Source { } : System.String AngouriMath.Core.Transformations.RewriteRule.SourceLine { } : System.Int32 AngouriMath.Core.Transformations.RewriteRule.ToString() : System.String diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs new file mode 100644 index 000000000..46b779677 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleMetadataTest.cs @@ -0,0 +1,160 @@ +// +// 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.Linq; +using AngouriMath.Core.Transformations; +using AngouriMath.Core.Transformations.Matching; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// What a rule says about itself, and whether the registry is able to repeat it. + /// #746 tier 2 asks for + /// rules that are data carrying "identity, name, direction, applicability conditions, + /// justification tier, provenance, cost effect", and for metadata "rich enough that v5.0 can + /// render a step as a sentence". + /// + /// + /// + /// The registry runs one thing and describes another. 27 of the 30 sets execute + /// , and 29 of them take their + /// from RuleRegistryGenerator reading the + /// switch those sets no longer run. That is + /// #825's open half. + /// + /// + /// This file is about the three things that had to be true of + /// before it could be what the registry reads: + /// growth that is the rule's own answer rather than a proxy for it, a justification tier per + /// rule, and somewhere for the identity to live. + /// + /// + [Trait("Area", "Core")] + public sealed class RuleMetadataTest + { + /// + /// Growth is the rule's exact answer, not a guess from how long the rendering is. + /// + /// + /// + /// AsAddressable used to compare the lengths of the two rendered pattern strings, + /// which is what RuleRegistryGenerator has to do — it reads C# source text and has + /// no tree to count nodes on. Here there is a tree, and the proxy disagreed with it + /// 23 times in 322, in both directions: + /// + /// + /// thirteen Boolean rules that declare Collects on a code-built + /// replacement read as Unknown, because with no string to measure the proxy threw + /// the author's declaration away; + /// two CollapseTrigonometricFunctions rules read as Expands because + /// Cosecantf is a longer word than Sinf — the same number of nodes; + /// two DivisionPreparing rules read as Collects for that reason + /// reversed. + /// + /// + [Fact] + public void AddressableGrowthIsTheRulesOwnAnswer() + { + foreach (var set in MatchedRules.All) + { + var addressable = set.AsAddressable(); + Assert.Equal(set.Rules.Count, addressable.Count); + for (var i = 0; i < set.Rules.Count; i++) + Assert.Equal(set.Rules[i].Growth, addressable[i].Growth); + } + } + + /// + /// A set's tier is the minimum over its rules, so reading it as every rule's tier + /// understates most of them. + /// + /// + /// All thirty registry sets declare , and one + /// conditional rule is enough to make that true of a set of a hundred. Asked per rule + /// instead, 181 of the 322 rules written as data are — + /// they hold for every complex argument, with nothing assumed. The counts are asserted + /// rather than the ratio, because the interesting failure is a rule quietly changing tier. + /// + [Fact] + public void SoundnessIsFinerPerRuleThanPerSet() + { + var rules = MatchedRules.All.SelectMany(set => set.Rules).ToList(); + Assert.Equal(322, rules.Count); + Assert.Equal(181, rules.Count(rule => rule.Soundness is Soundness.Sound)); + Assert.Equal(141, rules.Count(rule => rule.Soundness is Soundness.SoundUnderAssumptions)); + + // And every set still reports the weakest of them, which is what makes the set grain + // uninformative rather than wrong. + Assert.All(RewriteRules.All, + set => Assert.Equal(Soundness.SoundUnderAssumptions, set.Soundness)); + } + + /// + /// A rule's own tier reaches the registry, and a switch arm's absence of one is + /// reported as absent rather than as its set's. + /// + [Fact] + public void ARuleWrittenAsDataCarriesItsTierIntoTheRegistry() + { + var rationalize = RewriteRules.RationalizeDenominator; + Assert.All(rationalize.Rules, rule => Assert.NotNull(rule.Soundness)); + + // Every other set is still described by the generator, which has no tier to give. + var generated = RewriteRules.All.Where(set => set.Name != rationalize.Name); + Assert.All(generated, set => Assert.All(set.Rules, rule => Assert.Null(rule.Soundness))); + } + + /// + /// The identity has somewhere to live now, which is what blocked the registry from + /// describing the rules it runs. + /// + /// + /// + /// RuleRegistryGenerator reads the comment above a switch arm into + /// , and 95 of the registry's 407 arms carry one + /// — a / (b / c) = a * c / b and its like, which is the sentence a step would be + /// rendered as. A rule written as data has its identity in a comment too, and a comment is + /// not readable at run time, so converting a set to data used to lose the + /// description. Now it does not have to. + /// + /// + /// Demonstrated end to end on the one set the registry already describes from its data + /// form: two rules that reported no identity at all now report one, through the public + /// surface. + /// + /// + [Fact] + public void ADescriptionSurvivesTheJourneyIntoTheRegistry() + { + var described = RewriteRules.RationalizeDenominator.Rules; + Assert.Equal(2, described.Count); + Assert.Equal("k * (value / d) = (k * value) / d", described[0].Description); + Assert.Equal("num / (a + b) = num * (a - b) / (a^2 - b^2)", described[1].Description); + } + + /// + /// A rule read backwards says so, rather than repeating the forward identity as though it + /// were the same claim. + /// + [Fact] + public void AReversedRuleDoesNotClaimTheForwardIdentity() + { + var described = MatchedRules.All + .SelectMany(set => set.Rules) + .Where(rule => rule.Description is not null && rule.Reversed is not null) + .ToList(); + Assert.All(described, rule => + Assert.StartsWith("read backwards: ", rule.Reversed!.Description!)); + + var undescribed = MatchedRules.All + .SelectMany(set => set.Rules) + .Where(rule => rule.Description is null && rule.Reversed is not null); + Assert.All(undescribed, rule => Assert.Null(rule.Reversed!.Description)); + } + } +}