doc-src/Ref/syntax.tex
 changeset 332 01b87a921967 parent 323 361a71713176 child 499 5a54c796b808
--- a/doc-src/Ref/syntax.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/syntax.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -64,7 +64,7 @@
%
Isabelle uses an S-expression syntax for abstract syntax trees.  Constant
atoms are shown as quoted strings, variable atoms as non-quoted strings and
-applications as a parenthesized list of subtrees.  For example, the \AST
+applications as a parenthesised list of subtrees.  For example, the \AST
\begin{ttbox}
Appl [Constant "_constrain",
Appl [Constant "_abs", Variable "x", Variable "t"],
@@ -270,11 +270,11 @@
\]
\end{itemize}
%
-Type constraints are inserted to allow the printing of types.  This is
-governed by the boolean variable \ttindex{show_types}:
+Type constraints\index{type constraints} are inserted to allow the printing
+of types.  This is governed by the boolean variable \ttindex{show_types}:
\begin{itemize}
\item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or
-    \ttindex{show_types} not set to {\tt true}.
+    \ttindex{show_types} is set to {\tt false}.

\item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, \astofterm{\tau}}$ \ otherwise.
@@ -289,7 +289,7 @@
%
The \AST{}, after application of macros (see \S\ref{sec:macros}), is
transformed into the final output string.  The built-in {\bf print AST
-  translations}\indexbold{translations!print AST} effectively reverse the
+  translations}\indexbold{translations!print AST} reverse the
parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.

For the actual printing process, the names attached to productions
@@ -338,11 +338,11 @@
Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set
theory.\footnote{This and the following theories are complete working
examples, though they specify only syntax, no axioms.  The file {\tt
-    ZF/zf.thy} presents the full set theory definition, including many
+    ZF/ZF.thy} presents the full set theory definition, including many
macro rules.}  Theory {\tt SET} defines constants for set comprehension
({\tt Collect}), replacement ({\tt Replace}) and bounded universal
quantification ({\tt Ball}).  Each of these binds some variables.  Without
-additional syntax we should have to express $\forall x \in A. P$ as {\tt
+additional syntax we should have to write $\forall x \in A. P$ as {\tt
Ball(A,\%x.P)}, and similarly for the others.

\begin{figure}
@@ -464,7 +464,7 @@
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 {\tt Ball(A, P)}; the print rule does
+\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).
@@ -491,10 +491,10 @@
\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
-normalized by applying macro rules in the manner of a traditional term
+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 normalized and $(l, r)$ some
+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
@@ -546,10 +546,10 @@
\end{ttbox}
The term {\tt Nil} will be printed as {\tt []}, just as expected.
The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be
-expected!
+expected!  How is the type~{\tt Nil} printed?

Normalizing an \AST{} involves repeatedly applying macro rules until none
-is applicable.  Macro rules are chosen in the order that they appear in the
+are applicable.  Macro rules are chosen in the order that they appear in the
{\tt translations} section.  You can watch the normalization of \AST{}s
during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to
{\tt true}.\index{tracing!of macros} Alternatively, use
@@ -626,7 +626,7 @@
The parse rules only work in the order given.

\begin{warn}
-  The \AST{} rewriter cannot discern constants from variables and looks
+  The \AST{} rewriter cannot distinguish constants from variables and looks
only for names of atoms.  Thus the names of {\tt Constant}s occurring in
the (internal) left-hand side of translation rules should be regarded as
\rmindex{reserved words}.  Choose non-identifiers like {\tt\at Finset} or
@@ -635,7 +635,7 @@
\begin{ttbox}
\%empty insert. insert(x, empty)
\end{ttbox}
-  gets printed as \verb|%empty insert. {x}|.
+\par\noindent is printed as \verb|%empty insert. {x}|.
\end{warn}

@@ -690,8 +690,8 @@
This section describes the translation function mechanism.  By writing
\ML{} functions, you can do almost everything with terms or \AST{}s during
parsing and printing.  The logic \LK\ is a good example of sophisticated
-transformations between internal and external representations of
-associative sequences; here, macros would be useless.
+transformations between internal and external representations of sequents;
+here, macros would be useless.

A full understanding of translations requires some familiarity
with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
@@ -805,9 +805,10 @@
else list_comb (Const (r, dummyT) $A$ B, ts)
| dependent_tr' _ _ = raise Match;
\end{ttbox}
-The argument {\tt (q,r)} is supplied to {\tt dependent_tr'} by a curried
-function application during its installation.  We could set up print
-translations for both {\tt Pi} and {\tt Sigma} by including
+The argument {\tt (q,r)} is supplied to the curried function {\tt
+  dependent_tr'} by a partial application during its installation.  We
+can set up print translations for both {\tt Pi} and {\tt Sigma} by
+including
\begin{ttbox}\index{*ML section}
val print_translation =
[("Pi",    dependent_tr' ("{\at}PROD", "{\at}->")),
@@ -815,11 +816,11 @@
\end{ttbox}
within the {\tt ML} section.  The first of these transforms ${\tt Pi}(A, \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
-$\hbox{\tt{\at}->}r(A, B)$, choosing the latter form if $B$ does not depend
+$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not depend
on~$x$.  It checks this using \ttindex{loose_bnos}, yet another function
from {\tt Pure/term.ML}.  Note that $x'$ is a version of $x$ renamed away
-from all names in $B$, and $B'$ the body $B$ with {\tt Bound} nodes
-referring to our {\tt Abs} node replaced by $\ttfct{Free} (x', +from all names in$B$, and$B'$is the body$B$with {\tt Bound} nodes +referring to the {\tt Abs} node replaced by$\ttfct{Free} (x',
\mtt{dummyT})\$.

We must be careful with types here.  While types of {\tt Const}s are