author | wenzelm |
Fri, 07 Dec 2018 21:42:08 +0100 | |
changeset 69422 | 472af2d7835d |
parent 68484 | 59793df7f853 |
child 69505 | cc2d676d5395 |
permissions | -rw-r--r-- |
28213 | 1 |
theory Further |
69422
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
wenzelm
parents:
68484
diff
changeset
|
2 |
imports Setup |
28213 | 3 |
begin |
4 |
||
59377 | 5 |
section \<open>Further issues \label{sec:further}\<close> |
28419 | 6 |
|
65041 | 7 |
subsection \<open>Incorporating generated code directly into the system runtime -- @{text code_reflect}\<close> |
8 |
||
9 |
subsubsection \<open>Static embedding of generated code into the system runtime\<close> |
|
10 |
||
11 |
text \<open> |
|
12 |
The @{ML_antiquotation code} antiquotation is lightweight, but the generated code |
|
13 |
is only accessible while the ML section is processed. Sometimes this |
|
14 |
is not appropriate, especially if the generated code contains datatype |
|
15 |
declarations which are shared with other parts of the system. In these |
|
16 |
cases, @{command_def code_reflect} can be used: |
|
17 |
\<close> |
|
18 |
||
19 |
code_reflect %quote Sum_Type |
|
20 |
datatypes sum = Inl | Inr |
|
21 |
functions "Sum_Type.sum.projl" "Sum_Type.sum.projr" |
|
22 |
||
23 |
text \<open> |
|
24 |
\noindent @{command code_reflect} takes a structure name and |
|
25 |
references to datatypes and functions; for these code is compiled |
|
26 |
into the named ML structure and the \emph{Eval} target is modified |
|
27 |
in a way that future code generation will reference these |
|
28 |
precompiled versions of the given datatypes and functions. This |
|
29 |
also allows to refer to the referenced datatypes and functions from |
|
30 |
arbitrary ML code as well. |
|
31 |
||
32 |
A typical example for @{command code_reflect} can be found in the |
|
68484 | 33 |
@{theory HOL.Predicate} theory. |
65041 | 34 |
\<close> |
35 |
||
36 |
||
37 |
subsubsection \<open>Separate compilation\<close> |
|
38 |
||
39 |
text \<open> |
|
40 |
For technical reasons it is sometimes necessary to separate |
|
41 |
generation and compilation of code which is supposed to be used in |
|
42 |
the system runtime. For this @{command code_reflect} with an |
|
43 |
optional \<^theory_text>\<open>file\<close> argument can be used: |
|
44 |
\<close> |
|
45 |
||
46 |
code_reflect %quote Rat |
|
47 |
datatypes rat |
|
48 |
functions Fract |
|
49 |
"(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
|
50 |
"(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
|
65981
e2c25346b156
more robust -- avoid race condition wrt. Haskell output in $ISABELLE_TMP/examples/
wenzelm
parents:
65041
diff
changeset
|
51 |
file "$ISABELLE_TMP/rat.ML" |
65041 | 52 |
|
53 |
text \<open> |
|
54 |
\noindent This merely generates the referenced code to the given |
|
55 |
file which can be included into the system runtime later on. |
|
56 |
\<close> |
|
57 |
||
59377 | 58 |
subsection \<open>Specialities of the @{text Scala} target language \label{sec:scala}\<close> |
42096 | 59 |
|
59377 | 60 |
text \<open> |
42096 | 61 |
@{text Scala} deviates from languages of the ML family in a couple |
62 |
of aspects; those which affect code generation mainly have to do with |
|
63 |
@{text Scala}'s type system: |
|
64 |
||
65 |
\begin{itemize} |
|
66 |
||
67 |
\item @{text Scala} prefers tupled syntax over curried syntax. |
|
68 |
||
69 |
\item @{text Scala} sacrifices Hindely-Milner type inference for a |
|
70 |
much more rich type system with subtyping etc. For this reason |
|
71 |
type arguments sometimes have to be given explicitly in square |
|
46520 | 72 |
brackets (mimicking System F syntax). |
42096 | 73 |
|
74 |
\item In contrast to @{text Haskell} where most specialities of |
|
75 |
the type system are implemented using \emph{type classes}, |
|
76 |
@{text Scala} provides a sophisticated system of \emph{implicit |
|
77 |
arguments}. |
|
78 |
||
79 |
\end{itemize} |
|
80 |
||
81 |
\noindent Concerning currying, the @{text Scala} serializer counts |
|
82 |
arguments in code equations to determine how many arguments |
|
83 |
shall be tupled; remaining arguments and abstractions in terms |
|
84 |
rather than function definitions are always curried. |
|
85 |
||
86 |
The second aspect affects user-defined adaptations with @{command |
|
55372 | 87 |
code_printing}. For regular terms, the @{text Scala} serializer prints |
42096 | 88 |
all type arguments explicitly. For user-defined term adaptations |
89 |
this is only possible for adaptations which take no arguments: here |
|
90 |
the type arguments are just appended. Otherwise they are ignored; |
|
91 |
hence user-defined adaptations for polymorphic constants have to be |
|
92 |
designed very carefully to avoid ambiguity. |
|
67207
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66453
diff
changeset
|
93 |
|
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66453
diff
changeset
|
94 |
Note also that name clashes can occur when generating Scala code |
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66453
diff
changeset
|
95 |
to case-insensitive file systems; these can be avoid using the |
ad538f6c5d2f
dedicated case option for code generation to Scala
haftmann
parents:
66453
diff
changeset
|
96 |
``\<open>(case_insensitive)\<close>'' option for @{command export_code}. |
59377 | 97 |
\<close> |
42096 | 98 |
|
99 |
||
59377 | 100 |
subsection \<open>Modules namespace\<close> |
28419 | 101 |
|
59377 | 102 |
text \<open> |
40752 | 103 |
When invoking the @{command export_code} command it is possible to |
104 |
leave out the @{keyword "module_name"} part; then code is |
|
105 |
distributed over different modules, where the module name space |
|
106 |
roughly is induced by the Isabelle theory name space. |
|
38437 | 107 |
|
40752 | 108 |
Then sometimes the awkward situation occurs that dependencies |
109 |
between definitions introduce cyclic dependencies between modules, |
|
110 |
which in the @{text Haskell} world leaves you to the mercy of the |
|
111 |
@{text Haskell} implementation you are using, while for @{text |
|
112 |
SML}/@{text OCaml} code generation is not possible. |
|
38437 | 113 |
|
40752 | 114 |
A solution is to declare module names explicitly. Let use assume |
115 |
the three cyclically dependent modules are named \emph{A}, \emph{B} |
|
116 |
and \emph{C}. Then, by stating |
|
59377 | 117 |
\<close> |
38437 | 118 |
|
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51717
diff
changeset
|
119 |
code_identifier %quote |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51717
diff
changeset
|
120 |
code_module A \<rightharpoonup> (SML) ABC |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51717
diff
changeset
|
121 |
| code_module B \<rightharpoonup> (SML) ABC |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51717
diff
changeset
|
122 |
| code_module C \<rightharpoonup> (SML) ABC |
38437 | 123 |
|
59377 | 124 |
text \<open> |
40752 | 125 |
\noindent we explicitly map all those modules on \emph{ABC}, |
126 |
resulting in an ad-hoc merge of this three modules at serialisation |
|
127 |
time. |
|
59377 | 128 |
\<close> |
28419 | 129 |
|
59377 | 130 |
subsection \<open>Locales and interpretation\<close> |
37426 | 131 |
|
59377 | 132 |
text \<open> |
37426 | 133 |
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
|
134 |
specifications stemming from locale interpretation into global |
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61779
diff
changeset
|
135 |
theories. |
37426 | 136 |
|
40752 | 137 |
Let us assume a locale specifying a power operation on arbitrary |
138 |
types: |
|
59377 | 139 |
\<close> |
37426 | 140 |
|
141 |
locale %quote power = |
|
142 |
fixes power :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" |
|
143 |
assumes power_commute: "power x \<circ> power y = power y \<circ> power x" |
|
144 |
begin |
|
145 |
||
59377 | 146 |
text \<open> |
40752 | 147 |
\noindent Inside that locale we can lift @{text power} to exponent |
61779 | 148 |
lists by means of a specification relative to that locale: |
59377 | 149 |
\<close> |
37426 | 150 |
|
151 |
primrec %quote powers :: "'a list \<Rightarrow> 'b \<Rightarrow> 'b" where |
|
152 |
"powers [] = id" |
|
153 |
| "powers (x # xs) = power x \<circ> powers xs" |
|
154 |
||
155 |
lemma %quote powers_append: |
|
156 |
"powers (xs @ ys) = powers xs \<circ> powers ys" |
|
157 |
by (induct xs) simp_all |
|
158 |
||
159 |
lemma %quote powers_power: |
|
160 |
"powers xs \<circ> power x = power x \<circ> powers xs" |
|
161 |
by (induct xs) |
|
49739 | 162 |
(simp_all del: o_apply id_apply add: comp_assoc, |
37426 | 163 |
simp del: o_apply add: o_assoc power_commute) |
164 |
||
165 |
lemma %quote powers_rev: |
|
166 |
"powers (rev xs) = powers xs" |
|
167 |
by (induct xs) (simp_all add: powers_append powers_power) |
|
168 |
||
169 |
end %quote |
|
170 |
||
59377 | 171 |
text \<open> |
38505 | 172 |
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
|
173 |
global_interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f |
61779 | 174 |
:: 'a \<Rightarrow> 'a). f ^^ n)"}), one could naively expect to have a constant @{text |
37426 | 175 |
"fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code |
176 |
can be generated. But this not the case: internally, the term |
|
177 |
@{text "fun_power.powers"} is an abbreviation for the foundational |
|
178 |
term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"} |
|
58620 | 179 |
(see @{cite "isabelle-locale"} for the details behind). |
37426 | 180 |
|
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61779
diff
changeset
|
181 |
Fortunately, a succint solution is available: a dedicated |
61779 | 182 |
rewrite definition: |
59377 | 183 |
\<close> |
37426 | 184 |
|
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61779
diff
changeset
|
185 |
global_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)" |
61779 | 186 |
defines funpows = fun_power.powers |
187 |
by unfold_locales |
|
188 |
(simp_all add: fun_eq_iff funpow_mult mult.commute) |
|
37426 | 189 |
|
59377 | 190 |
text \<open> |
61779 | 191 |
\noindent This amends the interpretation morphisms such that |
192 |
occurrences of the foundational term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"} |
|
193 |
are folded to a newly defined constant @{const funpows}. |
|
37426 | 194 |
|
195 |
After this setup procedure, code generation can continue as usual: |
|
59377 | 196 |
\<close> |
37426 | 197 |
|
59377 | 198 |
text %quotetypewriter \<open> |
39683 | 199 |
@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)} |
61779 | 200 |
\<close> |
37426 | 201 |
|
202 |
||
59377 | 203 |
subsection \<open>Parallel computation\<close> |
51172 | 204 |
|
59377 | 205 |
text \<open> |
63680 | 206 |
Theory @{text Parallel} in \<^dir>\<open>~~/src/HOL/Library\<close> contains |
51172 | 207 |
operations to exploit parallelism inside the Isabelle/ML |
208 |
runtime engine. |
|
59377 | 209 |
\<close> |
51172 | 210 |
|
59377 | 211 |
subsection \<open>Imperative data structures\<close> |
28419 | 212 |
|
59377 | 213 |
text \<open> |
38437 | 214 |
If you consider imperative data structures as inevitable for a |
215 |
specific application, you should consider \emph{Imperative |
|
216 |
Functional Programming with Isabelle/HOL} |
|
58620 | 217 |
@{cite "bulwahn-et-al:2008:imperative"}; the framework described there |
40752 | 218 |
is available in session @{text Imperative_HOL}, together with a |
219 |
short primer document. |
|
59377 | 220 |
\<close> |
28419 | 221 |
|
28213 | 222 |
end |