# HG changeset patch # User wenzelm # Date 1304364801 -7200 # Node ID 8749742785b8cfe2519c8264a25756a24eb02a15 # Parent 6ac8c55c657ede22016db59a59846019a17ca731 moved material about old codegen to isar-ref manual; eliminated old rail diagram; diff -r 6ac8c55c657e -r 8749742785b8 doc-src/HOL/HOL.tex --- 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" ("\bswfrec?") -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}'' 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 diff -r 6ac8c55c657e -r 8749742785b8 doc-src/HOL/logics-HOL.rai --- 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; } diff -r 6ac8c55c657e -r 8749742785b8 doc-src/IsarRef/Thy/HOL_Specific.thy --- 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 \"} \\ @@ -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 \ theory"} \\ - @{command_def (HOL) "code_library"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "consts_code"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "types_code"} & : & @{text "theory \ theory"} \\ + @{command_def "code_module"} & : & @{text "theory \ theory"} \\ + @{command_def "code_library"} & : & @{text "theory \ theory"} \\ + @{command_def "consts_code"} & : & @{text "theory \ theory"} \\ + @{command_def "types_code"} & : & @{text "theory \ 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 \ 'b \ ('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 ("\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 + "\"}'' 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, \, t\<^sub>n) \ + 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 {* diff -r 6ac8c55c657e -r 8749742785b8 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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%