author | wenzelm |
Sat, 10 Sep 2022 16:12:52 +0200 | |
changeset 76107 | 4dedb6e2dac2 |
parent 75647 | 34cd1d210b92 |
permissions | -rw-r--r-- |
31050 | 1 |
theory Adaptation |
69422
472af2d7835d
clarified session dependencies: faster build_doc/build_release;
wenzelm
parents:
68484
diff
changeset
|
2 |
imports Setup |
28213 | 3 |
begin |
4 |
||
59377 | 5 |
setup %invisible \<open>Code_Target.add_derived_target ("\<SML>", [("SML", I)]) |
6 |
#> Code_Target.add_derived_target ("\<SMLdummy>", [("Haskell", I)])\<close> |
|
28561 | 7 |
|
59377 | 8 |
section \<open>Adaptation to target languages \label{sec:adaptation}\<close> |
28419 | 9 |
|
59377 | 10 |
subsection \<open>Adapting code generation\<close> |
28561 | 11 |
|
59377 | 12 |
text \<open> |
28561 | 13 |
The aspects of code generation introduced so far have two aspects |
14 |
in common: |
|
15 |
||
16 |
\begin{itemize} |
|
38450 | 17 |
|
18 |
\item They act uniformly, without reference to a specific target |
|
19 |
language. |
|
20 |
||
28561 | 21 |
\item They are \emph{safe} in the sense that as long as you trust |
22 |
the code generator meta theory and implementation, you cannot |
|
38450 | 23 |
produce programs that yield results which are not derivable in |
24 |
the logic. |
|
25 |
||
28561 | 26 |
\end{itemize} |
27 |
||
38450 | 28 |
\noindent In this section we will introduce means to \emph{adapt} |
29 |
the serialiser to a specific target language, i.e.~to print program |
|
30 |
fragments in a way which accommodates \qt{already existing} |
|
31 |
ingredients of a target language environment, for three reasons: |
|
28561 | 32 |
|
33 |
\begin{itemize} |
|
28593 | 34 |
\item improving readability and aesthetics of generated code |
28561 | 35 |
\item gaining efficiency |
36 |
\item interface with language parts which have no direct counterpart |
|
69505 | 37 |
in \<open>HOL\<close> (say, imperative data structures) |
28561 | 38 |
\end{itemize} |
39 |
||
40 |
\noindent Generally, you should avoid using those features yourself |
|
41 |
\emph{at any cost}: |
|
42 |
||
43 |
\begin{itemize} |
|
38450 | 44 |
|
45 |
\item The safe configuration methods act uniformly on every target |
|
46 |
language, whereas for adaptation you have to treat each target |
|
47 |
language separately. |
|
48 |
||
49 |
\item Application is extremely tedious since there is no |
|
50 |
abstraction which would allow for a static check, making it easy |
|
51 |
to produce garbage. |
|
52 |
||
34155 | 53 |
\item Subtle errors can be introduced unconsciously. |
38450 | 54 |
|
28561 | 55 |
\end{itemize} |
56 |
||
38450 | 57 |
\noindent However, even if you ought refrain from setting up |
69505 | 58 |
adaptation yourself, already \<open>HOL\<close> comes with some |
38450 | 59 |
reasonable default adaptations (say, using target language list |
60 |
syntax). There also some common adaptation cases which you can |
|
61 |
setup by importing particular library theories. In order to |
|
62 |
understand these, we provide some clues here; these however are not |
|
63 |
supposed to replace a careful study of the sources. |
|
59377 | 64 |
\<close> |
28561 | 65 |
|
38450 | 66 |
|
59377 | 67 |
subsection \<open>The adaptation principle\<close> |
28561 | 68 |
|
59377 | 69 |
text \<open> |
38450 | 70 |
Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is |
71 |
conceptually supposed to be: |
|
28601 | 72 |
|
60768 | 73 |
\begin{figure}[h] |
52742 | 74 |
\begin{tikzpicture}[scale = 0.5] |
75 |
\tikzstyle water=[color = blue, thick] |
|
76 |
\tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white] |
|
77 |
\tikzstyle process=[color = green, semithick, ->] |
|
78 |
\tikzstyle adaptation=[color = red, semithick, ->] |
|
79 |
\tikzstyle target=[color = black] |
|
80 |
\foreach \x in {0, ..., 24} |
|
81 |
\draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin |
|
82 |
+ (0.25, -0.25) cos + (0.25, 0.25); |
|
83 |
\draw[style=ice] (1, 0) -- |
|
84 |
(3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle; |
|
85 |
\draw[style=ice] (9, 0) -- |
|
86 |
(11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle; |
|
87 |
\draw[style=ice] (15, -6) -- |
|
88 |
(19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle; |
|
89 |
\draw[style=process] |
|
90 |
(3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3); |
|
91 |
\draw[style=process] |
|
92 |
(11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3); |
|
93 |
\node (adaptation) at (11, -2) [style=adaptation] {adaptation}; |
|
94 |
\node at (19, 3) [rotate=90] {generated}; |
|
95 |
\node at (19.5, -5) {language}; |
|
96 |
\node at (19.5, -3) {library}; |
|
97 |
\node (includes) at (19.5, -1) {includes}; |
|
98 |
\node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57 |
|
99 |
\draw[style=process] |
|
100 |
(includes) -- (serialisation); |
|
101 |
\draw[style=process] |
|
102 |
(reserved) -- (serialisation); |
|
103 |
\draw[style=adaptation] |
|
104 |
(adaptation) -- (serialisation); |
|
105 |
\draw[style=adaptation] |
|
106 |
(adaptation) -- (includes); |
|
107 |
\draw[style=adaptation] |
|
108 |
(adaptation) -- (reserved); |
|
109 |
\end{tikzpicture} |
|
31050 | 110 |
\caption{The adaptation principle} |
111 |
\label{fig:adaptation} |
|
28601 | 112 |
\end{figure} |
113 |
||
114 |
\noindent In the tame view, code generation acts as broker between |
|
69505 | 115 |
\<open>logic\<close>, \<open>intermediate language\<close> and \<open>target |
116 |
language\<close> by means of \<open>translation\<close> and \<open>serialisation\<close>; for the latter, the serialiser has to observe the |
|
117 |
structure of the \<open>language\<close> itself plus some \<open>reserved\<close> |
|
38450 | 118 |
keywords which have to be avoided for generated code. However, if |
69505 | 119 |
you consider \<open>adaptation\<close> mechanisms, the code generated by |
38450 | 120 |
the serializer is just the tip of the iceberg: |
28601 | 121 |
|
122 |
\begin{itemize} |
|
38450 | 123 |
|
69505 | 124 |
\item \<open>serialisation\<close> can be \emph{parametrised} such that |
28635 | 125 |
logical entities are mapped to target-specific ones |
38450 | 126 |
(e.g. target-specific list syntax, see also |
127 |
\secref{sec:adaptation_mechanisms}) |
|
128 |
||
28635 | 129 |
\item Such parametrisations can involve references to a |
69597 | 130 |
target-specific standard \<open>library\<close> (e.g. using the \<open>Haskell\<close> \<^verbatim>\<open>Maybe\<close> type instead of the \<open>HOL\<close> |
131 |
\<^type>\<open>option\<close> type); if such are used, the corresponding |
|
132 |
identifiers (in our example, \<^verbatim>\<open>Maybe\<close>, \<^verbatim>\<open>Nothing\<close> and \<^verbatim>\<open>Just\<close>) also have to be considered \<open>reserved\<close>. |
|
38450 | 133 |
|
28635 | 134 |
\item Even more, the user can enrich the library of the |
69505 | 135 |
target-language by providing code snippets (\qt{\<open>includes\<close>}) which are prepended to any generated code (see |
38450 | 136 |
\secref{sec:include}); this typically also involves further |
69505 | 137 |
\<open>reserved\<close> identifiers. |
38450 | 138 |
|
28601 | 139 |
\end{itemize} |
28635 | 140 |
|
38450 | 141 |
\noindent As figure \ref{fig:adaptation} illustrates, all these |
142 |
adaptation mechanisms have to act consistently; it is at the |
|
143 |
discretion of the user to take care for this. |
|
59377 | 144 |
\<close> |
28561 | 145 |
|
65041 | 146 |
subsection \<open>Common adaptation applications \label{sec:common_adaptation}\<close> |
28419 | 147 |
|
59377 | 148 |
text \<open> |
69597 | 149 |
The \<^theory>\<open>Main\<close> theory of Isabelle/HOL already provides a code |
38450 | 150 |
generator setup which should be suitable for most applications. |
151 |
Common extensions and modifications are available by certain |
|
63680 | 152 |
theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in |
38450 | 153 |
applications, they may serve as a tutorial for customising the code |
154 |
generator setup (see below \secref{sec:adaptation_mechanisms}). |
|
28419 | 155 |
|
156 |
\begin{description} |
|
157 |
||
69597 | 158 |
\item[\<^theory>\<open>HOL.Code_Numeral\<close>] provides additional numeric |
159 |
types \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close> isomorphic to types |
|
160 |
\<^typ>\<open>int\<close> and \<^typ>\<open>nat\<close> respectively. Type \<^typ>\<open>integer\<close> |
|
161 |
is mapped to target-language built-in integers; \<^typ>\<open>natural\<close> |
|
162 |
is implemented as abstract type over \<^typ>\<open>integer\<close>. |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48985
diff
changeset
|
163 |
Useful for code setups which involve e.g.~indexing |
69505 | 164 |
of target-language arrays. Part of \<open>HOL-Main\<close>. |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48985
diff
changeset
|
165 |
|
69597 | 166 |
\item[\<^theory>\<open>HOL.String\<close>] provides an additional datatype \<^typ>\<open>String.literal\<close> which is isomorphic to lists of 7-bit (ASCII) characters; |
167 |
\<^typ>\<open>String.literal\<close>s are mapped to target-language strings. |
|
68028 | 168 |
|
69597 | 169 |
Literal values of type \<^typ>\<open>String.literal\<close> can be written |
69505 | 170 |
as \<open>STR ''\<dots>''\<close> for sequences of printable characters and |
171 |
\<open>STR 0x\<dots>\<close> for one single ASCII code point given |
|
69597 | 172 |
as hexadecimal numeral; \<^typ>\<open>String.literal\<close> supports concatenation |
69505 | 173 |
\<open>\<dots> + \<dots>\<close> for all standard target languages. |
68028 | 174 |
|
175 |
Note that the particular notion of \qt{string} is target-language |
|
176 |
specific (sequence of 8-bit units, sequence of unicode code points, \ldots); |
|
177 |
hence ASCII is the only reliable common base e.g.~for |
|
178 |
printing (error) messages; more sophisticated applications |
|
179 |
like verifying parsing algorithms require a dedicated |
|
180 |
target-language specific model. |
|
181 |
||
69597 | 182 |
Nevertheless \<^typ>\<open>String.literal\<close>s can be analyzed; the core operations |
183 |
for this are \<^term_type>\<open>String.asciis_of_literal\<close> and |
|
184 |
\<^term_type>\<open>String.literal_of_asciis\<close> which are implemented |
|
185 |
in a target-language-specific way; particularly \<^const>\<open>String.asciis_of_literal\<close> |
|
68028 | 186 |
checks its argument at runtime to make sure that it does |
187 |
not contain non-ASCII-characters, to safeguard consistency. |
|
69597 | 188 |
On top of these, more abstract conversions like \<^term_type>\<open>String.explode\<close> and \<^term_type>\<open>String.implode\<close> |
68028 | 189 |
are implemented. |
190 |
||
69505 | 191 |
Part of \<open>HOL-Main\<close>. |
68028 | 192 |
|
69597 | 193 |
\item[\<open>Code_Target_Int\<close>] implements type \<^typ>\<open>int\<close> |
194 |
by \<^typ>\<open>integer\<close> and thus by target-language built-in integers. |
|
38450 | 195 |
|
69505 | 196 |
\item[\<open>Code_Binary_Nat\<close>] implements type |
69597 | 197 |
\<^typ>\<open>nat\<close> using a binary rather than a linear representation, |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48985
diff
changeset
|
198 |
which yields a considerable speedup for computations. |
69597 | 199 |
Pattern matching with \<^term>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated |
51171
e8b2d90da499
corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
haftmann
parents:
51162
diff
changeset
|
200 |
by a preprocessor.\label{abstract_nat} |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48985
diff
changeset
|
201 |
|
69597 | 202 |
\item[\<open>Code_Target_Nat\<close>] implements type \<^typ>\<open>nat\<close> |
203 |
by \<^typ>\<open>integer\<close> and thus by target-language built-in integers. |
|
204 |
Pattern matching with \<^term>\<open>0::nat\<close> / \<^const>\<open>Suc\<close> is eliminated |
|
51171
e8b2d90da499
corrected and clarified Code_Binary_Nat vs. Code_Target_Nat
haftmann
parents:
51162
diff
changeset
|
205 |
by a preprocessor. |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
48985
diff
changeset
|
206 |
|
69505 | 207 |
\item[\<open>Code_Target_Numeral\<close>] is a convenience theory |
208 |
containing both \<open>Code_Target_Nat\<close> and |
|
209 |
\<open>Code_Target_Int\<close>. |
|
38450 | 210 |
|
75647
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
69690
diff
changeset
|
211 |
\item[\<open>Code_Abstract_Char\<close>] implements type \<^typ>\<open>char\<close> by target language |
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
69690
diff
changeset
|
212 |
integers, sacrificing pattern patching in exchange for dramatically |
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
69690
diff
changeset
|
213 |
increased performance for comparisions. |
34cd1d210b92
officical abstract characters for code generation
haftmann
parents:
69690
diff
changeset
|
214 |
|
69597 | 215 |
\item[\<^theory>\<open>HOL-Library.IArray\<close>] provides a type \<^typ>\<open>'a iarray\<close> |
51162 | 216 |
isomorphic to lists but implemented by (effectively immutable) |
217 |
arrays \emph{in SML only}. |
|
28419 | 218 |
|
51162 | 219 |
\end{description} |
59377 | 220 |
\<close> |
28419 | 221 |
|
222 |
||
59377 | 223 |
subsection \<open>Parametrising serialisation \label{sec:adaptation_mechanisms}\<close> |
28419 | 224 |
|
59377 | 225 |
text \<open> |
38450 | 226 |
Consider the following function and its corresponding SML code: |
59377 | 227 |
\<close> |
28419 | 228 |
|
28564 | 229 |
primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where |
28419 | 230 |
"in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l" |
28447 | 231 |
(*<*) |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
232 |
code_printing %invisible |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
233 |
type_constructor bool \<rightharpoonup> (SML) |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
234 |
| constant True \<rightharpoonup> (SML) |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
235 |
| constant False \<rightharpoonup> (SML) |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
236 |
| constant HOL.conj \<rightharpoonup> (SML) |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
237 |
| constant Not \<rightharpoonup> (SML) |
28447 | 238 |
(*>*) |
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
239 |
text %quote \<open> |
39683 | 240 |
@{code_stmts in_interval (SML)} |
59377 | 241 |
\<close> |
28419 | 242 |
|
59377 | 243 |
text \<open> |
38450 | 244 |
\noindent Though this is correct code, it is a little bit |
245 |
unsatisfactory: boolean values and operators are materialised as |
|
246 |
distinguished entities with have nothing to do with the SML-built-in |
|
247 |
notion of \qt{bool}. This results in less readable code; |
|
248 |
additionally, eager evaluation may cause programs to loop or break |
|
69597 | 249 |
which would perfectly terminate when the existing SML \<^verbatim>\<open>bool\<close> would be used. To map the HOL \<^typ>\<open>bool\<close> on SML \<^verbatim>\<open>bool\<close>, we may use \qn{custom serialisations}: |
59377 | 250 |
\<close> |
28419 | 251 |
|
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
252 |
code_printing %quotett |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
253 |
type_constructor bool \<rightharpoonup> (SML) "bool" |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
254 |
| constant True \<rightharpoonup> (SML) "true" |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
255 |
| constant False \<rightharpoonup> (SML) "false" |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
256 |
| constant HOL.conj \<rightharpoonup> (SML) "_ andalso _" |
28213 | 257 |
|
59377 | 258 |
text \<open> |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
259 |
\noindent The @{command_def code_printing} command takes a series |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
260 |
of symbols (contants, type constructor, \ldots) |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
261 |
together with target-specific custom serialisations. Each |
38450 | 262 |
custom serialisation starts with a target language identifier |
263 |
followed by an expression, which during code serialisation is |
|
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
264 |
inserted whenever the type constructor would occur. Each |
69597 | 265 |
``\<^verbatim>\<open>_\<close>'' in a serialisation expression is treated as a |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
266 |
placeholder for the constant's or the type constructor's arguments. |
59377 | 267 |
\<close> |
28419 | 268 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
269 |
text %quote \<open> |
39683 | 270 |
@{code_stmts in_interval (SML)} |
59377 | 271 |
\<close> |
28419 | 272 |
|
59377 | 273 |
text \<open> |
38450 | 274 |
\noindent This still is not perfect: the parentheses around the |
275 |
\qt{andalso} expression are superfluous. Though the serialiser by |
|
276 |
no means attempts to imitate the rich Isabelle syntax framework, it |
|
277 |
provides some common idioms, notably associative infixes with |
|
278 |
precedences which may be used here: |
|
59377 | 279 |
\<close> |
28419 | 280 |
|
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
281 |
code_printing %quotett |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
282 |
constant HOL.conj \<rightharpoonup> (SML) infixl 1 "andalso" |
28419 | 283 |
|
69660
2bc2a8599369
canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents:
69597
diff
changeset
|
284 |
text %quote \<open> |
39683 | 285 |
@{code_stmts in_interval (SML)} |
59377 | 286 |
\<close> |
28419 | 287 |
|
59377 | 288 |
text \<open> |
38450 | 289 |
\noindent The attentive reader may ask how we assert that no |
290 |
generated code will accidentally overwrite. For this reason the |
|
291 |
serialiser has an internal table of identifiers which have to be |
|
292 |
avoided to be used for new declarations. Initially, this table |
|
293 |
typically contains the keywords of the target language. It can be |
|
294 |
extended manually, thus avoiding accidental overwrites, using the |
|
38505 | 295 |
@{command_def "code_reserved"} command: |
59377 | 296 |
\<close> |
28561 | 297 |
|
40351 | 298 |
code_reserved %quote "\<SMLdummy>" bool true false andalso |
28561 | 299 |
|
59377 | 300 |
text \<open> |
28447 | 301 |
\noindent Next, we try to map HOL pairs to SML pairs, using the |
69597 | 302 |
infix ``\<^verbatim>\<open>*\<close>'' type constructor and parentheses: |
59377 | 303 |
\<close> |
28447 | 304 |
(*<*) |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
305 |
code_printing %invisible |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
306 |
type_constructor prod \<rightharpoonup> (SML) |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
307 |
| constant Pair \<rightharpoonup> (SML) |
28447 | 308 |
(*>*) |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
309 |
code_printing %quotett |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
310 |
type_constructor prod \<rightharpoonup> (SML) infix 2 "*" |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
311 |
| constant Pair \<rightharpoonup> (SML) "!((_),/ (_))" |
28419 | 312 |
|
59377 | 313 |
text \<open> |
69597 | 314 |
\noindent The initial bang ``\<^verbatim>\<open>!\<close>'' tells the serialiser |
38450 | 315 |
never to put parentheses around the whole expression (they are |
316 |
already present), while the parentheses around argument place |
|
317 |
holders tell not to put parentheses around the arguments. The slash |
|
69597 | 318 |
``\<^verbatim>\<open>/\<close>'' (followed by arbitrary white space) inserts a |
38450 | 319 |
space which may be used as a break if necessary during pretty |
320 |
printing. |
|
28419 | 321 |
|
38450 | 322 |
These examples give a glimpse what mechanisms custom serialisations |
323 |
provide; however their usage requires careful thinking in order not |
|
324 |
to introduce inconsistencies -- or, in other words: custom |
|
325 |
serialisations are completely axiomatic. |
|
28419 | 326 |
|
39643 | 327 |
A further noteworthy detail is that any special character in a |
69597 | 328 |
custom serialisation may be quoted using ``\<^verbatim>\<open>'\<close>''; thus, |
329 |
in ``\<^verbatim>\<open>fn '_ => _\<close>'' the first ``\<^verbatim>\<open>_\<close>'' is a |
|
330 |
proper underscore while the second ``\<^verbatim>\<open>_\<close>'' is a |
|
38450 | 331 |
placeholder. |
59377 | 332 |
\<close> |
28419 | 333 |
|
334 |
||
69505 | 335 |
subsection \<open>\<open>Haskell\<close> serialisation\<close> |
28419 | 336 |
|
59377 | 337 |
text \<open> |
69505 | 338 |
For convenience, the default \<open>HOL\<close> setup for \<open>Haskell\<close> |
69597 | 339 |
maps the \<^class>\<open>equal\<close> class to its counterpart in \<open>Haskell\<close>, |
340 |
giving custom serialisations for the class \<^class>\<open>equal\<close> |
|
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
341 |
and its operation @{const [source] HOL.equal}. |
59377 | 342 |
\<close> |
28419 | 343 |
|
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
344 |
code_printing %quotett |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
345 |
type_class equal \<rightharpoonup> (Haskell) "Eq" |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
346 |
| constant HOL.equal \<rightharpoonup> (Haskell) infixl 4 "==" |
28419 | 347 |
|
59377 | 348 |
text \<open> |
38450 | 349 |
\noindent A problem now occurs whenever a type which is an instance |
69597 | 350 |
of \<^class>\<open>equal\<close> in \<open>HOL\<close> is mapped on a \<open>Haskell\<close>-built-in type which is also an instance of \<open>Haskell\<close> |
69505 | 351 |
\<open>Eq\<close>: |
59377 | 352 |
\<close> |
28419 | 353 |
|
28564 | 354 |
typedecl %quote bar |
28419 | 355 |
|
39063 | 356 |
instantiation %quote bar :: equal |
28419 | 357 |
begin |
358 |
||
61076 | 359 |
definition %quote "HOL.equal (x::bar) y \<longleftrightarrow> x = y" |
28419 | 360 |
|
61169 | 361 |
instance %quote by standard (simp add: equal_bar_def) |
28213 | 362 |
|
30880 | 363 |
end %quote (*<*) |
364 |
||
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
365 |
(*>*) code_printing %quotett |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
366 |
type_constructor bar \<rightharpoonup> (Haskell) "Integer" |
28419 | 367 |
|
59377 | 368 |
text \<open> |
38450 | 369 |
\noindent The code generator would produce an additional instance, |
69505 | 370 |
which of course is rejected by the \<open>Haskell\<close> compiler. To |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
371 |
suppress this additional instance: |
59377 | 372 |
\<close> |
28419 | 373 |
|
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
374 |
code_printing %quotett |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
375 |
class_instance bar :: "HOL.equal" \<rightharpoonup> (Haskell) - |
28419 | 376 |
|
28561 | 377 |
|
59377 | 378 |
subsection \<open>Enhancing the target language context \label{sec:include}\<close> |
28561 | 379 |
|
59377 | 380 |
text \<open> |
28593 | 381 |
In rare cases it is necessary to \emph{enrich} the context of a |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
382 |
target language; this can also be accomplished using the @{command |
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
383 |
"code_printing"} command: |
59377 | 384 |
\<close> |
28561 | 385 |
|
69690 | 386 |
code_printing %quotett code_module "Errno" \<rightharpoonup> (Haskell) |
387 |
\<open>module Errno(errno) where |
|
388 |
||
389 |
errno i = error ("Error number: " ++ show i)\<close> |
|
28561 | 390 |
|
39745 | 391 |
code_reserved %quotett Haskell Errno |
28561 | 392 |
|
59377 | 393 |
text \<open> |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
394 |
\noindent Such named modules are then prepended to every |
38450 | 395 |
generated code. Inspect such code in order to find out how |
52378
08dbf9ff2140
documentation on code_printing and code_identifier
haftmann
parents:
51172
diff
changeset
|
396 |
this behaves with respect to a particular |
38450 | 397 |
target language. |
59377 | 398 |
\<close> |
28561 | 399 |
|
28419 | 400 |
end |