53 *} |
53 *} |
54 |
54 |
55 subsection {* The adaption principle *} |
55 subsection {* The adaption principle *} |
56 |
56 |
57 text {* |
57 text {* |
58 \begin{tikzpicture} |
58 The following figure illustrates what \qt{adaption} is conceptually |
59 \draw (0, 0) circle (1cm); |
59 supposed to be: |
60 \draw (0.5, 0) circle (0.5cm); |
60 |
61 \draw (0, 0.5) circle (0.5cm); |
61 \begin{figure}[here] |
62 \draw (-0.5, 0) circle (0.5cm); |
62 \begin{tikzpicture}[scale = 0.5] |
63 \draw (0, -0.5) circle (0.5cm); |
63 \tikzstyle water=[color = blue, thick] |
64 \end{tikzpicture} |
64 \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white] |
|
65 \tikzstyle process=[color = green, semithick, ->] |
|
66 \tikzstyle adaption=[color = red, semithick, ->] |
|
67 \tikzstyle target=[color = black] |
|
68 \foreach \x in {0, ..., 24} |
|
69 \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin |
|
70 + (0.25, -0.25) cos + (0.25, 0.25); |
|
71 \draw[style=ice] (1, 0) -- |
|
72 (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle; |
|
73 \draw[style=ice] (9, 0) -- |
|
74 (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle; |
|
75 \draw[style=ice] (15, -6) -- |
|
76 (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle; |
|
77 \draw[style=process] |
|
78 (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3); |
|
79 \draw[style=process] |
|
80 (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3); |
|
81 \node (adaption) at (11, -2) [style=adaption] {adaption}; |
|
82 \node at (19, 3) [rotate=90] {generated}; |
|
83 \node at (19.5, -5) {language}; |
|
84 \node at (19.5, -3) {library}; |
|
85 \node (includes) at (19.5, -1) {includes}; |
|
86 \node (reserved) at (16.5, -3) [rotate=71.57] {reserved}; |
|
87 \draw[style=process] |
|
88 (includes) -- (serialisation); |
|
89 \draw[style=process] |
|
90 (reserved) -- (serialisation); |
|
91 \draw[style=adaption] |
|
92 (adaption) -- (serialisation); |
|
93 \draw[style=adaption] |
|
94 (adaption) -- (includes); |
|
95 \draw[style=adaption] |
|
96 (adaption) -- (reserved); |
|
97 \end{tikzpicture} |
|
98 \caption{The adaption principle} |
|
99 \label{fig:adaption} |
|
100 \end{figure} |
|
101 |
|
102 \noindent In the tame view, code generation acts as broker between |
|
103 @{text logic}, @{text "intermediate language"} and |
|
104 @{text "target language"} by means of @{text translation} and |
|
105 @{text serialisation}; for the latter, the serialiser has to observe |
|
106 the structure of the @{text language} itself plus some @{text reserved} |
|
107 keywords which have to be avoided for generated code. |
|
108 However, if you consider @{text adaption} mechanisms, the code generated |
|
109 by the serializer is just the tip of the iceberg: |
|
110 |
|
111 \begin{itemize} |
|
112 \item parametrise @{text serialisation} |
|
113 \item @{text library} @{text reserved} |
|
114 \item @{text "includes"} @{text reserved} |
|
115 \end{itemize} |
65 *} |
116 *} |
66 |
117 |
67 subsection {* Common adaption cases *} |
118 subsection {* Common adaption cases *} |
68 |
119 |
69 text {* |
120 text {* |
178 for new declarations. Initially, this table typically contains the |
229 for new declarations. Initially, this table typically contains the |
179 keywords of the target language. It can be extended manually, thus avoiding |
230 keywords of the target language. It can be extended manually, thus avoiding |
180 accidental overwrites, using the @{command "code_reserved"} command: |
231 accidental overwrites, using the @{command "code_reserved"} command: |
181 *} |
232 *} |
182 |
233 |
183 code_reserved %quote "SML " bool true false andalso |
234 code_reserved %quote "\<SML>" bool true false andalso |
184 |
235 |
185 text {* |
236 text {* |
186 \noindent Next, we try to map HOL pairs to SML pairs, using the |
237 \noindent Next, we try to map HOL pairs to SML pairs, using the |
187 infix ``@{verbatim "*"}'' type constructor and parentheses: |
238 infix ``@{verbatim "*"}'' type constructor and parentheses: |
188 *} |
239 *} |