moved material about old codegen to isar-ref manual;
eliminated old rail diagram;
--- 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{OCaml}, Haskell \cite{haskell-revised-report} and Scala
- \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{OCaml}, Haskell \cite{haskell-revised-report} and Scala
- \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@term{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
+\rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
\rail@nextbar{1}
-\rail@term{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]
+\rail@term{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]
\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}
+
+ After 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}}}}
+ 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
+\ \ \isakeyword{contains}\ test\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}foldl\ op\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{4}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{5}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent This binds the result of compiling the given term to
+ the ML identifier \verb|Test.test|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
+\isaantiq
+assert{}%
+\endisaantiq
+\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{2E}{\isachardot}}test\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\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}}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp{\isaliteral{5F}{\isacharunderscore}}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\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%