Rewriting rules

Rewriting rules are specified in a rewrite declaration. The syntax of a rewriting specification is as follows:

Rewrite_Decl	::=	rewrite Id	variant 1
		{ [ Index_Decl ] case Rewrite_Rules  ¼ case Rewrite_Rules }
	|	rewrite Id	variant 2
		{ [ Index_Decl ] Rewrite_Rules  - ¼ - Rewrite_Rules }
Rewrite_Rule	::=	[ Rewrite_Modifier ] [ Id -> ]
		Pat [ Guard ] [ Cost ] : Rewrite_Action
Rewrite_Modifier	::=	bottomup:	bottom up mode
	|	topdown:	top down mode
	|	before:	before actions
	|	preorder:	preorder actions
	|	postorder:	postorder actions
Rewrite_Action	::=	{ Code }
	|	Exp

The name of a rewrite declaration should match the name of a rewrite class. The two syntactic forms of rewrite have equivalent semantics.

The special statement rewrite(e) may be used inside the rhs action to rewrite the current redex into e. Note that rewrite(e) is a branching statement; statements after rewrite are not reachable.