author | wenzelm |
Fri, 12 Aug 2016 11:53:47 +0200 | |
changeset 63670 | 8e0148e1f5f4 |
parent 63175 | d191892b1c23 |
child 65041 | 2525e680f94f |
permissions | -rw-r--r-- |
38510 | 1 |
theory Evaluation |
2 |
imports Setup |
|
59378
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
3 |
begin (*<*) |
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
4 |
|
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
5 |
ML \<open> |
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
6 |
Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples")) |
065f349852e6
separate image for prerequisites of codegen tutorial
haftmann
parents:
59377
diff
changeset
|
7 |
\<close> (*>*) |
38510 | 8 |
|
59377 | 9 |
section \<open>Evaluation \label{sec:evaluation}\<close> |
38510 | 10 |
|
59377 | 11 |
text \<open> |
39599 | 12 |
Recalling \secref{sec:principle}, code generation turns a system of |
13 |
equations into a program with the \emph{same} equational semantics. |
|
14 |
As a consequence, this program can be used as a \emph{rewrite |
|
15 |
engine} for terms: rewriting a term @{term "t"} using a program to a |
|
16 |
term @{term "t'"} yields the theorems @{prop "t \<equiv> t'"}. This |
|
17 |
application of code generation in the following is referred to as |
|
18 |
\emph{evaluation}. |
|
59377 | 19 |
\<close> |
38510 | 20 |
|
21 |
||
59377 | 22 |
subsection \<open>Evaluation techniques\<close> |
38510 | 23 |
|
59377 | 24 |
text \<open> |
40350 | 25 |
The existing infrastructure provides a rich palette of evaluation |
39599 | 26 |
techniques, each comprising different aspects: |
27 |
||
28 |
\begin{description} |
|
29 |
||
30 |
\item[Expressiveness.] Depending on how good symbolic computation |
|
31 |
is supported, the class of terms which can be evaluated may be |
|
32 |
bigger or smaller. |
|
38510 | 33 |
|
39599 | 34 |
\item[Efficiency.] The more machine-near the technique, the |
35 |
faster it is. |
|
38510 | 36 |
|
39599 | 37 |
\item[Trustability.] Techniques which a huge (and also probably |
38 |
more configurable infrastructure) are more fragile and less |
|
39 |
trustable. |
|
40 |
||
41 |
\end{description} |
|
59377 | 42 |
\<close> |
38510 | 43 |
|
44 |
||
59377 | 45 |
subsubsection \<open>The simplifier (@{text simp})\<close> |
38510 | 46 |
|
59377 | 47 |
text \<open> |
39599 | 48 |
The simplest way for evaluation is just using the simplifier with |
49 |
the original code equations of the underlying program. This gives |
|
50 |
fully symbolic evaluation and highest trustablity, with the usual |
|
51 |
performance of the simplifier. Note that for operations on abstract |
|
52 |
datatypes (cf.~\secref{sec:invariant}), the original theorems as |
|
53 |
given by the users are used, not the modified ones. |
|
59377 | 54 |
\<close> |
38510 | 55 |
|
56 |
||
59377 | 57 |
subsubsection \<open>Normalization by evaluation (@{text nbe})\<close> |
38510 | 58 |
|
59377 | 59 |
text \<open> |
58620 | 60 |
Normalization by evaluation @{cite "Aehlig-Haftmann-Nipkow:2008:nbe"} |
39599 | 61 |
provides a comparably fast partially symbolic evaluation which |
62 |
permits also normalization of functions and uninterpreted symbols; |
|
63 |
the stack of code to be trusted is considerable. |
|
59377 | 64 |
\<close> |
38510 | 65 |
|
66 |
||
59377 | 67 |
subsubsection \<open>Evaluation in ML (@{text code})\<close> |
39599 | 68 |
|
59377 | 69 |
text \<open> |
39599 | 70 |
Highest performance can be achieved by evaluation in ML, at the cost |
71 |
of being restricted to ground results and a layered stack of code to |
|
72 |
be trusted, including code generator configurations by the user. |
|
38510 | 73 |
|
39599 | 74 |
Evaluation is carried out in a target language \emph{Eval} which |
75 |
inherits from \emph{SML} but for convenience uses parts of the |
|
76 |
Isabelle runtime environment. The soundness of computation carried |
|
39609 | 77 |
out there depends crucially on the correctness of the code |
39643 | 78 |
generator setup; this is one of the reasons why you should not use |
39609 | 79 |
adaptation (see \secref{sec:adaptation}) frivolously. |
59377 | 80 |
\<close> |
38510 | 81 |
|
82 |
||
59377 | 83 |
subsection \<open>Aspects of evaluation\<close> |
38510 | 84 |
|
59377 | 85 |
text \<open> |
39599 | 86 |
Each of the techniques can be combined with different aspects. The |
87 |
most important distinction is between dynamic and static evaluation. |
|
88 |
Dynamic evaluation takes the code generator configuration \qt{as it |
|
89 |
is} at the point where evaluation is issued. Best example is the |
|
90 |
@{command_def value} command which allows ad-hoc evaluation of |
|
91 |
terms: |
|
59377 | 92 |
\<close> |
38510 | 93 |
|
94 |
value %quote "42 / (12 :: rat)" |
|
95 |
||
59377 | 96 |
text \<open> |
56927 | 97 |
\noindent @{command value} tries first to evaluate using ML, falling |
98 |
back to normalization by evaluation if this fails. |
|
38510 | 99 |
|
58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
100 |
A particular technique may be specified in square brackets, e.g. |
59377 | 101 |
\<close> |
58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
102 |
|
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
103 |
value %quote [nbe] "42 / (12 :: rat)" |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
104 |
|
59377 | 105 |
text \<open> |
43656
9ece73262746
adding documentation of the value antiquotation to the code generation manual
bulwahn
parents:
41184
diff
changeset
|
106 |
To employ dynamic evaluation in the document generation, there is also |
56927 | 107 |
a @{text value} antiquotation with the same evaluation techniques |
108 |
as @{command value}. |
|
43656
9ece73262746
adding documentation of the value antiquotation to the code generation manual
bulwahn
parents:
41184
diff
changeset
|
109 |
|
39599 | 110 |
Static evaluation freezes the code generator configuration at a |
111 |
certain point and uses this context whenever evaluation is issued |
|
112 |
later on. This is particularly appropriate for proof procedures |
|
113 |
which use evaluation, since then the behaviour of evaluation is not |
|
114 |
changed or even compromised later on by actions of the user. |
|
115 |
||
116 |
As a technical complication, terms after evaluation in ML must be |
|
117 |
turned into Isabelle's internal term representation again. Since |
|
118 |
this is also configurable, it is never fully trusted. For this |
|
119 |
reason, evaluation in ML comes with further aspects: |
|
120 |
||
121 |
\begin{description} |
|
122 |
||
123 |
\item[Plain evaluation.] A term is normalized using the provided |
|
124 |
term reconstruction from ML to Isabelle; for applications which |
|
125 |
do not need to be fully trusted. |
|
126 |
||
127 |
\item[Property conversion.] Evaluates propositions; since these |
|
128 |
are monomorphic, the term reconstruction is fixed once and for all |
|
129 |
and therefore trustable. |
|
130 |
||
131 |
\item[Conversion.] Evaluates an arbitrary term @{term "t"} first |
|
132 |
by plain evaluation and certifies the result @{term "t'"} by |
|
133 |
checking the equation @{term "t \<equiv> t'"} using property |
|
134 |
conversion. |
|
135 |
||
136 |
\end{description} |
|
137 |
||
138 |
\noindent The picture is further complicated by the roles of |
|
139 |
exceptions. Here three cases have to be distinguished: |
|
140 |
||
141 |
\begin{itemize} |
|
142 |
||
143 |
\item Evaluation of @{term t} terminates with a result @{term |
|
144 |
"t'"}. |
|
145 |
||
63161
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
146 |
\item Evaluation of @{term t} terminates which an exception |
40350 | 147 |
indicating a pattern match failure or a non-implemented |
39599 | 148 |
function. As sketched in \secref{sec:partiality}, this can be |
149 |
interpreted as partiality. |
|
150 |
||
39643 | 151 |
\item Evaluation raises any other kind of exception. |
39599 | 152 |
|
153 |
\end{itemize} |
|
154 |
||
155 |
\noindent For conversions, the first case yields the equation @{term |
|
156 |
"t = t'"}, the second defaults to reflexivity @{term "t = t"}. |
|
39643 | 157 |
Exceptions of the third kind are propagated to the user. |
39599 | 158 |
|
159 |
By default return values of plain evaluation are optional, yielding |
|
40350 | 160 |
@{text "SOME t'"} in the first case, @{text "NONE"} in the |
161 |
second, and propagating the exception in the third case. A strict |
|
39599 | 162 |
variant of plain evaluation either yields @{text "t'"} or propagates |
51713 | 163 |
any exception, a liberal variant captures any exception in a result |
39599 | 164 |
of type @{text "Exn.result"}. |
165 |
||
166 |
For property conversion (which coincides with conversion except for |
|
167 |
evaluation in ML), methods are provided which solve a given goal by |
|
168 |
evaluation. |
|
59377 | 169 |
\<close> |
38510 | 170 |
|
171 |
||
59377 | 172 |
subsection \<open>Schematic overview\<close> |
39599 | 173 |
|
59377 | 174 |
text \<open> |
39693 | 175 |
\newcommand{\ttsize}{\fontsize{5.8pt}{8pt}\selectfont} |
176 |
\fontsize{9pt}{12pt}\selectfont |
|
39599 | 177 |
\begin{tabular}{ll||c|c|c} |
178 |
& & @{text simp} & @{text nbe} & @{text code} \tabularnewline \hline \hline |
|
58100
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
179 |
\multirow{5}{1ex}{\rotatebox{90}{dynamic}} |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
180 |
& interactive evaluation |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
181 |
& @{command value} @{text "[simp]"} & @{command value} @{text "[nbe]"} & @{command value} @{text "[code]"} |
f54a8a4134d3
restored generic value slot, retaining default behaviour and separate approximate command
haftmann
parents:
56927
diff
changeset
|
182 |
\tabularnewline |
39693 | 183 |
& plain evaluation & & & \ttsize@{ML "Code_Evaluation.dynamic_value"} \tabularnewline \cline{2-5} |
39599 | 184 |
& evaluation method & @{method code_simp} & @{method normalization} & @{method eval} \tabularnewline |
39693 | 185 |
& property conversion & & & \ttsize@{ML "Code_Runtime.dynamic_holds_conv"} \tabularnewline \cline{2-5} |
41184 | 186 |
& conversion & \ttsize@{ML "Code_Simp.dynamic_conv"} & \ttsize@{ML "Nbe.dynamic_conv"} |
187 |
& \ttsize@{ML "Code_Evaluation.dynamic_conv"} \tabularnewline \hline \hline |
|
39693 | 188 |
\multirow{3}{1ex}{\rotatebox{90}{static}} |
41184 | 189 |
& plain evaluation & & & \ttsize@{ML "Code_Evaluation.static_value"} \tabularnewline \cline{2-5} |
39599 | 190 |
& property conversion & & |
39693 | 191 |
& \ttsize@{ML "Code_Runtime.static_holds_conv"} \tabularnewline \cline{2-5} |
41184 | 192 |
& conversion & \ttsize@{ML "Code_Simp.static_conv"} |
193 |
& \ttsize@{ML "Nbe.static_conv"} |
|
194 |
& \ttsize@{ML "Code_Evaluation.static_conv"} |
|
39599 | 195 |
\end{tabular} |
59377 | 196 |
\<close> |
39599 | 197 |
|
63161
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
198 |
text \<open> |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
199 |
\noindent Note that @{ML Code_Evaluation.static_value} and |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
200 |
@{ML Code_Evaluation.static_conv} require certain code equations to |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
201 |
reconstruct Isabelle terms from results and certify results. This is |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
202 |
achieved as follows: |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
203 |
|
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
204 |
\<^enum> Identify which result types are expected. |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
205 |
|
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
206 |
\<^enum> Define an auxiliary operation which for each possible result type @{text \<tau>} |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
207 |
contains a term @{const Code_Evaluation.TERM_OF} of type @{text "\<tau> itself"} |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
208 |
(for @{ML Code_Evaluation.static_value}) or |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
209 |
a term @{const Code_Evaluation.TERM_OF_EQUAL} of type @{text "\<tau> itself"} |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
210 |
(for @{ML Code_Evaluation.static_conv}) respectively. |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
211 |
|
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
212 |
\<^enum> Include that auxiliary operation into the set of constants when generating |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
213 |
the static conversion. |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
214 |
\<close> |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
215 |
|
39599 | 216 |
|
59377 | 217 |
subsection \<open>Preprocessing HOL terms into evaluable shape\<close> |
52287 | 218 |
|
59377 | 219 |
text \<open> |
63161
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
220 |
When integrating decision procedures developed inside HOL into HOL itself, |
52287 | 221 |
it is necessary to somehow get from the Isabelle/ML representation to |
222 |
the representation used by the decision procedure itself (``reification''). |
|
223 |
One option is to hardcode it using code antiquotations (see \secref{sec:code_antiq}). |
|
224 |
Another option is to use pre-existing infrastructure in HOL: |
|
225 |
@{ML "Reification.conv"} and @{ML "Reification.tac"} |
|
226 |
||
63161
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
61337
diff
changeset
|
227 |
A simplistic example: |
59377 | 228 |
\<close> |
52287 | 229 |
|
58310 | 230 |
datatype %quote form_ord = T | F | Less nat nat |
52287 | 231 |
| And form_ord form_ord | Or form_ord form_ord | Neg form_ord |
232 |
||
233 |
primrec %quote interp :: "form_ord \<Rightarrow> 'a::order list \<Rightarrow> bool" |
|
234 |
where |
|
235 |
"interp T vs \<longleftrightarrow> True" |
|
236 |
| "interp F vs \<longleftrightarrow> False" |
|
237 |
| "interp (Less i j) vs \<longleftrightarrow> vs ! i < vs ! j" |
|
238 |
| "interp (And f1 f2) vs \<longleftrightarrow> interp f1 vs \<and> interp f2 vs" |
|
239 |
| "interp (Or f1 f2) vs \<longleftrightarrow> interp f1 vs \<or> interp f2 vs" |
|
240 |
| "interp (Neg f) vs \<longleftrightarrow> \<not> interp f vs" |
|
241 |
||
59377 | 242 |
text \<open> |
52287 | 243 |
The datatype @{type form_ord} represents formulae whose semantics is given by |
244 |
@{const interp}. Note that values are represented by variable indices (@{typ nat}) |
|
245 |
whose concrete values are given in list @{term vs}. |
|
59377 | 246 |
\<close> |
52287 | 247 |
|
59377 | 248 |
ML (*<*) \<open>\<close> |
61337 | 249 |
schematic_goal "thm": fixes x y z :: "'a::order" shows "x < y \<and> x < z \<equiv> ?P" |
52287 | 250 |
ML_prf |
59377 | 251 |
(*>*) \<open>val thm = |
252 |
Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*) |
|
60754 | 253 |
by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>) |
52287 | 254 |
(*>*) |
255 |
||
59377 | 256 |
text \<open> |
52287 | 257 |
By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion |
258 |
which, for this concrete example, yields @{thm thm [no_vars]}. Note that the argument |
|
59335 | 259 |
to @{const interp} does not contain any free variables and can thus be evaluated |
52287 | 260 |
using evaluation. |
261 |
||
262 |
A less meager example can be found in the AFP, session @{text "Regular-Sets"}, |
|
263 |
theory @{text Regexp_Method}. |
|
59377 | 264 |
\<close> |
52287 | 265 |
|
266 |
||
59377 | 267 |
subsection \<open>Intimate connection between logic and system runtime\<close> |
39599 | 268 |
|
59377 | 269 |
text \<open> |
39609 | 270 |
The toolbox of static evaluation conversions forms a reasonable base |
271 |
to interweave generated code and system tools. However in some |
|
272 |
situations more direct interaction is desirable. |
|
59377 | 273 |
\<close> |
39599 | 274 |
|
275 |
||
59377 | 276 |
subsubsection \<open>Static embedding of generated code into system runtime -- the @{text code} antiquotation \label{sec:code_antiq}\<close> |
39599 | 277 |
|
59377 | 278 |
text \<open> |
39609 | 279 |
The @{text code} antiquotation allows to include constants from |
280 |
generated code directly into ML system code, as in the following toy |
|
281 |
example: |
|
59377 | 282 |
\<close> |
38510 | 283 |
|
58310 | 284 |
datatype %quote form = T | F | And form form | Or form form (*<*) |
38510 | 285 |
|
59377 | 286 |
(*>*) ML %quotett \<open> |
38510 | 287 |
fun eval_form @{code T} = true |
288 |
| eval_form @{code F} = false |
|
289 |
| eval_form (@{code And} (p, q)) = |
|
290 |
eval_form p andalso eval_form q |
|
291 |
| eval_form (@{code Or} (p, q)) = |
|
292 |
eval_form p orelse eval_form q; |
|
59377 | 293 |
\<close> |
38510 | 294 |
|
59377 | 295 |
text \<open> |
39609 | 296 |
\noindent @{text code} takes as argument the name of a constant; |
297 |
after the whole ML is read, the necessary code is generated |
|
298 |
transparently and the corresponding constant names are inserted. |
|
299 |
This technique also allows to use pattern matching on constructors |
|
39643 | 300 |
stemming from compiled datatypes. Note that the @{text code} |
301 |
antiquotation may not refer to constants which carry adaptations; |
|
302 |
here you have to refer to the corresponding adapted code directly. |
|
38510 | 303 |
|
39609 | 304 |
For a less simplistic example, theory @{text Approximation} in |
305 |
the @{text Decision_Procs} session is a good reference. |
|
59377 | 306 |
\<close> |
38510 | 307 |
|
308 |
||
59377 | 309 |
subsubsection \<open>Static embedding of generated code into system runtime -- @{text code_reflect}\<close> |
39599 | 310 |
|
59377 | 311 |
text \<open> |
39609 | 312 |
The @{text code} antiquoation is lightweight, but the generated code |
313 |
is only accessible while the ML section is processed. Sometimes this |
|
314 |
is not appropriate, especially if the generated code contains datatype |
|
315 |
declarations which are shared with other parts of the system. In these |
|
316 |
cases, @{command_def code_reflect} can be used: |
|
59377 | 317 |
\<close> |
39609 | 318 |
|
319 |
code_reflect %quote Sum_Type |
|
320 |
datatypes sum = Inl | Inr |
|
55418 | 321 |
functions "Sum_Type.sum.projl" "Sum_Type.sum.projr" |
39609 | 322 |
|
59377 | 323 |
text \<open> |
39609 | 324 |
\noindent @{command_def code_reflect} takes a structure name and |
325 |
references to datatypes and functions; for these code is compiled |
|
326 |
into the named ML structure and the \emph{Eval} target is modified |
|
327 |
in a way that future code generation will reference these |
|
328 |
precompiled versions of the given datatypes and functions. This |
|
329 |
also allows to refer to the referenced datatypes and functions from |
|
330 |
arbitrary ML code as well. |
|
331 |
||
332 |
A typical example for @{command code_reflect} can be found in the |
|
333 |
@{theory Predicate} theory. |
|
59377 | 334 |
\<close> |
39609 | 335 |
|
39599 | 336 |
|
59377 | 337 |
subsubsection \<open>Separate compilation -- @{text code_reflect}\<close> |
39599 | 338 |
|
59377 | 339 |
text \<open> |
39609 | 340 |
For technical reasons it is sometimes necessary to separate |
341 |
generation and compilation of code which is supposed to be used in |
|
342 |
the system runtime. For this @{command code_reflect} with an |
|
63670 | 343 |
optional \<^theory_text>\<open>file\<close> argument can be used: |
59377 | 344 |
\<close> |
39609 | 345 |
|
346 |
code_reflect %quote Rat |
|
63175
d191892b1c23
explicit check that abstract constructors cannot be part of official interface
haftmann
parents:
63161
diff
changeset
|
347 |
datatypes rat |
39609 | 348 |
functions Fract |
349 |
"(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
|
350 |
"(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)" |
|
59334 | 351 |
file "$ISABELLE_TMP/examples/rat.ML" |
39609 | 352 |
|
59377 | 353 |
text \<open> |
39643 | 354 |
\noindent This merely generates the referenced code to the given |
39609 | 355 |
file which can be included into the system runtime later on. |
59377 | 356 |
\<close> |
39599 | 357 |
|
38510 | 358 |
end |
46522 | 359 |