38560
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Evaluation}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
\isacommand{theory}\isamarkupfalse%
|
|
11 |
\ Evaluation\isanewline
|
|
12 |
\isakeyword{imports}\ Setup\isanewline
|
|
13 |
\isakeyword{begin}%
|
|
14 |
\endisatagtheory
|
|
15 |
{\isafoldtheory}%
|
|
16 |
%
|
|
17 |
\isadelimtheory
|
|
18 |
%
|
|
19 |
\endisadelimtheory
|
|
20 |
%
|
|
21 |
\isamarkupsection{Evaluation%
|
|
22 |
}
|
|
23 |
\isamarkuptrue%
|
|
24 |
%
|
|
25 |
\begin{isamarkuptext}%
|
39599
|
26 |
Recalling \secref{sec:principle}, code generation turns a system of
|
|
27 |
equations into a program with the \emph{same} equational semantics.
|
|
28 |
As a consequence, this program can be used as a \emph{rewrite
|
|
29 |
engine} for terms: rewriting a term \isa{t} using a program to a
|
|
30 |
term \isa{t{\isacharprime}} yields the theorems \isa{t\ {\isasymequiv}\ t{\isacharprime}}. This
|
|
31 |
application of code generation in the following is referred to as
|
|
32 |
\emph{evaluation}.%
|
38560
|
33 |
\end{isamarkuptext}%
|
|
34 |
\isamarkuptrue%
|
|
35 |
%
|
|
36 |
\isamarkupsubsection{Evaluation techniques%
|
|
37 |
}
|
|
38 |
\isamarkuptrue%
|
|
39 |
%
|
|
40 |
\begin{isamarkuptext}%
|
40350
|
41 |
The existing infrastructure provides a rich palette of evaluation
|
39599
|
42 |
techniques, each comprising different aspects:
|
|
43 |
|
|
44 |
\begin{description}
|
|
45 |
|
|
46 |
\item[Expressiveness.] Depending on how good symbolic computation
|
|
47 |
is supported, the class of terms which can be evaluated may be
|
|
48 |
bigger or smaller.
|
|
49 |
|
|
50 |
\item[Efficiency.] The more machine-near the technique, the
|
|
51 |
faster it is.
|
|
52 |
|
|
53 |
\item[Trustability.] Techniques which a huge (and also probably
|
|
54 |
more configurable infrastructure) are more fragile and less
|
|
55 |
trustable.
|
|
56 |
|
|
57 |
\end{description}%
|
38560
|
58 |
\end{isamarkuptext}%
|
|
59 |
\isamarkuptrue%
|
|
60 |
%
|
39599
|
61 |
\isamarkupsubsubsection{The simplifier (\isa{simp})%
|
38560
|
62 |
}
|
|
63 |
\isamarkuptrue%
|
|
64 |
%
|
|
65 |
\begin{isamarkuptext}%
|
39599
|
66 |
The simplest way for evaluation is just using the simplifier with
|
|
67 |
the original code equations of the underlying program. This gives
|
|
68 |
fully symbolic evaluation and highest trustablity, with the usual
|
|
69 |
performance of the simplifier. Note that for operations on abstract
|
|
70 |
datatypes (cf.~\secref{sec:invariant}), the original theorems as
|
|
71 |
given by the users are used, not the modified ones.%
|
38560
|
72 |
\end{isamarkuptext}%
|
|
73 |
\isamarkuptrue%
|
|
74 |
%
|
39599
|
75 |
\isamarkupsubsubsection{Normalization by evaluation (\isa{nbe})%
|
38560
|
76 |
}
|
|
77 |
\isamarkuptrue%
|
|
78 |
%
|
|
79 |
\begin{isamarkuptext}%
|
39599
|
80 |
Normalization by evaluation \cite{Aehlig-Haftmann-Nipkow:2008:nbe}
|
|
81 |
provides a comparably fast partially symbolic evaluation which
|
|
82 |
permits also normalization of functions and uninterpreted symbols;
|
|
83 |
the stack of code to be trusted is considerable.%
|
38560
|
84 |
\end{isamarkuptext}%
|
|
85 |
\isamarkuptrue%
|
|
86 |
%
|
39599
|
87 |
\isamarkupsubsubsection{Evaluation in ML (\isa{code})%
|
38560
|
88 |
}
|
|
89 |
\isamarkuptrue%
|
|
90 |
%
|
|
91 |
\begin{isamarkuptext}%
|
39599
|
92 |
Highest performance can be achieved by evaluation in ML, at the cost
|
|
93 |
of being restricted to ground results and a layered stack of code to
|
|
94 |
be trusted, including code generator configurations by the user.
|
|
95 |
|
|
96 |
Evaluation is carried out in a target language \emph{Eval} which
|
|
97 |
inherits from \emph{SML} but for convenience uses parts of the
|
|
98 |
Isabelle runtime environment. The soundness of computation carried
|
39609
|
99 |
out there depends crucially on the correctness of the code
|
39643
|
100 |
generator setup; this is one of the reasons why you should not use
|
39609
|
101 |
adaptation (see \secref{sec:adaptation}) frivolously.%
|
39599
|
102 |
\end{isamarkuptext}%
|
|
103 |
\isamarkuptrue%
|
|
104 |
%
|
|
105 |
\isamarkupsubsection{Aspects of evaluation%
|
|
106 |
}
|
|
107 |
\isamarkuptrue%
|
|
108 |
%
|
|
109 |
\begin{isamarkuptext}%
|
|
110 |
Each of the techniques can be combined with different aspects. The
|
|
111 |
most important distinction is between dynamic and static evaluation.
|
|
112 |
Dynamic evaluation takes the code generator configuration \qt{as it
|
|
113 |
is} at the point where evaluation is issued. Best example is the
|
|
114 |
\indexdef{}{command}{value}\hypertarget{command.value}{\hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}}} command which allows ad-hoc evaluation of
|
|
115 |
terms:%
|
38560
|
116 |
\end{isamarkuptext}%
|
|
117 |
\isamarkuptrue%
|
|
118 |
%
|
|
119 |
\isadelimquote
|
|
120 |
%
|
|
121 |
\endisadelimquote
|
|
122 |
%
|
|
123 |
\isatagquote
|
|
124 |
\isacommand{value}\isamarkupfalse%
|
|
125 |
\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}%
|
|
126 |
\endisatagquote
|
|
127 |
{\isafoldquote}%
|
|
128 |
%
|
|
129 |
\isadelimquote
|
|
130 |
%
|
|
131 |
\endisadelimquote
|
|
132 |
%
|
|
133 |
\begin{isamarkuptext}%
|
39599
|
134 |
\noindent By default \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} tries all available evaluation
|
|
135 |
techniques and prints the result of the first succeeding one. A particular
|
|
136 |
technique may be specified in square brackets, e.g.%
|
38560
|
137 |
\end{isamarkuptext}%
|
|
138 |
\isamarkuptrue%
|
|
139 |
%
|
|
140 |
\isadelimquote
|
|
141 |
%
|
|
142 |
\endisadelimquote
|
|
143 |
%
|
|
144 |
\isatagquote
|
39599
|
145 |
\isacommand{value}\isamarkupfalse%
|
|
146 |
\ {\isacharbrackleft}nbe{\isacharbrackright}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}%
|
38560
|
147 |
\endisatagquote
|
|
148 |
{\isafoldquote}%
|
|
149 |
%
|
|
150 |
\isadelimquote
|
|
151 |
%
|
|
152 |
\endisadelimquote
|
|
153 |
%
|
|
154 |
\begin{isamarkuptext}%
|
39599
|
155 |
Static evaluation freezes the code generator configuration at a
|
|
156 |
certain point and uses this context whenever evaluation is issued
|
|
157 |
later on. This is particularly appropriate for proof procedures
|
|
158 |
which use evaluation, since then the behaviour of evaluation is not
|
|
159 |
changed or even compromised later on by actions of the user.
|
|
160 |
|
|
161 |
As a technical complication, terms after evaluation in ML must be
|
|
162 |
turned into Isabelle's internal term representation again. Since
|
|
163 |
this is also configurable, it is never fully trusted. For this
|
|
164 |
reason, evaluation in ML comes with further aspects:
|
|
165 |
|
|
166 |
\begin{description}
|
|
167 |
|
|
168 |
\item[Plain evaluation.] A term is normalized using the provided
|
|
169 |
term reconstruction from ML to Isabelle; for applications which
|
|
170 |
do not need to be fully trusted.
|
|
171 |
|
|
172 |
\item[Property conversion.] Evaluates propositions; since these
|
|
173 |
are monomorphic, the term reconstruction is fixed once and for all
|
|
174 |
and therefore trustable.
|
|
175 |
|
|
176 |
\item[Conversion.] Evaluates an arbitrary term \isa{t} first
|
|
177 |
by plain evaluation and certifies the result \isa{t{\isacharprime}} by
|
|
178 |
checking the equation \isa{t\ {\isasymequiv}\ t{\isacharprime}} using property
|
|
179 |
conversion.
|
|
180 |
|
|
181 |
\end{description}
|
|
182 |
|
|
183 |
\noindent The picture is further complicated by the roles of
|
|
184 |
exceptions. Here three cases have to be distinguished:
|
|
185 |
|
|
186 |
\begin{itemize}
|
|
187 |
|
|
188 |
\item Evaluation of \isa{t} terminates with a result \isa{t{\isacharprime}}.
|
|
189 |
|
|
190 |
\item Evaluation of \isa{t} terminates which en exception
|
40350
|
191 |
indicating a pattern match failure or a non-implemented
|
39599
|
192 |
function. As sketched in \secref{sec:partiality}, this can be
|
|
193 |
interpreted as partiality.
|
|
194 |
|
39643
|
195 |
\item Evaluation raises any other kind of exception.
|
39599
|
196 |
|
|
197 |
\end{itemize}
|
|
198 |
|
|
199 |
\noindent For conversions, the first case yields the equation \isa{t\ {\isacharequal}\ t{\isacharprime}}, the second defaults to reflexivity \isa{t\ {\isacharequal}\ t}.
|
39643
|
200 |
Exceptions of the third kind are propagated to the user.
|
39599
|
201 |
|
|
202 |
By default return values of plain evaluation are optional, yielding
|
40350
|
203 |
\isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} in the
|
|
204 |
second, and propagating the exception in the third case. A strict
|
39599
|
205 |
variant of plain evaluation either yields \isa{t{\isacharprime}} or propagates
|
|
206 |
any exception, a liberal variant caputures any exception in a result
|
|
207 |
of type \isa{Exn{\isachardot}result}.
|
|
208 |
|
|
209 |
For property conversion (which coincides with conversion except for
|
|
210 |
evaluation in ML), methods are provided which solve a given goal by
|
|
211 |
evaluation.%
|
38560
|
212 |
\end{isamarkuptext}%
|
|
213 |
\isamarkuptrue%
|
|
214 |
%
|
39599
|
215 |
\isamarkupsubsection{Schematic overview%
|
38560
|
216 |
}
|
|
217 |
\isamarkuptrue%
|
|
218 |
%
|
|
219 |
\begin{isamarkuptext}%
|
39693
|
220 |
\newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont}
|
|
221 |
\fontsize{9pt}{12pt}\selectfont
|
|
222 |
\begin{tabular}{ll||c|c|c}
|
39599
|
223 |
& & \isa{simp} & \isa{nbe} & \isa{code} \tabularnewline \hline \hline
|
39693
|
224 |
\multirow{5}{1ex}{\rotatebox{90}{dynamic}}
|
|
225 |
& interactive evaluation
|
39599
|
226 |
& \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}simp{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}nbe{\isacharbrackright}} & \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} \isa{{\isacharbrackleft}code{\isacharbrackright}}
|
|
227 |
\tabularnewline
|
39693
|
228 |
& plain evaluation & & & \ttsize\verb|Code_Evaluation.dynamic_value| \tabularnewline \cline{2-5}
|
39599
|
229 |
& evaluation method & \hyperlink{method.code-simp}{\mbox{\isa{code{\isacharunderscore}simp}}} & \hyperlink{method.normalization}{\mbox{\isa{normalization}}} & \hyperlink{method.eval}{\mbox{\isa{eval}}} \tabularnewline
|
39693
|
230 |
& property conversion & & & \ttsize\verb|Code_Runtime.dynamic_holds_conv| \tabularnewline \cline{2-5}
|
|
231 |
& conversion & \ttsize\verb|Code_Simp.dynamic_eval_conv| & \ttsize\verb|Nbe.dynamic_eval_conv|
|
|
232 |
& \ttsize\verb|Code_Evaluation.dynamic_eval_conv| \tabularnewline \hline \hline
|
|
233 |
\multirow{3}{1ex}{\rotatebox{90}{static}}
|
|
234 |
& plain evaluation & & & \ttsize\verb|Code_Evaluation.static_value| \tabularnewline \cline{2-5}
|
39599
|
235 |
& property conversion & &
|
39693
|
236 |
& \ttsize\verb|Code_Runtime.static_holds_conv| \tabularnewline \cline{2-5}
|
|
237 |
& conversion & \ttsize\verb|Code_Simp.static_eval_conv|
|
|
238 |
& \ttsize\verb|Nbe.static_eval_conv|
|
|
239 |
& \ttsize\verb|Code_Evaluation.static_eval_conv|
|
39599
|
240 |
\end{tabular}%
|
|
241 |
\end{isamarkuptext}%
|
|
242 |
\isamarkuptrue%
|
|
243 |
%
|
|
244 |
\isamarkupsubsection{Intimate connection between logic and system runtime%
|
|
245 |
}
|
|
246 |
\isamarkuptrue%
|
|
247 |
%
|
|
248 |
\begin{isamarkuptext}%
|
39609
|
249 |
The toolbox of static evaluation conversions forms a reasonable base
|
|
250 |
to interweave generated code and system tools. However in some
|
|
251 |
situations more direct interaction is desirable.%
|
39599
|
252 |
\end{isamarkuptext}%
|
|
253 |
\isamarkuptrue%
|
|
254 |
%
|
39609
|
255 |
\isamarkupsubsubsection{Static embedding of generated code into system runtime -- the \isa{code} antiquotation%
|
39599
|
256 |
}
|
|
257 |
\isamarkuptrue%
|
|
258 |
%
|
|
259 |
\begin{isamarkuptext}%
|
39609
|
260 |
The \isa{code} antiquotation allows to include constants from
|
|
261 |
generated code directly into ML system code, as in the following toy
|
|
262 |
example:%
|
38560
|
263 |
\end{isamarkuptext}%
|
|
264 |
\isamarkuptrue%
|
|
265 |
%
|
|
266 |
\isadelimquote
|
|
267 |
%
|
|
268 |
\endisadelimquote
|
|
269 |
%
|
|
270 |
\isatagquote
|
|
271 |
\isacommand{datatype}\isamarkupfalse%
|
39745
|
272 |
\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
|
|
273 |
\endisatagquote
|
|
274 |
{\isafoldquote}%
|
|
275 |
%
|
|
276 |
\isadelimquote
|
|
277 |
%
|
|
278 |
\endisadelimquote
|
|
279 |
%
|
|
280 |
\isadelimquotett
|
|
281 |
\ %
|
|
282 |
\endisadelimquotett
|
|
283 |
%
|
|
284 |
\isatagquotett
|
|
285 |
\isacommand{ML}\isamarkupfalse%
|
38560
|
286 |
\ {\isacharverbatimopen}\isanewline
|
|
287 |
\ \ fun\ eval{\isacharunderscore}form\ %
|
|
288 |
\isaantiq
|
|
289 |
code\ T%
|
|
290 |
\endisaantiq
|
|
291 |
\ {\isacharequal}\ true\isanewline
|
|
292 |
\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ %
|
|
293 |
\isaantiq
|
|
294 |
code\ F%
|
|
295 |
\endisaantiq
|
|
296 |
\ {\isacharequal}\ false\isanewline
|
|
297 |
\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
|
|
298 |
\isaantiq
|
|
299 |
code\ And%
|
|
300 |
\endisaantiq
|
|
301 |
\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
|
|
302 |
\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ andalso\ eval{\isacharunderscore}form\ q\isanewline
|
|
303 |
\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
|
|
304 |
\isaantiq
|
|
305 |
code\ Or%
|
|
306 |
\endisaantiq
|
|
307 |
\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
|
|
308 |
\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
|
|
309 |
{\isacharverbatimclose}%
|
39745
|
310 |
\endisatagquotett
|
|
311 |
{\isafoldquotett}%
|
38560
|
312 |
%
|
39745
|
313 |
\isadelimquotett
|
38560
|
314 |
%
|
39745
|
315 |
\endisadelimquotett
|
38560
|
316 |
%
|
|
317 |
\begin{isamarkuptext}%
|
39609
|
318 |
\noindent \isa{code} takes as argument the name of a constant;
|
|
319 |
after the whole ML is read, the necessary code is generated
|
|
320 |
transparently and the corresponding constant names are inserted.
|
|
321 |
This technique also allows to use pattern matching on constructors
|
39643
|
322 |
stemming from compiled datatypes. Note that the \isa{code}
|
|
323 |
antiquotation may not refer to constants which carry adaptations;
|
|
324 |
here you have to refer to the corresponding adapted code directly.
|
38560
|
325 |
|
39609
|
326 |
For a less simplistic example, theory \isa{Approximation} in
|
|
327 |
the \isa{Decision{\isacharunderscore}Procs} session is a good reference.%
|
38560
|
328 |
\end{isamarkuptext}%
|
|
329 |
\isamarkuptrue%
|
|
330 |
%
|
39599
|
331 |
\isamarkupsubsubsection{Static embedding of generated code into system runtime -- \isa{code{\isacharunderscore}reflect}%
|
|
332 |
}
|
|
333 |
\isamarkuptrue%
|
|
334 |
%
|
|
335 |
\begin{isamarkuptext}%
|
39609
|
336 |
The \isa{code} antiquoation is lightweight, but the generated code
|
|
337 |
is only accessible while the ML section is processed. Sometimes this
|
|
338 |
is not appropriate, especially if the generated code contains datatype
|
|
339 |
declarations which are shared with other parts of the system. In these
|
|
340 |
cases, \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} can be used:%
|
|
341 |
\end{isamarkuptext}%
|
|
342 |
\isamarkuptrue%
|
|
343 |
%
|
|
344 |
\isadelimquote
|
|
345 |
%
|
|
346 |
\endisadelimquote
|
|
347 |
%
|
|
348 |
\isatagquote
|
|
349 |
\isacommand{code{\isacharunderscore}reflect}\isamarkupfalse%
|
|
350 |
\ Sum{\isacharunderscore}Type\isanewline
|
|
351 |
\ \ \isakeyword{datatypes}\ sum\ {\isacharequal}\ Inl\ {\isacharbar}\ Inr\isanewline
|
|
352 |
\ \ \isakeyword{functions}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projl{\isachardoublequoteclose}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projr{\isachardoublequoteclose}%
|
|
353 |
\endisatagquote
|
|
354 |
{\isafoldquote}%
|
|
355 |
%
|
|
356 |
\isadelimquote
|
|
357 |
%
|
|
358 |
\endisadelimquote
|
|
359 |
%
|
|
360 |
\begin{isamarkuptext}%
|
|
361 |
\noindent \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} takes a structure name and
|
|
362 |
references to datatypes and functions; for these code is compiled
|
|
363 |
into the named ML structure and the \emph{Eval} target is modified
|
|
364 |
in a way that future code generation will reference these
|
|
365 |
precompiled versions of the given datatypes and functions. This
|
|
366 |
also allows to refer to the referenced datatypes and functions from
|
|
367 |
arbitrary ML code as well.
|
|
368 |
|
|
369 |
A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} can be found in the
|
|
370 |
\hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.%
|
39599
|
371 |
\end{isamarkuptext}%
|
|
372 |
\isamarkuptrue%
|
|
373 |
%
|
|
374 |
\isamarkupsubsubsection{Separate compilation -- \isa{code{\isacharunderscore}reflect}%
|
|
375 |
}
|
|
376 |
\isamarkuptrue%
|
|
377 |
%
|
|
378 |
\begin{isamarkuptext}%
|
39609
|
379 |
For technical reasons it is sometimes necessary to separate
|
|
380 |
generation and compilation of code which is supposed to be used in
|
|
381 |
the system runtime. For this \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} with an
|
|
382 |
optional \isa{file} argument can be used:%
|
|
383 |
\end{isamarkuptext}%
|
|
384 |
\isamarkuptrue%
|
|
385 |
%
|
|
386 |
\isadelimquote
|
|
387 |
%
|
|
388 |
\endisadelimquote
|
|
389 |
%
|
|
390 |
\isatagquote
|
|
391 |
\isacommand{code{\isacharunderscore}reflect}\isamarkupfalse%
|
|
392 |
\ Rat\isanewline
|
|
393 |
\ \ \isakeyword{datatypes}\ rat\ {\isacharequal}\ Frct\isanewline
|
|
394 |
\ \ \isakeyword{functions}\ Fract\isanewline
|
|
395 |
\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}plus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}minus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
396 |
\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}times\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}divide\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline
|
|
397 |
\ \ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}rat{\isachardot}ML{\isachardoublequoteclose}%
|
|
398 |
\endisatagquote
|
|
399 |
{\isafoldquote}%
|
|
400 |
%
|
|
401 |
\isadelimquote
|
|
402 |
%
|
|
403 |
\endisadelimquote
|
|
404 |
%
|
|
405 |
\begin{isamarkuptext}%
|
39643
|
406 |
\noindent This merely generates the referenced code to the given
|
39609
|
407 |
file which can be included into the system runtime later on.%
|
39599
|
408 |
\end{isamarkuptext}%
|
|
409 |
\isamarkuptrue%
|
|
410 |
%
|
38560
|
411 |
\isadelimtheory
|
|
412 |
%
|
|
413 |
\endisadelimtheory
|
|
414 |
%
|
|
415 |
\isatagtheory
|
|
416 |
\isacommand{end}\isamarkupfalse%
|
|
417 |
%
|
|
418 |
\endisatagtheory
|
|
419 |
{\isafoldtheory}%
|
|
420 |
%
|
|
421 |
\isadelimtheory
|
|
422 |
%
|
|
423 |
\endisadelimtheory
|
|
424 |
\isanewline
|
|
425 |
\end{isabellebody}%
|
|
426 |
%%% Local Variables:
|
|
427 |
%%% mode: latex
|
|
428 |
%%% TeX-master: "root"
|
|
429 |
%%% End:
|