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 *}