diff -r e21f4d5b9636 -r 8537313dd261 doc-src/Ref/syntax.tex --- a/doc-src/Ref/syntax.tex Tue Jun 19 22:06:08 2012 +0200 +++ b/doc-src/Ref/syntax.tex Wed Jun 20 20:50:04 2012 +0200 @@ -234,101 +234,6 @@ by a slash~({\tt/}) to allow a line break. \index{ASTs|)} - -\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. - %%% Local Variables: %%% mode: latex %%% TeX-master: "ref"