--- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Wed Oct 01 12:18:18 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy Wed Oct 01 13:33:54 2008 +0200
@@ -66,12 +66,12 @@
primrec %quoteme in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
"in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
-
+(*<*)
code_type %invisible bool
(SML)
code_const %invisible True and False and "op \<and>" and Not
(SML and and and)
-
+(*>*)
text %quoteme {*@{code_stmts in_interval (SML)}*}
text {*
@@ -92,7 +92,7 @@
(SML "true" and "false" and "_ andalso _")
text {*
- The @{command code_type} command takes a type constructor
+ \noindent The @{command code_type} command takes a type constructor
as arguments together with a list of custom serialisations.
Each custom serialisation starts with a target language
identifier followed by an expression, which during
@@ -120,22 +120,22 @@
text %quoteme {*@{code_stmts in_interval (SML)}*}
text {*
- Next, we try to map HOL pairs to SML pairs, using the
+ \noindent Next, we try to map HOL pairs to SML pairs, using the
infix ``@{verbatim "*"}'' type constructor and parentheses:
*}
-
+(*<*)
code_type %invisible *
(SML)
code_const %invisible Pair
(SML)
-
+(*>*)
code_type %tt *
(SML infix 2 "*")
code_const %tt Pair
(SML "!((_),/ (_))")
text {*
- The initial bang ``@{verbatim "!"}'' tells the serializer to never put
+ \noindent The initial bang ``@{verbatim "!"}'' tells the serializer to never put
parentheses around the whole expression (they are already present),
while the parentheses around argument place holders
tell not to put parentheses around the arguments.
@@ -178,7 +178,7 @@
(Haskell infixl 4 "==")
text {*
- A problem now occurs whenever a type which
+ \noindent A problem now occurs whenever a type which
is an instance of @{class eq} in @{text HOL} is mapped
on a @{text Haskell}-built-in type which is also an instance
of @{text Haskell} @{text Eq}:
@@ -199,7 +199,7 @@
(Haskell "Integer")
text {*
- The code generator would produce
+ \noindent The code generator would produce
an additional instance, which of course is rejectedby the @{text Haskell}
compiler.
To suppress this additional instance, use
--- a/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Wed Oct 01 12:18:18 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy Wed Oct 01 13:33:54 2008 +0200
@@ -2,7 +2,7 @@
imports Setup
begin
-section {* Further topics \label{sec:further} *}
+section {* Further issues \label{sec:further} *}
subsection {* Further reading *}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Wed Oct 01 12:18:18 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy Wed Oct 01 13:33:54 2008 +0200
@@ -28,19 +28,21 @@
The code generator aims to be usable with no further ado
in most cases while allowing for detailed customisation.
This manifests in the structure of this tutorial: after a short
- conceptual introduction with an example \secref{sec:intro},
- we discuss the generic customisation facilities \secref{sec:program}.
- A further section \secref{sec:adaption} is dedicated to the matter of
+ conceptual introduction with an example (\secref{sec:intro}),
+ we discuss the generic customisation facilities (\secref{sec:program}).
+ A further section (\secref{sec:adaption}) is dedicated to the matter of
\qn{adaption} to specific target language environments. After some
- further issues \secref{sec:further} we conclude with an overview
- of some ML programming interfaces \secref{sec:ml}.
+ further issues (\secref{sec:further}) we conclude with an overview
+ of some ML programming interfaces (\secref{sec:ml}).
\begin{warn}
Ultimately, the code generator which this tutorial deals with
- is supposed to replace the already established code generator
+ is supposed to replace the existing code generator
by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
So, for the moment, there are two distinct code generators
- in Isabelle.
+ in Isabelle. In case of ambiguity, we will refer to the framework
+ described here as @{text "generic code generator"}, to the
+ other as @{text "SML code generator"}.
Also note that while the framework itself is
object-logic independent, only @{theory HOL} provides a reasonable
framework setup.
@@ -59,7 +61,6 @@
@{command definition}/@{command primrec}/@{command fun} declarations form
the core of a functional programming language. The default code generator setup
allows to turn those into functional programs immediately.
-
This means that \qt{naive} code generation can proceed without further ado.
For example, here a simple \qt{implementation} of amortised queues:
*}
@@ -75,11 +76,13 @@
fun %quoteme dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
"dequeue (Queue [] []) = (None, Queue [] [])"
| "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)"
- | "dequeue (Queue xs []) = (case rev xs of y # ys \<Rightarrow> (Some y, Queue [] ys))"
+ | "dequeue (Queue xs []) =
+ (case rev xs of y # ys \<Rightarrow> (Some y, Queue [] ys))"
text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
-export_code %quoteme empty dequeue enqueue in SML module_name Example file "examples/example.ML"
+export_code %quoteme empty dequeue enqueue in SML
+ module_name Example file "examples/example.ML"
text {* \noindent resulting in the following code: *}
@@ -88,7 +91,7 @@
text {*
\noindent The @{command export_code} command takes a space-separated list of
constants for which code shall be generated; anything else needed for those
- is added implicitly. Then follows by a target language identifier
+ is added implicitly. Then follows a target language identifier
(@{text SML}, @{text OCaml} or @{text Haskell}) and a freely chosen module name.
A file name denotes the destination to store the generated code. Note that
the semantics of the destination depends on the target language: for
@@ -97,7 +100,8 @@
(with extension @{text ".hs"}) is written:
*}
-export_code %quoteme empty dequeue enqueue in Haskell module_name Example file "examples/"
+export_code %quoteme empty dequeue enqueue in Haskell
+ module_name Example file "examples/"
text {*
\noindent This is how the corresponding code in @{text Haskell} looks like:
@@ -107,10 +111,10 @@
text {*
\noindent This demonstrates the basic usage of the @{command export_code} command;
- for more details see \secref{sec:serializer}.
+ for more details see \secref{sec:further}.
*}
-subsection {* Code generator architecture *}
+subsection {* Code generator architecture \label{sec:concept} *}
text {*
What you have seen so far should be already enough in a lot of cases. If you
@@ -125,10 +129,6 @@
\label{fig:arch}
\end{figure}
- The code generator itself consists of three major components
- which operate sequentially, i.e. the result of one is the input
- of the next in the chain, see diagram \ref{fig:arch}:
-
The code generator employs a notion of executability
for three foundational executable ingredients known
from functional programming:
@@ -138,8 +138,10 @@
(an equation headed by a constant @{text f} with arguments
@{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}).
Code generation aims to turn defining equations
- into a functional program by running through the following
- process:
+ into a functional program. This is achieved by three major
+ components which operate sequentially, i.e. the result of one is
+ the input
+ of the next in the chain, see diagram \ref{fig:arch}:
\begin{itemize}
@@ -165,7 +167,10 @@
of defining equations.
\item These defining equations are \qn{translated} to a program
- in an abstract intermediate language.
+ in an abstract intermediate language. Think of it as a kind
+ of \qt{Mini-Haskell} with four \qn{statements}: @{text data}
+ (for datatypes), @{text fun} (stemming from defining equations),
+ also @{text class} and @{text inst} (for type classes).
\item Finally, the abstract program is \qn{serialised} into concrete
source code of a target language.
--- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Wed Oct 01 12:18:18 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Wed Oct 01 13:33:54 2008 +0200
@@ -108,12 +108,6 @@
involves using those primitive interfaces
but also storing code-dependent data and various
other things.
-
- \begin{warn}
- Some interfaces discussed here have not reached
- a final state yet.
- Changes likely to occur in future.
- \end{warn}
*}
subsubsection {* Data depending on the theory's executable content *}
@@ -152,7 +146,7 @@
\end{description}
- An instance of @{ML_functor CodeDataFun} provides the following
+ \noindent An instance of @{ML_functor CodeDataFun} provides the following
interface:
\medskip
@@ -175,6 +169,8 @@
*}
text {*
+ \bigskip
+
\emph{Happy proving, happy hacking!}
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Wed Oct 01 12:18:18 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy Wed Oct 01 13:33:54 2008 +0200
@@ -6,20 +6,30 @@
subsection {* The @{text "Isabelle/HOL"} default setup *}
-subsection {* Selecting code equations *}
-
text {*
We have already seen how by default equations stemming from
@{command definition}/@{command primrec}/@{command fun}
- statements are used for code generation. Deviating from this
- \emph{default} behaviour is always possible -- e.g.~we
- could provide an alternative @{text fun} for @{const dequeue} proving
- the following equations explicitly:
+ statements are used for code generation. This default behaviour
+ can be changed, e.g. by providing different defining equations.
+ All kinds of customization shown in this section is \emph{safe}
+ in the sense that the user does not have to worry about
+ correctness -- all programs generatable that way are partially
+ correct.
+*}
+
+subsection {* Selecting code equations *}
+
+text {*
+ Coming back to our introductory example, we
+ could provide an alternative defining equations for @{const dequeue}
+ explicitly:
*}
lemma %quoteme [code func]:
- "dequeue (Queue xs []) = (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))"
- "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)"
+ "dequeue (Queue xs []) =
+ (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))"
+ "dequeue (Queue xs (y # ys)) =
+ (Some y, Queue xs ys)"
by (cases xs, simp_all) (cases "rev xs", simp_all)
text {*
@@ -60,7 +70,7 @@
subsection {* @{text class} and @{text instantiation} *}
text {*
- Concerning type classes and code generation, let us again examine an example
+ Concerning type classes and code generation, let us examine an example
from abstract algebra:
*}
@@ -105,7 +115,7 @@
on monoids:
*}
-primrec %quoteme pow :: "nat \<Rightarrow> 'a\<Colon>monoid \<Rightarrow> 'a\<Colon>monoid" where
+primrec %quoteme (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
"pow 0 a = \<one>"
| "pow (Suc n) a = a \<otimes> pow n a"
@@ -123,31 +133,16 @@
text %quoteme {*@{code_stmts bexp (Haskell)}*}
text {*
- \noindent An inspection reveals that the equations stemming from the
- @{command primrec} statement within instantiation of class
- @{class semigroup} with type @{typ nat} are mapped to a separate
- function declaration @{verbatim mult_nat} which in turn is used
- to provide the right hand side for the @{verbatim "instance Semigroup Nat"}.
- This perfectly
- agrees with the restriction that @{text inst} statements may
- only contain one single equation for each class class parameter
- The @{command instantiation} mechanism manages that for each
- overloaded constant @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}
- a \emph{shadow constant} @{text "f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"} is
- declared satisfying @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>] \<equiv> f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}.
- this equation is indeed the one used for the statement;
- using it as a rewrite rule, defining equations for
- @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"} can be turned into
- defining equations for @{text "f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}. This
- happens transparently, providing the illusion that class parameters
- can be instantiated with more than one equation.
-
- This is a convenient place to show how explicit dictionary construction
+ \noindent This is a convenient place to show how explicit dictionary construction
manifests in generated code (here, the same example in @{text SML}):
*}
text %quoteme {*@{code_stmts bexp (SML)}*}
+text {*
+ \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
+ which are the dictionary parameters.
+*}
subsection {* The preprocessor \label{sec:preproc} *}
@@ -199,7 +194,7 @@
*}
text {*
- \emph{Function transformers} provide a very general interface,
+ \noindent \emph{Function transformers} provide a very general interface,
transforming a list of function theorems to another
list of function theorems, provided that neither the heading
constant nor its type change. The @{term "0\<Colon>nat"} / @{const Suc}
@@ -215,8 +210,9 @@
\begin{warn}
The attribute \emph{code unfold}
- associated with the existing code generator also applies to
- the new one: \emph{code unfold} implies \emph{code inline}.
+ associated with the @{text "SML code generator"} also applies to
+ the @{text "generic code generator"}:
+ \emph{code unfold} implies \emph{code inline}.
\end{warn}
*}
@@ -246,7 +242,7 @@
"Dig1 n = Suc (2 * n)"
text {*
- \noindent We will use these two ">digits"< to represent natural numbers
+ \noindent We will use these two \qt{digits} to represent natural numbers
in binary digits, e.g.:
*}
@@ -299,9 +295,7 @@
text %quoteme {*@{code_stmts "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (SML)}*}
text {*
- \medskip
-
- From this example, it can be easily glimpsed that using own constructor sets
+ \noindent From this example, it can be easily glimpsed that using own constructor sets
is a little delicate since it changes the set of valid patterns for values
of that type. Without going into much detail, here some practical hints:
@@ -334,9 +328,8 @@
by the code generator:
*}
-primrec %quoteme
- collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "collect_duplicates xs ys [] = xs"
+primrec %quoteme collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+ "collect_duplicates xs ys [] = xs"
| "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
then if z \<in> set ys
then collect_duplicates xs ys zs
@@ -356,7 +349,8 @@
way using a type class. How is this achieved? HOL introduces
an explicit class @{class eq} with a corresponding operation
@{const eq_class.eq} such that @{thm eq [no_vars]}.
- The preprocessing framework does the rest.
+ The preprocessing framework does the rest by propagating the
+ @{class eq} constraints through all dependent defining equations.
For datatypes, instances of @{class eq} are implicitly derived
when possible. For other types, you may instantiate @{text eq}
manually like any other type class.
@@ -365,50 +359,54 @@
the way, a subtlety
enters the stage when definitions of overloaded constants
are dependent on operational equality. For example, let
- us define a lexicographic ordering on tuples:
+ us define a lexicographic ordering on tuples
+ (also see theory @{theory Product_ord}):
*}
-instantiation %quoteme * :: (ord, ord) ord
+instantiation %quoteme "*" :: (order, order) order
begin
definition %quoteme [code func del]:
- "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))"
+ "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
definition %quoteme [code func del]:
- "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))"
+ "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
-instance %quoteme ..
+instance %quoteme proof
+qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
end %quoteme
-lemma %quoteme ord_prod [code func]:
- "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
- "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
- unfolding less_prod_def less_eq_prod_def by simp_all
+lemma %quoteme order_prod [code func]:
+ "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
+ x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
+ "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
+ x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
+ by (simp_all add: less_prod_def less_eq_prod_def)
text {*
\noindent Then code generation will fail. Why? The definition
of @{term "op \<le>"} depends on equality on both arguments,
which are polymorphic and impose an additional @{class eq}
- class constraint, which the preprocessort does not propagate for technical
- reasons.
+ class constraint, which the preprocessor does not propagate
+ (for technical reasons).
The solution is to add @{class eq} explicitly to the first sort arguments in the
code theorems:
*}
-lemma ord_prod_code [code func]:
- "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
- "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow>
- x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
- unfolding ord_prod by rule+
+lemma %quoteme order_prod_code [code func]:
+ "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
+ x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
+ "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
+ x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
+ by (simp_all add: less_prod_def less_eq_prod_def)
text {*
\noindent Then code generation succeeds:
*}
-text %quoteme {*@{code_stmts "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" (SML)}*}
+text %quoteme {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
text {*
In some cases, the automatically derived defining equations
@@ -434,7 +432,7 @@
recursive @{text inst} and @{text fun} definitions,
but the SML serializer does not support this.
- In such cases, you have to provide you own equality equations
+ In such cases, you have to provide your own equality equations
involving auxiliary constants. In our case,
@{const [show_types] list_all2} can do the job:
*}
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Wed Oct 01 12:18:18 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy Wed Oct 01 13:33:54 2008 +0200
@@ -3,7 +3,8 @@
uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML"
begin
-ML {* no_document use_thys ["Efficient_Nat", "Code_Char_chr"] *}
+ML {* no_document use_thys
+ ["Efficient_Nat", "Code_Char_chr", "Product_ord"] *}
ML_val {* Code_Target.code_width := 74 *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex Wed Oct 01 13:33:54 2008 +0200
@@ -0,0 +1,484 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Adaption}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Adaption\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Adaption to target languages \label{sec:adaption}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Common adaption cases%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
+ generator setup
+ which should be suitable for most applications. Common extensions
+ and modifications are available by certain theories of the \isa{HOL}
+ library; beside being useful in applications, they may serve
+ as a tutorial for customising the code generator setup (see below
+ \secref{sec:adaption_mechanisms}).
+
+ \begin{description}
+
+ \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
+ integer literals in target languages.
+ \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by
+ character literals in target languages.
+ \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
+ but also offers treatment of character codes; includes
+ \hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}.
+ \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
+ which in general will result in higher efficiency; pattern
+ matching with \isa{{\isadigit{0}}} / \isa{Suc}
+ is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}.
+ \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
+ \isa{index} which is mapped to target-language built-in integers.
+ Useful for code setups which involve e.g. indexing of
+ target-language arrays.
+ \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
+ \isa{message{\isacharunderscore}string} which is isomorphic to strings;
+ \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
+ Useful for code setups which involve e.g. printing (error) messages.
+
+ \end{description}
+
+ \begin{warn}
+ When importing any of these theories, they should form the last
+ items in an import list. Since these theories adapt the
+ code generator setup in a non-conservative fashion,
+ strange effects may occur otherwise.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Adaption mechanisms \label{sec:adaption_mechanisms}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{warn}
+ The mechanisms shown here are especially for the curious; the user
+ rarely needs to do anything on his own beyond the defaults in \isa{HOL}.
+ Adaption is a delicated task which requires a lot of dilligence since
+ it happend \emph{completely} outside the logic.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Consider the following function and its corresponding
+ SML code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{primrec}\isamarkupfalse%
+\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|datatype boola = False |\verb,|,\verb| True;|\newline%
+\newline%
+\verb|fun anda x True = x|\newline%
+\verb| |\verb,|,\verb| anda x False = False|\newline%
+\verb| |\verb,|,\verb| anda True x = x|\newline%
+\verb| |\verb,|,\verb| anda False x = False;|\newline%
+\newline%
+\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
+\verb| |\verb,|,\verb| less_nat n Zero_nat = False|\newline%
+\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
+\verb| |\verb,|,\verb| less_eq_nat Zero_nat n = True;|\newline%
+\newline%
+\verb|fun in_interval (k, l) n = anda (less_eq_nat k n) (less_eq_nat n l);|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Though this is correct code, it is a little bit unsatisfactory:
+ boolean values and operators are materialised as distinguished
+ entities with have nothing to do with the SML-built-in notion
+ of \qt{bool}. This results in less readable code;
+ additionally, eager evaluation may cause programs to
+ loop or break which would perfectly terminate when
+ the existing SML \verb|bool| would be used. To map
+ the HOL \isa{bool} on SML \verb|bool|, we may use
+ \qn{custom serialisations}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ bool\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\begin{isamarkuptext}%
+\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
+ as arguments together with a list of custom serialisations.
+ Each custom serialisation starts with a target language
+ identifier followed by an expression, which during
+ code serialisation is inserted whenever the type constructor
+ would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
+ the corresponding mechanism. Each ``\verb|_|'' in
+ a serialisation expression is treated as a placeholder
+ for the type constructor's (the constant's) arguments.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
+\verb| |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
+\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
+\verb| |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
+\newline%
+\verb|fun in_interval (k, l) n = (less_eq_nat k n) andalso (less_eq_nat n l);|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent This still is not perfect: the parentheses
+ around the \qt{andalso} expression are superfluous.
+ Though the serializer
+ by no means attempts to imitate the rich Isabelle syntax
+ framework, it provides some common idioms, notably
+ associative infixes with precedences which may be used here:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|fun less_nat m (Suc n) = less_eq_nat m n|\newline%
+\verb| |\verb,|,\verb| less_nat n Zero_nat = false|\newline%
+\verb|and less_eq_nat (Suc m) n = less_nat m n|\newline%
+\verb| |\verb,|,\verb| less_eq_nat Zero_nat n = true;|\newline%
+\newline%
+\verb|fun in_interval (k, l) n = less_eq_nat k n andalso less_eq_nat n l;|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Next, we try to map HOL pairs to SML pairs, using the
+ infix ``\verb|*|'' type constructor and parentheses:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ {\isacharasterisk}\isanewline
+\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ Pair\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\begin{isamarkuptext}%
+\noindent The initial bang ``\verb|!|'' tells the serializer to never put
+ parentheses around the whole expression (they are already present),
+ while the parentheses around argument place holders
+ tell not to put parentheses around the arguments.
+ The slash ``\verb|/|'' (followed by arbitrary white space)
+ inserts a space which may be used as a break if necessary
+ during pretty printing.
+
+ These examples give a glimpse what mechanisms
+ custom serialisations provide; however their usage
+ requires careful thinking in order not to introduce
+ inconsistencies -- or, in other words:
+ custom serialisations are completely axiomatic.
+
+ A further noteworthy details is that any special
+ character in a custom serialisation may be quoted
+ using ``\verb|'|''; thus, in
+ ``\verb|fn '_ => _|'' the first
+ ``\verb|_|'' is a proper underscore while the
+ second ``\verb|_|'' is a placeholder.
+
+ The HOL theories provide further
+ examples for custom serialisations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{\isa{Haskell} serialisation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+For convenience, the default
+ \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
+ its counterpart in \isa{Haskell}, giving custom serialisations
+ for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
+ \isa{eq{\isacharunderscore}class{\isachardot}eq}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
+\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
+\ eq\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}HOL{\isachardot}eq{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\isanewline
+\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\begin{isamarkuptext}%
+\noindent A problem now occurs whenever a type which
+ is an instance of \isa{eq} in \isa{HOL} is mapped
+ on a \isa{Haskell}-built-in type which is also an instance
+ of \isa{Haskell} \isa{Eq}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{typedecl}\isamarkupfalse%
+\ bar\isanewline
+\isanewline
+\isacommand{instantiation}\isamarkupfalse%
+\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{by}\isamarkupfalse%
+\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+\isanewline
+%
+\isadelimtt
+\isanewline
+%
+\endisadelimtt
+%
+\isatagtt
+\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\ bar\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\begin{isamarkuptext}%
+\noindent The code generator would produce
+ an additional instance, which of course is rejectedby the \isa{Haskell}
+ compiler.
+ To suppress this additional instance, use
+ \isa{code{\isacharunderscore}instance}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtt
+%
+\endisadelimtt
+%
+\isatagtt
+\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
+\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
+\endisatagtt
+{\isafoldtt}%
+%
+\isadelimtt
+%
+\endisadelimtt
+\isanewline
+%
+\isadelimtheory
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex Wed Oct 01 13:33:54 2008 +0200
@@ -0,0 +1,108 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Further}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Further\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Further issues \label{sec:further}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Further reading%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Do dive deeper into the issue of code generation, you should visit
+ the Isabelle/Isar Reference Manual \cite{isabelle-isar-ref} which
+ constains exhaustive syntax diagrams.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Modules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When invoking the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command it is possible to leave
+ out the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} part; then code is distributed over
+ different modules, where the module name space roughly is induced
+ by the \isa{Isabelle} theory namespace.
+
+ Then sometimes the awkward situation occurs that dependencies between
+ definitions introduce cyclic dependencies between modules, which in the
+ \isa{Haskell} world leaves you to the mercy of the \isa{Haskell} implementation
+ you are using, while for \isa{SML}/\isa{OCaml} code generation is not possible.
+
+ A solution is to declare module names explicitly.
+ Let use assume the three cyclically dependent
+ modules are named \emph{A}, \emph{B} and \emph{C}.
+ Then, by stating%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}modulename}\isamarkupfalse%
+\ SML\isanewline
+\ \ A\ ABC\isanewline
+\ \ B\ ABC\isanewline
+\ \ C\ ABC%
+\begin{isamarkuptext}%
+we explicitly map all those modules on \emph{ABC},
+ resulting in an ad-hoc merge of this three modules
+ at serialisation time.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Evaluation oracle%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Code antiquotation%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Creating new targets%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+extending targets, adding targets%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Imperative data structures%
+}
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex Wed Oct 01 13:33:54 2008 +0200
@@ -0,0 +1,369 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Introduction}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Introduction\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Code generation from \isa{Isabelle{\isacharslash}HOL} theories%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Introduction and Overview%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This tutorial introduces a generic code generator for the
+ \isa{Isabelle} system.
+ Generic in the sense that the
+ \qn{target language} for which code shall ultimately be
+ generated is not fixed but may be an arbitrary state-of-the-art
+ functional programming language (currently, the implementation
+ supports \isa{SML} \cite{SML}, \isa{OCaml} \cite{OCaml} and \isa{Haskell}
+ \cite{haskell-revised-report}).
+
+ Conceptually the code generator framework is part
+ of Isabelle's \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} meta logic framework; the logic
+ \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} which is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}
+ already comes with a reasonable framework setup and thus provides
+ a good working horse for raising code-generation-driven
+ applications. So, we assume some familiarity and experience
+ with the ingredients of the \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} distribution theories.
+ (see also \cite{isa-tutorial}).
+
+ The code generator aims to be usable with no further ado
+ in most cases while allowing for detailed customisation.
+ This manifests in the structure of this tutorial: after a short
+ conceptual introduction with an example (\secref{sec:intro}),
+ we discuss the generic customisation facilities (\secref{sec:program}).
+ A further section (\secref{sec:adaption}) is dedicated to the matter of
+ \qn{adaption} to specific target language environments. After some
+ further issues (\secref{sec:further}) we conclude with an overview
+ of some ML programming interfaces (\secref{sec:ml}).
+
+ \begin{warn}
+ Ultimately, the code generator which this tutorial deals with
+ is supposed to replace the existing code generator
+ by Stefan Berghofer \cite{Berghofer-Nipkow:2002}.
+ So, for the moment, there are two distinct code generators
+ in Isabelle. In case of ambiguity, we will refer to the framework
+ described here as \isa{generic\ code\ generator}, to the
+ other as \isa{SML\ code\ generator}.
+ Also note that while the framework itself is
+ object-logic independent, only \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} provides a reasonable
+ framework setup.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Code generation via shallow embedding \label{sec:intro}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The key concept for understanding \isa{Isabelle}'s code generation is
+ \emph{shallow embedding}, i.e.~logical entities like constants, types and
+ classes are identified with corresponding concepts in the target language.
+
+ Inside \hyperlink{theory.HOL}{\mbox{\isa{HOL}}}, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and
+ \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form
+ the core of a functional programming language. The default code generator setup
+ allows to turn those into functional programs immediately.
+ This means that \qt{naive} code generation can proceed without further ado.
+ For example, here a simple \qt{implementation} of amortised queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{datatype}\isamarkupfalse%
+\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Then we can generate code e.g.~for \isa{SML} as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
+\ empty\ dequeue\ enqueue\ \isakeyword{in}\ SML\isanewline
+\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}example{\isachardot}ML{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent resulting in the following code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|fun foldl f a [] = a|\newline%
+\verb| |\verb,|,\verb| foldl f a (x :: xs) = foldl f (f a x) xs;|\newline%
+\newline%
+\verb|fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;|\newline%
+\newline%
+\verb|fun list_case f1 f2 (a :: lista) = f2 a lista|\newline%
+\verb| |\verb,|,\verb| list_case f1 f2 [] = f1;|\newline%
+\newline%
+\verb|datatype 'a queue = Queue of 'a list * 'a list;|\newline%
+\newline%
+\verb|val empty : 'a queue = Queue ([], []);|\newline%
+\newline%
+\verb|fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))|\newline%
+\verb| |\verb,|,\verb| dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys))|\newline%
+\verb| |\verb,|,\verb| dequeue (Queue (v :: va, [])) =|\newline%
+\verb| let|\newline%
+\verb| val y :: ys = rev (v :: va);|\newline%
+\verb| in|\newline%
+\verb| (SOME y, Queue ([], ys))|\newline%
+\verb| end;|\newline%
+\newline%
+\verb|fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated list of
+ constants for which code shall be generated; anything else needed for those
+ is added implicitly. Then follows a target language identifier
+ (\isa{SML}, \isa{OCaml} or \isa{Haskell}) and a freely chosen module name.
+ A file name denotes the destination to store the generated code. Note that
+ the semantics of the destination depends on the target language: for
+ \isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell}
+ it denotes a \emph{directory} where a file named as the module name
+ (with extension \isa{{\isachardot}hs}) is written:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
+\ empty\ dequeue\ enqueue\ \isakeyword{in}\ Haskell\isanewline
+\ \ \isakeyword{module{\isacharunderscore}name}\ Example\ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent This is how the corresponding code in \isa{Haskell} looks like:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|module Example where {|\newline%
+\newline%
+\newline%
+\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline%
+\verb|foldla f a [] = a;|\newline%
+\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline%
+\newline%
+\verb|rev :: forall a. [a] -> [a];|\newline%
+\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline%
+\newline%
+\verb|list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;|\newline%
+\verb|list_case f1 f2 (a : list) = f2 a list;|\newline%
+\verb|list_case f1 f2 [] = f1;|\newline%
+\newline%
+\verb|data Queue a = Queue [a] [a];|\newline%
+\newline%
+\verb|empty :: forall a. Queue a;|\newline%
+\verb|empty = Queue [] [];|\newline%
+\newline%
+\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
+\verb|dequeue (Queue [] []) = (Nothing, Queue [] []);|\newline%
+\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
+\verb|dequeue (Queue (v : va) []) =|\newline%
+\verb| let {|\newline%
+\verb| (y : ys) = rev (v : va);|\newline%
+\verb| } in (Just y, Queue [] ys);|\newline%
+\newline%
+\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline%
+\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline%
+\newline%
+\verb|}|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent This demonstrates the basic usage of the \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command;
+ for more details see \secref{sec:further}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Code generator architecture \label{sec:concept}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+What you have seen so far should be already enough in a lot of cases. If you
+ are content with this, you can quit reading here. Anyway, in order to customise
+ and adapt the code generator, it is inevitable to gain some understanding
+ how it works.
+
+ \begin{figure}[h]
+ \centering
+ \includegraphics[width=0.7\textwidth]{codegen_process}
+ \caption{Code generator architecture}
+ \label{fig:arch}
+ \end{figure}
+
+ The code generator employs a notion of executability
+ for three foundational executable ingredients known
+ from functional programming:
+ \emph{defining equations}, \emph{datatypes}, and
+ \emph{type classes}. A defining equation as a first approximation
+ is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t}
+ (an equation headed by a constant \isa{f} with arguments
+ \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}).
+ Code generation aims to turn defining equations
+ into a functional program. This is achieved by three major
+ components which operate sequentially, i.e. the result of one is
+ the input
+ of the next in the chain, see diagram \ref{fig:arch}:
+
+ \begin{itemize}
+
+ \item Out of the vast collection of theorems proven in a
+ \qn{theory}, a reasonable subset modelling
+ defining equations is \qn{selected}.
+
+ \item On those selected theorems, certain
+ transformations are carried out
+ (\qn{preprocessing}). Their purpose is to turn theorems
+ representing non- or badly executable
+ specifications into equivalent but executable counterparts.
+ The result is a structured collection of \qn{code theorems}.
+
+ \item Before the selected defining equations are continued with,
+ they can be \qn{preprocessed}, i.e. subjected to theorem
+ transformations. This \qn{preprocessor} is an interface which
+ allows to apply
+ the full expressiveness of ML-based theorem transformations
+ to code generation; motivating examples are shown below, see
+ \secref{sec:preproc}.
+ The result of the preprocessing step is a structured collection
+ of defining equations.
+
+ \item These defining equations are \qn{translated} to a program
+ in an abstract intermediate language. Think of it as a kind
+ of \qt{Mini-Haskell} with four \qn{statements}: \isa{data}
+ (for datatypes), \isa{fun} (stemming from defining equations),
+ also \isa{class} and \isa{inst} (for type classes).
+
+ \item Finally, the abstract program is \qn{serialised} into concrete
+ source code of a target language.
+
+ \end{itemize}
+
+ \noindent From these steps, only the two last are carried out outside the logic; by
+ keeping this layer as thin as possible, the amount of code to trust is
+ kept to a minimum.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/ML.tex Wed Oct 01 13:33:54 2008 +0200
@@ -0,0 +1,255 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{ML}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
+\isakeyword{imports}\ Setup\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{ML system interfaces \label{sec:ml}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Since the code generator framework not only aims to provide
+ a nice Isar interface but also to form a base for
+ code-generation-based applications, here a short
+ description of the most important ML interfaces.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Executable theory content: \isa{Code}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This Pure module implements the core notions of
+ executable content of a theory.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Managing executable content%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
+ \indexml{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
+ \indexml{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory| \\
+ \indexml{Code.map\_pre}\verb|Code.map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
+ \indexml{Code.map\_post}\verb|Code.map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory| \\
+ \indexml{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
+\verb| -> theory -> theory| \\
+ \indexml{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\
+ \indexml{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
+ \indexml{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline%
+\verb| -> (string * sort) list * (string * typ list) list| \\
+ \indexml{Code.get\_datatype\_of\_constr}\verb|Code.get_datatype_of_constr: theory -> string -> string option|
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
+ theorem \isa{thm} to executable content.
+
+ \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
+ theorem \isa{thm} from executable content, if present.
+
+ \item \verb|Code.add_eqnl|~\isa{{\isacharparenleft}const{\isacharcomma}\ lthms{\isacharparenright}}~\isa{thy} adds
+ suspended defining equations \isa{lthms} for constant
+ \isa{const} to executable content.
+
+ \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes
+ the preprocessor simpset.
+
+ \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
+ function transformer \isa{f} (named \isa{name}) to executable content;
+ \isa{f} is a transformer of the defining equations belonging
+ to a certain function definition, depending on the
+ current theory context. Returning \isa{NONE} indicates that no
+ transformation took place; otherwise, the whole process will be iterated
+ with the new defining equations.
+
+ \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes
+ function transformer named \isa{name} from executable content.
+
+ \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
+ a datatype to executable content, with generation
+ set \isa{cs}.
+
+ \item \verb|Code.get_datatype_of_constr|~\isa{thy}~\isa{const}
+ returns type constructor corresponding to
+ constructor \isa{const}; returns \isa{NONE}
+ if \isa{const} is no constructor.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Auxiliary%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\
+ \indexml{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\
+ \indexml{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: MetaSimplifier.simpset -> thm -> thm| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s}
+ reads a constant as a concrete term expression \isa{s}.
+
+ \item \verb|Code_Unit.head_eqn|~\isa{thy}~\isa{thm}
+ extracts the constant and its type from a defining equation \isa{thm}.
+
+ \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm}
+ rewrites a defining equation \isa{thm} with a simpset \isa{ss};
+ only arguments and right hand side are rewritten,
+ not the head of the defining equation.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Implementing code generator applications%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Implementing code generator applications on top
+ of the framework set out so far usually not only
+ involves using those primitive interfaces
+ but also storing code-dependent data and various
+ other things.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Data depending on the theory's executable content%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Due to incrementality of code generation, changes in the
+ theory's executable content have to be propagated in a
+ certain fashion. Additionally, such changes may occur
+ not only during theory extension but also during theory
+ merge, which is a little bit nasty from an implementation
+ point of view. The framework provides a solution
+ to this technical challenge by providing a functorial
+ data slot \verb|CodeDataFun|; on instantiation
+ of this functor, the following types and operations
+ are required:
+
+ \medskip
+ \begin{tabular}{l}
+ \isa{type\ T} \\
+ \isa{val\ empty{\isacharcolon}\ T} \\
+ \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodeUnit{\isachardot}const\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
+ \end{tabular}
+
+ \begin{description}
+
+ \item \isa{T} the type of data to store.
+
+ \item \isa{empty} initial (empty) data.
+
+ \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
+ \isa{consts} indicates the kind
+ of change: \verb|NONE| stands for a fundamental change
+ which invalidates any existing code, \isa{SOME\ consts}
+ hints that executable content for constants \isa{consts}
+ has changed.
+
+ \end{description}
+
+ \noindent An instance of \verb|CodeDataFun| provides the following
+ interface:
+
+ \medskip
+ \begin{tabular}{l}
+ \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
+ \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
+ \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
+ \end{tabular}
+
+ \begin{description}
+
+ \item \isa{get} retrieval of the current data.
+
+ \item \isa{change} update of current data (cached!)
+ by giving a continuation.
+
+ \item \isa{change{\isacharunderscore}yield} update with side result.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\bigskip
+
+ \emph{Happy proving, happy hacking!}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex Wed Oct 01 13:33:54 2008 +0200
@@ -0,0 +1,1127 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Program}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ Program\isanewline
+\isakeyword{imports}\ Introduction\isanewline
+\isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupsection{Turning Theories into Programs \label{sec:program}%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+We have already seen how by default equations stemming from
+ \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
+ statements are used for code generation. This default behaviour
+ can be changed, e.g. by providing different defining equations.
+ All kinds of customization shown in this section is \emph{safe}
+ in the sense that the user does not have to worry about
+ correctness -- all programs generatable that way are partially
+ correct.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Selecting code equations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Coming back to our introductory example, we
+ could provide an alternative defining equations for \isa{dequeue}
+ explicitly:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent The annotation \isa{{\isacharbrackleft}code\ func{\isacharbrackright}} is an \isa{Isar}
+ \isa{attribute} which states that the given theorems should be
+ considered as defining equations for a \isa{fun} statement --
+ the corresponding constant is determined syntactically. The resulting code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|module Example where {|\newline%
+\newline%
+\newline%
+\verb|foldla :: forall a b. (a -> b -> a) -> a -> [b] -> a;|\newline%
+\verb|foldla f a [] = a;|\newline%
+\verb|foldla f a (x : xs) = foldla f (f a x) xs;|\newline%
+\newline%
+\verb|rev :: forall a. [a] -> [a];|\newline%
+\verb|rev xs = foldla (\ xsa x -> x : xsa) [] xs;|\newline%
+\newline%
+\verb|nulla :: forall a. [a] -> Bool;|\newline%
+\verb|nulla (x : xs) = False;|\newline%
+\verb|nulla [] = True;|\newline%
+\newline%
+\verb|data Queue a = Queue [a] [a];|\newline%
+\newline%
+\verb|empty :: forall a. Queue a;|\newline%
+\verb|empty = Queue [] [];|\newline%
+\newline%
+\verb|dequeue :: forall a. Queue a -> (Maybe a, Queue a);|\newline%
+\verb|dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);|\newline%
+\verb|dequeue (Queue xs []) =|\newline%
+\verb| (if nulla xs then (Nothing, Queue [] [])|\newline%
+\verb| else dequeue (Queue [] (rev xs)));|\newline%
+\newline%
+\verb|enqueue :: forall a. a -> Queue a -> Queue a;|\newline%
+\verb|enqueue x (Queue xs ys) = Queue (x : xs) ys;|\newline%
+\newline%
+\verb|}|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
+ replaced by the predicate \isa{null\ xs}. This is due to the default
+ setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
+
+ Changing the default constructor set of datatypes is also
+ possible but rarely desired in practice. See \secref{sec:datatypes} for an example.
+
+ As told in \secref{sec:concept}, code generation is based
+ on a structured collection of code theorems.
+ For explorative purpose, this collection
+ may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
+\ dequeue%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent prints a table with \emph{all} defining equations
+ for \isa{dequeue}, including
+ \emph{all} defining equations those equations depend
+ on recursively.
+
+ Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
+ visualising dependencies between defining equations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{\isa{class} and \isa{instantiation}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Concerning type classes and code generation, let us examine an example
+ from abstract algebra:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{class}\isamarkupfalse%
+\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{class}\isamarkupfalse%
+\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
+\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instantiation}\isamarkupfalse%
+\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
+\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{fix}\isamarkupfalse%
+\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
+\ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
+\isacommand{qed}\isamarkupfalse%
+\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent We define the natural operation of the natural numbers
+ on monoids:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{primrec}\isamarkupfalse%
+\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent This we use to define the discrete exponentiation function:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{definition}\isamarkupfalse%
+\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent The corresponding code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|module Example where {|\newline%
+\newline%
+\newline%
+\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|class Semigroup a where {|\newline%
+\verb| mult :: a -> a -> a;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|class (Semigroup a) => Monoid a where {|\newline%
+\verb| neutral :: a;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
+\verb|pow (Suc n) a = mult a (pow n a);|\newline%
+\verb|pow Zero_nat a = neutral;|\newline%
+\newline%
+\verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
+\verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
+\verb|plus_nat Zero_nat n = n;|\newline%
+\newline%
+\verb|neutral_nat :: Nat;|\newline%
+\verb|neutral_nat = Suc Zero_nat;|\newline%
+\newline%
+\verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
+\verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
+\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
+\newline%
+\verb|instance Semigroup Nat where {|\newline%
+\verb| mult = mult_nat;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|instance Monoid Nat where {|\newline%
+\verb| neutral = neutral_nat;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|bexp :: Nat -> Nat;|\newline%
+\verb|bexp n = pow n (Suc (Suc Zero_nat));|\newline%
+\newline%
+\verb|}|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent This is a convenient place to show how explicit dictionary construction
+ manifests in generated code (here, the same example in \isa{SML}):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
+\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
+\newline%
+\verb|type 'a monoid = {Program__semigroup_monoid : 'a semigroup, neutral : 'a};|\newline%
+\verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
+\verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
+\newline%
+\verb|fun pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a)|\newline%
+\verb| |\verb,|,\verb| pow A_ Zero_nat a = neutral A_;|\newline%
+\newline%
+\verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
+\verb| |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
+\newline%
+\verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
+\newline%
+\verb|fun mult_nat (Suc m) n = plus_nat n (mult_nat m n)|\newline%
+\verb| |\verb,|,\verb| mult_nat Zero_nat n = Zero_nat;|\newline%
+\newline%
+\verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
+\newline%
+\verb|val monoid_nat =|\newline%
+\verb| {Program__semigroup_monoid = semigroup_nat, neutral = neutral_nat} :|\newline%
+\verb| nat monoid;|\newline%
+\newline%
+\verb|fun bexp n = pow monoid_nat n (Suc (Suc Zero_nat));|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Note the parameters with trailing underscore (\verb|A_|)
+ which are the dictionary parameters.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The preprocessor \label{sec:preproc}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Before selected function theorems are turned into abstract
+ code, a chain of definitional transformation steps is carried
+ out: \emph{preprocessing}. In essence, the preprocessor
+ consists of two components: a \emph{simpset} and \emph{function transformers}.
+
+ The \emph{simpset} allows to employ the full generality of the Isabelle
+ simplifier. Due to the interpretation of theorems
+ as defining equations, rewrites are applied to the right
+ hand side and the arguments of the left hand side of an
+ equation, but never to the constant heading the left hand side.
+ An important special case are \emph{inline theorems} which may be
+ declared and undeclared using the
+ \emph{code inline} or \emph{code inline del} attribute respectively.
+
+ Some common applications:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{itemize}
+%
+\begin{isamarkuptext}%
+\item replacing non-executable constructs by executable ones:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\item eliminating superfluous constants:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\item replacing executable but inconvenient constructs:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\end{itemize}
+%
+\begin{isamarkuptext}%
+\noindent \emph{Function transformers} provide a very general interface,
+ transforming a list of function theorems to another
+ list of function theorems, provided that neither the heading
+ constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
+ pattern elimination implemented in
+ theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
+ interface.
+
+ \noindent The current setup of the preprocessor may be inspected using
+ the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+ \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
+ mechanism to inspect the impact of a preprocessor setup
+ on defining equations.
+
+ \begin{warn}
+ The attribute \emph{code unfold}
+ associated with the \isa{SML\ code\ generator} also applies to
+ the \isa{generic\ code\ generator}:
+ \emph{code unfold} implies \emph{code inline}.
+ \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Datatypes \label{sec:datatypes}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Conceptually, any datatype is spanned by a set of
+ \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
+ where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all}
+ type variables in \isa{{\isasymtau}}. The HOL datatype package
+ by default registers any new datatype in the table
+ of datatypes, which may be inspected using
+ the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+
+ In some cases, it may be convenient to alter or
+ extend this table; as an example, we will develop an alternative
+ representation of natural numbers as binary digits, whose
+ size does increase logarithmically with its value, not linear
+ \footnote{Indeed, the \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}} theory (see \ref{eff_nat})
+ does something similar}. First, the digit representation:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{definition}\isamarkupfalse%
+\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent We will use these two \qt{digits} to represent natural numbers
+ in binary digits, e.g.:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Of course we also have to provide proper code equations for
+ the operations, e.g. \isa{op\ {\isacharplus}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
+ \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
+ datatype constructors:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent For the former constructor \isa{Suc}, we provide a code
+ equation and remove some parts of the default code generator setup
+ which are an obstacle here:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent This yields the following code:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|datatype nat = Dig1 of nat |\verb,|,\verb| Dig0 of nat |\verb,|,\verb| One_nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat)|\newline%
+\verb| |\verb,|,\verb| plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n)|\newline%
+\verb| |\verb,|,\verb| plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n)|\newline%
+\verb| |\verb,|,\verb| plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n)|\newline%
+\verb| |\verb,|,\verb| plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat)|\newline%
+\verb| |\verb,|,\verb| plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat)|\newline%
+\verb| |\verb,|,\verb| plus_nat (Dig0 m) One_nat = Dig1 m|\newline%
+\verb| |\verb,|,\verb| plus_nat One_nat (Dig0 n) = Dig1 n|\newline%
+\verb| |\verb,|,\verb| plus_nat m Zero_nat = m|\newline%
+\verb| |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent From this example, it can be easily glimpsed that using own constructor sets
+ is a little delicate since it changes the set of valid patterns for values
+ of that type. Without going into much detail, here some practical hints:
+
+ \begin{itemize}
+ \item When changing the constructor set for datatypes, take care to
+ provide an alternative for the \isa{case} combinator (e.g.~by replacing
+ it using the preprocessor).
+ \item Values in the target language need not to be normalised -- different
+ values in the target language may represent the same value in the
+ logic (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}).
+ \item Usually, a good methodology to deal with the subtleties of pattern
+ matching is to see the type as an abstract type: provide a set
+ of operations which operate on the concrete representation of the type,
+ and derive further operations by combinations of these primitive ones,
+ without relying on a particular representation.
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
+\isacommand{declare}\isamarkupfalse%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ simp%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\isamarkupsubsection{Equality and wellsortedness%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Surely you have already noticed how equality is treated
+ by the code generator:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{primrec}\isamarkupfalse%
+\ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
+\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
+\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
+\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
+\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent The membership test during preprocessing is rewritten,
+ resulting in \isa{op\ mem}, which itself
+ performs an explicit equality check.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
+\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
+\newline%
+\verb|fun eqop A_ a b = eq A_ a b;|\newline%
+\newline%
+\verb|fun member A_ x (y :: ys) = (if eqop A_ y x then true else member A_ x ys)|\newline%
+\verb| |\verb,|,\verb| member A_ x [] = false;|\newline%
+\newline%
+\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
+\verb| (if member A_ z xs|\newline%
+\verb| then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
+\verb| else collect_duplicates A_ xs (z :: ys) zs)|\newline%
+\verb| else collect_duplicates A_ (z :: xs) (z :: ys) zs)|\newline%
+\verb| |\verb,|,\verb| collect_duplicates A_ xs ys [] = xs;|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Obviously, polymorphic equality is implemented the Haskell
+ way using a type class. How is this achieved? HOL introduces
+ an explicit class \isa{eq} with a corresponding operation
+ \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
+ The preprocessing framework does the rest by propagating the
+ \isa{eq} constraints through all dependent defining equations.
+ For datatypes, instances of \isa{eq} are implicitly derived
+ when possible. For other types, you may instantiate \isa{eq}
+ manually like any other type class.
+
+ Though this \isa{eq} class is designed to get rarely in
+ the way, a subtlety
+ enters the stage when definitions of overloaded constants
+ are dependent on operational equality. For example, let
+ us define a lexicographic ordering on tuples
+ (also see theory \hyperlink{theory.Product-ord}{\mbox{\isa{Product{\isacharunderscore}ord}}}):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{instantiation}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}order{\isacharcomma}\ order{\isacharparenright}\ order\isanewline
+\isakeyword{begin}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{instance}\isamarkupfalse%
+\ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\isacommand{qed}\isamarkupfalse%
+\ {\isacharparenleft}auto\ simp{\isacharcolon}\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}prod{\isacharunderscore}def\ intro{\isacharcolon}\ order{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}\isanewline
+\isanewline
+\isacommand{end}\isamarkupfalse%
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ order{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
+\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
+\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Then code generation will fail. Why? The definition
+ of \isa{op\ {\isasymle}} depends on equality on both arguments,
+ which are polymorphic and impose an additional \isa{eq}
+ class constraint, which the preprocessor does not propagate
+ (for technical reasons).
+
+ The solution is to add \isa{eq} explicitly to the first sort arguments in the
+ code theorems:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
+\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
+\ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharparenright}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Then code generation succeeds:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
+\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
+\newline%
+\verb|type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};|\newline%
+\verb|fun less_eq (A_:'a ord) = #less_eq A_;|\newline%
+\verb|fun less (A_:'a ord) = #less A_;|\newline%
+\newline%
+\verb|fun eqop A_ a b = eq A_ a b;|\newline%
+\newline%
+\verb|type 'a preorder = {Orderings__ord_preorder : 'a ord};|\newline%
+\verb|fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;|\newline%
+\newline%
+\verb|type 'a order = {Orderings__preorder_order : 'a preorder};|\newline%
+\verb|fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;|\newline%
+\newline%
+\verb|fun less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline%
+\verb| less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline%
+\verb| eqop A1_ x1 x2 andalso|\newline%
+\verb| less_eq ((ord_preorder o preorder_order) B_) y1 y2|\newline%
+\verb| |\verb,|,\verb| less_eqa (A1_, A2_) B_ (x1, y1) (x2, y2) =|\newline%
+\verb| less ((ord_preorder o preorder_order) A2_) x1 x2 orelse|\newline%
+\verb| eqop A1_ x1 x2 andalso|\newline%
+\verb| less_eq ((ord_preorder o preorder_order) B_) y1 y2;|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+In some cases, the automatically derived defining equations
+ for equality on a particular type may not be appropriate.
+ As example, watch the following datatype representing
+ monomorphic parametric types (where type constructors
+ are referred to by natural numbers):%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{datatype}\isamarkupfalse%
+\ monotype\ {\isacharequal}\ Mono\ nat\ {\isachardoublequoteopen}monotype\ list{\isachardoublequoteclose}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Then code generation for SML would fail with a message
+ that the generated code contains illegal mutual dependencies:
+ the theorem \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}} already requires the
+ instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
+ \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}}; Haskell has no problem with mutually
+ recursive \isa{inst} and \isa{fun} definitions,
+ but the SML serializer does not support this.
+
+ In such cases, you have to provide your own equality equations
+ involving auxiliary constants. In our case,
+ \isa{list{\isacharunderscore}all{\isadigit{2}}} can do the job:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{lemma}\isamarkupfalse%
+\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
+\ \ \ \ \ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent does not depend on instance \isa{monotype\ {\isasymColon}\ eq}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
+\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
+\newline%
+\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|fun eqop A_ a b = eq A_ a b;|\newline%
+\newline%
+\verb|fun null (x :: xs) = false|\newline%
+\verb| |\verb,|,\verb| null [] = true;|\newline%
+\newline%
+\verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
+\verb| |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
+\verb| |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline%
+\verb| |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline%
+\newline%
+\verb|val eq_nata = {eq = eq_nat} : nat eq;|\newline%
+\newline%
+\verb|datatype monotype = Mono of nat * monotype list;|\newline%
+\newline%
+\verb|fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys|\newline%
+\verb| |\verb,|,\verb| list_all2 p xs [] = null xs|\newline%
+\verb| |\verb,|,\verb| list_all2 p [] ys = null ys;|\newline%
+\newline%
+\verb|fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =|\newline%
+\verb| eqop eq_nata tyco1 tyco2 andalso|\newline%
+\verb| list_all2 eq_monotype typargs1 typargs2;|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isamarkupsubsection{Partiality%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, examples: maps%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Wed Oct 01 12:18:18 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Wed Oct 01 13:33:54 2008 +0200
@@ -48,7 +48,7 @@
\maketitle
\begin{abstract}
- This tutorial gives am introduction to a generic code generator framework in Isabelle
+ This tutorial gives an introduction to a generic code generator framework in Isabelle
for generating executable code in functional programming languages from logical
specifications in Isabelle/HOL.
\end{abstract}