Skip to content

A guide to writing a rewrite rule, with every figure in it under test - #1111

Merged
Rafael-SOWNet merged 1 commit into
masterfrom
rule-authoring-guide
Aug 30, 2026
Merged

Rafael-SOWNet merged 1 commit into
masterfrom
rule-authoring-guide

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

#746 tier 2 lists five major deliverables. Four exist — the rule registry, the rewrite graph with
pluggable extraction, the canonicalisation framework (#1105), the confluence and termination checker.
This is the fifth: the rule-authoring guide.

Docs/Contributing/WritingARule.md is the how. Whether a rule is allowed is a harder question
and a different document — SimplificationContract.md comes first, and the guide says so in its
opening line, because a rule written beautifully that holds only on the positive reals while claiming
to hold everywhere is a wrong answer with good spelling.

What it covers

  • where a rule goes, and why not in a switch;
  • the seven things a rule carries, as one annotated example;
  • why the name is a sentence rather than an identifier — it is read aloud by
    DerivationPath.Explain(), so a-quotient-of-a-thing-by-itself-is-one-unless-it-is-zero is right
    and DivideByItself is not, with the reason rather than the rule;
  • that the name, the identity and the rendered pattern are three different things, all worth
    having;
  • the pattern language, and the two families it deliberately cannot build — binders, because
    DirectChildren renames the bound variable, and variable-arity nodes, because a pattern fixes an
    arity;
  • what choosing a code replacement costs: a direction and an exact growth;
  • that soundness is per rule, and the set grain says nothing because a set's tier is the minimum over
    its rules;
  • when the order of two rules is yours to choose and when subsumption has already decided it;
  • the ten tests that will check a new rule;
  • and the whole of it once, on one rule.

Every count in it is under test

RuleAuthoringGuideTest, and the guide says so at the top.

A document that states a number goes stale silently, and a guide is the worst case: it is read by
somebody who does not yet know the code, and is therefore in no position to notice that "33 of the
322 rules have a pattern on both sides"
stopped being true two releases ago.

Nine facts are held — the set and rule counts, the 293 distinct names and their four-to-sixteen-word
range, the 59 identities, the 44 buildable node types, the 33 two-sided rules and 32 directions, the
181 Sound against 141 conditional, the 268 at Unknown growth, and the 28 pairs ordered by
subsumption. The failure message names the claim and says which way to fix it:

WritingARule.md says how many rules are Sound is 181; it is 179.
Update the document, not this test.

Two more are not counts:

  • the ten tests the guide sends a contributor to are checked to exist, by reflection over the
    test assembly. A guide that names a test which has since been renamed is worse than one that names
    none — the reader concludes the check does not exist, rather than that the document is old;
  • the worked example at the end is looked up in the library and applied, so it cannot quietly
    become a rule that is not there.

One thing writing it found

The guide asserted that the single one-way two-sided rule is the Pythagorean identity — which is what
the surrounding documentation calls it — and the test matched on the name containing pythagorean.
The rule is called squared-sine-and-cosine-of-one-argument-sum-to-one. The prose is right; the
assertion was matching the prose rather than the rule, which is exactly the failure the rest of this
file exists to prevent. It now matches the rule.

Also indexes the guide in the contributing README, whose numbering had two entries at 10.

State

Full suite: 8988 passed, 14 skipped, 0 failed. No public API change; documentation and one test.

Part of #746 tier 2.

#746 tier 2 lists five major deliverables. Four exist -- the rule registry, the rewrite
graph with pluggable extraction, the canonicalisation framework, the confluence and
termination checker. This is the fifth.

`Docs/Contributing/WritingARule.md` is the *how*. Whether a rule is **allowed** is a harder
question and a different document: `SimplificationContract.md` comes first, and the guide
says so in its opening line, because a rule written beautifully that holds only on the
positive reals while claiming to hold everywhere is a wrong answer with good spelling.

What it covers: where a rule goes and why not in a `switch`; the seven things a rule
carries; why the name is a sentence rather than an identifier, and how it is read aloud by
`DerivationPath.Explain()`; that the name, the identity and the rendered pattern are three
different things all worth having; the pattern language and the two families it deliberately
cannot build; what choosing a code replacement costs -- a direction and an exact growth; that
soundness is per rule and the set grain says nothing; when the order of two rules is yours to
choose and when subsumption has already decided; the ten tests that will check a new rule;
and the whole of it once, on one rule.

**Every count in it is asserted by `RuleAuthoringGuideTest`, and the guide says so at the
top.** A document that states a number goes stale silently, and a guide is the worst case:
it is read by somebody who does not yet know the code and is therefore in no position to
notice that "33 of the 322 rules have a pattern on both sides" stopped being true two
releases ago. Nine facts are held: the set and rule counts, the 293 distinct names and their
four-to-sixteen-word range, the 59 identities, the 44 buildable node types, the 33 two-sided
rules and 32 directions, the 181 Sound against 141 conditional, the 268 at Unknown growth,
and the 28 pairs ordered by subsumption. The failure message names the claim and says to
update the document rather than the test.

Two more that are not counts. The ten tests the guide sends a contributor to are checked to
exist, by reflection over the test assembly -- a guide that names a test which has been
renamed is worse than one that names none, since the reader concludes the check does not
exist rather than that the document is old. And the worked example at the end is looked up in
the library and applied, so it cannot become a rule that is not there.

Writing it found one thing: the guide asserted the one-way rule is the Pythagorean identity,
which is what the documentation calls it, and matched on the name containing "pythagorean".
The rule is called `squared-sine-and-cosine-of-one-argument-sum-to-one`. The prose is right
and the assertion was matching the prose rather than the rule; it now matches the rule.

Also indexes the guide in the contributing README, whose numbering had two entries at 10.

Full suite: 8988 passed, 14 skipped, 0 failed. No public API change.

Part of #746 tier 2.
@Rafael-SOWNet
Rafael-SOWNet merged commit 5a2cd73 into master Aug 30, 2026
31 checks passed
Rafael-SOWNet added a commit that referenced this pull request Aug 30, 2026
…s are written out

Boolean, NumericNeat and Factorization. The third tranche of the repoint, and the first
where identities had to be **written** rather than carried across.

`Boolean`'s comments name the laws -- De Morgan, idempotence, distributivity, absorption,
contraposition -- which is the right thing for a comment above a rule and is not an identity.
All twenty were read off the rules' own patterns and replacements:

    (not a) and (not b) = not (a or b)
    ((k and p) or (k and q)) = (k and (p or q))
    (a or ((not a) and b)) = (a or b)
    ((not a) implies (not b)) = (b implies a)

`NumericNeat` and `Factorization` already had identities in their comments and needed only
the arrow turned into an equals sign, and the commentary after it dropped.

**Forty-two arms become zero rules lost.** They are arms the data form writes once. Boolean's
thirty-six are twenty, because a commutative pattern finds a shared operand wherever it sits,
so eight arms of distributivity are two rules and absorption's four-arms-each is one rule
twice. Factorization's twenty-two are eleven for the same reason. NumericNeat's sixteen are
eleven, six of them being three rules written once per side a negative factor can sit on. The
registry total goes 407 -> 365 and described rules 95 -> 180.

**And seven growths are now declared rather than guessed.** `GrowthSaysWhichWayTheSetMoves`
failed the moment Factorization stopped being described by the `switch`: the string-length
proxy had guessed `Collects` and the exact answer for a code-built rule nobody declared is
`Unknown`. The fix is the one the authoring guide asks for -- declare it where you can
justify it -- so the two splitters are `Expands`, and the four shared-factor collectors plus
`a^b * c^b = (a*c)^b` are `Collects`, each with the node count in the comment. Four are left
at `Unknown` on purpose: `k + k*q = k*(1 + q)` and its three siblings are the same size on
both sides, and a code replacement has no tree to count, so declaring `Rearranges` would be a
claim about arithmetic nobody did.

That took `Unknown` from 268 to 261, which failed `RuleAuthoringGuideTest` -- the guide from
#1111 states that figure and the test holds it. Both updated. That is the mechanism working
on its first day.

Twenty-three of the thirty registered sets now describe what they run. Of the seven left,
three are the `CanonicalOrder` family, which still *runs* its `switch`. The four others are
where repointing still costs something: `Common` would lose 33 descriptions, `Power` 22,
`Trigonometric` 13 and `InequalityEquality` 11.

Full suite: 8988 passed, 14 skipped, 0 failed. No public API change.

Part of #746 tier 2 and #825.
Rafael-SOWNet added a commit that referenced this pull request Aug 30, 2026
…s are written out (#1112)

Boolean, NumericNeat and Factorization. The third tranche of the repoint, and the first
where identities had to be **written** rather than carried across.

`Boolean`'s comments name the laws -- De Morgan, idempotence, distributivity, absorption,
contraposition -- which is the right thing for a comment above a rule and is not an identity.
All twenty were read off the rules' own patterns and replacements:

    (not a) and (not b) = not (a or b)
    ((k and p) or (k and q)) = (k and (p or q))
    (a or ((not a) and b)) = (a or b)
    ((not a) implies (not b)) = (b implies a)

`NumericNeat` and `Factorization` already had identities in their comments and needed only
the arrow turned into an equals sign, and the commentary after it dropped.

**Forty-two arms become zero rules lost.** They are arms the data form writes once. Boolean's
thirty-six are twenty, because a commutative pattern finds a shared operand wherever it sits,
so eight arms of distributivity are two rules and absorption's four-arms-each is one rule
twice. Factorization's twenty-two are eleven for the same reason. NumericNeat's sixteen are
eleven, six of them being three rules written once per side a negative factor can sit on. The
registry total goes 407 -> 365 and described rules 95 -> 180.

**And seven growths are now declared rather than guessed.** `GrowthSaysWhichWayTheSetMoves`
failed the moment Factorization stopped being described by the `switch`: the string-length
proxy had guessed `Collects` and the exact answer for a code-built rule nobody declared is
`Unknown`. The fix is the one the authoring guide asks for -- declare it where you can
justify it -- so the two splitters are `Expands`, and the four shared-factor collectors plus
`a^b * c^b = (a*c)^b` are `Collects`, each with the node count in the comment. Four are left
at `Unknown` on purpose: `k + k*q = k*(1 + q)` and its three siblings are the same size on
both sides, and a code replacement has no tree to count, so declaring `Rearranges` would be a
claim about arithmetic nobody did.

That took `Unknown` from 268 to 261, which failed `RuleAuthoringGuideTest` -- the guide from
#1111 states that figure and the test holds it. Both updated. That is the mechanism working
on its first day.

Twenty-three of the thirty registered sets now describe what they run. Of the seven left,
three are the `CanonicalOrder` family, which still *runs* its `switch`. The four others are
where repointing still costs something: `Common` would lose 33 descriptions, `Power` 22,
`Trigonometric` 13 and `InequalityEquality` 11.

Full suite: 8988 passed, 14 skipped, 0 failed. No public API change.

Part of #746 tier 2 and #825.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant