doc-src/IsarAdvanced/Codegen/Thy/Program.thy

 
 section {* Turning Theories into Programs \label{sec:program} *}
 
 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 {*
   \noindent The annotation @{text "[code func]"} is an @{text Isar}
   @{text attribute} which states that the given theorems should be

 *}
 
 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:
 *}
 
 class %quoteme semigroup = type +
   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)

 text {*
   \noindent We define the natural operation of the natural numbers
   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"
 
 text {*
   \noindent This we use to define the discrete exponentiation function:

 *}
 
 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} *}
 
 text {*
   Before selected function theorems are turned into abstract

 text_raw {*
   \end{itemize}
 *}
 
 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}
   pattern elimination implemented in
   theory @{text Efficient_Nat} (see \secref{eff_nat}) uses this

   mechanism to inspect the impact of a preprocessor setup
   on defining equations.
 
   \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}
 *}
 
 subsection {* Datatypes \label{sec:datatypes} *}
 

 
 definition %quoteme  Dig1 :: "nat \<Rightarrow> nat" where
   "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.:
 *}
 
 lemma %quoteme 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
   by (simp add: Dig0_def Dig1_def)

 *}
 
 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:
 
   \begin{itemize}
     \item When changing the constructor set for datatypes, take care to

 text {*
   Surely you have already noticed how equality is treated
   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
         else collect_duplicates xs (z#ys) zs
       else collect_duplicates (z#xs) (z#ys) zs)"

 text {*
   \noindent Obviously, polymorphic equality is implemented the Haskell
   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.
 
   Though this @{text 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:
-*}
-
-instantiation %quoteme * :: (ord, ord) ord
+  us define a lexicographic ordering on tuples
+  (also see theory @{theory Product_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))"
-
-instance %quoteme ..
+  "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
+
+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
   for equality on a particular type may not be appropriate.
   As example, watch the following datatype representing

   instance @{text "monotype \<Colon> eq"}, which itself requires
   @{thm monotype_eq [no_vars]};  Haskell has no problem with mutually
   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:
 *}
 
 lemma %quoteme monotype_eq_list_all2 [code func]: