diff --git a/Sources/.editorconfig b/Sources/.editorconfig index 638469163..d95adc5c3 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -18,6 +18,9 @@ file_header_template=\nCopyright (c) 2019-2022 Angouri.\nAngouriMath is licensed # IDE0073 fail on all 367 files that already carry the old one, which is a rewrite of every # header folded into whatever branch happened to need a new file -- so the year moves per # directory as directories are added, not all at once. +[AngouriMath/Core/Transformations/Matching/*.cs] +file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n + [AngouriMath/Core/Transformations/*.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchPattern.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchPattern.cs new file mode 100644 index 000000000..6ee005390 --- /dev/null +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchPattern.cs @@ -0,0 +1,217 @@ +// +// 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; + +namespace AngouriMath.Core.Transformations.Matching +{ + /// A set of named holes and what they stood for. + internal sealed class Bindings + { + private readonly Dictionary bound; + + internal static Bindings Empty { get; } = new(new Dictionary()); + + private Bindings(Dictionary bound) => this.bound = bound; + + internal bool TryGet(string name, out Entity value) => bound.TryGetValue(name, out value!); + + internal Entity this[string name] => bound[name]; + + internal int Count => bound.Count; + + /// + /// A new set with one more name bound. Copied rather than mutated because matching + /// backtracks: a branch that fails must leave nothing behind for the branch tried next, + /// and sharing one dictionary across attempts is how a matcher silently starts + /// accepting things it should not. + /// + internal Bindings With(string name, Entity value) + { + var copy = new Dictionary(bound) { [name] = value }; + return new Bindings(copy); + } + } + + /// + /// The left-hand side of a rewrite rule, as a value rather than as an arm of a + /// switch. + /// + /// + /// + /// #746 v1.0 asks for + /// "pattern matching as a data structure, not a switch: matchable, enumerable, + /// testable, with commutative and n-ary matching handled by the engine" + /// (#248). Three + /// things tier 2 wants are blocked on rules not being values: a rule cannot carry its own + /// justification tier, a rule cannot be addressed individually + /// (#825), and an + /// e-graph cannot match against an e-class because there is no pattern to match with. + /// + /// + /// Matching enumerates solutions rather than returning one, and that is not a + /// refinement — it is what commutativity requires. b*a + c*a has to match + /// k*p + k*q with k = a, and a matcher that commits to the first way of + /// matching the left operand binds k = b and then fails on the right, in both + /// orders of the sum. Only backtracking finds it, so every pattern yields every way it can + /// match and the caller takes the first that survives to the end. + /// + /// + /// Commutativity is over a binary node: a + b matches b + a. Matching + /// across a flattened chain — a + b + c against x + y with x = a + b — + /// is the n-ary half of #248 and is not here; the associative case wants the operands + /// gathered first and is a larger change than the commutative one. + /// + /// + internal abstract class MatchPattern + { + /// + /// Every way can match, extending . + /// Empty where it cannot. Lazy, so a caller that wants one solution does not pay for + /// the rest. + /// + internal abstract IEnumerable Match(Entity expr, Bindings bindings); + + /// The names this pattern binds, so a right-hand side can be checked for a typo. + internal abstract IEnumerable BoundNames { get; } + + /// Whether it matches at all, which is asked for one answer. + internal bool Matches(Entity expr) => Match(expr, Bindings.Empty).Any(); + + /// Matches anything and binds it. + internal static MatchPattern Any(string name) => new AnyPattern(name, null, null); + + /// Matches anything of the given node type and binds it. + internal static MatchPattern Any(string name) where T : Entity + => new AnyPattern(name, typeof(T), null); + + /// + /// Matches anything of the given node type that also satisfies . + /// + /// + /// The C# property pattern — Integer { IsPositive: true } — as data. A predicate + /// on the node travels with the hole and can be read off a rule, where a condition about + /// the match as a whole belongs in the rule's when and cannot. + /// + internal static MatchPattern Any(string name, Func where) where T : Entity + => new AnyPattern(name, typeof(T), node => where((T)node)); + + /// Matches exactly this expression, binding nothing. + internal static MatchPattern Exact(Entity value) => new ExactPattern(value); + + /// Matches a node of the given type whose children match, in order. + internal static MatchPattern Node(params MatchPattern[] children) where T : Entity + => new NodePattern(typeof(T), children, commutative: false); + + /// + /// Matches a two-child node of the given type whose children match in either + /// order. One of these replaces the four arms a switch needs to say the same + /// thing about a commutative operator. + /// + internal static MatchPattern Commutative(MatchPattern left, MatchPattern right) where T : Entity + => new NodePattern(typeof(T), new[] { left, right }, commutative: true); + + private sealed class AnyPattern : MatchPattern + { + private readonly string name; + private readonly Type? required; + private readonly Func? where; + + internal AnyPattern(string name, Type? required, Func? where) + { + this.name = name; + this.required = required; + this.where = where; + } + + internal override IEnumerable BoundNames => new[] { name }; + + internal override IEnumerable Match(Entity expr, Bindings bindings) + { + if (required is not null && !required.IsInstanceOfType(expr)) yield break; + if (where is not null && !where(expr)) yield break; + // A repeated name is the `when any1 == any1a` guard, made structural: the + // second occurrence matches only what the first one already stood for. + if (bindings.TryGet(name, out var already)) + { + if (already.Equals(expr)) yield return bindings; + yield break; + } + yield return bindings.With(name, expr); + } + } + + private sealed class ExactPattern : MatchPattern + { + private readonly Entity value; + + internal ExactPattern(Entity value) => this.value = value; + + internal override IEnumerable BoundNames => Array.Empty(); + + internal override IEnumerable Match(Entity expr, Bindings bindings) + { + if (value.Equals(expr)) yield return bindings; + } + } + + private sealed class NodePattern : MatchPattern + { + private readonly Type nodeType; + private readonly MatchPattern[] children; + private readonly bool commutative; + + internal NodePattern(Type nodeType, MatchPattern[] children, bool commutative) + { + this.nodeType = nodeType; + this.children = children; + this.commutative = commutative; + if (commutative && children.Length != 2) + throw new ArgumentException("commutative matching is over a two-child node", + nameof(children)); + } + + internal override IEnumerable BoundNames => children.SelectMany(c => c.BoundNames); + + internal override IEnumerable Match(Entity expr, Bindings bindings) + { + if (!nodeType.IsInstanceOfType(expr)) yield break; + var actual = expr.DirectChildren; + if (actual.Count != children.Length) yield break; + + foreach (var solution in MatchInOrder(actual, bindings, 0)) + yield return solution; + if (!commutative) yield break; + // The other way round. Yielded second so that a rule reading the first solution + // sees the same one a `switch` arm written in this order would have produced. + var swapped = new[] { actual[1], actual[0] }; + foreach (var solution in MatchInOrder(swapped, bindings, 0)) + yield return solution; + } + + /// + /// The cross product over the children: every way the first child matches, times + /// every way the rest match given that. This is where backtracking happens, and it + /// is why returns a sequence. + /// + private IEnumerable MatchInOrder( + IReadOnlyList actual, Bindings bindings, int index) + { + if (index == children.Length) + { + yield return bindings; + yield break; + } + foreach (var head in children[index].Match(actual[index], bindings)) + foreach (var rest in MatchInOrder(actual, head, index + 1)) + yield return rest; + } + } + } +} diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs new file mode 100644 index 000000000..8779991a2 --- /dev/null +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs @@ -0,0 +1,123 @@ +// +// 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; + +namespace AngouriMath.Core.Transformations.Matching +{ + /// + /// One rewrite rule, addressable on its own: a name, a pattern to match, a side condition, + /// what to build, and the tier its claim is justified at. + /// + /// + /// + /// This is what #825 + /// asks for and what a switch arm cannot be. A rule here can be listed, named in a + /// bug report, tested by itself, and — the part that matters most — + /// carry its own . Today the tier is declared per rule *set*, + /// and since a set's tier is the minimum over its arms, one conditional arm drags eighteen + /// unconditional ones down with it; that is why all thirty sets in the registry declare the + /// same value and the field distinguishes nothing. + /// + /// + /// The right-hand side is a builder over the bindings rather than a second pattern. That is + /// a deliberate first step and not the end state: a rule whose right-hand side is also data + /// can be read backwards, which is what tier 2's "direction" field wants. Building it as + /// data before the matching half is proven would be guessing at two shapes at once. + /// + /// + internal sealed class MatchedRule + { + internal MatchedRule( + string name, + MatchPattern left, + Func right, + Soundness soundness, + Func? when = null) + { + Name = name ?? throw new ArgumentNullException(nameof(name)); + Left = left ?? throw new ArgumentNullException(nameof(left)); + this.right = right ?? throw new ArgumentNullException(nameof(right)); + Soundness = soundness; + this.when = when; + } + + private readonly Func right; + private readonly Func? when; + + /// What to call this rule in a report, a test or a bug. + internal string Name { get; } + + /// The shape it fires on. + internal MatchPattern Left { get; } + + /// How well justified this rule's claim is — per rule, which is the point. + internal Soundness Soundness { get; } + + /// + /// The rewritten expression, or where the rule does not apply. + /// Never throws: a builder that fails on the bindings it was handed is a rule that did + /// not apply, which is a refusal rather than an error. + /// + internal Entity? TryApply(Entity expr) + { + // Every way the pattern matches, in order, and the first that also satisfies the + // side condition wins. Taking only the first *match* would be wrong: commutativity + // means `b*a + c*a` matches `k*p + k*q` several ways and only some of them bind + // `k` to the factor the condition is about. + foreach (var bindings in Left.Match(expr, Bindings.Empty)) + { + if (when is not null && !when(bindings)) + continue; + try { return right(bindings); } + catch { return null; } + } + return null; + } + } + + /// + /// An ordered list of , applied first-match-wins over every node — + /// the same discipline the switch-based rule sets follow, so that one can be + /// exchanged for the other and the two compared. + /// + internal sealed class MatchedRuleSet + { + internal MatchedRuleSet(string name, params MatchedRule[] rules) + { + Name = name ?? throw new ArgumentNullException(nameof(name)); + Rules = rules ?? throw new ArgumentNullException(nameof(rules)); + } + + internal string Name { get; } + + /// The rules, in the order they are tried. Enumerable, which is the whole point. + internal IReadOnlyList Rules { get; } + + /// + /// The weakest tier any of its rules is justified at — derived rather than declared, + /// so it cannot drift from the rules it is about. + /// + internal Soundness Soundness + => Rules.Count == 0 ? Soundness.Sound : Rules.Max(rule => rule.Soundness); + + /// The first rule that applies at this node, or null. + internal MatchedRule? FirstMatching(Entity expr) + => Rules.FirstOrDefault(rule => rule.TryApply(expr) is not null); + + /// One rewrite at this node only, leaving children alone. + internal Entity ApplyHere(Entity expr) + { + foreach (var rule in Rules) + if (rule.TryApply(expr) is { } rewritten) + return rewritten; + return expr; + } + } +} diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs new file mode 100644 index 000000000..63aa5f48e --- /dev/null +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRules.cs @@ -0,0 +1,221 @@ +// +// 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 static AngouriMath.Entity; +using static AngouriMath.Entity.Number; + +namespace AngouriMath.Core.Transformations.Matching +{ + /// + /// Rule sets written as data. One so far, deliberately: the value of this file is that a + /// set expressed here can be checked against the switch that already expresses it, + /// so the migration is proven one set at a time rather than asserted wholesale. + /// + /// + /// MatchedRulesAgreeWithTheSwitchTest is that check. It runs both forms over + /// generated expressions and requires them to agree on every one, which is what makes + /// replacing the switch a mechanical step rather than a leap. + /// + internal static class MatchedRules + { + /// + /// , as data. + /// + /// + /// Chosen first because it is three rules with no side conditions, so it exercises node + /// matching, a literal, a typed hole and a repeated-free binding without also needing + /// commutativity — which the matcher does not have and which #248 is about. + /// + internal static MatchedRuleSet DivisionPreparing { get; } = new( + nameof(DivisionPreparing), + + // a * (1 / b) -> a / b + new MatchedRule( + "reciprocal-factor-becomes-a-quotient", + MatchPattern.Node( + MatchPattern.Any("a"), + MatchPattern.Node(MatchPattern.Exact(Integer.Create(1)), MatchPattern.Any("b"))), + bound => bound["a"] / bound["b"], + // a * (1/b) and a/b are undefined at exactly the same points, but the quotient + // is a quotient either way, so this inherits division's own condition rather + // than adding one. Left at the conservative tier until the audit reaches it. + Soundness.SoundUnderAssumptions), + + // (c * a) / b -> c * (a / b), for a numeric c + new MatchedRule( + "numeric-factor-out-of-a-quotient", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("a")), + MatchPattern.Any("b")), + bound => bound["c"] * (bound["a"] / bound["b"]), + Soundness.SoundUnderAssumptions), + + // (c / a) * b -> c * (b / a), for a numeric c + new MatchedRule( + "numeric-numerator-out-of-a-product", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("a")), + MatchPattern.Any("b")), + bound => bound["c"] * (bound["b"] / bound["a"]), + Soundness.SoundUnderAssumptions)); + + /// + /// , as data. + /// + /// + /// + /// The second set expressed here, and chosen because it is harder in three ways that + /// test whether the shape generalises rather than whether it works once. It has eight + /// rules instead of three; 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; and it needs a predicate on a + /// hole — Integer { IsPositive: true } — which the matcher did not have. + /// + /// + /// One feature was added for it and nothing else changed, which is the answer to the + /// question this set was picked to ask. + /// + /// + internal static MatchedRuleSet CollapseMultipleFractions { get; } = new( + nameof(CollapseMultipleFractions), + + // (a / b) ^ c -> a^c / b^c, for a positive whole c + new MatchedRule( + "positive-power-of-a-quotient-distributes", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), + MatchPattern.Any("c", whole => whole.IsPositive)), + bound => bound["a"].Pow(bound["c"]) / bound["b"].Pow(bound["c"]), + Soundness.SoundUnderAssumptions), + + // (a * b) ^ c -> a^c * b^c, for a positive whole c + new MatchedRule( + "positive-power-of-a-product-distributes", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), + MatchPattern.Any("c", whole => whole.IsPositive)), + bound => bound["a"].Pow(bound["c"]) * bound["b"].Pow(bound["c"]), + Soundness.SoundUnderAssumptions), + + // (a/b) * (c/d) -> (a*c) / (b*d). Before the two below it, which are more general. + new MatchedRule( + "product-of-two-quotients", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("d"))), + bound => bound["a"] * bound["c"] / (bound["b"] * bound["d"]), + Soundness.SoundUnderAssumptions), + + new MatchedRule( + "product-with-a-quotient-on-the-right", + MatchPattern.Node( + MatchPattern.Any("a"), + MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("c"))), + bound => bound["a"] * bound["b"] / bound["c"], + Soundness.SoundUnderAssumptions), + + new MatchedRule( + "product-with-a-quotient-on-the-left", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), + MatchPattern.Any("c")), + bound => bound["a"] * bound["c"] / bound["b"], + Soundness.SoundUnderAssumptions), + + // (a/b) / (c/d) -> (a*d) / (b*c). Likewise before the two below it. + new MatchedRule( + "quotient-of-two-quotients", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), + MatchPattern.Node(MatchPattern.Any("c"), MatchPattern.Any("d"))), + bound => bound["a"] * bound["d"] / (bound["b"] * bound["c"]), + Soundness.SoundUnderAssumptions), + + new MatchedRule( + "quotient-whose-numerator-is-a-quotient", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), + MatchPattern.Any("c")), + bound => bound["a"] / (bound["b"] * bound["c"]), + Soundness.SoundUnderAssumptions), + + new MatchedRule( + "quotient-whose-denominator-is-a-quotient", + MatchPattern.Node( + MatchPattern.Any("a"), + MatchPattern.Node(MatchPattern.Any("b"), MatchPattern.Any("c"))), + bound => bound["a"] * bound["c"] / bound["b"], + Soundness.SoundUnderAssumptions)); + + /// + /// The one rule from that carries a real + /// side condition, as data. + /// + /// + /// + /// The third set expressed here, and the one that exercises the last piece of the + /// design: a condition about the match as a whole rather than about one hole. + /// (a^b)^c = a^(b*c) is true for a positive base whatever the exponents, and for + /// any base when the outer exponent is whole — and false outside those two, which is + /// #752: applied + /// unconditionally it turned sqrt(x^2) into x, which at -0.63 is -0.63 + /// where the expression is 0.63. + /// + /// + /// It is also the first rule here whose carries information + /// rather than repeating its neighbours'. The condition is what makes it + /// , and a reader can see the condition + /// and the tier in one place — which is the whole argument for rules being data, since + /// in the switch the tier lives on the set and the condition lives forty lines + /// away from it. + /// + /// + internal static MatchedRuleSet PowerOfPower { get; } = new( + nameof(PowerOfPower), + + new MatchedRule( + "power-of-a-power-multiplies-its-exponents", + MatchPattern.Node( + MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("b")), + MatchPattern.Any("c")), + bound => new Powf(bound["a"], bound["b"] * bound["c"]), + Soundness.SoundUnderAssumptions, + // Two bindings at once, which no predicate on a single hole can express. + when: bound => bound["c"] is Integer + || bound["a"].Evaled is Real { IsPositive: true })); + + /// + /// k*p + k*q = k*(p + q), written once, where the switch writes it four + /// times. + /// + /// + /// + /// This is what #248 + /// is for. Patterns.CommonRules spells the same identity out in four arms — + /// (k*p) + (k*q), (p*k) + (k*q), (k*p) + (q*k), (p*k) + (q*k) + /// — because a C# pattern cannot say "either way round". One commutative pattern says + /// it, and the four arms become one rule. + /// + /// + /// It is also the first rule here that is . + /// Distributivity holds for every complex k, p and q with no side + /// condition and no branch to choose, so the tier says something its neighbours' does + /// not — which is the whole reason a tier belongs on a rule rather than on a set. + /// + /// + internal static MatchedRuleSet SharedFactor { get; } = new( + nameof(SharedFactor), + + new MatchedRule( + "a-shared-factor-comes-out-of-a-sum", + MatchPattern.Commutative( + MatchPattern.Commutative(MatchPattern.Any("k"), MatchPattern.Any("p")), + MatchPattern.Commutative(MatchPattern.Any("k"), MatchPattern.Any("q"))), + bound => bound["k"] * (bound["p"] + bound["q"]), + Soundness.Sound)); + } +} diff --git a/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs b/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs new file mode 100644 index 000000000..4e8f65419 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/MatchedRulesAgreeWithTheSwitchTest.cs @@ -0,0 +1,424 @@ +// +// 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.Collections.Generic; +using System.Linq; +using AngouriMath; +using AngouriMath.Core.Transformations; +using AngouriMath.Core.Transformations.Matching; +using AngouriMath.Extensions; +using AngouriMath.Functions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// A rule set written as **data** has to do exactly what the switch that already + /// expresses it does. https://github.com/asc-community/AngouriMath/issues/746 v1.0 asks for + /// pattern matching as a data structure; this is what makes replacing a `switch` with one a + /// mechanical step rather than a leap of faith. + /// + /// + /// The comparison is differential and generative: both forms are run over every expression + /// a small grammar produces, and they must agree on all of them. A hand-written list of + /// cases would only prove the cases someone thought of, and the interesting disagreements + /// in a matcher are the shapes nobody pictured — a literal that is a `Rational` rather than + /// an `Integer`, a node whose child count differs from the pattern's, a name bound twice. + /// + [Trait("Area", "Core")] + public sealed class MatchedRulesAgreeWithTheSwitchTest + { + private static readonly string[] Leaves = { "x", "y", "2", "-1", "1/2", "1", "0" }; + + private static readonly string[] Unary = + { + "-({0})", "1 / ({0})", "({0}) ^ 2", "sqrt({0})", "sin({0})", "abs({0})", + }; + + private static readonly string[] Binary = + { + "({0}) + ({1})", "({0}) - ({1})", "({0}) * ({1})", "({0}) / ({1})", "({0}) ^ ({1})", + }; + + private static List Corpus() + { + var level1 = new List(Leaves); + var level2 = new List(); + foreach (var shape in Unary) + foreach (var inner in level1) + level2.Add(string.Format(shape, inner)); + foreach (var shape in Binary) + foreach (var left in level1) + foreach (var right in level1) + level2.Add(string.Format(shape, left, right)); + var level3 = new List(); + foreach (var shape in Binary) + foreach (var left in level2.Where((_, i) => i % 17 == 0)) + foreach (var right in level2.Where((_, i) => i % 23 == 0)) + level3.Add(string.Format(shape, left, right)); + + var parsed = new List(); + foreach (var source in level1.Concat(level2).Concat(level3)) + { + try { parsed.Add(source.ToEntity()); } + catch { /* the generator makes some strings the parser declines; not its subject */ } + } + return parsed; + } + + private static void AssertAgrees( + string what, System.Func bySwitch, MatchedRuleSet byData, int leastFirings) + { + var corpus = Corpus(); + Assert.True(corpus.Count > 500, $"the corpus is only {corpus.Count} expressions"); + + var disagreements = new List(); + var fired = 0; + foreach (var expr in corpus) + { + var expected = bySwitch(expr); + var actual = byData.ApplyHere(expr); + if (!expected.Equals(expr)) fired++; + if (!expected.Equals(actual)) + disagreements.Add($"{expr.Stringize()}: switch gave {expected.Stringize()}, " + + $"data gave {actual.Stringize()}"); + } + + // The set has to actually fire, or agreement is the agreement of two things that + // both did nothing. + Assert.True(fired >= leastFirings, + $"{what}: the rules only fired on {fired} of {corpus.Count} expressions"); + Assert.True(disagreements.Count == 0, + $"{what}: {disagreements.Count} of {corpus.Count} disagreed:\n" + + string.Join("\n", disagreements.Take(10))); + } + + [Fact] + public void DivisionPreparingAsDataMatchesTheSwitch() + => AssertAgrees("DivisionPreparing", Patterns.DivisionPreparingRules, + MatchedRules.DivisionPreparing, leastFirings: 20); + + /// + /// The second set, and the one that says whether the shape generalises. It is harder in + /// three ways: eight rules rather than three, an order that is load-bearing — the + /// quotient-times-quotient rule has to be tried before the general product rule or the + /// general one swallows it — and a predicate on a hole, + /// Integer { IsPositive: true }. + /// + [Fact] + public void CollapseMultipleFractionsAsDataMatchesTheSwitch() + => AssertAgrees("CollapseMultipleFractions", Patterns.CollapseMultipleFractions, + MatchedRules.CollapseMultipleFractions, leastFirings: 50); + + /// + /// A predicate on a hole refuses what fails it, which is the C# property pattern + /// Integer { IsPositive: true } as data. + /// + [Theory] + [InlineData("(x / y) ^ 2", true)] + [InlineData("(x / y) ^ (-2)", false)] + [InlineData("(x / y) ^ 0", false)] + [InlineData("(x / y) ^ z", false)] + public void APredicateOnAHoleIsChecked(string expression, bool shouldFire) + { + var expr = expression.ToEntity(); + var rewritten = MatchedRules.CollapseMultipleFractions.ApplyHere(expr); + Assert.Equal(shouldFire, !rewritten.Equals(expr)); + } + + /// + /// 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. + /// + [Fact] + public void TheOrderOfTheRulesIsLoadBearing() + { + var expr = "(a / b) * (c / d)".ToEntity(); + var asWritten = MatchedRules.CollapseMultipleFractions.FirstMatching(expr); + Assert.Equal("product-of-two-quotients", asWritten!.Name); + + var reversed = new MatchedRuleSet("reversed", + MatchedRules.CollapseMultipleFractions.Rules.Reverse().ToArray()); + Assert.NotEqual("product-of-two-quotients", reversed.FirstMatching(expr)!.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 + /// exponents, and for any base when the outer exponent is whole. + /// + /// + /// Compared against the switch only where the comparison is meaningful. + /// PowerRules is a large set and an earlier arm may fire on the same expression, + /// so a case counts only where the switch either did nothing or produced exactly the + /// power-of-a-power answer; anything else means a different arm matched and says + /// nothing about this rule. That the rule cannot be isolated from its `switch` any + /// other way is itself the argument for rules being data. + /// + [Fact] + public void AGuardOverTwoBindingsMatchesTheSwitch() + { + var disagreements = new List(); + var compared = 0; + var fired = 0; + foreach (var expr in Corpus()) + { + if (expr is not Entity.Powf(Entity.Powf(var a, var b), var c)) continue; + var expected = Patterns.PowerRules(expr); + var mine = MatchedRules.PowerOfPower.ApplyHere(expr); + var theAnswer = (Entity)new Entity.Powf(a, b * c); + + if (!expected.Equals(expr) && !expected.Equals(theAnswer)) continue; + compared++; + if (!expected.Equals(expr)) fired++; + if (!expected.Equals(mine)) + disagreements.Add($"{expr.Stringize()}: switch gave {expected.Stringize()}, " + + $"data gave {mine.Stringize()}"); + } + Assert.True(compared > 20, $"only {compared} comparable cases"); + Assert.True(fired > 0, "the switch never applied this rule, so agreement proves nothing"); + Assert.True(disagreements.Count == 0, + $"{disagreements.Count} of {compared} disagreed:\n" + string.Join("\n", disagreements.Take(10))); + } + + /// + /// The guard is the whole point: #752 is what happens when this rule is applied without + /// one. sqrt(x^2) must not become x, since at -0.63 that is -0.63 where + /// the expression is 0.63. + /// + [Theory] + [InlineData("(x ^ 2) ^ 3", true)] // whole outer exponent, any base + [InlineData("(x ^ 2) ^ (-1)", true)] // still whole + [InlineData("(2 ^ x) ^ (1/2)", true)] // base is a positive real + [InlineData("(x ^ 2) ^ (1/2)", false)] // neither, and this one is #752 + [InlineData("(x ^ 2) ^ (3/2)", false)] + [InlineData("(x ^ y) ^ z", false)] + public void TheGuardDecidesWhetherItFires(string expression, bool shouldFire) + { + var expr = expression.ToEntity(); + Assert.Equal(shouldFire, !MatchedRules.PowerOfPower.ApplyHere(expr).Equals(expr)); + } + + /// + /// And where it does fire the value survives, checked at a negative point — which is + /// where the unguarded version went wrong. + /// + [Theory] + [InlineData("(x ^ 2) ^ 3", -0.63)] + [InlineData("(x ^ 2) ^ (-1)", -1.7)] + [InlineData("(x ^ 3) ^ 2", -2.4)] + public void WhereItFiresTheValueSurvives(string expression, double at) + { + var expr = expression.ToEntity(); + var rewritten = MatchedRules.PowerOfPower.ApplyHere(expr); + Assert.NotEqual(expr, rewritten); + var before = expr.Substitute("x", at).EvalNumerical().RealPart.EDecimal.ToDouble(); + var after = rewritten.Substitute("x", at).EvalNumerical().RealPart.EDecimal.ToDouble(); + Assert.Equal(before, after, 8); + } + + /// + /// Every p*q + r*s over a handful of operands. The general corpus above only + /// happens to contain five expressions of that shape, which is too few to conclude + /// anything from, and the shape is the whole subject here — so it is generated rather + /// than hoped for. Four operands give 256 sums, most sharing a factor and some sharing + /// two, which is the case the tie-break is about. + /// + private static List ProductSums() + { + var operands = new[] { "x", "y", "z", "2" }; + var made = new List(); + foreach (var p in operands) + foreach (var q in operands) + foreach (var r in operands) + foreach (var s in operands) + { + try { made.Add($"{p} * {q} + {r} * {s}".ToEntity()); } + catch { /* every one of these parses; the guard is for the generator */ } + } + return made; + } + + /// + /// The four hand-written arms of `{1}*{2} + {1}*{3}`, as an oracle. `CommonRules` + /// writes the identity out once per ordering because a C# pattern cannot say "either + /// way round"; this reproduces them, in their order, so the one commutative rule can be + /// held against them. + /// + private static Entity? TheFourArms(Entity expr) + { + if (expr is not Entity.Sumf(Entity.Mulf(var l1, var l2), Entity.Mulf(var r1, var r2))) + return null; + if (l1.Equals(r1)) return l1 * (l2 + r2); + if (l2.Equals(r1)) return l2 * (l1 + r2); + if (l1.Equals(r2)) return l1 * (l2 + r1); + if (l2.Equals(r2)) return l2 * (l1 + r1); + return null; + } + + /// + /// **One commutative rule fires exactly where the four arms fire.** That is the claim + /// #248 is about, and it holds. + /// + /// + /// The *value* is always the same. The *tree* is not always the same, and that is a + /// real finding rather than a defect in either: where more than one factor is shared, + /// the four arms and the commutative rule pull out different ones — `a*b + b*a` gives + /// `b*(a+a)` from the arms and `a*(b+b)` from the rule, both of which are `2ab`. Which + /// one you get is a tie-break that the `switch` fixes by the order its arms happen to be + /// written in, and that nothing ever chose deliberately. Migrating this rule is + /// therefore **not** purely mechanical: it needs a tie-break convention, or the printed + /// answer moves for expressions with two shared factors. + /// + [Fact] + public void OneCommutativeRuleFiresWhereTheFourArmsDo() + { + var firedBoth = 0; + var sameTree = 0; + var disagreedOnWhether = new List(); + var differentTree = new List(); + + foreach (var expr in ProductSums()) + { + var byArms = TheFourArms(expr); + var byRule = MatchedRules.SharedFactor.Rules[0].TryApply(expr); + + if ((byArms is null) != (byRule is null)) + { + disagreedOnWhether.Add($"{expr.Stringize()}: arms {(byArms is null ? "no" : "yes")}, " + + $"rule {(byRule is null ? "no" : "yes")}"); + continue; + } + if (byArms is null) continue; + firedBoth++; + if (byArms.Equals(byRule)) sameTree++; + else differentTree.Add($"{expr.Stringize()}: arms {byArms.Stringize()}, " + + $"rule {byRule!.Stringize()}"); + } + + Assert.True(firedBoth > 100, $"only {firedBoth} expressions exercised the rule"); + Assert.True(disagreedOnWhether.Count == 0, + $"{disagreedOnWhether.Count} disagreed about *whether* to fire:\n" + + string.Join("\n", disagreedOnWhether.Take(10))); + + // Where the trees differ, the values must not. Checked numerically rather than + // asserted, because "both are correct" is the entire claim being made. + foreach (var expr in ProductSums()) + { + var byArms = TheFourArms(expr); + var byRule = MatchedRules.SharedFactor.Rules[0].TryApply(expr); + if (byArms is null || byRule is null || byArms.Equals(byRule)) continue; + foreach (var at in new[] { 0.37, -1.7, 2.4 }) + { + static Entity Point(Entity e, double at) + => e.Substitute("x", at).Substitute("y", at + 1).Substitute("z", at - 0.5); + var one = Point(byArms, at); + var two = Point(byRule, at); + if (!one.EvaluableNumerical || !two.EvaluableNumerical) continue; + var left = one.EvalNumerical().RealPart.EDecimal.ToDouble(); + var right = two.EvalNumerical().RealPart.EDecimal.ToDouble(); + if (double.IsNaN(left) || double.IsNaN(right)) continue; + Assert.Equal(left, right, 8); + } + } + } + + /// + /// Backtracking, which commutativity needs and a first-match matcher does not have. + /// `b*a + c*a` shares `a`, and finding it means abandoning the first way the left + /// product matched — bind `k = b`, fail on the right, come back and try `k = a`. + /// + [Theory] + [InlineData("b * a + c * a")] + [InlineData("a * b + a * c")] + [InlineData("a * b + c * a")] + [InlineData("b * a + a * c")] + public void CommutativeMatchingBacktracks(string expression) + => Assert.NotNull(MatchedRules.SharedFactor.Rules[0].TryApply(expression.ToEntity())); + + /// And it does not invent a shared factor where there is none. + [Theory] + [InlineData("a * b + c * d")] + [InlineData("a + b")] + [InlineData("a * b - a * c")] + public void CommutativeMatchingDoesNotOverreach(string expression) + => Assert.Null(MatchedRules.SharedFactor.Rules[0].TryApply(expression.ToEntity())); + + /// + /// Distributivity needs no condition, so this is the first rule here whose tier says + /// something its neighbours' does not. + /// + [Fact] + public void ARuleCanBeSoundWhileItsNeighboursAreNot() + { + Assert.Equal(Soundness.Sound, MatchedRules.SharedFactor.Soundness); + Assert.Equal(Soundness.SoundUnderAssumptions, MatchedRules.PowerOfPower.Soundness); + } + + /// + /// A name used twice binds the same subexpression both times — which is the + /// when any1 == any1a guard the existing rules write out by hand, made + /// structural. + /// + [Fact] + public void ARepeatedNameMustMatchTheSameSubexpression() + { + var pattern = MatchPattern.Node(MatchPattern.Any("a"), MatchPattern.Any("a")); + Assert.NotNull(new MatchedRule("doubles", pattern, + bound => 2 * bound["a"], Soundness.Sound).TryApply("x + x".ToEntity())); + Assert.Null(new MatchedRule("doubles", pattern, + bound => 2 * bound["a"], Soundness.Sound).TryApply("x + y".ToEntity())); + } + + /// A typed hole refuses what is not of its type. + [Fact] + public void ATypedHoleIsTyped() + { + var rule = new MatchedRule("numeric-left", + MatchPattern.Node( + MatchPattern.Any("c"), MatchPattern.Any("a")), + bound => bound["c"] + bound["a"], Soundness.Sound); + Assert.NotNull(rule.TryApply("2 * x".ToEntity())); + Assert.Null(rule.TryApply("y * x".ToEntity())); + } + + /// + /// The set is enumerable and each rule is addressable by name — the property the + /// `switch` cannot have and the reason three separate tier-2 items are blocked on this. + /// + [Fact] + public void TheRulesAreEnumerableAndNamed() + { + var rules = MatchedRules.DivisionPreparing.Rules; + Assert.Equal(3, rules.Count); + Assert.All(rules, rule => Assert.False(string.IsNullOrWhiteSpace(rule.Name))); + Assert.Equal(rules.Count, rules.Select(rule => rule.Name).Distinct().Count()); + Assert.NotNull(MatchedRules.DivisionPreparing.FirstMatching("2 / x * y".ToEntity())); + } + + /// + /// A set's tier is derived from its rules rather than declared beside them, so it + /// cannot drift from what it is about. That is the fix for the registry's thirty sets + /// all declaring the same value. + /// + [Fact] + public void TheSetsTierIsTheWeakestOfItsRules() + { + Assert.Equal(Soundness.SoundUnderAssumptions, MatchedRules.DivisionPreparing.Soundness); + + var mixed = new MatchedRuleSet("mixed", + new MatchedRule("sound", MatchPattern.Any("a"), b => b["a"], Soundness.Sound), + new MatchedRule("heuristic", MatchPattern.Any("a"), b => b["a"], Soundness.Heuristic)); + Assert.Equal(Soundness.Heuristic, mixed.Soundness); + + var allSound = new MatchedRuleSet("sound", + new MatchedRule("one", MatchPattern.Any("a"), b => b["a"], Soundness.Sound)); + Assert.Equal(Soundness.Sound, allSound.Soundness); + } + } +}