A.2 Matching Commands

Matching commands are used to directly invoke the rewriting engine's term pattern matcher. They can be useful for figuring out exactly what subjects can be matched by a complex pattern.

match {[ number ]} {in module :} pattern <=? subject .

This performs straight-forward matching in the given module. This kind of matching is used by the engine for applying membership axioms. The result is a list of at most number matching substitutions. If the upper bound clause is omitted, infinity is assumed. Example:

match [5] in FOO : +(X, *(X, Y)) <=? +(*(a, b), *(c, d)) .

xmatch {[ number ]} {in module :} pattern <=? subject .

This works similarly to the previous command, except that it performs matching with extension for those theories that need it (currently just those including the assoc attribute). If the subject (after theory-normalization) has a symbol f from an extension theory on top, only a piece of the top theory layer with f on top need be matched. This kind of matching is used by the engine for applying equations and rules in order to accurately simulate congruence class rewriting. The result is a list of all matches. If only part of the subject was matched, that part is given. Example:

xmatch +(*(P, Q), *(X, Y)) <=? +(*(a, b), *(c, d), *(a, e)) .