--- a/doc-src/Ref/syntax.tex Tue Jun 19 20:51:15 2012 +0200
+++ b/doc-src/Ref/syntax.tex Tue Jun 19 22:06:08 2012 +0200
@@ -235,98 +235,6 @@
\index{ASTs|)}
-
-\section{Macros: syntactic rewriting} \label{sec:macros}
-\index{macros|(}\index{rewriting!syntactic|(}
-
-\subsection{Specifying macros}
-
-\begin{warn}
-If a macro rule works incorrectly, inspect its internal form as
-shown above, recalling that constants appear as quoted strings and
-variables without quotes.
-\end{warn}
-
-\begin{warn}
-If \ttindex{eta_contract} is set to {\tt true}, terms will be
-$\eta$-contracted {\em before\/} the \AST{} rewriter sees them. Thus some
-abstraction nodes needed for print rules to match may vanish. For example,
-\verb|Ball(A, %x. P(x))| contracts to {\tt Ball(A, P)}; the print rule does
-not apply and the output will be {\tt Ball(A, P)}. This problem would not
-occur if \ML{} translation functions were used instead of macros (as is
-done for binder declarations).
-\end{warn}
-
-
-\begin{warn}
-Another trap concerns type constraints. If \ttindex{show_types} is set to
-{\tt true}, bound variables will be decorated by their meta types at the
-binding place (but not at occurrences in the body). Matching with
-\verb|Collect(A, %x. P)| binds {\tt x} to something like {\tt ("_constrain" y
-"i")} rather than only {\tt y}. \AST{} rewriting will cause the constraint to
-appear in the external form, say \verb|{y::i:A::i. P::o}|.
-
-To allow such constraints to be re-read, your syntax should specify bound
-variables using the nonterminal~\ndx{idt}. This is the case in our
-example. Choosing {\tt id} instead of {\tt idt} is a common error.
-\end{warn}
-
-
-
-\subsection{Applying rules}
-As a term is being parsed or printed, an \AST{} is generated as an
-intermediate form (recall Fig.\ts\ref{fig:parse_print}). The \AST{} is
-normalised by applying macro rules in the manner of a traditional term
-rewriting system. We first examine how a single rule is applied.
-
-Let $t$ be the abstract syntax tree to be normalised and $(l, r)$ some
-translation rule. A subtree~$u$ of $t$ is a {\bf redex} if it is an
-instance of~$l$; in this case $l$ is said to {\bf match}~$u$. A redex
-matched by $l$ may be replaced by the corresponding instance of~$r$, thus
-{\bf rewriting} the \AST~$t$. Matching requires some notion of {\bf
- place-holders} that may occur in rule patterns but not in ordinary
-\AST{}s; {\tt Variable} atoms serve this purpose.
-
-The matching of the object~$u$ by the pattern~$l$ is performed as follows:
-\begin{itemize}
- \item Every constant matches itself.
-
- \item $\Variable x$ in the object matches $\Constant x$ in the pattern.
- This point is discussed further below.
-
- \item Every \AST{} in the object matches $\Variable x$ in the pattern,
- binding~$x$ to~$u$.
-
- \item One application matches another if they have the same number of
- subtrees and corresponding subtrees match.
-
- \item In every other case, matching fails. In particular, {\tt
- Constant}~$x$ can only match itself.
-\end{itemize}
-A successful match yields a substitution that is applied to~$r$, generating
-the instance that replaces~$u$.
-
-The second case above may look odd. This is where {\tt Variable}s of
-non-rule \AST{}s behave like {\tt Constant}s. Recall that \AST{}s are not
-far removed from parse trees; at this level it is not yet known which
-identifiers will become constants, bounds, frees, types or classes. As
-\S\ref{sec:asts} describes, former parse tree heads appear in \AST{}s as
-{\tt Constant}s, while the name tokens \ndx{id}, \ndx{var}, \ndx{tid},
-\ndx{tvar}, \ndx{num}, \ndx{xnum} and \ndx{xstr} become {\tt Variable}s. On the other
-hand, when \AST{}s generated from terms for printing, all constants and type
-constructors become {\tt Constant}s; see \S\ref{sec:asts}. Thus \AST{}s may
-contain a messy mixture of {\tt Variable}s and {\tt Constant}s. This is
-insignificant at macro level because matching treats them alike.
-
-Normalizing an \AST{} involves repeatedly applying macro rules until none are
-applicable. Macro rules are chosen in order of appearance in the theory
-definitions. You can watch the normalization of \AST{}s during parsing and
-printing by setting \ttindex{Syntax.trace_ast} to {\tt true}.\index{tracing!of
- macros} The information displayed when tracing includes the \AST{} before
-normalization ({\tt pre}), redexes with results ({\tt rewrote}), the normal
-form finally reached ({\tt post}) and some statistics ({\tt normalize}).
-
-
\section{Translation functions} \label{sec:tr_funs}
\index{translations|(}
%