author | wenzelm |
Tue, 01 Nov 2016 01:20:33 +0100 | |
changeset 64439 | 2bafda87b524 |
parent 63680 | 6e1e8b5abbfa |
child 65041 | 2525e680f94f |
permissions | -rw-r--r-- |
28213 | 1 |
theory Further |
59378
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
2 |
imports Setup |
28213 | 3 |
begin |
4 |
||
59377 | 5 |
section \<open>Further issues \label{sec:further}\<close> |
28419 | 6 |
|
59377 | 7 |
subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close> |
42096 | 8 |
|
59377 | 9 |
text \<open> |
42096 | 10 |
@{text Scala} deviates from languages of the ML family in a couple |
11 |
of aspects; those which affect code generation mainly have to do with |
|
12 |
@{text Scala}'s type system: |
|
13 |
||
14 |
\begin{itemize} |
|
15 |
||
16 |
\item @{text Scala} prefers tupled syntax over curried syntax. |
|
17 |
||
18 |
\item @{text Scala} sacrifices Hindely-Milner type inference for a |
|
19 |
much more rich type system with subtyping etc. For this reason |
|
20 |
type arguments sometimes have to be given explicitly in square |
|
46520 | 21 |
brackets (mimicking System F syntax). |
42096 | 22 |
|
23 |
\item In contrast to @{text Haskell} where most specialities of |
|
24 |
the type system are implemented using \emph{type classes}, |
|
25 |
@{text Scala} provides a sophisticated system of \emph{implicit |
|
26 |
arguments}. |
|
27 |
||
28 |
\end{itemize} |
|
29 |
||
30 |
\noindent Concerning currying, the @{text Scala} serializer counts |
|
31 |
arguments in code equations to determine how many arguments |
|
32 |
shall be tupled; remaining arguments and abstractions in terms |
|
33 |
rather than function definitions are always curried. |
|
34 |
||
35 |
The second aspect affects user-defined adaptations with @{command |
|
55372 | 36 |
code_printing}. For regular terms, the @{text Scala} serializer prints |
42096 | 37 |
all type arguments explicitly. For user-defined term adaptations |
38 |
this is only possible for adaptations which take no arguments: here |
|
39 |
the type arguments are just appended. Otherwise they are ignored; |
|
40 |
hence user-defined adaptations for polymorphic constants have to be |
|
41 |
designed very carefully to avoid ambiguity. |
|
59377 | 42 |
\<close> |
42096 | 43 |
|
44 |
||
59377 | 45 |
subsection \<open>Modules namespace\<close> |
28419 | 46 |
|
59377 | 47 |
text \<open> |
40752 | 48 |
When invoking the @{command export_code} command it is possible to |
49 |
leave out the @{keyword "module_name"} part; then code is |
|
50 |
distributed over different modules, where the module name space |
|
51 |
roughly is induced by the Isabelle theory name space. |
|
38437 | 52 |
|
40752 | 53 |
Then sometimes the awkward situation occurs that dependencies |
54 |
between definitions introduce cyclic dependencies between modules, |
|
55 |
which in the @{text Haskell} world leaves you to the mercy of the |
|
56 |
@{text Haskell} implementation you are using, while for @{text |
|
57 |
SML}/@{text OCaml} code generation is not possible. |
|
38437 | 58 |
|
40752 | 59 |
A solution is to declare module names explicitly. Let use assume |
60 |
the three cyclically dependent modules are named \emph{A}, \emph{B} |
|
61 |
and \emph{C}. Then, by stating |
|
59377 | 62 |
\<close> |
38437 | 63 |
|
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51717
diff
changeset
|
64 |
code_identifier %quote |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51717
diff
changeset
|
65 |
code_module A \<rightharpoonup> (SML) ABC |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51717
diff
changeset
|
66 |
| code_module B \<rightharpoonup> (SML) ABC |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51717
diff
changeset
|
67 |
| code_module C \<rightharpoonup> (SML) ABC |
38437 | 68 |
|
59377 | 69 |
text \<open> |
40752 | 70 |
\noindent we explicitly map all those modules on \emph{ABC}, |
71 |
resulting in an ad-hoc merge of this three modules at serialisation |
|
72 |
time. |
|
59377 | 73 |
\<close> |
28419 | 74 |
|
59377 | 75 |
subsection \<open>Locales and interpretation\<close> |
37426 | 76 |
|
59377 | 77 |
text \<open> |
37426 | 78 |
A technical issue comes to surface when generating code from |
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61779
diff
changeset
|
79 |
specifications stemming from locale interpretation into global |
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61779
diff
changeset
|
80 |
theories. |
37426 | 81 |
|
40752 | 82 |
Let us assume a locale specifying a power operation on arbitrary |
83 |
types: |
|
59377 | 84 |
\<close> |
37426 | 85 |
|
86 |
locale %quote power = |
|
87 |
fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
88 |
assumes power_commute: "power x \<circ> power y = power y \<circ> power x" |
|
89 |
begin |
|
90 |
||
59377 | 91 |
text \<open> |
40752 | 92 |
\noindent Inside that locale we can lift @{text power} to exponent |
61779 | 93 |
lists by means of a specification relative to that locale: |
59377 | 94 |
\<close> |
37426 | 95 |
|
96 |
primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where |
|
97 |
"powers [] = id" |
|
98 |
| "powers (x # xs) = power x \<circ> powers xs" |
|
99 |
||
100 |
lemma %quote powers_append: |
|
101 |
"powers (xs @ ys) = powers xs \<circ> powers ys" |
|
102 |
by (induct xs) simp_all |
|
103 |
||
104 |
lemma %quote powers_power: |
|
105 |
"powers xs \<circ> power x = power x \<circ> powers xs" |
|
106 |
by (induct xs) |
|
49739 | 107 |
(simp_all del: o_apply id_apply add: comp_assoc, |
37426 | 108 |
simp del: o_apply add: o_assoc power_commute) |
109 |
||
110 |
lemma %quote powers_rev: |
|
111 |
"powers (rev xs) = powers xs" |
|
112 |
by (induct xs) (simp_all add: powers_append powers_power) |
|
113 |
||
114 |
end %quote |
|
115 |
||
59377 | 116 |
text \<open> |
38505 | 117 |
After an interpretation of this locale (say, @{command_def |
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61779
diff
changeset
|
118 |
global_interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f |
61779 | 119 |
:: 'a \<Rightarrow> 'a). f ^^ n)"}), one could naively expect to have a constant @{text |
37426 | 120 |
"fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code |
121 |
can be generated. But this not the case: internally, the term |
|
122 |
@{text "fun_power.powers"} is an abbreviation for the foundational |
|
123 |
term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"} |
|
58620 | 124 |
(see @{cite "isabelle-locale"} for the details behind). |
37426 | 125 |
|
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61779
diff
changeset
|
126 |
Fortunately, a succint solution is available: a dedicated |
61779 | 127 |
rewrite definition: |
59377 | 128 |
\<close> |
37426 | 129 |
|
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61779
diff
changeset
|
130 |
global_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" |
61779 | 131 |
defines funpows = fun_power.powers |
132 |
by unfold_locales |
|
133 |
(simp_all add: fun_eq_iff funpow_mult mult.commute) |
|
37426 | 134 |
|
59377 | 135 |
text \<open> |
61779 | 136 |
\noindent This amends the interpretation morphisms such that |
137 |
occurrences of the foundational term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"} |
|
138 |
are folded to a newly defined constant @{const funpows}. |
|
37426 | 139 |
|
140 |
After this setup procedure, code generation can continue as usual: |
|
59377 | 141 |
\<close> |
37426 | 142 |
|
59377 | 143 |
text %quotetypewriter \<open> |
39683 | 144 |
@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)} |
61779 | 145 |
\<close> |
37426 | 146 |
|
147 |
||
59377 | 148 |
subsection \<open>Parallel computation\<close> |
51172 | 149 |
|
59377 | 150 |
text \<open> |
63680 | 151 |
Theory @{text Parallel} in \<^dir>\<open>~~/src/HOL/Library\<close> contains |
51172 | 152 |
operations to exploit parallelism inside the Isabelle/ML |
153 |
runtime engine. |
|
59377 | 154 |
\<close> |
51172 | 155 |
|
59377 | 156 |
subsection \<open>Imperative data structures\<close> |
28419 | 157 |
|
59377 | 158 |
text \<open> |
38437 | 159 |
If you consider imperative data structures as inevitable for a |
160 |
specific application, you should consider \emph{Imperative |
|
161 |
Functional Programming with Isabelle/HOL} |
|
58620 | 162 |
@{cite "bulwahn-et-al:2008:imperative"}; the framework described there |
40752 | 163 |
is available in session @{text Imperative_HOL}, together with a |
164 |
short primer document. |
|
59377 | 165 |
\<close> |
28419 | 166 |
|
28213 | 167 |
|
59377 | 168 |
subsection \<open>ML system interfaces \label{sec:ml}\<close> |
38405 | 169 |
|
59377 | 170 |
text \<open> |
38510 | 171 |
Since the code generator framework not only aims to provide a nice |
172 |
Isar interface but also to form a base for code-generation-based |
|
173 |
applications, here a short description of the most fundamental ML |
|
174 |
interfaces. |
|
59377 | 175 |
\<close> |
38405 | 176 |
|
59377 | 177 |
subsubsection \<open>Managing executable content\<close> |
38405 | 178 |
|
59377 | 179 |
text %mlref \<open> |
38405 | 180 |
\begin{mldecls} |
38510 | 181 |
@{index_ML Code.read_const: "theory -> string -> string"} \\ |
63239
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
61891
diff
changeset
|
182 |
@{index_ML Code.add_eqn: "Code.kind * bool -> thm -> theory -> theory"} \\ |
38405 | 183 |
@{index_ML Code.del_eqn: "thm -> theory -> theory"} \\ |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51172
diff
changeset
|
184 |
@{index_ML Code_Preproc.map_pre: "(Proof.context -> Proof.context) -> theory -> theory"} \\ |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51172
diff
changeset
|
185 |
@{index_ML Code_Preproc.map_post: "(Proof.context -> Proof.context) -> theory -> theory"} \\ |
38507 | 186 |
@{index_ML Code_Preproc.add_functrans: " |
55757 | 187 |
string * (Proof.context -> (thm * bool) list -> (thm * bool) list option) |
38507 | 188 |
-> theory -> theory"} \\ |
38405 | 189 |
@{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\ |
190 |
@{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\ |
|
191 |
@{index_ML Code.get_type: "theory -> string |
|
40752 | 192 |
-> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool"} \\ |
38405 | 193 |
@{index_ML Code.get_type_of_constr_or_abstr: "theory -> string -> (string * bool) option"} |
194 |
\end{mldecls} |
|
195 |
||
196 |
\begin{description} |
|
197 |
||
38510 | 198 |
\item @{ML Code.read_const}~@{text thy}~@{text s} |
199 |
reads a constant as a concrete term expression @{text s}. |
|
200 |
||
63239
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
61891
diff
changeset
|
201 |
\item @{ML Code.add_eqn}~@{text "(kind, default)"}~@{text "thm"}~@{text "thy"} adds code equation |
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
61891
diff
changeset
|
202 |
@{text "thm"} to executable content. |
38405 | 203 |
|
63239
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
61891
diff
changeset
|
204 |
\item @{ML Code.del_eqn}~@{text "thm"}~@{text "thy"} removes code equation |
d562c9948dee
explicit tagging of code equations de-baroquifies interface
haftmann
parents:
61891
diff
changeset
|
205 |
@{text "thm"} from executable content, if present. |
38405 | 206 |
|
207 |
\item @{ML Code_Preproc.map_pre}~@{text "f"}~@{text "thy"} changes |
|
208 |
the preprocessor simpset. |
|
209 |
||
210 |
\item @{ML Code_Preproc.add_functrans}~@{text "(name, f)"}~@{text "thy"} adds |
|
211 |
function transformer @{text f} (named @{text name}) to executable content; |
|
212 |
@{text f} is a transformer of the code equations belonging |
|
213 |
to a certain function definition, depending on the |
|
214 |
current theory context. Returning @{text NONE} indicates that no |
|
215 |
transformation took place; otherwise, the whole process will be iterated |
|
216 |
with the new code equations. |
|
217 |
||
218 |
\item @{ML Code_Preproc.del_functrans}~@{text "name"}~@{text "thy"} removes |
|
219 |
function transformer named @{text name} from executable content. |
|
220 |
||
221 |
\item @{ML Code.add_datatype}~@{text cs}~@{text thy} adds |
|
222 |
a datatype to executable content, with generation |
|
223 |
set @{text cs}. |
|
224 |
||
225 |
\item @{ML Code.get_type_of_constr_or_abstr}~@{text "thy"}~@{text "const"} |
|
226 |
returns type constructor corresponding to |
|
227 |
constructor @{text const}; returns @{text NONE} |
|
228 |
if @{text const} is no constructor. |
|
229 |
||
230 |
\end{description} |
|
59377 | 231 |
\<close> |
38405 | 232 |
|
233 |
||
59377 | 234 |
subsubsection \<open>Data depending on the theory's executable content\<close> |
38405 | 235 |
|
59377 | 236 |
text \<open> |
40752 | 237 |
Implementing code generator applications on top of the framework set |
238 |
out so far usually not only involves using those primitive |
|
239 |
interfaces but also storing code-dependent data and various other |
|
240 |
things. |
|
38405 | 241 |
|
40752 | 242 |
Due to incrementality of code generation, changes in the theory's |
243 |
executable content have to be propagated in a certain fashion. |
|
244 |
Additionally, such changes may occur not only during theory |
|
245 |
extension but also during theory merge, which is a little bit nasty |
|
246 |
from an implementation point of view. The framework provides a |
|
247 |
solution to this technical challenge by providing a functorial data |
|
248 |
slot @{ML_functor Code_Data}; on instantiation of this functor, the |
|
249 |
following types and operations are required: |
|
38405 | 250 |
|
251 |
\medskip |
|
252 |
\begin{tabular}{l} |
|
253 |
@{text "type T"} \\ |
|
254 |
@{text "val empty: T"} \\ |
|
255 |
\end{tabular} |
|
256 |
||
257 |
\begin{description} |
|
258 |
||
259 |
\item @{text T} the type of data to store. |
|
260 |
||
261 |
\item @{text empty} initial (empty) data. |
|
262 |
||
263 |
\end{description} |
|
264 |
||
40752 | 265 |
\noindent An instance of @{ML_functor Code_Data} provides the |
266 |
following interface: |
|
38405 | 267 |
|
268 |
\medskip |
|
269 |
\begin{tabular}{l} |
|
270 |
@{text "change: theory \<rightarrow> (T \<rightarrow> T) \<rightarrow> T"} \\ |
|
271 |
@{text "change_yield: theory \<rightarrow> (T \<rightarrow> 'a * T) \<rightarrow> 'a * T"} |
|
272 |
\end{tabular} |
|
273 |
||
274 |
\begin{description} |
|
275 |
||
40752 | 276 |
\item @{text change} update of current data (cached!) by giving a |
277 |
continuation. |
|
38405 | 278 |
|
279 |
\item @{text change_yield} update with side result. |
|
280 |
||
281 |
\end{description} |
|
59377 | 282 |
\<close> |
38405 | 283 |
|
28213 | 284 |
end |