1.1 --- a/doc-src/HOL/HOL.tex	Sat Dec 29 18:36:12 2001 +0100
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon Dec 31 14:08:23 2001 +0100
     1.3 @@ -3009,6 +3009,100 @@
     1.4  \index{*coinductive|)} \index{*inductive|)}
     1.5  
     1.6  
     1.7 +\section{Executable specifications}
     1.8 +\index{code generator}
     1.9 +
    1.10 +For validation purposes, it is often useful to {\em execute} specifications.
    1.11 +In principle, specifications could be ``executed'' using Isabelle's
    1.12 +inference kernel, i.e. by a combination of resolution and simplification.
    1.13 +Unfortunately, this approach is rather inefficient. A more efficient way
    1.14 +of executing specifications is to translate them into a functional
    1.15 +programming language such as ML. Isabelle's built-in code generator
    1.16 +supports this.
    1.17 +
    1.18 +\begin{figure}
    1.19 +\begin{rail}
    1.20 +codegen : 'generate_code' ( () | '(' string ')') (code +);
    1.21 +
    1.22 +code : name '=' string;
    1.23 +
    1.24 +constscode : 'consts_code' (codespec +);
    1.25 +
    1.26 +codespec : name ( () | '::' type) '(' mixfix ')';
    1.27 +
    1.28 +typescode : 'types_code' (tycodespec +);
    1.29 +
    1.30 +tycodespec : name '(' mixfix ')';
    1.31 +\end{rail}
    1.32 +\caption{Code generator syntax}
    1.33 +\label{fig:HOL:codegen}
    1.34 +\end{figure}
    1.35 +
    1.36 +\subsection{Invoking the code generator}
    1.37 +
    1.38 +The code generator is invoked via the \ttindex{generate_code} command
    1.39 +(see Fig.~\ref{fig:HOL:codegen}). The code can either be written to a file,
    1.40 +in which case a file name has to be specified in parentheses, or be
    1.41 +loaded directly into Isabelle's ML environment. In the latter case,
    1.42 +the \texttt{ML} theory command can be used to inspect the results
    1.43 +interactively.
    1.44 +The \texttt{generate_code} command takes a list of pairs, consisting
    1.45 +of an ML identifier and a string representing a term. The result of
    1.46 +compiling the term is bound to the corresponding ML identifier.
    1.47 +For example,
    1.48 +\begin{ttbox}
    1.49 +generate_code
    1.50 +  test = "foldl op + (0::int) [1,2,3,4,5]"
    1.51 +\end{ttbox}
    1.52 +binds the result of compiling the term
    1.53 +\texttt{foldl op + (0::int) [1,2,3,4,5]}
    1.54 +(i.e.~\texttt{15}) to the ML identifier \texttt{test}.
    1.55 +
    1.56 +\subsection{Configuring the code generator}
    1.57 +
    1.58 +When generating code for a complex term, the code generator recursively
    1.59 +calls itself for all subterms.
    1.60 +When it arrives at a constant, the default strategy of the code
    1.61 +generator is to look up its definition and try to generate code for it.
    1.62 +Some primitive constants of a logic, which have no definitions that
    1.63 +are immediately executable, may be associated with a piece of ML
    1.64 +code manually using the \ttindex{consts_code} command
    1.65 +(see Fig.~\ref{fig:HOL:codegen}).
    1.66 +It takes a list whose elements consist of a constant name, together
    1.67 +with an optional type constraint (to account for overloading), and a
    1.68 +mixfix template describing the ML code. The latter is very much the
    1.69 +same as the mixfix templates used when declaring new constants.
    1.70 +The most notable difference is that terms may be included in the ML
    1.71 +template using antiquotation brackets \verb|{*|~$\ldots$~\verb|*}|.
    1.72 +A similar mechanism is available for
    1.73 +types: \ttindex{types_code} associates type constructors with
    1.74 +specific ML code.
    1.75 +
    1.76 +Another possibility of configuring the code generator is to register
    1.77 +theorems to be used for code generation. Theorems can be registered
    1.78 +via the \ttindex{code} attribute. It takes an optional name as
    1.79 +an argument, which indicates the format of the theorem. Currently
    1.80 +supported formats are equations (this is the default when no name
    1.81 +is specified) and horn clauses (this is indicated by the name
    1.82 +\texttt{ind}). The left-hand sides of equations may only contain
    1.83 +constructors and distinct variables, whereas horn clauses must have
    1.84 +the same format as introduction rules of inductive definitions.
    1.85 +
    1.86 +\subsection{Specific HOL code generators}
    1.87 +
    1.88 +The basic code generator framework offered by Isabelle/Pure has
    1.89 +already been extended with additional code generators for specific
    1.90 +HOL constructs. These include datatypes, recursive functions and
    1.91 +inductive relations. The code generator for inductive relations
    1.92 +can handle expressions of the form $(t@1,\ldots,t@n) \in r$, where
    1.93 +$r$ is an inductively defined relation. In case at least one of the
    1.94 +$t@i$ is a dummy pattern $_$, the above expression evaluates to a
    1.95 +sequence of possible answers. If all of the $t@i$ are proper
    1.96 +terms, the expression evaluates to a boolean value. The theory
    1.97 +underlying the HOL code generator is described more detailed in
    1.98 +\cite{Berghofer-Nipkow:2002}.
    1.99 +
   1.100 +
   1.101  \section{The examples directories}
   1.102  
   1.103  Directory \texttt{HOL/Auth} contains theories for proving the correctness of