AngouriMath

Navigation

MatchedRule


← Back to list of classes

Description

Summary

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.

Remarks

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 Soundness. A *set's* tier is the minimum over its arms,
so one conditional arm drags every unconditional one down with it and every set in the
registry ends up declaring the same value — which is the honest label for a set and a
useless one for a rule. A rule declares its own, and unlike the set's it distinguishes:
both tiers are well populated. No count is repeated here, because a number in a comment
drifts silently; RuleAuthoringGuideTest measures the live ones and fails when they
move.
Where the right-hand side is a pattern too, the rule has two directions rather than
one.
Reversed is the same rule read the other way, and
Reversal says why a rule has no such reading when it has none. That was
#746 tier 2's first
missing piece; it is delivered and it has a production consumer, since
Saturation.RulesUpTo uses a declared inverse pair to keep the collecting direction
and withhold the expanding one. Docs/Contributing/ReversibleRules.md is the argument
for when a reversal is licensed.

Members

























Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4378 pages online