AngouriMath

Navigation

Home Quick start Wiki Almanac Research What's new Try Use Angouri.org GitHub Report a bug ~~Donate~~ Contacts

MatchPattern

← Back to list of classes

Description

Summary

The left-hand side of a rewrite rule, as a value rather than as an arm of a
switch.

Remarks

#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 over a binary node — a + b matches b + a — is
Commutative``1(AngouriMath.Core.Transformations.Matching.MatchPattern,AngouriMath.Core.Transformations.Matching.MatchPattern). Matching across a flattened chain, so that a rule about two
terms finds them among five, is Gathered``1(System.String,AngouriMath.Core.Transformations.Matching.MatchPattern[]): the n-ary half of #248.

AngouriMath

Table of contents

AngouriMath

MatchPattern

Description

Members