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