doc-src/Ref/syntax.tex
 author wenzelm Fri, 10 Nov 2000 19:02:37 +0100 changeset 10432 3dfbc913d184 parent 9695 ec7d7f877712 child 14893 55e83c32cdec permissions -rw-r--r--
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;

%% $Id$
\chapter{Syntax Transformations} \label{chap:syntax}
\mtt{dummyT})$. \item Schematic variables:$\termofast{\Variable \mtt{"?}xi\mtt"} =
\ttfct{Var} ((x, i), \mtt{dummyT})$, where$x$is the base name and$i$the index extracted from~$xi$. \item Free variables:$\termofast{\Variable x} = \ttfct{Free} (x,
\mtt{dummyT})$. \item Function applications with$n$arguments: $\termofast{\Appl{f, x@1, \ldots, x@n}} = \termofast{f} \ttapp \termofast{x@1} \ttapp \ldots \ttapp \termofast{x@n}$ \end{itemize} Here \ttindex{Const}, \ttindex{Var}, \ttindex{Free} and \verb|$|\index{$@{\tt\$}} are constructors of the datatype \mltydx{term},
while \ttindex{dummyT} stands for some dummy type that is ignored during
type inference.

So far the outcome is still a first-order term.  Abstractions and bound
variables (constructors \ttindex{Abs} and \ttindex{Bound}) are introduced
by parse translations.  Such translations are attached to {\tt "_abs"},
{\tt "!!"} and user-defined binders.

\section{Printing of terms}

The output phase is essentially the inverse of the input phase.  Terms are
translated via abstract syntax trees into strings.  Finally the strings are
pretty printed.

Print translations (\S\ref{sec:tr_funs}) may affect the transformation of
terms into \AST{}s.  Ignoring those, the transformation maps
term constants, variables and applications to the corresponding constructs
on \AST{}s.  Abstractions are mapped to applications of the special
constant {\tt _abs}.

More precisely, the mapping $\astofterm{-}$ is defined as follows:
\begin{itemize}
\item $\astofterm{\ttfct{Const} (x, \tau)} = \Constant x$.

\item $\astofterm{\ttfct{Free} (x, \tau)} = constrain (\Variable x, \tau)$.

\item $\astofterm{\ttfct{Var} ((x, i), \tau)} = constrain (\Variable \mtt{"?}xi\mtt", \tau)$, where $\mtt?xi$ is the string representation of
the {\tt indexname} $(x, i)$.

\item For the abstraction $\lambda x::\tau.t$, let $x'$ be a variant
of~$x$ renamed to differ from all names occurring in~$t$, and let $t'$
be obtained from~$t$ by replacing all bound occurrences of~$x$ by
the free variable $x'$.  This replaces corresponding occurrences of the
constructor \ttindex{Bound} by the term $\ttfct{Free} (x', \mtt{dummyT})$:
$\astofterm{\ttfct{Abs} (x, \tau, t)} = \Appl{\Constant \mtt{"_abs"}, constrain(\Variable x', \tau), \astofterm{t'}}$

\item $\astofterm{\ttfct{Bound} i} = \Variable \mtt{"B.}i\mtt"$.
The occurrence of constructor \ttindex{Bound} should never happen
when printing well-typed terms; it indicates a de Bruijn index with no
matching abstraction.

\item Where $f$ is not an application,
$\astofterm{f \ttapp x@1 \ttapp \ldots \ttapp x@n} = \Appl{\astofterm{f}, \astofterm{x@1}, \ldots,\astofterm{x@n}}$
\end{itemize}
%
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} is set to {\tt false}.

\item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, \astofterm{\tau}}$ \ otherwise.

Here, $\astofterm{\tau}$ is the \AST{} encoding of $\tau$: type
constructors go to {\tt Constant}s; type identifiers go to {\tt
Variable}s; type applications go to {\tt Appl}s with the type
constructor as the first element.  If \ttindex{show_sorts} is set to
{\tt true}, some type variables are decorated with an \AST{} encoding
of their sort.
\end{itemize}
%
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} reverse the
parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.

For the actual printing process, the names attached to productions
of the form $\ldots A^{(p@1)}@1 \ldots A^{(p@n)}@n \ldots \mtt{=>} c$ play
a vital role.  Each \AST{} with constant head $c$, namely $\mtt"c\mtt"$ or
$(\mtt"c\mtt"~ x@1 \ldots x@n)$, is printed according to the production
for~$c$.  Each argument~$x@i$ is converted to a string, and put in
parentheses if its priority~$(p@i)$ requires this.  The resulting strings
and their syntactic sugar (denoted by \dots{} above) are joined to make a
single string.

If an application $(\mtt"c\mtt"~ x@1 \ldots x@m)$ has more arguments
than the corresponding production, it is first split into
$((\mtt"c\mtt"~ x@1 \ldots x@n) ~ x@{n+1} \ldots x@m)$.  Applications
with too few arguments or with non-constant head or without a
corresponding production are printed as $f(x@1, \ldots, x@l)$ or
$(\alpha@1, \ldots, \alpha@l) ty$.  Multiple productions associated
with some name $c$ are tried in order of appearance.  An occurrence of
$\Variable x$ is simply printed as~$x$.

Blanks are {\em not\/} inserted automatically.  If blanks are required to
separate tokens, specify them in the mixfix declaration, possibly preceded
by a slash~({\tt/}) to allow a line break.
\index{ASTs|)}

\section{Macros: syntactic rewriting} \label{sec:macros}
\index{macros|(}\index{rewriting!syntactic|(}

Mixfix declarations alone can handle situations where there is a direct
connection between the concrete syntax and the underlying term.  Sometimes
we require a more elaborate concrete syntax, such as quantifiers and list
notation.  Isabelle's {\bf macros} and {\bf translation functions} can
perform translations such as
\begin{center}\tt
\begin{tabular}{r@{$\quad\protect\rightleftharpoons\quad$}l}
ALL x:A.P   & Ball(A, \%x.P)        \\ \relax
[x, y, z]   & Cons(x, Cons(y, Cons(z, Nil)))
\end{tabular}
\end{center}
Translation functions (see \S\ref{sec:tr_funs}) must be coded in ML; they
are the most powerful translation mechanism but are difficult to read or
write.  Macros are specified by first-order rewriting systems that operate
on abstract syntax trees.  They are usually easy to read and write, and can
express all but the most obscure translations.

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 a full set theory definition,
including many macro rules.} Theory {\tt SetSyntax} declares
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 write $\forall x \in A. P$ as {\tt Ball(A,\%x.P)}, and
similarly for the others.

\begin{figure}
\begin{ttbox}
SetSyntax = Pure +
types
i o
arities
i, o :: logic
consts
Trueprop      :: o => prop                ("_" 5)
Collect       :: [i, i => o] => i
Replace       :: [i, [i, i] => o] => i
Ball          :: [i, i => o] => o
syntax
"{\at}Collect"    :: [idt, i, o] => i         ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
"{\at}Replace"    :: [idt, idt, i, o] => i    ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
"{\at}Ball"       :: [idt, i, o] => o         ("(3ALL _:_./ _)" 10)
translations
"{\ttlbrace}x:A. P{\ttrbrace}"    == "Collect(A, \%x. P)"
"{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
"ALL x:A. P"  == "Ball(A, \%x. P)"
end
\end{ttbox}
\caption{Macro example: set theory}\label{fig:set_trans}
\end{figure}

The theory specifies a variable-binding syntax through additional productions
that have mixfix declarations.  Each non-copy production must specify some
constant, which is used for building \AST{}s. \index{constants!syntactic} The
additional constants are decorated with {\tt\at} to stress their purely
syntactic purpose; they may not occur within the final well-typed terms,
being declared as {\tt syntax} rather than {\tt consts}.

The translations cause the replacement of external forms by internal forms
after parsing, and vice versa before printing of terms.  As a specification
of the set theory notation, they should be largely self-explanatory.  The
syntactic constants, {\tt\at Collect}, {\tt\at Replace} and {\tt\at Ball},
appear implicitly in the macro rules via their mixfix forms.

Macros can define variable-binding syntax because they operate on \AST{}s,
which have no inbuilt notion of bound variable.  The macro variables {\tt
x} and~{\tt y} have type~{\tt idt} and therefore range over identifiers,
in this case bound variables.  The macro variables {\tt P} and~{\tt Q}
range over formulae containing bound variable occurrences.

Other applications of the macro system can be less straightforward, and
there are peculiarities.  The rest of this section will describe in detail
how Isabelle macros are preprocessed and applied.

\subsection{Specifying macros}
Macros are basically rewrite rules on \AST{}s.  But unlike other macro
systems found in programming languages, Isabelle's macros work in both
directions.  Therefore a syntax contains two lists of rewrites: one for
parsing and one for printing.

\index{*translations section}
The {\tt translations} section specifies macros.  The syntax for a macro is
$(root)\; string \quad \left\{\begin{array}[c]{c} \mtt{=>} \\ \mtt{<=} \\ \mtt{==} \end{array} \right\} \quad (root)\; string$
%
This specifies a parse rule ({\tt =>}), a print rule ({\tt <=}), or both
({\tt ==}).  The two strings specify the left and right-hand sides of the
macro rule.  The $(root)$ specification is optional; it specifies the
nonterminal for parsing the $string$ and if omitted defaults to {\tt
logic}.  \AST{} rewrite rules $(l, r)$ must obey certain conditions:
\begin{itemize}
\item Rules must be left linear: $l$ must not contain repeated variables.

\item Every variable in~$r$ must also occur in~$l$.
\end{itemize}

Macro rules may refer to any syntax from the parent theories.  They
may also refer to anything defined before the current {\tt
translations} section --- including any mixfix declarations.

Upon declaration, both sides of the macro rule undergo parsing and parse
\AST{} translations (see \S\ref{sec:asts}), but do not themselves undergo
macro expansion.  The lexer runs in a different mode that additionally
accepts identifiers of the form $\_~letter~quasiletter^*$ (like {\tt _idt},
{\tt _K}).  Thus, a constant whose name starts with an underscore can
appear in macro rules but not in ordinary terms.

Some atoms of the macro rule's \AST{} are designated as constants for
matching.  These are all names that have been declared as classes, types or
constants (logical and syntactic).

The result of this preprocessing is two lists of macro rules, each
stored as a pair of \AST{}s.  They can be viewed using {\tt
print_syntax} (sections \ttindex{parse_rules} and
\ttindex{print_rules}).  For theory~{\tt SetSyntax} of
Fig.~\ref{fig:set_trans} these are
\begin{ttbox}
parse_rules:
("{\at}Collect" x A P)  ->  ("Collect" A ("_abs" x P))
("{\at}Replace" y x A Q)  ->  ("Replace" A ("_abs" x ("_abs" y Q)))
("{\at}Ball" x A P)  ->  ("Ball" A ("_abs" x P))
print_rules:
("Collect" A ("_abs" x P))  ->  ("{\at}Collect" x A P)
("Replace" A ("_abs" x ("_abs" y Q)))  ->  ("{\at}Replace" y x A Q)
("Ball" A ("_abs" x P))  ->  ("{\at}Ball" x A P)
\end{ttbox}

\begin{warn}
Avoid choosing variable names that have previously been used as
constants, types or type classes; the {\tt consts} section in the output
of {\tt print_syntax} lists all such names.  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{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.

Because of this behaviour, different kinds of atoms with the same name are
indistinguishable, which may make some rules prone to misbehaviour.  Example:
\begin{ttbox}
types
Nil
consts
Nil     :: 'a list
syntax
"[]"    :: 'a list    ("[]")
translations
"[]"    == "Nil"
\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!  Guess how type~{\tt Nil} is printed?

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} Alternatively, use
\ttindex{Syntax.test_read}.  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}).

\subsection{Example: the syntax of finite sets}
\index{examples!of macros}

This example demonstrates the use of recursive macros to implement a
convenient notation for finite sets.
\index{*empty constant}\index{*insert constant}\index{{}@\verb'{}' symbol}
\index{"@Enum@{\tt\at Enum} constant}
\index{"@Finset@{\tt\at Finset} constant}
\begin{ttbox}
FinSyntax = SetSyntax +
types
is
syntax
""            :: i => is                  ("_")
"{\at}Enum"       :: [i, is] => is            ("_,/ _")
consts
empty         :: i                        ("{\ttlbrace}{\ttrbrace}")
insert        :: [i, i] => i
syntax
"{\at}Finset"     :: is => i                  ("{\ttlbrace}(_){\ttrbrace}")
translations
"{\ttlbrace}x, xs{\ttrbrace}"     == "insert(x, {\ttlbrace}xs{\ttrbrace})"
"{\ttlbrace}x{\ttrbrace}"         == "insert(x, {\ttlbrace}{\ttrbrace})"
end
\end{ttbox}
Finite sets are internally built up by {\tt empty} and {\tt insert}.  The
declarations above specify \verb|{x, y, z}| as the external representation
of
\begin{ttbox}
insert(x, insert(y, insert(z, empty)))
\end{ttbox}
The nonterminal symbol~\ndx{is} stands for one or more objects of type~{\tt
i} separated by commas.  The mixfix declaration \hbox{\verb|"_,/ _"|}
allows a line break after the comma for \rmindex{pretty printing}; if no
line break is required then a space is printed instead.

The nonterminal is declared as the type~{\tt is}, but with no {\tt arities}
declaration.  Hence {\tt is} is not a logical type and may be used safely as
a new nonterminal for custom syntax.  The nonterminal~{\tt is} can later be
re-used for other enumerations of type~{\tt i} like lists or tuples.  If we
had needed polymorphic enumerations, we could have used the predefined
nonterminal symbol \ndx{args} and skipped this part altogether.

\index{"@Finset@{\tt\at Finset} constant}
Next follows {\tt empty}, which is already equipped with its syntax
\verb|{}|, and {\tt insert} without concrete syntax.  The syntactic
constant {\tt\at Finset} provides concrete syntax for enumerations of~{\tt
i} enclosed in curly braces.  Remember that a pair of parentheses, as in
\verb|"{(_)}"|, specifies a block of indentation for pretty printing.

The translations may look strange at first.  Macro rules are best
understood in their internal forms:
\begin{ttbox}
parse_rules:
("{\at}Finset" ("{\at}Enum" x xs))  ->  ("insert" x ("{\at}Finset" xs))
("{\at}Finset" x)  ->  ("insert" x "empty")
print_rules:
("insert" x ("{\at}Finset" xs))  ->  ("{\at}Finset" ("{\at}Enum" x xs))
("insert" x "empty")  ->  ("{\at}Finset" x)
\end{ttbox}
This shows that \verb|{x,xs}| indeed matches any set enumeration of at least
two elements, binding the first to {\tt x} and the rest to {\tt xs}.
Likewise, \verb|{xs}| and \verb|{x}| represent any set enumeration.
The parse rules only work in the order given.

\begin{warn}
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
sufficiently long and strange names.  If a bound variable's name gets
rewritten, the result will be incorrect; for example, the term
\begin{ttbox}
\%empty insert. insert(x, empty)
\end{ttbox}
\par\noindent is incorrectly printed as \verb|%empty insert. {x}|.
\end{warn}

\subsection{Example: a parse macro for dependent types}\label{prod_trans}
\index{examples!of macros}

As stated earlier, a macro rule may not introduce new {\tt Variable}s on
the right-hand side.  Something like \verb|"K(B)" => "%x.B"| is illegal;
if allowed, it could cause variable capture.  In such cases you usually
must fall back on translation functions.  But a trick can make things
readable in some cases: {\em calling\/} translation functions by parse
macros:
\begin{ttbox}
ProdSyntax = SetSyntax +
consts
Pi            :: [i, i => i] => i
syntax
"{\at}PROD"       :: [idt, i, i] => i       ("(3PROD _:_./ _)" 10)
"{\at}->"         :: [i, i] => i            ("(_ ->/ _)" [51, 50] 50)
\ttbreak
translations
"PROD x:A. B" => "Pi(A, \%x. B)"
"A -> B"      => "Pi(A, _K(B))"
end
ML
val print_translation = [("Pi", dependent_tr' ("{\at}PROD", "{\at}->"))];
\end{ttbox}

Here {\tt Pi} is a logical constant for constructing general products.
Two external forms exist: the general case {\tt PROD x:A.B} and the
function space {\tt A -> B}, which abbreviates \verb|Pi(A, %x.B)| when {\tt B}
does not depend on~{\tt x}.

The second parse macro introduces {\tt _K(B)}, which later becomes
\verb|%x.B| due to a parse translation associated with \cdx{_K}.
Unfortunately there is no such trick for printing, so we have to add a {\tt
ML} section for the print translation \ttindex{dependent_tr'}.

Recall that identifiers with a leading {\tt _} are allowed in translation
rules, but not in ordinary terms.  Thus we can create \AST{}s containing
names that are not directly expressible.

The parse translation for {\tt _K} is already installed in Pure, and the
function {\tt dependent_tr'} is exported by the syntax module for public use.
See \S\ref{sec:tr_funs} below for more of the arcane lore of translation
functions.  \index{macros|)}\index{rewriting!syntactic|)}

\section{Translation functions} \label{sec:tr_funs}
\index{translations|(}
%
This section describes the translation function mechanism.  By writing \ML{}
functions, you can do almost everything to terms or \AST{}s during parsing and
printing.  The logic LK is a good example of sophisticated 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},
{\tt Syntax.ast} and the encodings of types and terms as such at the various
stages of the parsing or printing process.  Most users should never need to
use translation functions.

\subsection{Declaring translation functions}
There are four kinds of translation functions, with one of these
coming in two variants.  Each such function is associated with a name,
which triggers calls to it.  Such names can be constants (logical or
syntactic) or type constructors.

Function {\tt print_syntax} displays the sets of names associated with the
translation functions of a theory under \texttt{parse_ast_translation}, etc.
You can add new ones via the {\tt ML} section\index{*ML section} of a theory
definition file.  Even though the {\tt ML} section is the very last part of
the file, newly installed translation functions are already effective when
processing all of the preceding sections.

The {\tt ML} section's contents are simply copied verbatim near the
beginning of the \ML\ file generated from a theory definition file.
Definitions made here are accessible as components of an \ML\
structure; to make some parts private, use an \ML{} {\tt local}
declaration.  The {\ML} code may install translation functions by
declaring any of the following identifiers:
\begin{ttbox}
val parse_ast_translation   : (string * (ast list -> ast)) list
val print_ast_translation   : (string * (ast list -> ast)) list
val parse_translation       : (string * (term list -> term)) list
val print_translation       : (string * (term list -> term)) list
val typed_print_translation :
(string * (bool -> typ -> term list -> term)) list
\end{ttbox}

\subsection{The translation strategy}
The different kinds of translation functions are called during the
transformations between parse trees, \AST{}s and terms (recall
Fig.\ts\ref{fig:parse_print}).  Whenever a combination of the form
$(\mtt"c\mtt"~x@1 \ldots x@n)$ is encountered, and a translation
function $f$ of appropriate kind exists for $c$, the result is
computed by the \ML{} function call $f \mtt[ x@1, \ldots, x@n \mtt]$.

For \AST{} translations, the arguments $x@1, \ldots, x@n$ are \AST{}s.
A combination has the form $\Constant c$ or $\Appl{\Constant c, x@1, \ldots, x@n}$.  For term translations, the arguments are terms and a
combination has the form $\ttfct{Const} (c, \tau)$ or $\ttfct{Const} (c, \tau) \ttapp x@1 \ttapp \ldots \ttapp x@n$.  Terms allow more
sophisticated transformations than \AST{}s do, typically involving
abstractions and bound variables. {\em Typed} print translations may
even peek at the type $\tau$ of the constant they are invoked on; they
are also passed the current value of the \ttindex{show_sorts} flag.

Regardless of whether they act on terms or \AST{}s, translation
functions called during the parsing process differ from those for
printing more fundamentally in their overall behaviour:
\begin{description}
\item[Parse translations] are applied bottom-up.  The arguments are already in
translated form.  The translations must not fail; exceptions trigger an
error message.  There may never be more than one function associated with
any syntactic name.

\item[Print translations] are applied top-down.  They are supplied with
arguments that are partly still in internal form.  The result again
undergoes translation; therefore a print translation should not introduce as
head the very constant that invoked it.  The function may raise exception
\xdx{Match} to indicate failure; in this event it has no effect.  Multiple
functions associated with some syntactic name are tried in an unspecified
order.
\end{description}

Only constant atoms --- constructor \ttindex{Constant} for \AST{}s and
\ttindex{Const} for terms --- can invoke translation functions.  This
causes another difference between parsing and printing.

Parsing starts with a string and the constants are not yet identified.
Only parse tree heads create {\tt Constant}s in the resulting \AST, as
described in \S\ref{sec:astofpt}.  Macros and parse \AST{} translations may
introduce further {\tt Constant}s.  When the final \AST{} is converted to a
term, all {\tt Constant}s become {\tt Const}s, as described in
\S\ref{sec:termofast}.

Printing starts with a well-typed term and all the constants are known.  So
all logical constants and type constructors may invoke print translations.
These, and macros, may introduce further constants.

\subsection{Example: a print translation for dependent types}
\index{examples!of translations}\indexbold{*dependent_tr'}

Let us continue the dependent type example (page~\pageref{prod_trans}) by
examining the parse translation for~\cdx{_K} and the print translation
{\tt dependent_tr'}, which are both built-in.  By convention, parse
translations have names ending with {\tt _tr} and print translations have
names ending with {\tt _tr'}.  Search for such names in the Isabelle
sources to locate more examples.

Here is the parse translation for {\tt _K}:
\begin{ttbox}
fun k_tr [t] = Abs ("x", dummyT, incr_boundvars 1 t)
| k_tr ts = raise TERM ("k_tr", ts);
\end{ttbox}
If {\tt k_tr} is called with exactly one argument~$t$, it creates a new
{\tt Abs} node with a body derived from $t$.  Since terms given to parse
translations are not yet typed, the type of the bound variable in the new
{\tt Abs} is simply {\tt dummyT}.  The function increments all {\tt Bound}
nodes referring to outer abstractions by calling \ttindex{incr_boundvars},
a basic term manipulation function defined in {\tt Pure/term.ML}.

Here is the print translation for dependent types:
\begin{ttbox}
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
if 0 mem (loose_bnos B) then
let val (x', B') = Syntax.variant_abs' (x, dummyT, B) in
list_comb
(Const (q,dummyT) $Syntax.mark_boundT (x',{\thinspace}T)$ A $B', ts) end else list_comb (Const (r, dummyT)$ A $B, ts) | dependent_tr' _ _ = raise Match; \end{ttbox} The argument {\tt (q,{\thinspace}r)} is supplied to the curried function {\tt dependent_tr'} by a partial application during its installation. For example, we could 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}->")), ("Sigma", dependent_tr' ("{\at}SUM", "{\at}*"))]; \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}->}(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'$is the body$B$with {\tt Bound} nodes referring to the {\tt Abs} node replaced by$\ttfct{Free} (x', \mtt{dummyT})$(but marked as representing a bound variable). We must be careful with types here. While types of {\tt Const}s are ignored, type constraints may be printed for some {\tt Free}s and {\tt Var}s if \ttindex{show_types} is set to {\tt true}. Variables of type \ttindex{dummyT} are never printed with constraint, though. The line \begin{ttbox} let val (x', B') = Syntax.variant_abs' (x, dummyT, B); \end{ttbox}\index{*Syntax.variant_abs'} replaces bound variable occurrences in~$B$by the free variable$x'$with type {\tt dummyT}. Only the binding occurrence of~$x'$is given the correct type~{\tt T}, so this is the only place where a type constraint might appear. Also note that we are responsible to mark free identifiers that actually represent bound variables. This is achieved by \ttindex{Syntax.variant_abs'} and \ttindex{Syntax.mark_boundT} above. Failing to do so may cause these names to be printed in the wrong style. \index{translations|)} \index{syntax!transformations|)} \section{Token translations} \label{sec:tok_tr} \index{token translations|(} % Isabelle's meta-logic features quite a lot of different kinds of identifiers, namely {\em class}, {\em tfree}, {\em tvar}, {\em free}, {\em bound}, {\em var}. One might want to have these printed in different styles, e.g.\ in bold or italic, or even transcribed into something more readable like$\alpha, \alpha', \beta$instead of {\tt 'a}, {\tt 'aa}, {\tt 'b} for type variables. Token translations provide a means to such ends, enabling the user to install certain \ML{} functions associated with any logical \rmindex{token class} and depending on some \rmindex{print mode}. The logical class of identifiers can not necessarily be determined by its syntactic category, though. For example, consider free vs.\ bound variables. So Isabelle's pretty printing mechanism, starting from fully typed terms, has to be careful to preserve this additional information\footnote{This is done by marking atoms in abstract syntax trees appropriately. The marks are actually visible by print translation functions -- they are just special constants applied to atomic asts, for example \texttt{("_bound" x)}.}. In particular, user-supplied print translation functions operating on terms have to be well-behaved in this respect. Free identifiers introduced to represent bound variables have to be marked appropriately (cf.\ the example at the end of \S\ref{sec:tr_funs}). \medskip Token translations may be installed by declaring the \ttindex{token_translation} value within the \texttt{ML} section of a theory definition file: \begin{ttbox} val token_translation: (string * string * (string -> string * real)) list \end{ttbox} The elements of this list are of the form$(m, c, f)$, where$m$is a print mode identifier,$c$a token class, and$f\colon string \to string \times
real$the actual translation function. Assuming that$x$is of identifier class$c$, and print mode$m$is the first (active) mode providing some translation for$c$, then$x$is output according to$f(x) = (x', len)$. Thereby$x'$is the modified identifier name and$len$its visual length in terms of characters (e.g.\ length 1.0 would correspond to$1/2$\,em in \LaTeX). Thus$x'\$ may include non-printing parts like control sequences or
markup information for typesetting systems.

\index{token translations|)}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
%%% End: