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); + } + } +}