doc-src/IsarAdvanced/Codegen/Thy/Program.thy
changeset 28447 df77ed974a78
parent 28428 fd007794561f
child 28456 7a558c872104
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Wed Oct 01 12:18:18 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Wed Oct 01 13:33:54 2008 +0200
     1.3 @@ -6,20 +6,30 @@
     1.4  
     1.5  subsection {* The @{text "Isabelle/HOL"} default setup *}
     1.6  
     1.7 -subsection {* Selecting code equations *}
     1.8 -
     1.9  text {*
    1.10    We have already seen how by default equations stemming from
    1.11    @{command definition}/@{command primrec}/@{command fun}
    1.12 -  statements are used for code generation.  Deviating from this
    1.13 -  \emph{default} behaviour is always possible -- e.g.~we
    1.14 -  could provide an alternative @{text fun} for @{const dequeue} proving
    1.15 -  the following equations explicitly:
    1.16 +  statements are used for code generation.  This default behaviour
    1.17 +  can be changed, e.g. by providing different defining equations.
    1.18 +  All kinds of customization shown in this section is \emph{safe}
    1.19 +  in the sense that the user does not have to worry about
    1.20 +  correctness -- all programs generatable that way are partially
    1.21 +  correct.
    1.22 +*}
    1.23 +
    1.24 +subsection {* Selecting code equations *}
    1.25 +
    1.26 +text {*
    1.27 +  Coming back to our introductory example, we
    1.28 +  could provide an alternative defining equations for @{const dequeue}
    1.29 +  explicitly:
    1.30  *}
    1.31  
    1.32  lemma %quoteme [code func]:
    1.33 -  "dequeue (Queue xs []) = (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))"
    1.34 -  "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)"
    1.35 +  "dequeue (Queue xs []) =
    1.36 +     (if xs = [] then (None, Queue [] []) else dequeue (Queue [] (rev xs)))"
    1.37 +  "dequeue (Queue xs (y # ys)) =
    1.38 +     (Some y, Queue xs ys)"
    1.39    by (cases xs, simp_all) (cases "rev xs", simp_all)
    1.40  
    1.41  text {*
    1.42 @@ -60,7 +70,7 @@
    1.43  subsection {* @{text class} and @{text instantiation} *}
    1.44  
    1.45  text {*
    1.46 -  Concerning type classes and code generation, let us again examine an example
    1.47 +  Concerning type classes and code generation, let us examine an example
    1.48    from abstract algebra:
    1.49  *}
    1.50  
    1.51 @@ -105,7 +115,7 @@
    1.52    on monoids:
    1.53  *}
    1.54  
    1.55 -primrec %quoteme pow :: "nat \<Rightarrow> 'a\<Colon>monoid \<Rightarrow> 'a\<Colon>monoid" where
    1.56 +primrec %quoteme (in monoid) pow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.57      "pow 0 a = \<one>"
    1.58    | "pow (Suc n) a = a \<otimes> pow n a"
    1.59  
    1.60 @@ -123,31 +133,16 @@
    1.61  text %quoteme {*@{code_stmts bexp (Haskell)}*}
    1.62  
    1.63  text {*
    1.64 -  \noindent An inspection reveals that the equations stemming from the
    1.65 -  @{command primrec} statement within instantiation of class
    1.66 -  @{class semigroup} with type @{typ nat} are mapped to a separate
    1.67 -  function declaration @{verbatim mult_nat} which in turn is used
    1.68 -  to provide the right hand side for the @{verbatim "instance Semigroup Nat"}.
    1.69 -  This perfectly
    1.70 -  agrees with the restriction that @{text inst} statements may
    1.71 -  only contain one single equation for each class class parameter
    1.72 -  The @{command instantiation} mechanism manages that for each
    1.73 -  overloaded constant @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}
    1.74 -  a \emph{shadow constant} @{text "f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"} is
    1.75 -  declared satisfying @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>] \<equiv> f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}.
    1.76 -  this equation is indeed the one used for the statement;
    1.77 -  using it as a rewrite rule, defining equations for 
    1.78 -  @{text "f [\<kappa> \<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"} can be turned into
    1.79 -  defining equations for @{text "f\<^isub>\<kappa> [\<^bvec>\<alpha>\<Colon>s\<^isub>k\<^evec>]"}.  This
    1.80 -  happens transparently, providing the illusion that class parameters
    1.81 -  can be instantiated with more than one equation.
    1.82 -
    1.83 -  This is a convenient place to show how explicit dictionary construction
    1.84 +  \noindent This is a convenient place to show how explicit dictionary construction
    1.85    manifests in generated code (here, the same example in @{text SML}):
    1.86  *}
    1.87  
    1.88  text %quoteme {*@{code_stmts bexp (SML)}*}
    1.89  
    1.90 +text {*
    1.91 +  \noindent Note the parameters with trailing underscore (@{verbatim "A_"})
    1.92 +    which are the dictionary parameters.
    1.93 +*}
    1.94  
    1.95  subsection {* The preprocessor \label{sec:preproc} *}
    1.96  
    1.97 @@ -199,7 +194,7 @@
    1.98  *}
    1.99  
   1.100  text {*
   1.101 -  \emph{Function transformers} provide a very general interface,
   1.102 +  \noindent \emph{Function transformers} provide a very general interface,
   1.103    transforming a list of function theorems to another
   1.104    list of function theorems, provided that neither the heading
   1.105    constant nor its type change.  The @{term "0\<Colon>nat"} / @{const Suc}
   1.106 @@ -215,8 +210,9 @@
   1.107  
   1.108    \begin{warn}
   1.109      The attribute \emph{code unfold}
   1.110 -    associated with the existing code generator also applies to
   1.111 -    the new one: \emph{code unfold} implies \emph{code inline}.
   1.112 +    associated with the @{text "SML code generator"} also applies to
   1.113 +    the @{text "generic code generator"}:
   1.114 +    \emph{code unfold} implies \emph{code inline}.
   1.115    \end{warn}
   1.116  *}
   1.117  
   1.118 @@ -246,7 +242,7 @@
   1.119    "Dig1 n = Suc (2 * n)"
   1.120  
   1.121  text {*
   1.122 -  \noindent We will use these two ">digits"< to represent natural numbers
   1.123 +  \noindent We will use these two \qt{digits} to represent natural numbers
   1.124    in binary digits, e.g.:
   1.125  *}
   1.126  
   1.127 @@ -299,9 +295,7 @@
   1.128  text %quoteme {*@{code_stmts "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (SML)}*}
   1.129  
   1.130  text {*
   1.131 -  \medskip
   1.132 -
   1.133 -  From this example, it can be easily glimpsed that using own constructor sets
   1.134 +  \noindent From this example, it can be easily glimpsed that using own constructor sets
   1.135    is a little delicate since it changes the set of valid patterns for values
   1.136    of that type.  Without going into much detail, here some practical hints:
   1.137  
   1.138 @@ -334,9 +328,8 @@
   1.139    by the code generator:
   1.140  *}
   1.141  
   1.142 -primrec %quoteme
   1.143 -  collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.144 -    "collect_duplicates xs ys [] = xs"
   1.145 +primrec %quoteme collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.146 +  "collect_duplicates xs ys [] = xs"
   1.147    | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
   1.148        then if z \<in> set ys
   1.149          then collect_duplicates xs ys zs
   1.150 @@ -356,7 +349,8 @@
   1.151    way using a type class.  How is this achieved?  HOL introduces
   1.152    an explicit class @{class eq} with a corresponding operation
   1.153    @{const eq_class.eq} such that @{thm eq [no_vars]}.
   1.154 -  The preprocessing framework does the rest.
   1.155 +  The preprocessing framework does the rest by propagating the
   1.156 +  @{class eq} constraints through all dependent defining equations.
   1.157    For datatypes, instances of @{class eq} are implicitly derived
   1.158    when possible.  For other types, you may instantiate @{text eq}
   1.159    manually like any other type class.
   1.160 @@ -365,50 +359,54 @@
   1.161    the way, a subtlety
   1.162    enters the stage when definitions of overloaded constants
   1.163    are dependent on operational equality.  For example, let
   1.164 -  us define a lexicographic ordering on tuples:
   1.165 +  us define a lexicographic ordering on tuples
   1.166 +  (also see theory @{theory Product_ord}):
   1.167  *}
   1.168  
   1.169 -instantiation %quoteme * :: (ord, ord) ord
   1.170 +instantiation %quoteme "*" :: (order, order) order
   1.171  begin
   1.172  
   1.173  definition %quoteme [code func del]:
   1.174 -  "p1 < p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 < y2))"
   1.175 +  "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
   1.176  
   1.177  definition %quoteme [code func del]:
   1.178 -  "p1 \<le> p2 \<longleftrightarrow> (let (x1, y1) = p1; (x2, y2) = p2 in x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2))"
   1.179 +  "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
   1.180  
   1.181 -instance %quoteme ..
   1.182 +instance %quoteme proof
   1.183 +qed (auto simp: less_eq_prod_def less_prod_def intro: order_less_trans)
   1.184  
   1.185  end %quoteme
   1.186  
   1.187 -lemma %quoteme ord_prod [code func]:
   1.188 -  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.189 -  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
   1.190 -  unfolding less_prod_def less_eq_prod_def by simp_all
   1.191 +lemma %quoteme order_prod [code func]:
   1.192 +  "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
   1.193 +     x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   1.194 +  "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
   1.195 +     x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   1.196 +  by (simp_all add: less_prod_def less_eq_prod_def)
   1.197  
   1.198  text {*
   1.199    \noindent Then code generation will fail.  Why?  The definition
   1.200    of @{term "op \<le>"} depends on equality on both arguments,
   1.201    which are polymorphic and impose an additional @{class eq}
   1.202 -  class constraint, which the preprocessort does not propagate for technical
   1.203 -  reasons.
   1.204 +  class constraint, which the preprocessor does not propagate
   1.205 +  (for technical reasons).
   1.206  
   1.207    The solution is to add @{class eq} explicitly to the first sort arguments in the
   1.208    code theorems:
   1.209  *}
   1.210  
   1.211 -lemma ord_prod_code [code func]:
   1.212 -  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow>
   1.213 -    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
   1.214 -  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow>
   1.215 -    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
   1.216 -  unfolding ord_prod by rule+
   1.217 +lemma %quoteme order_prod_code [code func]:
   1.218 +  "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
   1.219 +     x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   1.220 +  "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
   1.221 +     x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   1.222 +  by (simp_all add: less_prod_def less_eq_prod_def)
   1.223  
   1.224  text {*
   1.225    \noindent Then code generation succeeds:
   1.226  *}
   1.227  
   1.228 -text %quoteme {*@{code_stmts "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" (SML)}*}
   1.229 +text %quoteme {*@{code_stmts "op \<le> \<Colon> _ \<times> _ \<Rightarrow> _ \<times> _ \<Rightarrow> bool" (SML)}*}
   1.230  
   1.231  text {*
   1.232    In some cases, the automatically derived defining equations
   1.233 @@ -434,7 +432,7 @@
   1.234    recursive @{text inst} and @{text fun} definitions,
   1.235    but the SML serializer does not support this.
   1.236  
   1.237 -  In such cases, you have to provide you own equality equations
   1.238 +  In such cases, you have to provide your own equality equations
   1.239    involving auxiliary constants.  In our case,
   1.240    @{const [show_types] list_all2} can do the job:
   1.241  *}