3 \def\isabellecontext{Adaption}%
10 \isacommand{theory}\isamarkupfalse%
12 \isakeyword{imports}\ Setup\isanewline
28 \isacommand{setup}\isamarkupfalse%
29 \ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
37 \isamarkupsection{Adaption to target languages \label{sec:adaption}%
41 \isamarkupsubsection{Adapting code generation%
45 \begin{isamarkuptext}%
46 The aspects of code generation introduced so far have two aspects
50 \item They act uniformly, without reference to a specific
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
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
60 in a way which accommodates \qt{already existing} ingredients of
61 a target language environment, for three reasons:
64 \item improving readability and aesthetics of generated code
65 \item gaining efficiency
66 \item interface with language parts which have no direct counterpart
67 in \isa{HOL} (say, imperative data structures)
70 \noindent Generally, you should avoid using those features yourself
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
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.
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.%
90 \isamarkupsubsection{The adaption principle%
94 \begin{isamarkuptext}%
95 The following figure illustrates what \qt{adaption} is conceptually
99 \begin{tikzpicture}[scale = 0.5]
100 \tikzstyle water=[color = blue, thick]
101 \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
102 \tikzstyle process=[color = green, semithick, ->]
103 \tikzstyle adaption=[color = red, semithick, ->]
104 \tikzstyle target=[color = black]
105 \foreach \x in {0, ..., 24}
106 \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
107 + (0.25, -0.25) cos + (0.25, 0.25);
108 \draw[style=ice] (1, 0) --
109 (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
110 \draw[style=ice] (9, 0) --
111 (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
112 \draw[style=ice] (15, -6) --
113 (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
115 (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
117 (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
118 \node (adaption) at (11, -2) [style=adaption] {adaption};
119 \node at (19, 3) [rotate=90] {generated};
120 \node at (19.5, -5) {language};
121 \node at (19.5, -3) {library};
122 \node (includes) at (19.5, -1) {includes};
123 \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
125 (includes) -- (serialisation);
127 (reserved) -- (serialisation);
128 \draw[style=adaption]
129 (adaption) -- (serialisation);
130 \draw[style=adaption]
131 (adaption) -- (includes);
132 \draw[style=adaption]
133 (adaption) -- (reserved);
135 \caption{The adaption principle}
139 \noindent In the tame view, code generation acts as broker between
140 \isa{logic}, \isa{intermediate\ language} and
141 \isa{target\ language} by means of \isa{translation} and
142 \isa{serialisation}; for the latter, the serialiser has to observe
143 the structure of the \isa{language} itself plus some \isa{reserved}
144 keywords which have to be avoided for generated code.
145 However, if you consider \isa{adaption} mechanisms, the code generated
146 by the serializer is just the tip of the iceberg:
149 \item \isa{serialisation} can be \emph{parametrised} such that
150 logical entities are mapped to target-specific ones
151 (e.g. target-specific list syntax,
152 see also \secref{sec:adaption_mechanisms})
153 \item Such parametrisations can involve references to a
154 target-specific standard \isa{library} (e.g. using
155 the \isa{Haskell} \verb|Maybe| type instead
156 of the \isa{HOL} \isa{option} type);
157 if such are used, the corresponding identifiers
158 (in our example, \verb|Maybe|, \verb|Nothing|
159 and \verb|Just|) also have to be considered \isa{reserved}.
160 \item Even more, the user can enrich the library of the
161 target-language by providing code snippets
162 (\qt{\isa{includes}}) which are prepended to
163 any generated code (see \secref{sec:include}); this typically
164 also involves further \isa{reserved} identifiers.
167 \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
168 have to act consistently; it is at the discretion of the user
169 to take care for this.%
173 \isamarkupsubsection{Common adaption patterns%
177 \begin{isamarkuptext}%
178 The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
180 which should be suitable for most applications. Common extensions
181 and modifications are available by certain theories of the \isa{HOL}
182 library; beside being useful in applications, they may serve
183 as a tutorial for customising the code generator setup (see below
184 \secref{sec:adaption_mechanisms}).
188 \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
189 integer literals in target languages.
190 \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by
191 character literals in target languages.
192 \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
193 but also offers treatment of character codes; includes
194 \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
195 \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
196 which in general will result in higher efficiency; pattern
197 matching with \isa{{\isadigit{0}}} / \isa{Suc}
198 is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
199 and \hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}.
200 \item[\hyperlink{theory.Code-Index}{\mbox{\isa{Code{\isacharunderscore}Index}}}] provides an additional datatype
201 \isa{index} which is mapped to target-language built-in integers.
202 Useful for code setups which involve e.g. indexing of
203 target-language arrays.
204 \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype
205 \isa{message{\isacharunderscore}string} which is isomorphic to strings;
206 \isa{message{\isacharunderscore}string}s are mapped to target-language strings.
207 Useful for code setups which involve e.g. printing (error) messages.
212 When importing any of these theories, they should form the last
213 items in an import list. Since these theories adapt the
214 code generator setup in a non-conservative fashion,
215 strange effects may occur otherwise.
220 \isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%
224 \begin{isamarkuptext}%
225 Consider the following function and its corresponding
235 \isacommand{primrec}\isamarkupfalse%
236 \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
237 \ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
247 \endisadeliminvisible
256 \endisadeliminvisible
264 \begin{isamarkuptext}%
267 \hspace*{0pt}structure Example = \\
268 \hspace*{0pt}struct\\
270 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
272 \hspace*{0pt}datatype boola = True | False;\\
274 \hspace*{0pt}fun anda x True = x\\
275 \hspace*{0pt} ~| anda x False = False\\
276 \hspace*{0pt} ~| anda True x = x\\
277 \hspace*{0pt} ~| anda False x = False;\\
279 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
280 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = False\\
281 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
282 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = True;\\
284 \hspace*{0pt}fun in{\char95}interval (k,~l) n = anda (less{\char95}eq{\char95}nat k n) (less{\char95}eq{\char95}nat n l);\\
286 \hspace*{0pt}end;~(*struct Example*)%
297 \begin{isamarkuptext}%
298 \noindent Though this is correct code, it is a little bit unsatisfactory:
299 boolean values and operators are materialised as distinguished
300 entities with have nothing to do with the SML-built-in notion
301 of \qt{bool}. This results in less readable code;
302 additionally, eager evaluation may cause programs to
303 loop or break which would perfectly terminate when
304 the existing SML \verb|bool| would be used. To map
305 the HOL \isa{bool} on SML \verb|bool|, we may use
306 \qn{custom serialisations}:%
315 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
317 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
318 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
319 \ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
320 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
328 \begin{isamarkuptext}%
329 \noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
330 as arguments together with a list of custom serialisations.
331 Each custom serialisation starts with a target language
332 identifier followed by an expression, which during
333 code serialisation is inserted whenever the type constructor
334 would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
335 the corresponding mechanism. Each ``\verb|_|'' in
336 a serialisation expression is treated as a placeholder
337 for the type constructor's (the constant's) arguments.%
347 \begin{isamarkuptext}%
350 \hspace*{0pt}structure Example = \\
351 \hspace*{0pt}struct\\
353 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
355 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
356 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
357 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
358 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
360 \hspace*{0pt}fun in{\char95}interval (k,~l) n = (less{\char95}eq{\char95}nat k n) andalso (less{\char95}eq{\char95}nat n l);\\
362 \hspace*{0pt}end;~(*struct Example*)%
373 \begin{isamarkuptext}%
374 \noindent This still is not perfect: the parentheses
375 around the \qt{andalso} expression are superfluous.
376 Though the serialiser
377 by no means attempts to imitate the rich Isabelle syntax
378 framework, it provides some common idioms, notably
379 associative infixes with precedences which may be used here:%
388 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
389 \ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
390 \ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
404 \begin{isamarkuptext}%
407 \hspace*{0pt}structure Example = \\
408 \hspace*{0pt}struct\\
410 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
412 \hspace*{0pt}fun less{\char95}nat m (Suc n) = less{\char95}eq{\char95}nat m n\\
413 \hspace*{0pt} ~| less{\char95}nat n Zero{\char95}nat = false\\
414 \hspace*{0pt}and less{\char95}eq{\char95}nat (Suc m) n = less{\char95}nat m n\\
415 \hspace*{0pt} ~| less{\char95}eq{\char95}nat Zero{\char95}nat n = true;\\
417 \hspace*{0pt}fun in{\char95}interval (k,~l) n = less{\char95}eq{\char95}nat k n andalso less{\char95}eq{\char95}nat n l;\\
419 \hspace*{0pt}end;~(*struct Example*)%
430 \begin{isamarkuptext}%
431 \noindent The attentive reader may ask how we assert that no generated
432 code will accidentally overwrite. For this reason the serialiser has
433 an internal table of identifiers which have to be avoided to be used
434 for new declarations. Initially, this table typically contains the
435 keywords of the target language. It can be extended manually, thus avoiding
436 accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
445 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
446 \ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
454 \begin{isamarkuptext}%
455 \noindent Next, we try to map HOL pairs to SML pairs, using the
456 infix ``\verb|*|'' type constructor and parentheses:%
462 \endisadeliminvisible
471 \endisadeliminvisible
478 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
479 \ {\isacharasterisk}\isanewline
480 \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
481 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
483 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
491 \begin{isamarkuptext}%
492 \noindent The initial bang ``\verb|!|'' tells the serialiser
494 parentheses around the whole expression (they are already present),
495 while the parentheses around argument place holders
496 tell not to put parentheses around the arguments.
497 The slash ``\verb|/|'' (followed by arbitrary white space)
498 inserts a space which may be used as a break if necessary
499 during pretty printing.
501 These examples give a glimpse what mechanisms
502 custom serialisations provide; however their usage
503 requires careful thinking in order not to introduce
504 inconsistencies -- or, in other words:
505 custom serialisations are completely axiomatic.
507 A further noteworthy details is that any special
508 character in a custom serialisation may be quoted
509 using ``\verb|'|''; thus, in
510 ``\verb|fn '_ => _|'' the first
511 ``\verb|_|'' is a proper underscore while the
512 second ``\verb|_|'' is a placeholder.%
516 \isamarkupsubsection{\isa{Haskell} serialisation%
520 \begin{isamarkuptext}%
521 For convenience, the default
522 \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
523 its counterpart in \isa{Haskell}, giving custom serialisations
524 for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
525 \isa{eq{\isacharunderscore}class{\isachardot}eq}%
534 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
536 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
538 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
539 \ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
540 \ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
548 \begin{isamarkuptext}%
549 \noindent A problem now occurs whenever a type which
550 is an instance of \isa{eq} in \isa{HOL} is mapped
551 on a \isa{Haskell}-built-in type which is also an instance
552 of \isa{Haskell} \isa{Eq}:%
561 \isacommand{typedecl}\isamarkupfalse%
564 \isacommand{instantiation}\isamarkupfalse%
565 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
566 \isakeyword{begin}\isanewline
568 \isacommand{definition}\isamarkupfalse%
569 \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}x{\isasymColon}bar{\isacharparenright}\ y\ {\isasymlongleftrightarrow}\ x\ {\isacharequal}\ y{\isachardoublequoteclose}\isanewline
571 \isacommand{instance}\isamarkupfalse%
572 \ \isacommand{by}\isamarkupfalse%
573 \ default\ {\isacharparenleft}simp\ add{\isacharcolon}\ eq{\isacharunderscore}bar{\isacharunderscore}def{\isacharparenright}\isanewline
575 \isacommand{end}\isamarkupfalse%
591 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
593 \ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
601 \begin{isamarkuptext}%
602 \noindent The code generator would produce
603 an additional instance, which of course is rejected by the \isa{Haskell}
605 To suppress this additional instance, use
606 \isa{code{\isacharunderscore}instance}:%
615 \isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
616 \ bar\ {\isacharcolon}{\isacharcolon}\ eq\isanewline
617 \ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
625 \isamarkupsubsection{Enhancing the target language context \label{sec:include}%
629 \begin{isamarkuptext}%
630 In rare cases it is necessary to \emph{enrich} the context of a
631 target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
641 \isacommand{code{\isacharunderscore}include}\isamarkupfalse%
642 \ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
643 {\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
645 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
654 \begin{isamarkuptext}%
655 \noindent Such named \isa{include}s are then prepended to every generated code.
656 Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves
657 with respect to a particular target language.%
666 \isacommand{end}\isamarkupfalse%
678 %%% TeX-master: "root"