From 87b8cd8ff66778a5667647c550fd2aef53260753 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 30 Aug 2026 12:13:54 +0000 Subject: [PATCH] Rule priorities, computed from the patterns rather than typed #746 tier 2 asks for "rule priorities and conflict resolution, with confluence and termination checked by tooling rather than asserted by authors". A rule set is first-match-wins, so where two rules fire at one node and disagree, whichever is tried first decides the answer -- and until now that was where somebody typed it. The one place it is written down is a comment on MatchedRules.CollapseMultipleFractions: the set "is order-dependent, since `Mulf(Divf, Divf)` has to be tried before `Mulf(a, Divf)` or the more general rule would swallow the special one". That is subsumption, observed by hand and then maintained by hand. `MatchPattern.Subsumes` computes it. It is a matching problem rather than a size comparison: a hole repeated across a pattern is an equality constraint, so `Mulf(a, a)` matches strictly less than `Mulf(a, b)` while having the same node count. So this matches one pattern against the other as a term, carrying an assignment from the wider pattern's holes to the narrower one's subpatterns and requiring a repeated hole to be assigned consistently. Sound in one direction only: true is a structural claim about every expression, false means not proved -- a hole carrying a predicate is arbitrary code, an Exact literal can equal a value of another runtime type, and a Gathered pattern is not reasoned about. Each of those refuses and leaves the pair ordered as written. `MatchedRuleSet.RulesByPriority` applies it, as a stable topological sort: no rule is tried before a rule its pattern subsumes, and declaration order everywhere else. **Four things measured.** Subsumption does not lie. Over all 322 rules, **961** ordered pairs claim it; **513** are put to the test by the corpus containing something the narrower pattern matches; **none** is contradicted across 56,892 nodes. The count of witnessed claims is asserted too, so a corpus that stopped reaching these shapes cannot turn that into a test which passes by asking nothing. It changes no answer today. Of the 5,480 within-set rule pairs, subsumption has an opinion about **28** -- across eight sets, Boolean and InequalityEquality carrying half -- and in every one the specific rule is already declared first. None is mutual. So this orders what was already ordered; what it adds is that inserting a general rule above a specific one no longer silently reverses an answer. `RulePriorityTest` holds the two orders equal, so the file stays readable as well as correct. The existing confluence corpus cannot see any of it. RuleConfluenceTest grows its third level with unary shapes only, so it never builds a quotient of quotients or a product of quotients -- which is exactly where a special rule and the general rule that would swallow it meet. On that corpus **none** of the 28 pairs overlaps at all. Growing the third level with binary shapes too takes the conflicts from **3 to 45**: six settled by priority, and **39** where neither pattern subsumes the other and the answer is decided by which was written first and by nothing else. Those 39 are recorded by name -- the data rules have names, which is what the note on `AConflictIsReportableAsThePatternsItIsBetween` asks for and what a `switch` arm cannot supply. None of them changes what Simplify returns. And one test asserted the opposite of this and had to change. TheOrderOfTheRulesIsLoadBearing built the set with its rules reversed and required the general rule to swallow the special one. It does not any more, which is the whole point -- the test's own comment gave the reason, that a `switch` gets its ordering "by accident of being written top to bottom". Replaced by two: the specific rule wins however the set is written, and where neither rule subsumes the other the order still decides everything. The classification also surfaced `quotient-of-two-quotients` answering 0 where the general rule answers NaN, on `x / (1/2) / (1 / 0)`. Left alone: Simplify returns NaN for that input, priority picks the same arm the declared order already picked, and the missing hypothesis is what Soundness.SoundUnderAssumptions on that rule is declaring. No public API change. Full suite: 8968 passed, 14 skipped, 0 failed. Part of #746 tier 2. --- .../Transformations/Matching/MatchPattern.cs | 194 +++++++++ .../Transformations/Matching/MatchedRule.cs | 112 ++++- .../Transformations/Matching/MatchedRules.cs | 9 + .../MatchedRulesAgreeWithTheSwitchTest.cs | 47 +- .../Transformations/RuleConfluenceTest.cs | 11 + .../Core/Transformations/RulePriorityTest.cs | 410 ++++++++++++++++++ 6 files changed, 772 insertions(+), 11 deletions(-) create mode 100644 Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchPattern.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchPattern.cs index 1eef70767..312649c78 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchPattern.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchPattern.cs @@ -313,6 +313,63 @@ private protected virtual bool TryMatchChoiceCore( /// internal abstract int NodeCount { get; } + /// + /// Whether every expression matches, this one matches too — so + /// that this pattern is the more general of the two, and a rule written on it + /// would swallow a rule written on if it were tried first. + /// + /// + /// + /// The fact behind an ordering that is currently a comment. + /// MatchedRules.CollapseMultipleFractions says of itself that it "is + /// order-dependent, since Mulf(Divf, Divf) has to be tried before + /// Mulf(a, Divf) or the more general rule would swallow the special one". That is + /// this relation, observed by hand and then maintained by hand. Computed instead, the + /// order it implies is derived from the patterns rather than from where somebody typed + /// them. + /// + /// + /// Sound in one direction only. is a claim — every + /// expression the other matches, this matches — and every clause below is structural, so + /// the claim holds for all expressions rather than for the ones a test happened to + /// generate. means not proved and never disproved: + /// a hole carrying a predicate is arbitrary code, an Exact literal can be equal to + /// a value of another runtime type (a rational that reduced to an integer), and an n-ary + /// Gathered pattern matches a family this does not attempt to reason about. Each of + /// those answers and leaves the pair ordered by where it was + /// written, which is what the code did before. + /// + /// + /// It is a matching problem, not a size comparison. A hole repeated across a + /// pattern is an equality constraint — Mulf(a, a) matches strictly less than + /// Mulf(a, b) while having the same node count — so this matches this pattern + /// against the other as a term, carrying an assignment from this pattern's holes to + /// the other's subpatterns and requiring a repeated hole to be assigned consistently. + /// Comparing would call those two equally general and get the + /// ordering wrong in the one case the ordering exists for. + /// + /// + internal bool Subsumes(MatchPattern other) + => other is not null + && SubsumesCore(other, new Dictionary(StringComparer.Ordinal)); + + /// + /// , carrying the assignment from this pattern's holes to the + /// subpatterns of the one being subsumed. Refusing is always sound, so the base answers + /// and a pattern kind that can reason about itself says so. + /// + private protected virtual bool SubsumesCore( + MatchPattern other, Dictionary assigned) => false; + + /// + /// Whether two patterns are written the same way, used to check that a repeated hole was + /// assigned consistently. Structural, and stricter than semantic equality: two patterns + /// that mean the same thing while being written differently answer + /// here, which loses a subsumption rather than inventing one. + /// + private protected virtual bool SameShapeAs(MatchPattern other) + => ReferenceEquals(this, other); + /// /// The expression this pattern stands for under , or /// where those bindings do not satisfy it. @@ -649,6 +706,50 @@ private protected override bool TryMatchOnceCore( internal override int NodeCount => 1; + /// + /// A hole is the most general thing a pattern can be, and it subsumes whatever it is + /// allowed to stand for — subject to the two constraints it may carry. + /// + /// + /// + /// A where predicate is arbitrary code over an expression, so what it admits + /// cannot be read off the pattern and this refuses rather than guesses. + /// + /// + /// A required type is checked against what the other pattern guarantees at its + /// root, which is — a necessary condition, and here the + /// direction that makes it usable: a pattern whose root is always a Divf is + /// certainly matched by a hole asking for an Entity. A pattern that guarantees + /// nothing, an Exact literal among them, is refused: two entities can be equal + /// without being the same runtime type, so a literal's own type is not what it + /// guarantees. + /// + /// + /// Then the assignment. A hole seen for the second time must stand for the same thing + /// it stood for the first time, which is what makes Mulf(a, a) strictly less + /// general than Mulf(a, b) rather than equally general. + /// + /// + private protected override bool SubsumesCore( + MatchPattern other, Dictionary assigned) + { + if (where is not null) return false; + if (required is not null + && (other.RequiredRootType is not { } guaranteed + || !required.IsAssignableFrom(guaranteed))) + return false; + if (assigned.TryGetValue(name, out var already)) + return already.SameShapeAs(other); + assigned[name] = other; + return true; + } + + private protected override bool SameShapeAs(MatchPattern other) + => other is AnyPattern that + && string.Equals(name, that.name, StringComparison.Ordinal) + && required == that.required + && where == that.where; + internal override bool TryBuild(Bindings bindings, out Entity built) { built = null!; @@ -745,6 +846,17 @@ private protected override bool TryMatchOnceCore( internal override int NodeCount => 1; + /// + /// A literal admits exactly one value, so it subsumes only a pattern admitting no + /// more than that — which among the kinds here is the same literal. + /// + private protected override bool SubsumesCore( + MatchPattern other, Dictionary assigned) + => other is ExactPattern that && value.Equals(that.value); + + private protected override bool SameShapeAs(MatchPattern other) + => other is ExactPattern that && value.Equals(that.value); + internal override bool TryBuild(Bindings bindings, out Entity built) { built = value; @@ -809,6 +921,88 @@ internal NodePattern(Type nodeType, MatchPattern[] children, bool commutative) internal override int NodeCount => nodeCount; + /// + /// A node pattern pins the node type and the arity, so it subsumes only another node + /// pattern of that type and arity whose children it subsumes in turn — under one + /// assignment, so that a hole repeated across children has to be assigned the same + /// subpattern in each. + /// + /// + /// Commutativity is a claim about this side. A commutative pattern matches a + /// node in either order, so subsuming needs only one of the two pairings to + /// work; a non-commutative one gets the written pairing and nothing else. When the + /// pattern being subsumed is the commutative one, it matches both orders, so this must + /// cover both — and a non-commutative pattern covers both only when its two children + /// are interchangeable, which the written pairing already decides. The assignment is + /// copied before each attempt, because a pairing that fails half way must not leave + /// its bindings behind for the other one. + /// + private protected override bool SubsumesCore( + MatchPattern other, Dictionary assigned) + { + if (other is not NodePattern that + || nodeType != that.nodeType + || children.Length != that.children.Length) + return false; + + if (that.commutative && !commutative) + { + var both = new Dictionary(assigned, StringComparer.Ordinal); + if (!InOrder(that.children, both, swapped: false)) return false; + if (!InOrder(that.children, both, swapped: true)) return false; + Adopt(assigned, both); + return true; + } + + if (commutative) + { + var straight = new Dictionary(assigned, StringComparer.Ordinal); + if (InOrder(that.children, straight, swapped: false)) + { + Adopt(assigned, straight); + return true; + } + var crossed = new Dictionary(assigned, StringComparer.Ordinal); + if (InOrder(that.children, crossed, swapped: true)) + { + Adopt(assigned, crossed); + return true; + } + return false; + } + + return InOrder(that.children, assigned, swapped: false); + } + + private bool InOrder( + MatchPattern[] theirs, Dictionary assigned, bool swapped) + { + for (var i = 0; i < children.Length; i++) + { + var theirIndex = swapped ? children.Length - 1 - i : i; + if (!children[i].SubsumesCore(theirs[theirIndex], assigned)) return false; + } + return true; + } + + private static void Adopt( + Dictionary into, Dictionary from) + { + foreach (var pair in from) into[pair.Key] = pair.Value; + } + + private protected override bool SameShapeAs(MatchPattern other) + { + if (other is not NodePattern that + || nodeType != that.nodeType + || commutative != that.commutative + || children.Length != that.children.Length) + return false; + for (var i = 0; i < children.Length; i++) + if (!children[i].SameShapeAs(that.children[i])) return false; + return true; + } + internal override IEnumerable BoundNames => children.SelectMany(c => c.BoundNames); public override string ToString() diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs index d6cd23301..96e4a89ac 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs @@ -416,6 +416,7 @@ internal MatchedRuleSet(string name, params MatchedRule[] rules) { Name = name ?? throw new ArgumentNullException(nameof(name)); this.rules = rules ?? throw new ArgumentNullException(nameof(rules)); + byPriority = ByPriority(this.rules); } /// @@ -427,6 +428,85 @@ internal MatchedRuleSet(string name, params MatchedRule[] rules) /// private readonly MatchedRule[] rules; + /// + /// The same rules in the order they are actually tried: the more specific rule + /// first, and declaration order wherever specificity has no opinion. See + /// . + /// + private readonly MatchedRule[] byPriority; + + /// + /// ordered so that no rule is tried before a rule its pattern + /// subsumes — the more specific one first — keeping declaration order everywhere else. + /// + /// + /// + /// What this replaces is the position somebody typed a rule at. A set is + /// first-match-wins, so where two rules both fire at a node and disagree, whichever comes + /// first decides the answer. Where one pattern subsumes the other that decision is not a + /// preference: the general rule would swallow the special one and the special one would + /// never fire at all, so the specific rule has to be tried first. That was maintained by + /// hand and written in a comment on one set; + /// computes it, and this applies it. + /// + /// + /// It changes no answer today, and that is a measurement rather than an intention. + /// Over the 5,480 within-set rule pairs in , subsumption has an + /// opinion about 28 of them — spread across eight sets, Boolean and + /// InequalityEquality carrying half — and in every one the specific rule is + /// already declared first. None is mutual. So this orders what was already ordered; what + /// it adds is that inserting a general rule above a specific one no longer silently + /// reverses an answer. RulePriorityTest holds the two orders equal, so the file + /// stays readable as well as correct. + /// + /// + /// A stable topological sort, taking the earliest-declared rule that has nothing left + /// which must precede it. Subsumption is conservative, so most pairs constrain nothing and + /// fall through to declaration order. It cannot cycle — a cycle would need each of two + /// rules to be strictly more general than the other — but a cycle is emitted in + /// declaration order rather than trusted not to happen, because a sort that silently drops + /// a rule would be a set quietly missing a rewrite. + /// + /// + private static MatchedRule[] ByPriority(MatchedRule[] declared) + { + var count = declared.Length; + if (count < 2) return declared; + + // mustPrecede[g] is the set of rules that have to be tried before rule g, which is + // every rule g's pattern strictly subsumes. + var waitingOn = new int[count]; + var blocks = new List[count]; + for (var g = 0; g < count; g++) + for (var sp = 0; sp < count; sp++) + { + if (g == sp) continue; + if (!declared[g].Left.Subsumes(declared[sp].Left)) continue; + if (declared[sp].Left.Subsumes(declared[g].Left)) continue; + (blocks[sp] ??= new List()).Add(g); + waitingOn[g]++; + } + + var ordered = new MatchedRule[count]; + var taken = new bool[count]; + for (var slot = 0; slot < count; slot++) + { + var next = -1; + for (var i = 0; i < count; i++) + if (!taken[i] && waitingOn[i] == 0) { next = i; break; } + // Only reachable if subsumption were not antisymmetric. Falling back to + // declaration order keeps every rule in the set. + if (next < 0) + for (var i = 0; i < count; i++) + if (!taken[i]) { next = i; break; } + taken[next] = true; + ordered[slot] = declared[next]; + if (blocks[next] is { } blocked) + foreach (var g in blocked) waitingOn[g]--; + } + return ordered; + } + // Indexing the rules by the node type each one requires -- the thing a `switch` cannot // do and a set of values can -- was tried here and is deliberately absent. Measured, a // per-runtime-type cache of the applicable rules cost 24 bytes per node and 912 bytes on @@ -438,7 +518,17 @@ internal MatchedRuleSet(string name, params MatchedRule[] rules) internal string Name { get; } - /// The rules, in the order they are tried. Enumerable, which is the whole point. + /// + /// The rules, in the order they are written. Enumerable, which is the whole + /// point. + /// + /// + /// Not necessarily the order they are tried in — see , which + /// puts a rule ahead of any rule whose pattern subsumes it. The two are equal today and + /// RulePriorityTest holds them equal, so this is the order to read the set in and to + /// index it by; and use it for that + /// reason. + /// internal IReadOnlyList Rules => rules; /// @@ -473,15 +563,25 @@ internal MatchedRuleSet Reversed internal Soundness Soundness => rules.Length == 0 ? Soundness.Sound : rules.Max(rule => rule.Soundness); - /// The first rule that applies at this node, or null. + /// + /// The first rule that applies at this node, or null — first in + /// 's order, which is the order it would be tried in. + /// internal MatchedRule? FirstMatching(Entity expr) { - foreach (var rule in rules) + foreach (var rule in byPriority) if (rule.TryApply(expr) is not null) return rule; return null; } + /// + /// The rules in the order they are tried, which is 's and not + /// necessarily 's. Exposed so that the two can be compared rather than + /// assumed equal. + /// + internal IReadOnlyList RulesByPriority => byPriority; + /// One rewrite at this node only, leaving children alone. /// /// These rules as values, so that a set written as data can @@ -575,11 +675,11 @@ private MatchedRule[] ApplicableTo(Type type) if (known.TryGetValue(type, out var found)) return found; - var matching = new List(rules.Length); - foreach (var rule in rules) + var matching = new List(byPriority.Length); + foreach (var rule in byPriority) if (rule.Left.RequiredRootType is not { } required || required.IsAssignableFrom(type)) matching.Add(rule); - found = matching.Count == rules.Length ? rules : matching.ToArray(); + found = matching.Count == byPriority.Length ? byPriority : matching.ToArray(); applicable = new Dictionary(known) { [type] = found }; return found; diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs index 33090086d..d7b6bcabd 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -117,6 +117,15 @@ internal static class MatchedRules /// One feature was added for it and nothing else changed, which is the answer to the /// question this set was picked to ask. /// + /// + /// The order-dependence above is no longer maintained by hand. + /// computes it — Mulf(a, Divf(b, c)) matches + /// everything Mulf(Divf(a, b), Divf(c, d)) matches and more — and + /// MatchedRuleSet.RulesByPriority puts the specific rule first because of that + /// rather than because of where it sits in this file. Four of this set's rule pairs are + /// ordered that way, and they are four of only six such conflicts in the whole registry; + /// RulePriorityTest lists them. + /// /// internal static MatchedRuleSet CollapseMultipleFractions { get; } = new( nameof(CollapseMultipleFractions), diff --git a/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs b/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs index e28d3814e..fe6ddb8ff 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs @@ -596,12 +596,20 @@ public void APredicateOnAHoleIsChecked(string expression, bool shouldFire) } /// - /// Order is part of the data. Reversing the two rules that overlap makes the general - /// one swallow the special one, which is what an ordered list is for and what a - /// switch gets by accident of being written top to bottom. + /// Order is part of the data — and where one pattern subsumes another it is no longer + /// part of the writing. Reversing this set used to make the general rule swallow the + /// special one; it does not any more, because the specific rule is put first by what the + /// two patterns are rather than by which was typed above the other. /// + /// + /// This test asserted the opposite until MatchedRuleSet.RulesByPriority existed, and + /// its own comment gave the reason to change it: a switch gets its ordering "by + /// accident of being written top to bottom", and an accident is what an ordered list of + /// values does not have to inherit. RulePriorityTest is where the mechanism and its + /// limits are. + /// [Fact] - public void TheOrderOfTheRulesIsLoadBearing() + public void ASubsumedRuleIsTriedFirstHoweverTheSetIsWritten() { var expr = "(a / b) * (c / d)".ToEntity(); var asWritten = MatchedRules.CollapseMultipleFractions.FirstMatching(expr); @@ -609,9 +617,38 @@ public void TheOrderOfTheRulesIsLoadBearing() var reversed = new MatchedRuleSet("reversed", MatchedRules.CollapseMultipleFractions.Rules.Reverse().ToArray()); - Assert.NotEqual("product-of-two-quotients", reversed.FirstMatching(expr)!.Name); + Assert.Equal("product-of-two-quotients", reversed.FirstMatching(expr)!.Name); + } + + /// + /// And where neither pattern subsumes the other, order is still the whole of the answer. + /// + /// + /// The two rules here both match a product of two quotients, and neither is more general + /// than the other — one takes the quotient on the left, the other the quotient on the + /// right — so nothing but their order decides which fires. Asked as a set of two so that + /// the rule which subsumes them both is out of the way; in the real set it wins, which is + /// the previous test. + /// + [Fact] + public void WhereNeitherRuleSubsumesTheOtherTheOrderStillDecides() + { + var expr = "(a / b) * (c / d)".ToEntity(); + var left = Named("product-with-a-quotient-on-the-left"); + var right = Named("product-with-a-quotient-on-the-right"); + + Assert.False(left.Left.Subsumes(right.Left)); + Assert.False(right.Left.Subsumes(left.Left)); + + Assert.Equal(left.Name, new MatchedRuleSet("left first", left, right) + .FirstMatching(expr)!.Name); + Assert.Equal(right.Name, new MatchedRuleSet("right first", right, left) + .FirstMatching(expr)!.Name); } + private static MatchedRule Named(string name) + => MatchedRules.CollapseMultipleFractions.Rules.Single(rule => rule.Name == name); + /// /// A rule-level guard over two bindings at once, which no predicate on a single /// hole can express: (a^b)^c = a^(b*c) holds for a positive base whatever the diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleConfluenceTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleConfluenceTest.cs index c8b841262..e4ca9735a 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/RuleConfluenceTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleConfluenceTest.cs @@ -38,6 +38,17 @@ namespace AngouriMath.Tests.Core.Transformations /// A sample, not a proof. Two arms that never overlap on the generated input say /// nothing either way, and are not recorded as agreeing. /// + /// + /// And a shallower sample than it reads as. The third level below is grown with unary + /// shapes only, so this corpus never builds a quotient of quotients or a product of quotients — + /// which is where a special rule and the general rule that would swallow it meet. + /// RulePriorityTest asks the same question of the same rules written as data, over a + /// corpus grown with binary shapes at every level, and finds 45 conflicts where this + /// finds three. It also names them as the rules they are between rather than as the indices + /// below, which is what the note on + /// asks for; a data rule has a name + /// and a switch arm does not. + /// /// [Trait("Area", "Core")] public sealed class RuleConfluenceTest diff --git a/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs new file mode 100644 index 000000000..c26b6ba98 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/RulePriorityTest.cs @@ -0,0 +1,410 @@ +// +// 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 System.Collections.Generic; +using System.Linq; +using AngouriMath.Core.Transformations.Matching; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// Which of two rules that both fire decides the answer, and why. + /// #746 tier 2 asks for + /// "rule priorities and conflict resolution, with confluence and termination checked by tooling + /// rather than asserted by authors". This is the priorities half; + /// is the confluence half. + /// + /// + /// + /// A rule set is first-match-wins, so where two rules fire at one node and disagree, + /// whichever is tried first decides the answer. Until now that was the position somebody + /// typed the rule at, and the one place it is written down is a comment on + /// : the set "is order-dependent, since + /// Mulf(Divf, Divf) has to be tried before Mulf(a, Divf) or the more general rule + /// would swallow the special one". + /// + /// + /// makes that a computed fact, and + /// MatchedRuleSet.RulesByPriority applies it. What is left over — a conflict where + /// neither pattern subsumes the other — is a bare choice, and those are recorded below by name + /// rather than left implicit in a file's layout. + /// + /// + [Trait("Area", "Core")] + public sealed class RulePriorityTest + { + private static readonly string[] Leaves = { "x", "y", "2", "-1", "1/2", "0", "1", "3" }; + + private static readonly string[] Unary = + { + "-({0})", "sqrt({0})", "abs({0})", "ln({0})", "e ^ ({0})", + "sin({0})", "cos({0})", "tan({0})", "sgn({0})", "1 / ({0})", + "({0}) ^ 2", "({0}) ^ (-1)", "({0}) ^ (1/2)", "({0})!", + }; + + private static readonly string[] Binary = + { + "({0}) + ({1})", "({0}) - ({1})", "({0}) * ({1})", "({0}) / ({1})", "({0}) ^ ({1})", + }; + + private static List Grow(IReadOnlyList below, bool binary) + { + var grown = new List(); + foreach (var shape in Unary) + foreach (var inner in below) + grown.Add(string.Format(shape, inner)); + if (binary) + foreach (var shape in Binary) + foreach (var left in below) + foreach (var right in below) + grown.Add(string.Format(shape, left, right)); + return grown; + } + + /// + /// Generated, deterministic, and three levels deep with binary shapes at every one, + /// which is the difference that matters here. + /// + /// + /// grows its third level with unary shapes only, so it + /// never builds a quotient of quotients or a product of quotients — and those are exactly + /// the shapes where a specific rule and the general rule that would swallow it both fire. + /// On that corpus none of the subsumption-ordered pairs below overlaps at all. + /// Growing the third level with binary shapes too finds six of them, and takes the + /// conflicts this sees from 3 to 45. + /// + private static List Expressions() + { + var level1 = new List(Leaves); + var level2 = Grow(level1, binary: true); + var level3 = Grow(level2.Where((_, i) => i % 11 == 0).ToList(), binary: true); + var parsed = new List(); + foreach (var source in level1.Concat(level2).Concat(level3)) + { + // Not every generated string parses, and that is the generator's business. + try { parsed.Add(source.ToEntity()); } + catch (Exception) { } + } + return parsed; + } + + private static List Nodes() + { + var nodes = new List(); + foreach (var expression in Expressions()) + foreach (var node in expression.Nodes) + nodes.Add(node); + return nodes; + } + + /// + /// Every pair of rules of one set where one pattern is strictly more general than the + /// other, as Set: specific before general — which is the order they have to be + /// tried in. + /// + private static SortedSet Subsumptions() + { + var found = new SortedSet(StringComparer.Ordinal); + foreach (var set in MatchedRules.All) + { + var rules = set.Rules; + for (var i = 0; i < rules.Count; i++) + for (var j = 0; j < rules.Count; j++) + { + if (i == j) continue; + if (!rules[i].Left.Subsumes(rules[j].Left)) continue; + if (rules[j].Left.Subsumes(rules[i].Left)) continue; + found.Add($"{set.Name}: {rules[j].Name} before {rules[i].Name}"); + } + } + return found; + } + + /// + /// The claim checked against the behaviour. + /// answers from the shape of two patterns, for every expression there is; this asks whether + /// it was telling the truth about the expressions there are. Wherever it claims one pattern + /// is at least as general as another, every node the narrower one matches has to be matched + /// by the wider one too. + /// + /// + /// Over all 322 rules rather than within a set, because the relation is about patterns and + /// nothing about it stops at a set boundary: 961 ordered pairs claim subsumption, + /// 513 of them are put to the test by the corpus containing something the narrower + /// pattern matches, and none is contradicted across 56,892 nodes. The count of witnessed + /// claims is asserted as well — a corpus that stopped reaching these shapes would otherwise + /// turn this into a test that passes by asking nothing. + /// + [Fact] + public void SubsumptionIsNeverContradictedByMatching() + { + var rules = MatchedRules.All + .SelectMany(set => set.Rules.Select(rule => (Set: set.Name, Rule: rule))) + .ToList(); + var claims = + new List<(string General, string Specific, MatchPattern Wide, MatchPattern Narrow)>(); + foreach (var wider in rules) + foreach (var narrower in rules) + { + if (ReferenceEquals(wider.Rule, narrower.Rule)) continue; + if (wider.Rule.Left.Subsumes(narrower.Rule.Left)) + claims.Add(( + $"{wider.Set}/{wider.Rule.Name}", + $"{narrower.Set}/{narrower.Rule.Name}", + wider.Rule.Left, + narrower.Rule.Left)); + } + + var nodes = Nodes(); + var witnessed = 0; + foreach (var (general, specific, wide, narrow) in claims) + { + var put = false; + foreach (var node in nodes) + { + bool narrowMatches; + try { narrowMatches = narrow.Matches(node); } + catch (Exception) { continue; } + if (!narrowMatches) continue; + put = true; + bool wideMatches; + try { wideMatches = wide.Matches(node); } + catch (Exception) { wideMatches = false; } + Assert.True(wideMatches, + $"'{general}' claims to subsume '{specific}', but {node.Stringize()} " + + $"matches {narrow} and not {wide}"); + } + if (put) witnessed++; + } + + Assert.Equal(961, claims.Count); + Assert.Equal(513, witnessed); + } + + /// + /// The invariant that used to be a comment. Where one rule of a set is strictly more + /// specific than another it has to be tried first, or it never fires at all and the set + /// quietly loses a rewrite. This holds the order rules are tried in equal to the order they + /// are written in, so the file stays readable as well as correct — and it is what fires + /// when somebody inserts a general rule above a specific one. + /// + [Fact] + public void TheOrderRulesAreTriedInIsTheOrderTheyAreWrittenIn() + { + foreach (var set in MatchedRules.All) + Assert.Equal( + set.Rules.Select(rule => rule.Name), + set.RulesByPriority.Select(rule => rule.Name)); + } + + /// + /// The orderings specificity has an opinion about, by name. + /// + /// + /// + /// Twenty-eight of the 5,480 within-set pairs, across eight sets, and none of them mutual. + /// They are recorded because the list is the thing that changes: a rule added to + /// Boolean or InequalityEquality whose pattern sits under an existing one + /// joins this list, and that is worth noticing when it happens rather than the first time + /// the two overlap. + /// + /// + /// One of the eight sets says anything about this in its own documentation, which is the + /// argument for computing it rather than writing it down. + /// + /// + [Fact] + public void TheRecordedSubsumptionsAreTheOnesThereAre() + { + var recorded = new[] + { + "Boolean: a-conjunction-of-negations-is-a-negated-disjunction before a-conjunction-with-a-falsehood-is-false", + "Boolean: a-conjunction-with-itself-is-itself before a-conjunction-with-a-falsehood-is-false", + "Boolean: a-disjunction-of-negations-is-a-negated-conjunction before a-disjunction-with-a-truth-is-true", + "Boolean: a-disjunction-of-negations-is-a-negated-conjunction before a-negation-or-something-is-an-implication", + "Boolean: a-disjunction-with-itself-is-itself before a-disjunction-with-a-truth-is-true", + "Boolean: a-negation-or-something-is-an-implication before a-disjunction-with-a-truth-is-true", + "CollapseMultipleFractions: product-of-two-quotients before product-with-a-quotient-on-the-left", + "CollapseMultipleFractions: product-of-two-quotients before product-with-a-quotient-on-the-right", + "CollapseMultipleFractions: quotient-of-two-quotients before quotient-whose-denominator-is-a-quotient", + "CollapseMultipleFractions: quotient-of-two-quotients before quotient-whose-numerator-is-a-quotient", + "CollapseTrigonometricFunctions: cosine-over-sine-is-the-cotangent before a-quotient-by-a-sine-is-a-cosecant", + "CollapseTrigonometricFunctions: sine-over-cosine-is-the-tangent before a-quotient-by-a-cosine-is-a-secant", + "Common: a-product-of-two-quotients-is-one-quotient before a-quotient-times-a-thing-keeps-the-divisor-outermost", + "Common: a-product-of-two-quotients-is-one-quotient before a-thing-times-a-quotient-keeps-the-divisor-outermost", + "ExpandFactorialDivisions: a-quotient-of-shifted-factorials before a-quotient-of-a-plain-factorial-by-a-shifted-one", + "ExpandFactorialDivisions: a-quotient-of-shifted-factorials before a-quotient-of-a-shifted-factorial-by-a-plain-one", + "FactorizeFactorialMultiplications: a-shifted-factorial-times-the-next-term before a-plain-factorial-times-the-next-term", + "FactorizeFactorialMultiplications: a-shifted-factorial-times-the-next-term before a-shifted-factorial-times-a-bare-term", + "InequalityEquality: a-greater-than-or-equal-as-written-is-at-least before two-comparisons-of-one-pair-that-leave-no-case-are-true", + "InequalityEquality: a-greater-than-or-equal-the-other-way-round-is-at-most before two-comparisons-of-one-pair-that-leave-no-case-are-true", + "InequalityEquality: a-less-than-or-equal-as-written-is-at-most before two-comparisons-of-one-pair-that-leave-no-case-are-true", + "InequalityEquality: a-less-than-or-equal-the-other-way-round-is-at-least before two-comparisons-of-one-pair-that-leave-no-case-are-true", + "InequalityEquality: an-equality-or-a-greater-than-as-written-is-at-least before two-comparisons-of-one-pair-that-leave-no-case-are-true", + "InequalityEquality: an-equality-or-a-greater-than-the-other-way-round-is-at-most before two-comparisons-of-one-pair-that-leave-no-case-are-true", + "InequalityEquality: an-equality-or-a-less-than-as-written-is-at-most before two-comparisons-of-one-pair-that-leave-no-case-are-true", + "InequalityEquality: an-equality-or-a-less-than-the-other-way-round-is-at-least before two-comparisons-of-one-pair-that-leave-no-case-are-true", + "Power: a-logarithm-of-a-reciprocal-in-a-reciprocal-base-turns-round-twice before a-logarithm-in-a-reciprocal-base-negates", + "Power: a-logarithm-of-a-reciprocal-in-a-reciprocal-base-turns-round-twice before a-logarithm-of-a-reciprocal-negates", + }; + Assert.Equal(recorded.OrderBy(name => name, StringComparer.Ordinal), Subsumptions()); + } + + /// + /// Every conflict observed on the corpus, split by whether priority decides it. + /// + private static (SortedSet ByPriority, SortedSet ByDeclaration) Conflicts() + { + var byPriority = new SortedSet(StringComparer.Ordinal); + var byDeclaration = new SortedSet(StringComparer.Ordinal); + var expressions = Expressions(); + foreach (var set in MatchedRules.All) + { + var rules = set.RulesByPriority; + foreach (var expression in expressions) + foreach (var node in expression.Nodes) + { + var firing = new List(); + for (var i = 0; i < rules.Count; i++) + { + Entity? applied; + try { applied = rules[i].TryApply(node); } + catch (Exception) { continue; } + // A rule that matches and hands the node back has not fired. + if (applied is not null && !applied.Equals(node)) firing.Add(i); + } + if (firing.Count < 2) continue; + + // Compared after normalisation, so that two rules writing one answer two + // ways are not called a conflict. + var settled = new Dictionary(); + foreach (var i in firing) + { + try { settled[i] = rules[i].TryApply(node)!.InnerSimplified; } + catch (Exception) { } + } + foreach (var i in firing) + foreach (var j in firing) + { + if (i >= j) continue; + if (!settled.TryGetValue(i, out var left)) continue; + if (!settled.TryGetValue(j, out var right)) continue; + if (left.Equals(right)) continue; + var key = $"{set.Name}: {rules[i].Name} | {rules[j].Name}"; + var wider = rules[i].Left.Subsumes(rules[j].Left); + var narrower = rules[j].Left.Subsumes(rules[i].Left); + if (wider ^ narrower) byPriority.Add(key); + else byDeclaration.Add(key); + } + } + } + return (byPriority, byDeclaration); + } + + /// + /// The conflicts priority settles: two rules fire, they disagree, and one pattern is + /// strictly more general than the other — so which of them wins is a consequence of what + /// the rules are rather than of where they were typed. + /// + /// + /// All six are a general and a special case of one rewrite meeting on a nested quotient, + /// and four are the pair describes in + /// prose. That the prose was right is the point: what it could not do is stay right on its + /// own. + /// + [Fact] + public void PrioritySettlesTheConflictsItHasAnOpinionAbout() + { + var recorded = new[] + { + "CollapseMultipleFractions: product-of-two-quotients | product-with-a-quotient-on-the-left", + "CollapseMultipleFractions: product-of-two-quotients | product-with-a-quotient-on-the-right", + "CollapseMultipleFractions: quotient-of-two-quotients | quotient-whose-denominator-is-a-quotient", + "CollapseMultipleFractions: quotient-of-two-quotients | quotient-whose-numerator-is-a-quotient", + "Common: a-product-of-two-quotients-is-one-quotient | a-quotient-times-a-thing-keeps-the-divisor-outermost", + "Common: a-product-of-two-quotients-is-one-quotient | a-thing-times-a-quotient-keeps-the-divisor-outermost", + }; + Assert.Equal( + recorded.OrderBy(name => name, StringComparer.Ordinal), Conflicts().ByPriority); + } + + /// + /// The conflicts priority does not settle: two rules fire and disagree, and neither + /// pattern is more general than the other, so the answer is decided by which was written + /// first and by nothing else. + /// + /// + /// + /// These are the ones a reader cannot see. Where one pattern subsumes another the + /// ordering is at least legible in the patterns; here it is legible nowhere, and this list + /// is the only place it is written down. + /// + /// + /// Three of them are what records at switch grain, + /// by index. The other thirty-six come from asking the data rules instead — which have + /// names, so an ordering can be recorded as the rules it is between rather than as two + /// numbers that move whenever somebody edits the file. + /// + /// + /// None of the thirty-nine changes what returns: the + /// normalisation and the passes after it converge. They are recorded because that is a fact + /// about the current rules and not a guarantee. + /// + /// + [Fact] + public void OnlyTheRecordedConflictsAreLeftToDeclarationOrder() + { + var recorded = new[] + { + "CollapseMultipleFractions: product-with-a-quotient-on-the-right | product-with-a-quotient-on-the-left", + "CollapseMultipleFractions: quotient-whose-numerator-is-a-quotient | quotient-whose-denominator-is-a-quotient", + "Common: a-common-factor-of-two-added-products-comes-out | a-negated-term-in-a-sum-is-a-subtraction", + "Common: a-common-factor-of-two-added-products-comes-out | a-term-added-to-itself-doubles", + "Common: a-common-factor-of-two-subtracted-products-comes-out | a-term-subtracted-from-itself-vanishes", + "Common: a-factor-shared-by-a-product-and-a-quotient-added-comes-out | a-negated-term-in-a-sum-is-a-subtraction", + "Common: a-factor-shared-by-a-quotient-and-a-product-added-comes-out | a-negated-term-in-a-sum-is-a-subtraction", + "Common: a-function-times-a-number-puts-the-number-first | a-negated-reciprocal-rational-factor-is-a-negated-division", + "Common: a-product-of-two-quotients-is-one-quotient | a-thing-times-itself-is-its-square", + "Common: a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero | a-difference-over-its-own-reverse-is-minus-one", + "Common: a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero | a-shared-factor-cancels-between-two-products", + "Common: a-quotient-times-a-thing-keeps-the-divisor-outermost | a-negated-reciprocal-rational-factor-is-a-negated-division", + "Common: a-quotient-times-a-thing-keeps-the-divisor-outermost | a-thing-times-a-quotient-keeps-the-divisor-outermost", + "Common: a-quotient-times-a-thing-keeps-the-divisor-outermost | a-thing-times-itself-is-its-square", + "Common: a-term-added-to-itself-doubles | a-negated-term-in-a-sum-is-a-subtraction", + "Common: a-thing-times-a-quotient-keeps-the-divisor-outermost | a-negated-reciprocal-rational-factor-is-a-negated-division", + "Common: a-thing-times-a-quotient-keeps-the-divisor-outermost | a-thing-times-itself-is-its-square", + "Common: a-variable-times-a-number-puts-the-number-first | a-reciprocal-rational-factor-is-a-division", + "Common: dividing-by-a-quotient-multiplies-by-its-reciprocal | a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero", + "Common: dividing-by-a-quotient-multiplies-by-its-reciprocal | dividing-twice-divides-by-the-product", + "Common: dividing-twice-divides-by-the-product | a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero", + "Common: two-numbers-around-a-factor-collect | a-negated-reciprocal-rational-factor-is-a-negated-division", + "Common: two-numeric-factors-around-a-variable-collect | a-negated-reciprocal-rational-factor-is-a-negated-division", + "Common: two-numeric-multiples-of-one-variable-add | a-common-factor-of-two-added-products-comes-out", + "Common: two-numeric-multiples-of-one-variable-add | a-negated-term-in-a-sum-is-a-subtraction", + "Common: two-numeric-multiples-of-one-variable-add | a-term-added-to-itself-doubles", + "Common: two-numeric-multiples-of-one-variable-subtract | a-common-factor-of-two-subtracted-products-comes-out", + "DivisionPreparing: reciprocal-factor-becomes-a-quotient | numeric-numerator-out-of-a-product", + "Factorization: a-factor-shared-by-two-added-products-comes-out | a-term-added-to-itself-doubles", + "Factorization: a-factor-shared-by-two-subtracted-products-comes-out | a-term-subtracted-from-itself-vanishes", + "Factorization: a-term-added-to-itself-doubles | a-common-factor-is-collected-out-of-a-whole-sum", + "NumericNeat: a-negative-factor-in-a-left-product-comes-out | a-negative-factor-in-a-right-product-comes-out", + "NumericNeat: a-negative-factor-in-a-numerator-comes-out | a-negative-factor-in-a-denominator-comes-out", + "Power: a-numeric-factor-comes-out-of-a-power-of-a-product | a-reciprocal-power-is-a-quotient", + "Power: a-power-of-a-power-multiplies-the-exponents | a-reciprocal-power-is-a-quotient", + "Power: a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero | two-powers-of-one-base-divide-by-subtracting-exponents", + "Power: a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero | two-powers-of-one-exponent-share-a-quotient-of-bases", + "Power: two-powers-of-one-base-divide-by-subtracting-exponents | two-powers-of-one-exponent-share-a-quotient-of-bases", + "Power: two-powers-of-one-base-multiply-by-adding-exponents | two-powers-of-one-exponent-share-a-base", + }; + Assert.Equal( + recorded.OrderBy(name => name, StringComparer.Ordinal), Conflicts().ByDeclaration); + } + } +}