\fasl{
The \p{subst} rewrite rule replaces each occurence of a bound variable
$v_i$ with the corresponding value $val_i$. Note that the precondition
of this rule states that, if the value $val_i$ is an abstraction, the
variable $v_i$ must be referenced exactly once. This precondition
prevents the TML code from growing arbitrarily large:
}

\tmlrewrite{subst} % $v_i$}
    {(val_i \not\in Abs \vee \tmlrefcount{app}{v_i} = 1)}
    {\applybbi{\fun{v_1..v_i..v_n}
                   {app}}
              {val_1..val_i..val_n}}
    {\applybbi{\fun{v_1..v_i..v_n}
                   {\tmlsubst{app}{val_i}{v_i}}}                
              {val_1..val_i..val_n}}

\fasl{
The \p{remove} rewrite rule strikes out a bound variable $v_i$ that is not referenced any
more. The corresponding value $val_i$ is also removed. Note that this is
possible because, due to syntactical restrictions (cf. figure
\ref{Fig:TML AST} on page \pageref{Fig:TML AST}),  $val_i$ cannot be
an application, and, therfore, cannot contain any calls to
side-effecting primitive procedures:
}

\tmlrewrite{remove} % $v_i$}
    {(\tmlrefcount{app}{v_i} = 0)}
    {\applybbi{\fun{v_1..v_i..v_n}
                   {app}}
              {val_1..val_i..val_n}}
    {\applybbi{\fun{v_1..v_{i-1}\:v_{i+1}..v_n}
                   {app}}
              {val_1..val_{i-1}\:val_{i+1}..val_n}}


\fasl{
The \p{reduce} rewrite rule simply removes applications of
$\lambda$-abstractions that do not bind any variables: }

\tmlrewrite{reduce}
    {}
    {\applyi{\fun{}{app\!}}{}}
    {app}
             
\fasl{
The \p{$\eta$-reduce} rewrite rule removes unnecessary abstractions:
}

\tmlrewrite{$\eta$-reduce}
    {}
    {\fun{v_1..v_n}
        {\applyi{val}
                {v_1..v_n}}}
    {val}
             
\fasl{
The \p{fold} rewrite rule uses an evaluation function {\it eval} that
knows details of the semantics of primitive procedures:
}

\tmlrewrite{fold} % p}
    {}
    {\applyi{prim}
            {val_1..val_n}}
    {eval(prim,val_1,..,val_n)}
             
\fasl{
Given an application of a certain primitive, it may be able to {\em
meta-evaluate} the call, yielding a somewhat simpler TML tree than the
original call. For example, if the evaluation function detects that a
given call to a primitive will always compute the same value and invoke
always the same continuation, it reduces the primitive call to an
application of the continuation to the result. Typically, this is
possible if some of the arguments are literal constants:
}

\tmlrewrite{fold +}{}
    {\applyiv{+}{1}{2}{c_1}{c_2}}
    {\applyi{c_2}{3}}
             
\fasl{
To give another example, a call to the object identity primitive will
fold if the value to be compared is identical to one of the case tags:
}

\tmlrewrite{fold ==}
    {}
    {\applyvii{==}{2}{1}{2}{3}{c_1}{c_2}{c_3}}
    {\apply{c_2}}

\fasl{
If the {\em eval} function cannot perform any useful meta-evaluation, it
simply returns the original call to the primitive.

The \p{case-subst} rewrite rule substitutes variables in case statements
with the tag value of the corresponding branch:
}

\tmlrewrite{case-subst} % v}
    {}
    {\applyiii{==}{v}{val_1..val_n}{val_1^c..val_n^c}}
    {\applyiii{==}{v}{val_1..val_n}
       {\tmlsubst{val^c_1}{val_1}{v}..\tmlsubst{val^c_n}{val_n}{v}}}
           
\tmlrewrite{case-subst} % v}
    {}
    {\applyiii{==}{v}{val_1..val_n}{val_1^c..val_n^c\:val_{n+1}^c}}
    {\applyiii{==}{v}{val_1..val_n}
       {\tmlsubst{val^c_1}{val_1}{v}..\tmlsubst{val^c_n}{val_n}{v}\:val_{n+1}^c}}
           
\fasl{
Finally, there are two rewrite rules that operate on calls to the
primitive procedure $Y$. The \p{Y-remove} rewrite rule strikes out any
recursive procedure that is not referenced from within the bodies of the
other (mutually) recursive procedures, wheras the \p{Y-reduce} rewrite
rule removes empty $Y$ applications:
}

\tmlrewrite{Y-remove}
    {(\tmlrefcount{app}{v_i} = 0 \quad \wedge \quad
      \forall_{i \neq j}\:\tmlrefcount{val_j}{v_i} = 0)}
    {\applyi{Y}
           {\funb{v_1..v_i..v_n\:c}
                 {\applybvi{c}
                           {abs_1}
                           {..}
                           {abs_i}
                           {..}
                           {abs_n}
                           {\cont{}{app}}}}}
    {\applyi{Y}
            {\funb{v_1..v_{i-1}\:{v_{i+1}}..v_n\:c}
                  {\applybvii{c}
                             {abs_1}
                             {..}
                             {abs_{i-1}}
                             {abs_{i+1}}
                             {..}
                             {abs_n}
                             {\cont{}{app}}}}}
    
\tmlrewrite{Y-reduce}
    {(\tmlrefcount{app}{c} = 0)}
    {\applyi{Y}
            {\fun{c}
                 {\applyi{c}
                         {\cont{}{app}}}}}
    {app}




