author wenzelm Mon, 02 May 2011 21:33:21 +0200 changeset 42627 8749742785b8 parent 42626 6ac8c55c657e child 42628 50f257ea2aba
moved material about old codegen to isar-ref manual; eliminated old rail diagram;
 doc-src/HOL/HOL.tex file | annotate | diff | comparison | revisions doc-src/HOL/logics-HOL.rai file | annotate | diff | comparison | revisions doc-src/IsarRef/Thy/HOL_Specific.thy file | annotate | diff | comparison | revisions doc-src/IsarRef/Thy/document/HOL_Specific.tex file | annotate | diff | comparison | revisions
--- a/doc-src/HOL/HOL.tex	Mon May 02 20:34:34 2011 +0200
+++ b/doc-src/HOL/HOL.tex	Mon May 02 21:33:21 2011 +0200
@@ -2770,196 +2770,6 @@
\index{*coinductive|)} \index{*inductive|)}

-\section{Executable specifications}
-\index{code generator}
-
-For validation purposes, it is often useful to {\em execute} specifications.
-In principle, specifications could be executed'' using Isabelle's
-inference kernel, i.e. by a combination of resolution and simplification.
-Unfortunately, this approach is rather inefficient. A more efficient way
-of executing specifications is to translate them into a functional
-programming language such as ML. Isabelle's built-in code generator
-supports this.
-
-\railalias{verblbrace}{\texttt{\ttlbrace*}}
-\railalias{verbrbrace}{\texttt{*\ttrbrace}}
-\railterm{verblbrace}
-\railterm{verbrbrace}
-
-\begin{figure}
-\begin{rail}
-codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\
-  ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
-  'contains' ( ( name '=' term ) + | term + );
-
-modespec : '(' ( name * ) ')';
-\end{rail}
-\caption{Code generator invocation syntax}
-\label{fig:HOL:codegen-invocation}
-\end{figure}
-
-\begin{figure}
-\begin{rail}
-constscode : 'consts_code' (codespec +);
-
-codespec : const template attachment ?;
-
-typescode : 'types_code' (tycodespec +);
-
-tycodespec : name template attachment ?;
-
-const : term;
-
-template: '(' string ')';
-
-attachment: 'attach' modespec ? verblbrace text verbrbrace;
-\end{rail}
-\caption{Code generator configuration syntax}
-\label{fig:HOL:codegen-configuration}
-\end{figure}
-
-\subsection{Invoking the code generator}
-
-The code generator is invoked via the \ttindex{code_module} and
-\ttindex{code_library} commands (see Fig.~\ref{fig:HOL:codegen-invocation}),
-which correspond to {\em incremental} and {\em modular} code generation,
-respectively.
-\begin{description}
-\item[Modular] For each theory, an ML structure is generated, containing the
-  code generated from the constants defined in this theory.
-\item[Incremental] All the generated code is emitted into the same structure.
-  This structure may import code from previously generated structures, which
-  can be specified via \texttt{imports}.
-  Moreover, the generated structure may also be referred to in later invocations
-  of the code generator.
-\end{description}
-After the \texttt{code_module} and \texttt{code_library} keywords, the user
-may specify an optional list of modes'' in parentheses. These can be used
-to instruct the code generator to emit additional code for special purposes,
-e.g.\ functions for converting elements of generated datatypes to Isabelle terms,
-or test data generators. The list of modes is followed by a module name.
-The module name is optional for modular code generation, but must be specified
-for incremental code generation.
-The code can either be written to a file,
-in which case a file name has to be specified after the \texttt{file} keyword, or be
-loaded directly into Isabelle's ML environment. In the latter case,
-the \texttt{ML} theory command can be used to inspect the results
-interactively.
-The terms from which to generate code can be specified after the
-\texttt{contains} keyword, either as a list of bindings, or just as
-a list of terms. In the latter case, the code generator just produces
-code for all constants and types occuring in the term, but does not
-bind the compiled terms to ML identifiers.
-For example,
-\begin{ttbox}
-code_module Test
-contains
-  test = "foldl op + (0::int) [1,2,3,4,5]"
-\end{ttbox}
-binds the result of compiling the term
-\texttt{foldl op + (0::int) [1,2,3,4,5]}
-(i.e.~\texttt{15}) to the ML identifier \texttt{Test.test}.
-
-\subsection{Configuring the code generator}
-
-When generating code for a complex term, the code generator recursively
-calls itself for all subterms.
-When it arrives at a constant, the default strategy of the code
-generator is to look up its definition and try to generate code for it.
-Constants which have no definitions that
-are immediately executable, may be associated with a piece of ML
-code manually using the \ttindex{consts_code} command
-(see Fig.~\ref{fig:HOL:codegen-configuration}).
-It takes a list whose elements consist of a constant (given in usual term syntax
--- an explicit type constraint accounts for overloading), and a
-mixfix template describing the ML code. The latter is very much the
-same as the mixfix templates used when declaring new constants.
-The most notable difference is that terms may be included in the ML
-template using antiquotation brackets \verb|{*|~$\ldots$~\verb|*}|.
-A similar mechanism is available for
-types: \ttindex{types_code} associates type constructors with
-specific ML code. For example, the declaration
-\begin{ttbox}
-types_code
-  "*"     ("(_ */ _)")
-
-consts_code
-  "Pair"    ("(_,/ _)")
-\end{ttbox}
-in theory \texttt{Product_Type} describes how the product type of Isabelle/HOL
-should be compiled to ML. Sometimes, the code associated with a
-constant or type may need to refer to auxiliary functions, which
-have to be emitted when the constant is used. Code for such auxiliary
-functions can be declared using \texttt{attach}. For example, the
-\texttt{wfrec} function from theory \texttt{Wellfounded_Recursion}
-is implemented as follows:
-\begin{ttbox}
-consts_code
-  "wfrec"   ("\bs<module>wfrec?")
-attach \{*
-fun wfrec f x = f (wfrec f) x;
-*\}
-\end{ttbox}
-If the code containing a call to \texttt{wfrec} resides in an ML structure
-different from the one containing the function definition attached to
-\texttt{wfrec}, the name of the ML structure (followed by a \texttt{.}'')
-is inserted in place of \texttt{\bs<module>}'' in the above template.
-The \texttt{?}'' means that the code generator should ignore the first
-argument of \texttt{wfrec}, i.e.\ the termination relation, which is
-usually not executable.
-
-Another possibility of configuring the code generator is to register
-theorems to be used for code generation. Theorems can be registered
-via the \ttindex{code} attribute. It takes an optional name as
-an argument, which indicates the format of the theorem. Currently
-supported formats are equations (this is the default when no name
-is specified) and horn clauses (this is indicated by the name
-\texttt{ind}). The left-hand sides of equations may only contain
-constructors and distinct variables, whereas horn clauses must have
-the same format as introduction rules of inductive definitions.
-For example, the declaration
-\begin{ttbox}
-lemma Suc_less_eq [iff, code]: "(Suc m < Suc n) = (m < n)" $$\langle\ldots\rangle$$
-lemma [code]: "((n::nat) < 0) = False" by simp
-lemma [code]: "(0 < Suc n) = True" by simp
-\end{ttbox}
-in theory \texttt{Nat} specifies three equations from which to generate
-code for \texttt{<} on natural numbers.
-
-\subsection{Specific HOL code generators}
-
-The basic code generator framework offered by Isabelle/Pure has
-already been extended with additional code generators for specific
-HOL constructs. These include datatypes, recursive functions and
-inductive relations. The code generator for inductive relations
-can handle expressions of the form $(t@1,\ldots,t@n) \in r$, where
-$r$ is an inductively defined relation. If at least one of the
-$t@i$ is a dummy pattern $_$'', the above expression evaluates to a
-sequence of possible answers. If all of the $t@i$ are proper
-terms, the expression evaluates to a boolean value.
-\begin{small}
-\begin{alltt}
-  theory Test = Lambda:
-
-  code_module Test
-  contains
-    test1 = "Abs (Var 0) $$\circ$$ Var 0 -> Var 0"
-    test2 = "Abs (Abs (Var 0 $$\circ$$ Var 0) $$\circ$$ (Abs (Var 0) $$\circ$$ Var 0)) -> _"
-\end{alltt}
-\end{small}
-In the above example, \texttt{Test.test1} evaluates to the boolean
-value \texttt{true}, whereas \texttt{Test.test2} is a sequence whose
-elements can be inspected using \texttt{Seq.pull} or similar functions.
-\begin{ttbox}
-ML \{* Seq.pull Test.test2 *\}  -- \{* This is the first answer *\}
-ML \{* Seq.pull (snd (the it)) *\}  -- \{* This is the second answer *\}
-\end{ttbox}
-The theory
-underlying the HOL code generator is described more detailed in
-\cite{Berghofer-Nipkow:2002}. More examples that illustrate the usage
-of the code generator can be found e.g.~in theories
-\texttt{MicroJava/J/JListExample} and \texttt{MicroJava/JVM/JVMListExample}.
-
\section{The examples directories}

Directory \texttt{HOL/Auth} contains theories for proving the correctness of
--- a/doc-src/HOL/logics-HOL.rai	Mon May 02 20:34:34 2011 +0200
+++ b/doc-src/HOL/logics-HOL.rai	Mon May 02 21:33:21 2011 +0200
@@ -2,14 +2,3 @@
type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
\rail@i{2}{ datatype : 'datatype' typedecls; \par
typedecls: ( newtype '=' (cons + '|') ) + 'and' ; newtype : typevarlist id ( () | '(' infix ')' ) ; cons : name (argtype *) ( () | ( '(' mixfix ')' ) ) ; argtype : id | tid | ('(' typevarlist id ')') ; }
-\rail@t{verblbrace}
-\rail@t{verbrbrace}
-\rail@i{3}{ codegen : ( 'code_module' | 'code_library' ) modespec ? name ? \\ ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\ 'contains' ( ( name '=' term ) + | term + ); \par
-modespec : '(' ( name * ) ')'; }
-\rail@i{4}{ constscode : 'consts_code' (codespec +); \par
-codespec : const template attachment ?; \par
-typescode : 'types_code' (tycodespec +); \par
-tycodespec : name template attachment ?; \par
-const : term; \par
-template: '(' string ')'; \par
-attachment: 'attach' modespec ? verblbrace text verbrbrace; }
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 02 20:34:34 2011 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 02 21:33:21 2011 +0200
@@ -1181,22 +1181,31 @@

section {* Executable code *}

-text {*
-  Isabelle/Pure provides two generic frameworks to support code
-  generation from executable specifications.  Isabelle/HOL
-  instantiates these mechanisms in a way that is amenable to end-user
-  applications.
+text {* For validation purposes, it is often useful to \emph{execute}
+  specifications.  In principle, execution could be simulated by
+  Isabelle's inference kernel, i.e. by a combination of resolution and
+  simplification.  Unfortunately, this approach is rather inefficient.
+  A more efficient way of executing specifications is to translate
+  them into a functional programming language such as ML.

-  \medskip One framework generates code from functional programs
+  Isabelle provides two generic frameworks to support code generation
+  from executable specifications.  Isabelle/HOL instantiates these
+  mechanisms in a way that is amenable to end-user applications.
+*}
+
+
+subsection {* The new code generator (F. Haftmann) *}
+
+text {* This framework generates code from functional programs
(including overloading using type classes) to SML \cite{SML}, OCaml
-  \cite{scala-overview-tech-report}.
-  Conceptually, code generation is split up in three steps:
-  \emph{selection} of code theorems, \emph{translation} into an
-  abstract executable view and \emph{serialization} to a specific
-  \emph{target language}.  Inductive specifications can be executed
-  using the predicate compiler which operates within HOL.
-  See \cite{isabelle-codegen} for an introduction.
+  \cite{scala-overview-tech-report}.  Conceptually, code generation is
+  split up in three steps: \emph{selection} of code theorems,
+  \emph{translation} into an abstract executable view and
+  \emph{serialization} to a specific \emph{target language}.
+  Inductive specifications can be executed using the predicate
+  compiler which operates within HOL.  See \cite{isabelle-codegen} for
+  an introduction.

\begin{matharray}{rcl}
@{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -1408,22 +1417,24 @@
generator setup.

\end{description}
+*}

-  The other framework generates code from both functional and
-  relational programs to SML.  See \cite{isabelle-HOL} for further
-  information (this actually covers the new-style theory format as
-  well).
+
+subsection {* The old code generator (S. Berghofer) *}
+
+text {* This framework generates code from both functional and
+  relational programs to SML, as explained below.

\begin{matharray}{rcl}
-    @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "types_code"} & : & @{text "theory \<rightarrow> theory"} \\
@{attribute_def code} & : & @{text attribute} \\
\end{matharray}

@{rail "
-  ( @@{command (HOL) code_module} | @@{command (HOL) code_library} ) modespec? @{syntax name}? \\
+  ( @@{command code_module} | @@{command code_library} ) modespec? @{syntax name}? \\
( @'file' name ) ? ( @'imports' ( @{syntax name} + ) ) ? \\
@'contains' ( ( @{syntax name} '=' @{syntax term} ) + | @{syntax term} + )
;
@@ -1457,6 +1468,166 @@
*}

+subsubsection {* Invoking the code generator *}
+
+text {* The code generator is invoked via the @{command code_module}
+  and @{command code_library} commands, which correspond to
+  \emph{incremental} and \emph{modular} code generation, respectively.
+
+  \begin{description}
+
+  \item [Modular] For each theory, an ML structure is generated,
+  containing the code generated from the constants defined in this
+  theory.
+
+  \item [Incremental] All the generated code is emitted into the same
+  structure.  This structure may import code from previously generated
+  structures, which can be specified via @{keyword "imports"}.
+  Moreover, the generated structure may also be referred to in later
+  invocations of the code generator.
+
+  \end{description}
+
+  After the @{command code_module} and @{command code_library}
+  keywords, the user may specify an optional list of modes'' in
+  parentheses. These can be used to instruct the code generator to
+  emit additional code for special purposes, e.g.\ functions for
+  converting elements of generated datatypes to Isabelle terms, or
+  test data generators. The list of modes is followed by a module
+  name.  The module name is optional for modular code generation, but
+  must be specified for incremental code generation.
+
+  The code can either be written to a file, in which case a file name
+  has to be specified after the @{keyword "file"} keyword, or be loaded
+  directly into Isabelle's ML environment. In the latter case, the
+  @{command ML} theory command can be used to inspect the results
+  interactively, for example.
+
+  The terms from which to generate code can be specified after the
+  @{keyword "contains"} keyword, either as a list of bindings, or just
+  as a list of terms. In the latter case, the code generator just
+  produces code for all constants and types occuring in the term, but
+  does not bind the compiled terms to ML identifiers.
+
+  Here is an example:
+*}
+
+code_module Test
+  contains test = "foldl op + (0 :: int) [1, 2, 3, 4, 5]"
+
+text {* \noindent This binds the result of compiling the given term to
+  the ML identifier @{ML Test.test}.  *}
+
+ML {* @{assert} (Test.test = 15) *}
+
+
+subsubsection {* Configuring the code generator *}
+
+text {* When generating code for a complex term, the code generator
+  recursively calls itself for all subterms.  When it arrives at a
+  constant, the default strategy of the code generator is to look up
+  its definition and try to generate code for it.  Constants which
+  have no definitions that are immediately executable, may be
+  associated with a piece of ML code manually using the @{command_ref
+  consts_code} command.  It takes a list whose elements consist of a
+  constant (given in usual term syntax -- an explicit type constraint
+  accounts for overloading), and a mixfix template describing the ML
+  code. The latter is very much the same as the mixfix templates used
+  when declaring new constants.  The most notable difference is that
+  terms may be included in the ML template using antiquotation
+  brackets @{verbatim "{"}@{verbatim "*"}~@{text "..."}~@{verbatim
+  "*"}@{verbatim "}"}.
+
+  A similar mechanism is available for types: @{command_ref
+  types_code} associates type constructors with specific ML code.
+
+  For example, the following declarations copied from @{file
+  "~~/src/HOL/Product_Type.thy"} describe how the product type of
+  Isabelle/HOL should be compiled to ML.  *}
+
+typedecl ('a, 'b) prod
+consts Pair :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) prod"
+
+types_code prod  ("(_ */ _)")
+consts_code Pair  ("(_,/ _)")
+
+text {* Sometimes, the code associated with a constant or type may
+  need to refer to auxiliary functions, which have to be emitted when
+  the constant is used. Code for such auxiliary functions can be
+  declared using @{keyword "attach"}. For example, the @{const wfrec}
+  function can be implemented as follows:
+*}
+
+consts_code wfrec  ("\<module>wfrec?")  (* FIXME !? *)
+  attach {* fun wfrec f x = f (wfrec f) x *}
+
+text {* If the code containing a call to @{const wfrec} resides in an
+  ML structure different from the one containing the function
+  definition attached to @{const wfrec}, the name of the ML structure
+  (followed by a @{text "."}'')  is inserted in place of @{text
+  "\<module>"}'' in the above template.  The @{text "?"}''  means that
+  the code generator should ignore the first argument of @{const
+  wfrec}, i.e.\ the termination relation, which is usually not
+  executable.
+
+  \medskip Another possibility of configuring the code generator is to
+  register theorems to be used for code generation. Theorems can be
+  registered via the @{attribute code} attribute. It takes an optional
+  name as an argument, which indicates the format of the
+  theorem. Currently supported formats are equations (this is the
+  default when no name is specified) and horn clauses (this is
+  indicated by the name \texttt{ind}). The left-hand sides of
+  equations may only contain constructors and distinct variables,
+  whereas horn clauses must have the same format as introduction rules
+  of inductive definitions.
+
+  The following example specifies three equations from which to
+  generate code for @{term "op <"} on natural numbers (see also
+  @{"file" "~~/src/HOL/Nat.thy"}).  *}
+
+lemma [code]: "(Suc m < Suc n) = (m < n)"
+  and [code]: "((n::nat) < 0) = False"
+  and [code]: "(0 < Suc n) = True" by simp_all
+
+
+subsubsection {* Specific HOL code generators *}
+
+text {* The basic code generator framework offered by Isabelle/Pure
+  has already been extended with additional code generators for
+  specific HOL constructs. These include datatypes, recursive
+  functions and inductive relations. The code generator for inductive
+  relations can handle expressions of the form @{text "(t\<^sub>1, \<dots>, t\<^sub>n) \<in>
+  r"}, where @{text "r"} is an inductively defined relation. If at
+  least one of the @{text "t\<^sub>i"} is a dummy pattern @{text "_"}'',
+  the above expression evaluates to a sequence of possible answers. If
+  all of the @{text "t\<^sub>i"} are proper terms, the expression evaluates
+  to a boolean value.
+
+  %FIXME
+  %\begin{ttbox}
+  %  theory Test = Lambda:
+  %
+  %  code_module Test
+  %  contains
+  %    test1 = "Abs (Var 0) $$\circ$$ Var 0 -> Var 0"
+  %    test2 = "Abs (Abs (Var 0 $$\circ$$ Var 0) $$\circ$$ (Abs (Var 0) $$\circ$$ Var 0)) -> _"
+  %\end{ttbox}
+  %In the above example, \texttt{Test.test1} evaluates to the boolean
+  %value \texttt{true}, whereas \texttt{Test.test2} is a sequence whose
+  %elements can be inspected using \texttt{Seq.pull} or similar functions.
+  %\begin{ttbox}
+  %ML \{* Seq.pull Test.test2 *\}  -- \{* This is the first answer *\}
+  %ML \{* Seq.pull (snd (the it)) *\}  -- \{* This is the second answer *\}
+  %\end{ttbox}
+
+  \medskip The theory underlying the HOL code generator is described
+  more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
+  illustrate the usage of the code generator can be found e.g.\ in
+  @{"file" "~~/src/HOL/MicroJava/J/JListExample.thy"} and @{"file"
+  "~~/src/HOL/MicroJava/JVM/JVMListExample.thy"}.
+*}
+
+
section {* Definition by specification \label{sec:hol-specification} *}

text {*
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 20:34:34 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 02 21:33:21 2011 +0200
@@ -10,6 +10,7 @@
\isacommand{theory}\isamarkupfalse%
\ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
\isakeyword{imports}\ Main\isanewline
+\isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
@@ -1699,21 +1700,34 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Isabelle/Pure provides two generic frameworks to support code
-  generation from executable specifications.  Isabelle/HOL
-  instantiates these mechanisms in a way that is amenable to end-user
-  applications.
+For validation purposes, it is often useful to \emph{execute}
+  specifications.  In principle, execution could be simulated by
+  Isabelle's inference kernel, i.e. by a combination of resolution and
+  simplification.  Unfortunately, this approach is rather inefficient.
+  A more efficient way of executing specifications is to translate
+  them into a functional programming language such as ML.

-  \medskip One framework generates code from functional programs
+  Isabelle provides two generic frameworks to support code generation
+  from executable specifications.  Isabelle/HOL instantiates these
+  mechanisms in a way that is amenable to end-user applications.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The new code generator (F. Haftmann)%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This framework generates code from functional programs
(including overloading using type classes) to SML \cite{SML}, OCaml
-  \cite{scala-overview-tech-report}.
-  Conceptually, code generation is split up in three steps:
-  \emph{selection} of code theorems, \emph{translation} into an
-  abstract executable view and \emph{serialization} to a specific
-  \emph{target language}.  Inductive specifications can be executed
-  using the predicate compiler which operates within HOL.
-  See \cite{isabelle-codegen} for an introduction.
+  \cite{scala-overview-tech-report}.  Conceptually, code generation is
+  split up in three steps: \emph{selection} of code theorems,
+  \emph{translation} into an abstract executable view and
+  \emph{serialization} to a specific \emph{target language}.
+  Inductive specifications can be executed using the predicate
+  compiler which operates within HOL.  See \cite{isabelle-codegen} for
+  an introduction.

\begin{matharray}{rcl}
\indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
@@ -2155,27 +2169,32 @@
is generated into that specified file without modifying the code
generator setup.

-  \end{description}
-
-  The other framework generates code from both functional and
-  relational programs to SML.  See \cite{isabelle-HOL} for further
-  information (this actually covers the new-style theory format as
-  well).
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The old code generator (S. Berghofer)%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This framework generates code from both functional and
+  relational programs to SML, as explained below.

\begin{matharray}{rcl}
-    \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
-    \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{code\_module}\hypertarget{command.code-module}{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{code\_library}\hypertarget{command.code-library}{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{consts\_code}\hypertarget{command.consts-code}{\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{types\_code}\hypertarget{command.types-code}{\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{attribute}{code}\hypertarget{attribute.code}{\hyperlink{attribute.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
\end{matharray}

\begin{railoutput}
\rail@begin{11}{\isa{}}
\rail@bar
\rail@nextbar{1}
\rail@endbar
\rail@bar
\rail@nextbar{1}
@@ -2282,6 +2301,205 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsubsection{Invoking the code generator%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The code generator is invoked via the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}
+  and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}} commands, which correspond to
+  \emph{incremental} and \emph{modular} code generation, respectively.
+
+  \begin{description}
+
+  \item [Modular] For each theory, an ML structure is generated,
+  containing the code generated from the constants defined in this
+  theory.
+
+  \item [Incremental] All the generated code is emitted into the same
+  structure.  This structure may import code from previously generated
+  structures, which can be specified via \hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}.
+  Moreover, the generated structure may also be referred to in later
+  invocations of the code generator.
+
+  \end{description}
+
+  keywords, the user may specify an optional list of modes'' in
+  parentheses. These can be used to instruct the code generator to
+  emit additional code for special purposes, e.g.\ functions for
+  converting elements of generated datatypes to Isabelle terms, or
+  test data generators. The list of modes is followed by a module
+  name.  The module name is optional for modular code generation, but
+  must be specified for incremental code generation.
+
+  The code can either be written to a file, in which case a file name
+  has to be specified after the \hyperlink{keyword.file}{\mbox{\isa{\isakeyword{file}}}} keyword, or be loaded
+  directly into Isabelle's ML environment. In the latter case, the
+  \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} theory command can be used to inspect the results
+  interactively, for example.
+
+  The terms from which to generate code can be specified after the
+  \hyperlink{keyword.contains}{\mbox{\isa{\isakeyword{contains}}}} keyword, either as a list of bindings, or just
+  as a list of terms. In the latter case, the code generator just
+  produces code for all constants and types occuring in the term, but
+  does not bind the compiled terms to ML identifiers.
+
+  Here is an example:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%
+\ Test\isanewline
+\begin{isamarkuptext}%
+\noindent This binds the result of compiling the given term to
+  the ML identifier \verb|Test.test|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+%
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
+\isaantiq
+assert{}%
+\endisaantiq
+\endisatagML
+{\isafoldML}%
+%
+%
+%
+\isamarkupsubsubsection{Configuring the code generator%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When generating code for a complex term, the code generator
+  recursively calls itself for all subterms.  When it arrives at a
+  constant, the default strategy of the code generator is to look up
+  its definition and try to generate code for it.  Constants which
+  have no definitions that are immediately executable, may be
+  associated with a piece of ML code manually using the \indexref{}{command}{consts\_code}\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}} command.  It takes a list whose elements consist of a
+  constant (given in usual term syntax -- an explicit type constraint
+  accounts for overloading), and a mixfix template describing the ML
+  code. The latter is very much the same as the mixfix templates used
+  when declaring new constants.  The most notable difference is that
+  terms may be included in the ML template using antiquotation
+  brackets \verb|{|\verb|*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*|\verb|}|.
+
+  A similar mechanism is available for types: \indexref{}{command}{types\_code}\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}} associates type constructors with specific ML code.
+
+  For example, the following declarations copied from \verb|~~/src/HOL/Product_Type.thy| describe how the product type of
+  Isabelle/HOL should be compiled to ML.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{typedecl}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod\isanewline
+\isacommand{consts}\isamarkupfalse%
+\ Pair\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
+\ prod\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
+\ Pair\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptext}%
+Sometimes, the code associated with a constant or type may
+  need to refer to auxiliary functions, which have to be emitted when
+  the constant is used. Code for such auxiliary functions can be
+  declared using \hyperlink{keyword.attach}{\mbox{\isa{\isakeyword{attach}}}}. For example, the \isa{wfrec}
+  function can be implemented as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
+\ wfrec\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}wfrec{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \ \isanewline
+\ \ \isakeyword{attach}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ fun\ wfrec\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}wfrec\ f{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
+\begin{isamarkuptext}%
+If the code containing a call to \isa{wfrec} resides in an
+  ML structure different from the one containing the function
+  definition attached to \isa{wfrec}, the name of the ML structure
+  (followed by a \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}'')  is inserted in place of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}{\isaliteral{22}{\isachardoublequote}}}'' in the above template.  The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''  means that
+  the code generator should ignore the first argument of \isa{wfrec}, i.e.\ the termination relation, which is usually not
+  executable.
+
+  \medskip Another possibility of configuring the code generator is to
+  register theorems to be used for code generation. Theorems can be
+  registered via the \hyperlink{attribute.code}{\mbox{\isa{code}}} attribute. It takes an optional
+  name as an argument, which indicates the format of the
+  theorem. Currently supported formats are equations (this is the
+  default when no name is specified) and horn clauses (this is
+  indicated by the name \texttt{ind}). The left-hand sides of
+  equations may only contain constructors and distinct variables,
+  whereas horn clauses must have the same format as introduction rules
+  of inductive definitions.
+
+  The following example specifies three equations from which to
+  generate code for \isa{{\isaliteral{22}{\isachardoublequote}}op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}} on natural numbers (see also
+  \verb|~~/src/HOL/Nat.thy|).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Suc\ m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{3C}{\isacharless}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}%
+\ %
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp{\isaliteral{5F}{\isacharunderscore}}all%
+\endisatagproof
+{\isafoldproof}%
+%
+%
+%
+\isamarkupsubsubsection{Specific HOL code generators%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The basic code generator framework offered by Isabelle/Pure
+  has already been extended with additional code generators for
+  specific HOL constructs. These include datatypes, recursive
+  functions and inductive relations. The code generator for inductive
+  relations can handle expressions of the form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{22}{\isachardoublequote}}} is an inductively defined relation. If at
+  least one of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} is a dummy pattern \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'',
+  the above expression evaluates to a sequence of possible answers. If
+  all of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} are proper terms, the expression evaluates
+  to a boolean value.
+
+  %FIXME
+  %\begin{ttbox}
+  %  theory Test = Lambda:
+  %
+  %  code_module Test
+  %  contains
+  %    test1 = "Abs (Var 0) $$\circ$$ Var 0 -> Var 0"
+  %    test2 = "Abs (Abs (Var 0 $$\circ$$ Var 0) $$\circ$$ (Abs (Var 0) $$\circ$$ Var 0)) -> _"
+  %\end{ttbox}
+  %In the above example, \texttt{Test.test1} evaluates to the boolean
+  %value \texttt{true}, whereas \texttt{Test.test2} is a sequence whose
+  %elements can be inspected using \texttt{Seq.pull} or similar functions.
+  %\begin{ttbox}
+  %ML \{* Seq.pull Test.test2 *\}  -- \{* This is the first answer *\}
+  %ML \{* Seq.pull (snd (the it)) *\}  -- \{* This is the second answer *\}
+  %\end{ttbox}
+
+  \medskip The theory underlying the HOL code generator is described
+  more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
+  illustrate the usage of the code generator can be found e.g.\ in
+  \verb|~~/src/HOL/MicroJava/J/JListExample.thy| and \verb|~~/src/HOL/MicroJava/JVM/JVMListExample.thy|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Definition by specification \label{sec:hol-specification}%
}
\isamarkuptrue%