diff r a01de3b3fa2e r df77ed974a78 docsrc/IsarAdvanced/Codegen/Thy/Program.thy
 a/docsrc/IsarAdvanced/Codegen/Thy/Program.thy Wed Oct 01 12:18:18 2008 +0200
+++ b/docsrc/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 \ 'a\monoid \ 'a\monoid" where
+primrec %quoteme (in monoid) pow :: "nat \ 'a \ 'a" where
"pow 0 a = \"
 "pow (Suc n) a = a \ 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 [\ \<^bvec>\\s\<^isub>k\<^evec>]"}
 a \emph{shadow constant} @{text "f\<^isub>\ [\<^bvec>\\s\<^isub>k\<^evec>]"} is
 declared satisfying @{text "f [\ \<^bvec>\\s\<^isub>k\<^evec>] \ f\<^isub>\ [\<^bvec>\\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 [\ \<^bvec>\\s\<^isub>k\<^evec>]"} can be turned into
 defining equations for @{text "f\<^isub>\ [\<^bvec>\\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\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 + \ nat \ nat \ 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 \ 'a list \ 'a list \ 'a list" where
 "collect_duplicates xs ys [] = xs"
+primrec %quoteme collect_duplicates :: "'a list \ 'a list \ 'a list \ 'a list" where
+ "collect_duplicates xs ys [] = xs"
 "collect_duplicates xs ys (z#zs) = (if z \ set xs
then if z \ 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 \ (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 < y2))"
+ "x \ y \ fst x < fst y \ fst x = fst y \ snd x \ snd y"
definition %quoteme [code func del]:
 "p1 \ p2 \ (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \ (x1 = x2 \ y1 \ y2))"
+ "x < y \ fst x < fst y \ fst x = fst y \ 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 \ 'a\ord, y1 \ 'b\ord) < (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 < y2)"
 "(x1 \ 'a\ord, y1 \ 'b\ord) \ (x2, y2) \ x1 < x2 \ (x1 = x2 \ y1 \ y2)"
 unfolding less_prod_def less_eq_prod_def by simp_all
+lemma %quoteme order_prod [code func]:
+ "(x1 \ 'a\order, y1 \ 'b\order) < (x2, y2) \
+ x1 < x2 \ x1 = x2 \ y1 < y2"
+ "(x1 \ 'a\order, y1 \ 'b\order) \ (x2, y2) \
+ x1 < x2 \ x1 = x2 \ y1 \ 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 \"} 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 \ 'a\{ord, eq}, y1 \ 'b\ord) < (x2, y2) \
 x1 < x2 \ (x1 = x2 \ y1 < y2)"
 "(x1 \ 'a\{ord, eq}, y1 \ 'b\ord) \ (x2, y2) \
 x1 < x2 \ (x1 = x2 \ y1 \ y2)"
 unfolding ord_prod by rule+
+lemma %quoteme order_prod_code [code func]:
+ "(x1 \ 'a\{order, eq}, y1 \ 'b\order) < (x2, y2) \
+ x1 < x2 \ x1 = x2 \ y1 < y2"
+ "(x1 \ 'a\{order, eq}, y1 \ 'b\order) \ (x2, y2) \
+ x1 < x2 \ x1 = x2 \ y1 \ y2"
+ by (simp_all add: less_prod_def less_eq_prod_def)
text {*
\noindent Then code generation succeeds:
*}
text %quoteme {*@{code_stmts "op \ \ 'a\{eq, ord} \ 'b\ord \ 'a \ 'b \ bool" (SML)}*}
+text %quoteme {*@{code_stmts "op \ \ _ \ _ \ _ \ _ \ 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:
*}