author | wenzelm |
Tue, 07 Apr 2009 21:24:39 +0200 | |
changeset 30882 | d15725e84091 |
parent 30880 | 257cbe43faa8 |
permissions | -rw-r--r-- |
28447 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Adaption}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Adaption\isanewline |
|
12 |
\isakeyword{imports}\ Setup\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
28561 | 18 |
\isanewline |
28447 | 19 |
% |
20 |
\endisadelimtheory |
|
21 |
% |
|
28561 | 22 |
\isadeliminvisible |
23 |
\isanewline |
|
24 |
% |
|
25 |
\endisadeliminvisible |
|
26 |
% |
|
27 |
\isataginvisible |
|
28 |
\isacommand{setup}\isamarkupfalse% |
|
28679 | 29 |
\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}% |
28561 | 30 |
\endisataginvisible |
31 |
{\isafoldinvisible}% |
|
32 |
% |
|
33 |
\isadeliminvisible |
|
34 |
% |
|
35 |
\endisadeliminvisible |
|
36 |
% |
|
28447 | 37 |
\isamarkupsection{Adaption to target languages \label{sec:adaption}% |
38 |
} |
|
39 |
\isamarkuptrue% |
|
40 |
% |
|
28561 | 41 |
\isamarkupsubsection{Adapting code generation% |
42 |
} |
|
43 |
\isamarkuptrue% |
|
44 |
% |
|
45 |
\begin{isamarkuptext}% |
|
46 |
The aspects of code generation introduced so far have two aspects |
|
47 |
in common: |
|
48 |
||
49 |
\begin{itemize} |
|
50 |
\item They act uniformly, without reference to a specific |
|
51 |
target language. |
|
52 |
\item They are \emph{safe} in the sense that as long as you trust |
|
53 |
the code generator meta theory and implementation, you cannot |
|
54 |
produce programs that yield results which are not derivable |
|
55 |
in the logic. |
|
56 |
\end{itemize} |
|
57 |
||
58 |
\noindent In this section we will introduce means to \emph{adapt} the serialiser |
|
59 |
to a specific target language, i.e.~to print program fragments |
|
28593 | 60 |
in a way which accommodates \qt{already existing} ingredients of |
28561 | 61 |
a target language environment, for three reasons: |
62 |
||
63 |
\begin{itemize} |
|
28593 | 64 |
\item improving readability and aesthetics of generated code |
28561 | 65 |
\item gaining efficiency |
66 |
\item interface with language parts which have no direct counterpart |
|
67 |
in \isa{HOL} (say, imperative data structures) |
|
68 |
\end{itemize} |
|
69 |
||
70 |
\noindent Generally, you should avoid using those features yourself |
|
71 |
\emph{at any cost}: |
|
72 |
||
73 |
\begin{itemize} |
|
74 |
\item The safe configuration methods act uniformly on every target language, |
|
75 |
whereas for adaption you have to treat each target language separate. |
|
76 |
\item Application is extremely tedious since there is no abstraction |
|
28593 | 77 |
which would allow for a static check, making it easy to produce garbage. |
78 |
\item More or less subtle errors can be introduced unconsciously. |
|
28561 | 79 |
\end{itemize} |
80 |
||
81 |
\noindent However, even if you ought refrain from setting up adaption |
|
82 |
yourself, already the \isa{HOL} comes with some reasonable default |
|
83 |
adaptions (say, using target language list syntax). There also some |
|
84 |
common adaption cases which you can setup by importing particular |
|
85 |
library theories. In order to understand these, we provide some clues here; |
|
86 |
these however are not supposed to replace a careful study of the sources.% |
|
87 |
\end{isamarkuptext}% |
|
88 |
\isamarkuptrue% |
|
89 |
% |
|
90 |
\isamarkupsubsection{The adaption principle% |
|
91 |
} |
|
92 |
\isamarkuptrue% |
|
93 |
% |
|
94 |
\begin{isamarkuptext}% |
|
30880 | 95 |
Figure \ref{fig:adaption} illustrates what \qt{adaption} is conceptually |
28601 | 96 |
supposed to be: |
97 |
||
98 |
\begin{figure}[here] |
|
30882
d15725e84091
moved generated eps/pdf to main directory, for proper display in dvi;
wenzelm
parents:
30880
diff
changeset
|
99 |
\includegraphics{adaption} |
28601 | 100 |
\caption{The adaption principle} |
101 |
\label{fig:adaption} |
|
102 |
\end{figure} |
|
103 |
||
104 |
\noindent In the tame view, code generation acts as broker between |
|
105 |
\isa{logic}, \isa{intermediate\ language} and |
|
106 |
\isa{target\ language} by means of \isa{translation} and |
|
107 |
\isa{serialisation}; for the latter, the serialiser has to observe |
|
108 |
the structure of the \isa{language} itself plus some \isa{reserved} |
|
109 |
keywords which have to be avoided for generated code. |
|
110 |
However, if you consider \isa{adaption} mechanisms, the code generated |
|
111 |
by the serializer is just the tip of the iceberg: |
|
112 |
||
113 |
\begin{itemize} |
|
28635 | 114 |
\item \isa{serialisation} can be \emph{parametrised} such that |
115 |
logical entities are mapped to target-specific ones |
|
116 |
(e.g. target-specific list syntax, |
|
117 |
see also \secref{sec:adaption_mechanisms}) |
|
118 |
\item Such parametrisations can involve references to a |
|
119 |
target-specific standard \isa{library} (e.g. using |
|
120 |
the \isa{Haskell} \verb|Maybe| type instead |
|
121 |
of the \isa{HOL} \isa{option} type); |
|
122 |
if such are used, the corresponding identifiers |
|
123 |
(in our example, \verb|Maybe|, \verb|Nothing| |
|
124 |
and \verb|Just|) also have to be considered \isa{reserved}. |
|
125 |
\item Even more, the user can enrich the library of the |
|
126 |
target-language by providing code snippets |
|
127 |
(\qt{\isa{includes}}) which are prepended to |
|
128 |
any generated code (see \secref{sec:include}); this typically |
|
129 |
also involves further \isa{reserved} identifiers. |
|
130 |
\end{itemize} |
|
131 |
||
132 |
\noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms |
|
133 |
have to act consistently; it is at the discretion of the user |
|
134 |
to take care for this.% |
|
28561 | 135 |
\end{isamarkuptext}% |
136 |
\isamarkuptrue% |
|
137 |
% |
|
28635 | 138 |
\isamarkupsubsection{Common adaption patterns% |
28447 | 139 |
} |
140 |
\isamarkuptrue% |
|
141 |
% |
|
142 |
\begin{isamarkuptext}% |
|
143 |
The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code |
|
144 |
generator setup |
|
28593 | 145 |
which should be suitable for most applications. Common extensions |
28447 | 146 |
and modifications are available by certain theories of the \isa{HOL} |
147 |
library; beside being useful in applications, they may serve |
|
148 |
as a tutorial for customising the code generator setup (see below |
|
149 |
\secref{sec:adaption_mechanisms}). |
|
150 |
||
151 |
\begin{description} |
|
152 |
||
153 |
\item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big |
|
154 |
integer literals in target languages. |
|
155 |
\item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by |
|
156 |
character literals in target languages. |
|
157 |
\item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char}, |
|
158 |
but also offers treatment of character codes; includes |
|
28561 | 159 |
\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}. |
28447 | 160 |
\item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers, |
161 |
which in general will result in higher efficiency; pattern |
|
162 |
matching with \isa{{\isadigit{0}}} / \isa{Suc} |
|
28561 | 163 |
is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}} |
164 |
and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}. |
|
28447 | 165 |
\item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype |
166 |
\isa{index} which is mapped to target-language built-in integers. |
|
167 |
Useful for code setups which involve e.g. indexing of |
|
168 |
target-language arrays. |
|
169 |
\item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype |
|
170 |
\isa{message{\isacharunderscore}string} which is isomorphic to strings; |
|
171 |
\isa{message{\isacharunderscore}string}s are mapped to target-language strings. |
|
172 |
Useful for code setups which involve e.g. printing (error) messages. |
|
173 |
||
174 |
\end{description} |
|
175 |
||
176 |
\begin{warn} |
|
177 |
When importing any of these theories, they should form the last |
|
178 |
items in an import list. Since these theories adapt the |
|
179 |
code generator setup in a non-conservative fashion, |
|
180 |
strange effects may occur otherwise. |
|
181 |
\end{warn}% |
|
182 |
\end{isamarkuptext}% |
|
183 |
\isamarkuptrue% |
|
184 |
% |
|
28635 | 185 |
\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}% |
28447 | 186 |
} |
187 |
\isamarkuptrue% |
|
188 |
% |
|
189 |
\begin{isamarkuptext}% |
|
28561 | 190 |
Consider the following function and its corresponding |
28447 | 191 |
SML code:% |
192 |
\end{isamarkuptext}% |
|
193 |
\isamarkuptrue% |
|
194 |
% |
|
28564 | 195 |
\isadelimquote |
28447 | 196 |
% |
28564 | 197 |
\endisadelimquote |
28447 | 198 |
% |
28564 | 199 |
\isatagquote |
28447 | 200 |
\isacommand{primrec}\isamarkupfalse% |
201 |
\ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
202 |
\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}% |
|
28564 | 203 |
\endisatagquote |
204 |
{\isafoldquote}% |
|
28447 | 205 |
% |
28564 | 206 |
\isadelimquote |
28447 | 207 |
% |
28564 | 208 |
\endisadelimquote |
28447 | 209 |
% |
210 |
\isadeliminvisible |
|
211 |
% |
|
212 |
\endisadeliminvisible |
|
213 |
% |
|
214 |
\isataginvisible |
|
215 |
% |
|
216 |
\endisataginvisible |
|
217 |
{\isafoldinvisible}% |
|
218 |
% |
|
219 |
\isadeliminvisible |
|
220 |
% |
|
221 |
\endisadeliminvisible |
|
222 |
% |
|
28564 | 223 |
\isadelimquote |
28447 | 224 |
% |
28564 | 225 |
\endisadelimquote |
28447 | 226 |
% |
28564 | 227 |
\isatagquote |
28447 | 228 |
% |
229 |
\begin{isamarkuptext}% |
|
28727 | 230 |
\isatypewriter% |
28447 | 231 |
\noindent% |
28714 | 232 |
\hspace*{0pt}structure Example = \\ |
233 |
\hspace*{0pt}struct\\ |
|
234 |
\hspace*{0pt}\\ |
|
30121 | 235 |
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
28714 | 236 |
\hspace*{0pt}\\ |
30121 | 237 |
\hspace*{0pt}datatype boola = True | False;\\ |
28714 | 238 |
\hspace*{0pt}\\ |
239 |
\hspace*{0pt}fun anda x True = x\\ |
|
240 |
\hspace*{0pt} ~| anda x False = False\\ |
|
241 |
\hspace*{0pt} ~| anda True x = x\\ |
|
242 |
\hspace*{0pt} ~| anda False x = False;\\ |
|
243 |
\hspace*{0pt}\\ |
|
244 |
\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ |
|
245 |
\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\ |
|
246 |
\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ |
|
247 |
\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\ |
|
248 |
\hspace*{0pt}\\ |
|
29297 | 249 |
\hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\ |
28714 | 250 |
\hspace*{0pt}\\ |
29297 | 251 |
\hspace*{0pt}end;~(*struct Example*)% |
28447 | 252 |
\end{isamarkuptext}% |
253 |
\isamarkuptrue% |
|
254 |
% |
|
28564 | 255 |
\endisatagquote |
256 |
{\isafoldquote}% |
|
28447 | 257 |
% |
28564 | 258 |
\isadelimquote |
28447 | 259 |
% |
28564 | 260 |
\endisadelimquote |
28447 | 261 |
% |
262 |
\begin{isamarkuptext}% |
|
263 |
\noindent Though this is correct code, it is a little bit unsatisfactory: |
|
264 |
boolean values and operators are materialised as distinguished |
|
265 |
entities with have nothing to do with the SML-built-in notion |
|
266 |
of \qt{bool}. This results in less readable code; |
|
267 |
additionally, eager evaluation may cause programs to |
|
268 |
loop or break which would perfectly terminate when |
|
269 |
the existing SML \verb|bool| would be used. To map |
|
270 |
the HOL \isa{bool} on SML \verb|bool|, we may use |
|
271 |
\qn{custom serialisations}:% |
|
272 |
\end{isamarkuptext}% |
|
273 |
\isamarkuptrue% |
|
274 |
% |
|
28564 | 275 |
\isadelimquotett |
28447 | 276 |
% |
28564 | 277 |
\endisadelimquotett |
28447 | 278 |
% |
28564 | 279 |
\isatagquotett |
28447 | 280 |
\isacommand{code{\isacharunderscore}type}\isamarkupfalse% |
281 |
\ bool\isanewline |
|
282 |
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
283 |
\isacommand{code{\isacharunderscore}const}\isamarkupfalse% |
|
284 |
\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline |
|
285 |
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}% |
|
28564 | 286 |
\endisatagquotett |
287 |
{\isafoldquotett}% |
|
28447 | 288 |
% |
28564 | 289 |
\isadelimquotett |
28447 | 290 |
% |
28564 | 291 |
\endisadelimquotett |
28447 | 292 |
% |
293 |
\begin{isamarkuptext}% |
|
294 |
\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor |
|
295 |
as arguments together with a list of custom serialisations. |
|
296 |
Each custom serialisation starts with a target language |
|
297 |
identifier followed by an expression, which during |
|
298 |
code serialisation is inserted whenever the type constructor |
|
299 |
would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements |
|
300 |
the corresponding mechanism. Each ``\verb|_|'' in |
|
301 |
a serialisation expression is treated as a placeholder |
|
302 |
for the type constructor's (the constant's) arguments.% |
|
303 |
\end{isamarkuptext}% |
|
304 |
\isamarkuptrue% |
|
305 |
% |
|
28564 | 306 |
\isadelimquote |
28447 | 307 |
% |
28564 | 308 |
\endisadelimquote |
28447 | 309 |
% |
28564 | 310 |
\isatagquote |
28447 | 311 |
% |
312 |
\begin{isamarkuptext}% |
|
28727 | 313 |
\isatypewriter% |
28447 | 314 |
\noindent% |
28714 | 315 |
\hspace*{0pt}structure Example = \\ |
316 |
\hspace*{0pt}struct\\ |
|
317 |
\hspace*{0pt}\\ |
|
30121 | 318 |
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
28714 | 319 |
\hspace*{0pt}\\ |
320 |
\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ |
|
321 |
\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\ |
|
322 |
\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ |
|
323 |
\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ |
|
324 |
\hspace*{0pt}\\ |
|
29297 | 325 |
\hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\ |
28714 | 326 |
\hspace*{0pt}\\ |
29297 | 327 |
\hspace*{0pt}end;~(*struct Example*)% |
28447 | 328 |
\end{isamarkuptext}% |
329 |
\isamarkuptrue% |
|
330 |
% |
|
28564 | 331 |
\endisatagquote |
332 |
{\isafoldquote}% |
|
28447 | 333 |
% |
28564 | 334 |
\isadelimquote |
28447 | 335 |
% |
28564 | 336 |
\endisadelimquote |
28447 | 337 |
% |
338 |
\begin{isamarkuptext}% |
|
339 |
\noindent This still is not perfect: the parentheses |
|
340 |
around the \qt{andalso} expression are superfluous. |
|
28593 | 341 |
Though the serialiser |
28447 | 342 |
by no means attempts to imitate the rich Isabelle syntax |
343 |
framework, it provides some common idioms, notably |
|
344 |
associative infixes with precedences which may be used here:% |
|
345 |
\end{isamarkuptext}% |
|
346 |
\isamarkuptrue% |
|
347 |
% |
|
28564 | 348 |
\isadelimquotett |
28447 | 349 |
% |
28564 | 350 |
\endisadelimquotett |
28447 | 351 |
% |
28564 | 352 |
\isatagquotett |
28447 | 353 |
\isacommand{code{\isacharunderscore}const}\isamarkupfalse% |
354 |
\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline |
|
355 |
\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}% |
|
28564 | 356 |
\endisatagquotett |
357 |
{\isafoldquotett}% |
|
28447 | 358 |
% |
28564 | 359 |
\isadelimquotett |
28447 | 360 |
% |
28564 | 361 |
\endisadelimquotett |
28447 | 362 |
% |
28564 | 363 |
\isadelimquote |
28447 | 364 |
% |
28564 | 365 |
\endisadelimquote |
28447 | 366 |
% |
28564 | 367 |
\isatagquote |
28447 | 368 |
% |
369 |
\begin{isamarkuptext}% |
|
28727 | 370 |
\isatypewriter% |
28447 | 371 |
\noindent% |
28714 | 372 |
\hspace*{0pt}structure Example = \\ |
373 |
\hspace*{0pt}struct\\ |
|
374 |
\hspace*{0pt}\\ |
|
30121 | 375 |
\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
28714 | 376 |
\hspace*{0pt}\\ |
377 |
\hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\ |
|
378 |
\hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\ |
|
379 |
\hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\ |
|
380 |
\hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\ |
|
381 |
\hspace*{0pt}\\ |
|
29297 | 382 |
\hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\ |
28714 | 383 |
\hspace*{0pt}\\ |
29297 | 384 |
\hspace*{0pt}end;~(*struct Example*)% |
28447 | 385 |
\end{isamarkuptext}% |
386 |
\isamarkuptrue% |
|
387 |
% |
|
28564 | 388 |
\endisatagquote |
389 |
{\isafoldquote}% |
|
28447 | 390 |
% |
28564 | 391 |
\isadelimquote |
28447 | 392 |
% |
28564 | 393 |
\endisadelimquote |
28447 | 394 |
% |
395 |
\begin{isamarkuptext}% |
|
28561 | 396 |
\noindent The attentive reader may ask how we assert that no generated |
397 |
code will accidentally overwrite. For this reason the serialiser has |
|
398 |
an internal table of identifiers which have to be avoided to be used |
|
399 |
for new declarations. Initially, this table typically contains the |
|
400 |
keywords of the target language. It can be extended manually, thus avoiding |
|
401 |
accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:% |
|
402 |
\end{isamarkuptext}% |
|
403 |
\isamarkuptrue% |
|
404 |
% |
|
28564 | 405 |
\isadelimquote |
28561 | 406 |
% |
28564 | 407 |
\endisadelimquote |
28561 | 408 |
% |
28564 | 409 |
\isatagquote |
28561 | 410 |
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse% |
28601 | 411 |
\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso% |
28564 | 412 |
\endisatagquote |
413 |
{\isafoldquote}% |
|
28561 | 414 |
% |
28564 | 415 |
\isadelimquote |
28561 | 416 |
% |
28564 | 417 |
\endisadelimquote |
28561 | 418 |
% |
419 |
\begin{isamarkuptext}% |
|
28447 | 420 |
\noindent Next, we try to map HOL pairs to SML pairs, using the |
421 |
infix ``\verb|*|'' type constructor and parentheses:% |
|
422 |
\end{isamarkuptext}% |
|
423 |
\isamarkuptrue% |
|
424 |
% |
|
425 |
\isadeliminvisible |
|
426 |
% |
|
427 |
\endisadeliminvisible |
|
428 |
% |
|
429 |
\isataginvisible |
|
430 |
% |
|
431 |
\endisataginvisible |
|
432 |
{\isafoldinvisible}% |
|
433 |
% |
|
434 |
\isadeliminvisible |
|
435 |
% |
|
436 |
\endisadeliminvisible |
|
437 |
% |
|
28564 | 438 |
\isadelimquotett |
28447 | 439 |
% |
28564 | 440 |
\endisadelimquotett |
28447 | 441 |
% |
28564 | 442 |
\isatagquotett |
28447 | 443 |
\isacommand{code{\isacharunderscore}type}\isamarkupfalse% |
444 |
\ {\isacharasterisk}\isanewline |
|
445 |
\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
446 |
\isacommand{code{\isacharunderscore}const}\isamarkupfalse% |
|
447 |
\ Pair\isanewline |
|
448 |
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}% |
|
28564 | 449 |
\endisatagquotett |
450 |
{\isafoldquotett}% |
|
28447 | 451 |
% |
28564 | 452 |
\isadelimquotett |
28447 | 453 |
% |
28564 | 454 |
\endisadelimquotett |
28447 | 455 |
% |
456 |
\begin{isamarkuptext}% |
|
28593 | 457 |
\noindent The initial bang ``\verb|!|'' tells the serialiser |
28561 | 458 |
never to put |
28447 | 459 |
parentheses around the whole expression (they are already present), |
460 |
while the parentheses around argument place holders |
|
461 |
tell not to put parentheses around the arguments. |
|
462 |
The slash ``\verb|/|'' (followed by arbitrary white space) |
|
463 |
inserts a space which may be used as a break if necessary |
|
464 |
during pretty printing. |
|
465 |
||
466 |
These examples give a glimpse what mechanisms |
|
467 |
custom serialisations provide; however their usage |
|
468 |
requires careful thinking in order not to introduce |
|
469 |
inconsistencies -- or, in other words: |
|
470 |
custom serialisations are completely axiomatic. |
|
471 |
||
472 |
A further noteworthy details is that any special |
|
473 |
character in a custom serialisation may be quoted |
|
474 |
using ``\verb|'|''; thus, in |
|
475 |
``\verb|fn '_ => _|'' the first |
|
476 |
``\verb|_|'' is a proper underscore while the |
|
28561 | 477 |
second ``\verb|_|'' is a placeholder.% |
28447 | 478 |
\end{isamarkuptext}% |
479 |
\isamarkuptrue% |
|
480 |
% |
|
481 |
\isamarkupsubsection{\isa{Haskell} serialisation% |
|
482 |
} |
|
483 |
\isamarkuptrue% |
|
484 |
% |
|
485 |
\begin{isamarkuptext}% |
|
486 |
For convenience, the default |
|
487 |
\isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to |
|
488 |
its counterpart in \isa{Haskell}, giving custom serialisations |
|
489 |
for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation |
|
490 |
\isa{eq{\isacharunderscore}class{\isachardot}eq}% |
|
491 |
\end{isamarkuptext}% |
|
492 |
\isamarkuptrue% |
|
493 |
% |
|
28564 | 494 |
\isadelimquotett |
28447 | 495 |
% |
28564 | 496 |
\endisadelimquotett |
28447 | 497 |
% |
28564 | 498 |
\isatagquotett |
28447 | 499 |
\isacommand{code{\isacharunderscore}class}\isamarkupfalse% |
500 |
\ eq\isanewline |
|
28714 | 501 |
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline |
28447 | 502 |
\isanewline |
503 |
\isacommand{code{\isacharunderscore}const}\isamarkupfalse% |
|
504 |
\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline |
|
505 |
\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}% |
|
28564 | 506 |
\endisatagquotett |
507 |
{\isafoldquotett}% |
|
28447 | 508 |
% |
28564 | 509 |
\isadelimquotett |
28447 | 510 |
% |
28564 | 511 |
\endisadelimquotett |
28447 | 512 |
% |
513 |
\begin{isamarkuptext}% |
|
514 |
\noindent A problem now occurs whenever a type which |
|
515 |
is an instance of \isa{eq} in \isa{HOL} is mapped |
|
516 |
on a \isa{Haskell}-built-in type which is also an instance |
|
517 |
of \isa{Haskell} \isa{Eq}:% |
|
518 |
\end{isamarkuptext}% |
|
519 |
\isamarkuptrue% |
|
520 |
% |
|
28564 | 521 |
\isadelimquote |
28447 | 522 |
% |
28564 | 523 |
\endisadelimquote |
28447 | 524 |
% |
28564 | 525 |
\isatagquote |
28447 | 526 |
\isacommand{typedecl}\isamarkupfalse% |
527 |
\ bar\isanewline |
|
528 |
\isanewline |
|
529 |
\isacommand{instantiation}\isamarkupfalse% |
|
530 |
\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline |
|
531 |
\isakeyword{begin}\isanewline |
|
532 |
\isanewline |
|
533 |
\isacommand{definition}\isamarkupfalse% |
|
534 |
\ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline |
|
535 |
\isanewline |
|
536 |
\isacommand{instance}\isamarkupfalse% |
|
537 |
\ \isacommand{by}\isamarkupfalse% |
|
538 |
\ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline |
|
539 |
\isanewline |
|
540 |
\isacommand{end}\isamarkupfalse% |
|
541 |
% |
|
28564 | 542 |
\endisatagquote |
543 |
{\isafoldquote}% |
|
28447 | 544 |
% |
28564 | 545 |
\isadelimquote |
28447 | 546 |
% |
28564 | 547 |
\endisadelimquote |
28447 | 548 |
% |
28564 | 549 |
\isadelimquotett |
30880 | 550 |
\ % |
28564 | 551 |
\endisadelimquotett |
28447 | 552 |
% |
28564 | 553 |
\isatagquotett |
28447 | 554 |
\isacommand{code{\isacharunderscore}type}\isamarkupfalse% |
555 |
\ bar\isanewline |
|
556 |
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}% |
|
28564 | 557 |
\endisatagquotett |
558 |
{\isafoldquotett}% |
|
28447 | 559 |
% |
28564 | 560 |
\isadelimquotett |
28447 | 561 |
% |
28564 | 562 |
\endisadelimquotett |
28447 | 563 |
% |
564 |
\begin{isamarkuptext}% |
|
565 |
\noindent The code generator would produce |
|
28593 | 566 |
an additional instance, which of course is rejected by the \isa{Haskell} |
28447 | 567 |
compiler. |
568 |
To suppress this additional instance, use |
|
569 |
\isa{code{\isacharunderscore}instance}:% |
|
570 |
\end{isamarkuptext}% |
|
571 |
\isamarkuptrue% |
|
572 |
% |
|
28564 | 573 |
\isadelimquotett |
28447 | 574 |
% |
28564 | 575 |
\endisadelimquotett |
28447 | 576 |
% |
28564 | 577 |
\isatagquotett |
28447 | 578 |
\isacommand{code{\isacharunderscore}instance}\isamarkupfalse% |
579 |
\ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline |
|
580 |
\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}% |
|
28564 | 581 |
\endisatagquotett |
582 |
{\isafoldquotett}% |
|
28447 | 583 |
% |
28564 | 584 |
\isadelimquotett |
28447 | 585 |
% |
28564 | 586 |
\endisadelimquotett |
28561 | 587 |
% |
28635 | 588 |
\isamarkupsubsection{Enhancing the target language context \label{sec:include}% |
28561 | 589 |
} |
590 |
\isamarkuptrue% |
|
591 |
% |
|
592 |
\begin{isamarkuptext}% |
|
28593 | 593 |
In rare cases it is necessary to \emph{enrich} the context of a |
28561 | 594 |
target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} |
595 |
command:% |
|
596 |
\end{isamarkuptext}% |
|
597 |
\isamarkuptrue% |
|
598 |
% |
|
28564 | 599 |
\isadelimquotett |
28561 | 600 |
% |
28564 | 601 |
\endisadelimquotett |
28561 | 602 |
% |
28564 | 603 |
\isatagquotett |
28561 | 604 |
\isacommand{code{\isacharunderscore}include}\isamarkupfalse% |
605 |
\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline |
|
606 |
{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline |
|
28447 | 607 |
\isanewline |
28561 | 608 |
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse% |
609 |
\ Haskell\ Errno% |
|
28564 | 610 |
\endisatagquotett |
611 |
{\isafoldquotett}% |
|
28561 | 612 |
% |
28564 | 613 |
\isadelimquotett |
28561 | 614 |
% |
28564 | 615 |
\endisadelimquotett |
28561 | 616 |
% |
617 |
\begin{isamarkuptext}% |
|
618 |
\noindent Such named \isa{include}s are then prepended to every generated code. |
|
619 |
Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves |
|
620 |
with respect to a particular target language.% |
|
621 |
\end{isamarkuptext}% |
|
622 |
\isamarkuptrue% |
|
28447 | 623 |
% |
624 |
\isadelimtheory |
|
625 |
% |
|
626 |
\endisadelimtheory |
|
627 |
% |
|
628 |
\isatagtheory |
|
629 |
\isacommand{end}\isamarkupfalse% |
|
630 |
% |
|
631 |
\endisatagtheory |
|
632 |
{\isafoldtheory}% |
|
633 |
% |
|
634 |
\isadelimtheory |
|
635 |
% |
|
636 |
\endisadelimtheory |
|
637 |
\isanewline |
|
638 |
\end{isabellebody}% |
|
639 |
%%% Local Variables: |
|
640 |
%%% mode: latex |
|
641 |
%%% TeX-master: "root" |
|
642 |
%%% End: |